How to Efficiently Translate Extensions of Temporal Logics into Alternating Automata

César Sánchez and Julian Samborski-Forlese
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.

In Proceedings of the 9th International Conference on Theoretical Aspects of Computing (ICTAC 2012), Bangalore, India, September 24-27, vol 7521 of LNCS, pp30-45, Springer, 2012.
Download: BIB PDF