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-21)

Type

inproceedings

Publisher

EasyChair Publications

Projects

Spot

Date

2017-04-03

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

• 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-21)},
  year		= {2017},
  editor	= {Thomas Eiter and David Sands and Geoff Sutcliffe},
  volume	= {XXX},
  series	= {EPiC Series in Computing},
  pages		= {XX--XX},
  month		= may,
  publisher	= {EasyChair Publications},
  note		= {To appear},
  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.}
}