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

Investor logo

Warning

This publication doesn't include Faculty of Education. 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:

You are running an old browser version. We recommend updating your browser to its latest version.