How to Translate Efficiently Extensions of Temporal Logics into Alternating Automata

Abstract

This paper presents studies efficient and general translations of extensions of linear temporal logic (LTL) into alternating automata, which can be applied to improve algorithms for the automata-theoretic approach to model-checking. In particular, we introduce—using a game theoretic framework—a novel finer grain complementation theorem for the parity condition. This result enables simple and efficient translations of temporal operators into pairs of automata accepting complement languages, using up to 3 colors. Moreover, our results: (1) allows to translate directly operators from LTL and different extensions (2) that can be combined without restriction; and (3) does not require to eliminate negation upfront, or to start from formulas in negation normal form.