Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization
Authors
BLAHOUDEK, František (203 Czech Republic), Alexandre DURET-LUTZ (250 France) and Jan STREJČEK (203 Czech Republic, guarantor, belonging to the institution)
Edition
Cham (Switzerland), Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II, p. 15-27, 13 pp. 2020
Publisher
Springer
Other information
Language
English
Type of outcome
Stať ve sborníku
Field of Study
10201 Computer sciences, information science, bioinformatics
We present the second generation of the tool Seminator that transforms transition-based generalized Büchi automata (TGBAs) into equivalent semi-deterministic automata. The tool has been extended with numerous optimizations and produces considerably smaller automata than its first version. In connection with the state-of-the-art LTL to TGBAs translator Spot, Seminator 2 produces smaller (on average) semi-deterministic automata than the direct LTL to semi-deterministic automata translator ltl2ldgba of the Owl library. Further, Seminator 2 has been extended with an improved NCSB complementation procedure for semi-deterministic automata, providing a new way to complement automata that is competitive with state-of-the-art complementation tools.
Links
GA19-24397S, research and development project
Name: Automaty v rozhodovacích procedurách a verifikaci (Acronym: AUTODEV)