ltl3tela: LTL to Small Deterministic or Nondeterministic Emerson-Lei 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

MAJOR Juraj BLAHOUDEK František STREJČEK Jan JÁNOŠOVÁ Miriama ZBONČÁKOVÁ Tatiana

Rok publikování 2019
Druh Článek ve sborníku
Konference Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www https://link.springer.com/chapter/10.1007/978-3-030-31784-3_21
Doi http://dx.doi.org/10.1007/978-3-030-31784-3_21
Klíčová slova ltl3tela; LTL; linear temporal logic; automata; automata over infinite words; LTL to automata
Popis The paper presents a new tool ltl3tela translating LTL to deterministic or nondeterministic transition-based Emerson-Lei automata (TELA). Emerson-Lei automata use generic acceptance formulae with basic terms corresponding to Büchi and co-Büchi acceptance. The tool combines algorithms of Spot library, a new translation of LTL to TELA via alternating automata, a pattern-based automata reduction method, and few other heuristics. Experimental evaluation shows that ltl3tela can produce deterministic automata that are, on average, noticeably smaller than deterministic TELA produced by state-of-the-art translators Delag, Rabinizer 4, and Spot. For nondeterministic automata, the improvement over Spot is smaller, but still measurable.
Související projekty:

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