Abstract
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.
Cite
CITATION STYLE
Major, J., Blahoudek, F., Strejček, J., Sasaráková, M., & Zbončáková, T. (2019). ltl3tela: LTL to Small Deterministic or Nondeterministic Emerson-Lei Automata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11781 LNCS, pp. 357–365). Springer. https://doi.org/10.1007/978-3-030-31784-3_21
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
