Reference : AIGEN: Random Generation of Symbolic Transition Systems
Scientific congresses, symposiums and conference proceedings : Paper published in a book
Engineering, computing & technology : Computer science
Security, Reliability and Trust
AIGEN: Random Generation of Symbolic Transition Systems
Sakr, Mouhammad mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > CritiX >]
Jacobs, Swen mailto [CISPA]
AIGEN: Random Generation of Symbolic Transition Systems
Sakr, Mouhammad mailto
Jacobs, Swen mailto
33rd International Conference on Computer-Aided Verification-CAV
from 18-07-2021 to 24-07-2021
[en] Symbolic Transition Systems ; Binary Decision Diagrams ; Hardware Model Checking ; Canonical Disjunctive Normal Form ; Boolean functions ; Safety Synthesis
AIGEN is an open source tool for the generation of transition systems in a symbolic representation. To ensure diversity, it employs a uniform random sampling over the space of all Boolean functions with a given number of variables. AIGEN relies on reduced ordered binary decision diagrams (ROBDDs) and canonical disjunctive normal form (CDNF) as canonical representations that allow us to enumerate Boolean functions, in the former case with an encoding that is inspired by data structures used to implement ROBDDs. Several parameters allow the user to restrict generation to Boolean functions or transition systems with certain properties, which are then output in AIGER format. We report on the use of AIGEN to generate random benchmark problems for the reactive synthesis competition SYNTCOMP 2019, and present a comparison of the two encodings with respect to time and memory efficiency in practice.

File(s) associated to this reference

Fulltext file(s):

Limited access
aigen.pdfAuthor preprint657.37 kBRequest a copy

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.