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

• 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
• 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

• 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