LTL to Smaller Self-Loop Alternating Automata and Back

Logo poskytovatele

Varování

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

BLAHOUDEK František MAJOR Juraj STREJČEK Jan

Rok publikování 2019
Druh Článek ve sborníku
Konference Theoretical Aspects of Computing - ICTAC 2019 - 16th International Colloquium, Hammamet, Tunisia, October 31 - November 4, 2019, Proceedings
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www https://link.springer.com/chapter/10.1007/978-3-030-32505-3_10
Doi http://dx.doi.org/10.1007/978-3-030-32505-3_10
Klíčová slova LTL; linear temporal logic; automata; automata over infinite words; alternating automata; LTL to automata; ltl3tela
Popis Self-loop alternating automata (SLAA) with Büchi or co-Büchi acceptance are popular intermediate formalisms in translations of LTL to deterministic or nondeterministic automata. This paper considers SLAA with generic transition-based Emerson-Lei acceptance and presents translations of LTL to these automata and back. Importantly, the translation of LTL to SLAA with generic acceptance produces considerably smaller automata than previous translations of LTL to Büchi or co-Büchi SLAA. Our translation is already implemented in the tool LTL3TELA, where it helps to produce small deterministic or nondeterministic automata for given LTL formulae.
Související projekty:

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