Seminator: A Tool for Semi-Determinization of Omega-Automata
| Authors | |
|---|---|
| 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 | |
| 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: |