LTL to Smaller Self-Loop Alternating Automata and Back
Formal Languages and Automata Theory
2019-10-17 v2
Abstract
Self-loop alternating automata (SLAA) with B\"uchi or co-B\"uchi acceptance are popular intermediate formalisms 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 B\"uchi or co-B\"uchi SLAA. Our translation is already implemented in the tool LTL3TELA, where it helps to produce small deterministic or nondeterministic automata for given LTL formulae.
Keywords
Cite
@article{arxiv.1908.04645,
title = {LTL to Smaller Self-Loop Alternating Automata and Back},
author = {František Blahoudek and Juraj Major and Jan Strejček},
journal= {arXiv preprint arXiv:1908.04645},
year = {2019}
}
Comments
This is a full version of the paper accepted to ICTAC 2019