(2021) AIGEN: Random Generation of Symbolic Transition Systems.
|
Text
camera-ready.pdf - Accepted Version Available under License Creative Commons Attribution. Download (673kB) | Preview |
Abstract
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.
| Item Type: | Conference or Workshop Item (A Paper) (Paper) |
|---|---|
| Additional Information: | AIGEN on Github: https://github.com/mhdsakr/AIGEN-Tool ----- Virtual Machine on Zenodo: https://doi.org/10.5281/zenodo.4721314 |
| Divisions: | Swen Jacobs (SJ) |
| Conference: | CAV Computer Aided Verification |
| Depositing User: | Swen Jacobs |
| Date Deposited: | 04 Jun 2021 08:27 |
| Last Modified: | 04 Jun 2021 08:27 |
| Primary Research Area: | NRA2: Reliable Security Guarantees |
| URI: | https://publications.cispa.saarland/id/eprint/3430 |
Actions
Actions (login required)
 |
View Item |