One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata

Abstract

We present a unified translation of LTL formulas into deterministic Rabin automata, limit-deterministic Büchi automata, and nondeterministic Büchi automata. The translations yield automata of asymptotically optimal size (double or single exponential, respectively). All three translations are derived from one single Master Theorem of purely logical nature. The Master Theorem decomposes the language of a formula into a positive boolean combination of languages that can be translated into ω-automata by elementary means. In particular, Safra's, ranking, and breakpoint constructions used in other translations are not needed.

References in corpus (4)

• One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata
• From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata
• Index appearance record for transforming Rabin automata into parity automata
• From LTL to Deterministic Automata: A Safraless Compositional Approach

Cited by in corpus (4)

• Practical Synthesis of Reactive Systems from LTL Specifications via Parity Games
• One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata
• An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata
• Satisfiability Bounds for $\omega$-Regular Properties in Bounded-Parameter Markov Decision Processes