An Automata-Theoretic Approach to Branching-Time Model Checking
---------------------------------------------------------------

Translating linear temporal logic formulas to automata has proven
to be an effective approach for implementing linear-time
model-checking, and for obtaining many extensions and improvements to
this verification method. On the other hand, for branching
temporal logic, automata-theoretic techniques have long been thought
to introduce an exponential penalty, making them essentially useless
for model-checking.
Recently, Bernholtz and Grumberg have shown that this exponential
penalty can be avoided, though they did not match the linear
complexity of non-automata-theoretic algorithms. In this paper we show 
that {\em alternating tree automata\/} are the key to a comprehensive
automata-theoretic framework for branching temporal logics. 
Not only, as was shown by Muller et al., can they be used to obtain
optimal decision procedures, but, as we show here, they also
make it possible to derive optimal model-checking algorithms.
Moreover, the simple combinatorial structure that emerges from the
automata-theoretic approach opens up new possibilities for the
implementation of branching-time model checking, and has enabled us to
derive improved space complexity bounds for this long-standing problem.