###
Unifying Truth and Validity Checking for Temporal Logics

Moshe Y. Vardi

Rice University
We describe an automata-theoretic approach to the automated
checking of truth and validity for temporal logics.
The basic idea underlying this approach is that for any formula
we can construct an alternating automaton that accepts precisely the
models of the formula. For linear temporal logics the automaton runs
on infinite words while for branching temporal logics the automaton
runs on infinite trees. The simple combinatorial structures that
emerge from the automata-theoretic approach decouple the logical and
algorithmic components of truth and validity checking and
yield clean and essentially optimal algorithms for both problems.