How to translate efficiently extensions of temporal logics into alternating automata

Abstract

This paper presents results that enable efficient 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 allows simple and efficient translations of extended temporal operators into pairs of automata accepting complementary languages, using only up to 3 colors. Our results: (1) allow 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. © 2012 Springer-Verlag.