LTL to self-loop alternating automata with generic acceptance and back

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 MAJOR Juraj STREJČEK Jan

Rok publikování 2020
Druh Článek v odborném periodiku
Časopis / Zdroj Theoretical Computer Science
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www https://www.sciencedirect.com/science/article/pii/S030439752030390X
Doi http://dx.doi.org/10.1016/j.tcs.2020.07.015
Klíčová slova LTL; Omega-automata; LTL to automata translation; Alternating automata; ltl3tela
Popis Self-loop alternating automata (SLAA) with Buchi or co-Buchi acceptance are popular formalisms also known as very weak alternating automata (VWAA). They are often used as an intermediate results 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 Buchi or co-Buchi SLAA. Our translation is already implemented in the tool ltl3tela, where it helps to produce small deterministic or nondeterministic transition-based Emerson-Lei automata for given LTL formulae. (C) 2020 Elsevier B.V. All rights reserved.
Související projekty:

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