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

From LRDE

(Redirected from Publications/blahoudek.20.atva)
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

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

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}
}