Reference : AIGEN: Random Generation of Symbolic Transition Systems

	Document type :	Scientific congresses, symposiums and conference proceedings : Paper published in a book
	Discipline(s) :	Engineering, computing & technology : Computer science
	Focus Areas :	Security, Reliability and Trust
	To cite this reference:	http://hdl.handle.net/10993/49028

Title :	AIGEN: Random Generation of Symbolic Transition Systems
Language :	English
Author, co-author :	Sakr, Mouhammad [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > CritiX >]
	Jacobs, Swen [CISPA]
Publication date :	18-Jul-2021
Main document title :	AIGEN: Random Generation of Symbolic Transition Systems
Author, co-author :	Sakr, Mouhammad
	Jacobs, Swen
Peer reviewed :	Yes
Event name :	33rd International Conference on Computer-Aided Verification-CAV
Event date :	from 18-07-2021 to 24-07-2021
Keywords :	[en] Symbolic Transition Systems ; Binary Decision Diagrams ; Hardware Model Checking ; Canonical Disjunctive Normal Form ; Boolean functions ; Safety Synthesis
Permalink :	http://hdl.handle.net/10993/49028
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.

	File(s) associated to this reference
	Fulltext file(s): File Commentary Version Size Access Limited access aigen.pdf Author preprint 657.37 kB Request a copy

All documents in ORBi^lu are protected by a user license.

 

University of Luxembourg Library |  Feedback |  Legal notices Site Map