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

Logo poskytovatele

Varování

Publikace nespadá pod Pedagogickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

BLAHOUDEK František DURET-LUTZ Alexandre KLOKOČKA Mikuláš KŘETÍNSKÝ Mojmír STREJČEK Jan

Rok publikování 2017
Druh Článek ve sborníku
Konference Proceedings of the 21th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2017)
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www http://easychair.org/publications/paper/Seminator_A_Tool_for_Semi-Determinization_of_Omega-Automata
Doi http://dx.doi.org/10.29007/k5nl
Obor Informatika
Klíčová slova semi deterministic automata; ltl to automata translation; omega automata
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.