How to Efficiently Translate Extensions of Temporal Logics into Alternating Automata
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
(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.