Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization
Autoři
BLAHOUDEK, František (203 Česká republika), Alexandre DURET-LUTZ (250 Francie) a Jan STREJČEK (203 Česká republika, garant, domácí)
Vydání
Cham (Switzerland), Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II, od s. 15-27, 13 s. 2020
Nakladatel
Springer
Další údaje
Jazyk
angličtina
Typ výsledku
Stať ve sborníku
Obor
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.
Návaznosti
GA19-24397S, projekt VaV
Název: Automaty v rozhodovacích procedurách a verifikaci (Akronym: AUTODEV)
Investor: Grantová agentura ČR, Automata for Decision Procedures and Verification