Seminator: A Tool for Semi-Determinization of Omega-Automata

Authors

František Blahoudek, Alexandre Duret-Lutz, Mikuláš Klokočka, Mojmír Křetínský, Jan Strejček

Where

Proceedings of the 21th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'17)

Type

inproceedings

Publisher

EasyChair Publications

Projects

Spot

Date

2017-04-03

Abstract

We present a tool that transforms nondeterministic $\omega$-automata to semi-deterministic $\omega$-automata. The tool Seminator accepts transition-based generalized Büchi automata (TGBA) as an input and produces automata with two kinds of semi-determinism. The implemented procedure performs degeneralization and semi-determinization simultaneously and employs several other optimizations. We experimentally evaluate Seminator in the context of LTL to semi-deterministic automata translation.

Documents

• Paper

Bibtex (lrde.bib)

@InProceedings{	  blahoudek.17.lpar,
  author	= {Franti\v{s}ek Blahoudek and Alexandre Duret-Lutz and
		  Mikul\'{a}\v{s} Kloko\v{c}ka and Mojm{\'i}r
		  K{\v{r}}et{\'i}nsk{\'y} and Jan Strej{\v{c}}ek},
  title		= {Seminator: A Tool for Semi-Determinization of
		  Omega-Automata},
  booktitle	= {Proceedings of the 21th International Conference on Logic
		  for Programming, Artificial Intelligence, and Reasoning
		  (LPAR'17)},
  year		= {2017},
  editor	= {Thomas Eiter and David Sands and Geoff Sutcliffe},
  volume	= {46},
  series	= {EPiC Series in Computing},
  pages		= {356--367},
  month		= may,
  publisher	= {EasyChair Publications},
  abstract	= {We present a tool that transforms nondeterministic
		  $\omega$-automata to semi-deterministic $\omega$-automata.
		  The tool Seminator accepts transition-based generalized
		  B\"uchi automata (TGBA) as an input and produces automata
		  with two kinds of semi-determinism. The implemented
		  procedure performs degeneralization and
		  semi-determinization simultaneously and employs several
		  other optimizations. We experimentally evaluate Seminator
		  in the context of LTL to semi-deterministic automata
		  translation.},
  doi		= {10.29007/k5nl}
}