LTL to Smaller Self-Loop Alternating Automata and Back
Franti\v{s}ek Blahoudek, Juraj Major, Jan Strej\v{c}ek
TL;DR
This paper introduces a translation method from LTL to smaller self-loop alternating automata with generic acceptance, resulting in more compact automata than previous methods, and implements it in the LTL3TELA tool.
Contribution
It presents a novel translation from LTL to smaller SLAA with generic acceptance, improving automata size and efficiency over prior approaches.
Findings
Smaller automata are produced compared to previous translations.
The translation is implemented in the LTL3TELA tool.
Automata are suitable for deterministic and nondeterministic automaton generation.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.