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

Warning

This publication doesn't include Faculty of Sports Studies. It includes Faculty of Informatics. Official publication website can be found on muni.cz.

Authors	BLAHOUDEK František DURET-LUTZ Alexandre KLOKOČKA Mikuláš KŘETÍNSKÝ Mojmír STREJČEK Jan
Year of publication	2017
Type	Article in Proceedings
Conference	Proceedings of the 21th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2017)
MU Faculty or unit	Faculty of Informatics
Citation
Web	http://easychair.org/publications/paper/Seminator_A_Tool_for_Semi-Determinization_of_Omega-Automata
Doi	http://dx.doi.org/10.29007/k5nl
Field	Informatics
Keywords	semi deterministic automata; ltl to automata translation; omega automata
Description	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.
Related projects:	Centrum excelence - Institut teoretické informatiky Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VI. Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity