I am happy to announce that the following paper has been accepted at
the 32nd International Conference on Computer-Aided Verification (CAV'20),
to be held virtually in July 2020.
Seminator 2 Can Complement Generalized Büchi Automata
via Improved Semi-Determinization
František Blahoudek¹, Alexandre Duret-Lutz², Jan Strejček³
¹University of Texas at Austin, USA
²LRDE, EPITA, Le Kremlin-Bicêtre, France
³Faculty of Informatics, Masaryk University, Brno, Czech Republic
https://www.lrde.epita.fr/wiki/Publications/blahoudek.20.atva
Abstract:
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.
--
Alexandre Duret-Lutz