A Unified Translation of Linear Temporal Logic to ω-Automata
Open Access
- 17 October 2020
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 67 (6), 1-61
- https://doi.org/10.1145/3417995
Abstract
We present a unified translation of linear temporal logic (LTL) formulas into deterministic Rabin automata (DRA), limit-deterministic Büchi automata (LDBA), and nondeterministic Büchi automata (NBA). 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. We further give evidence that this theoretical clean and compositional approach does not lead to large automata per se and in fact in the case of DRAs yields significantly smaller automata compared to the previously known approach using determinisation of NBAs.Keywords
Funding Information
- Deutsche Forschungsgemeinschaft (317422601)
- H2020 European Research Council (787367)
This publication has 60 references indexed in Scilit:
- From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity AutomataLogical Methods in Computer Science, 2007
- Experiments with deterministic ω-automata for formulas of linear temporal logicTheoretical Computer Science, 2006
- Deterministic generators and games for Ltl fragmentsACM Transactions on Computational Logic, 2004
- Partial derivatives of regular expressions and finite automaton constructionsTheoretical Computer Science, 1996
- The complexity of probabilistic verificationJournal of the ACM, 1995
- Safety, liveness and fairness in temporal logicFormal Aspects of Computing, 1994
- Automata-theoretic techniques for modal logics of programsJournal of Computer and System Sciences, 1986
- Alternating finite automata on ω-wordsTheoretical Computer Science, 1984
- The temporal semantics of concurrent programsTheoretical Computer Science, 1981
- Derivatives of Regular ExpressionsJournal of the ACM, 1964