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

Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

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

Year of publication 2019
Type Article in Proceedings
Conference Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings
MU Faculty or unit

Faculty of Informatics

Citation
Web 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
Keywords ltl3tela; LTL; linear temporal logic; automata; automata over infinite words; LTL to automata
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.