[Lrde Annonce] New publication: Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-Determinization

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