Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-Determinization

Authors

František Blahoudek, Alexandre Duret-Lutz, Jan Strejček

Where

Proceedings of the 32nd International Conference on Computer-Aided Verification (CAV'20)

Type

inproceedings

Publisher

Springer

Projects

Spot

Date

2020-05-14

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. FurtherSeminator 2 has been extended with an improved NCSB complementation procedure for semi-deterministic automataproviding a new way to complement automata that is competitive with state-of-the-art complementation tools.

Documents

• Paper

Bibtex (lrde.bib)

@InProceedings{	  blahoudek.20.cav,
  author	= {Franti\v{s}ek Blahoudek and Alexandre Duret-Lutz and Jan
		  Strej\v{c}ek},
  title		= {{S}eminator~2 Can Complement Generalized {B\"u}chi
		  Automata via Improved Semi-Determinization},
  booktitle	= {Proceedings of the 32nd International Conference on
		  Computer-Aided Verification (CAV'20)},
  year		= {2020},
  publisher	= {Springer},
  volume	= {12225},
  series	= {Lecture Notes in Computer Science},
  pages		= {15--27},
  month		= jul,
  abstract	= {We present the second generation of the tool Seminator
		  that transforms transition-based generalized B{\"u}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 \texttt{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.},
  doi		= {10.1007/978-3-030-53291-8_2}
}