ltl3tela: LTL to Small Deterministic or Nondeterministic Emerson-Lei Automata

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

• Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII.
• Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 19
• Automata for Decision Procedures and Verification