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

From LRDE

Abstract

We present a tool that transforms nondeterministic -automata to semi-deterministic -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

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