Paper published in a book (Scientific congresses, symposiums and conference proceedings)
AIGEN: Random Generation of Symbolic Transition Systems
Sakr, Mouhammad; Jacobs, Swen
2021In Sakr, Mouhammad; Jacobs, Swen (Eds.) AIGEN: Random Generation of Symbolic Transition Systems
Peer reviewed
 

Files


Full Text
aigen.pdf
Author preprint (673.15 kB)
Request a copy

All documents in ORBilu are protected by a user license.

Send to



Details



Keywords :
Symbolic Transition Systems; Binary Decision Diagrams; Hardware Model Checking; Canonical Disjunctive Normal Form; Boolean functions; Safety Synthesis
Disciplines :
Computer science
Author, co-author :
Sakr, Mouhammad ;  University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > CritiX
Jacobs, Swen;  CISPA
External co-authors :
yes
Language :
English
Title :
AIGEN: Random Generation of Symbolic Transition Systems
Publication date :
18 July 2021
Event name :
33rd International Conference on Computer-Aided Verification-CAV
Event date :
from 18-07-2021 to 24-07-2021
Main work title :
AIGEN: Random Generation of Symbolic Transition Systems
Author, co-author :
Sakr, Mouhammad 
Jacobs, Swen
Peer reviewed :
Peer reviewed
Focus Area :
Security, Reliability and Trust
Commentary :
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.
Available on ORBilu :
since 14 December 2021

Statistics


Number of views
113 (4 by Unilu)
Number of downloads
0 (0 by Unilu)

Scopus citations®
 
0
Scopus citations®
without self-citations
0
OpenCitations
 
0
WoS citations
 
0

Bibliography


Similar publications



Contact ORBilu