CISPA
Browse
cispa_all_3430.pdf (657.37 kB)

AIGEN: Random Generation of Symbolic Transition Systems

Download (657.37 kB)
conference contribution
posted on 2023-11-29, 18:16 authored by Swen JacobsSwen Jacobs, Mouhammad Sakr
AIGEN is an open source tool for the generation of tran- sition 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.

History

Preferred Citation

Swen Jacobs and Mouhammad Sakr. AIGEN: Random Generation of Symbolic Transition Systems. In: Computer Aided Verification (CAV). 2021.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

Computer Aided Verification (CAV)

Legacy Posted Date

2021-06-04

Open Access Type

  • CC

BibTeX

@inproceedings{cispa_all_3430, title = "AIGEN: Random Generation of Symbolic Transition Systems", author = "Jacobs, Swen and Sakr, Mouhammad", booktitle="{Computer Aided Verification (CAV)}", year="2021", }

Usage metrics

    Categories

    No categories selected

    Licence

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC