Branching-Time Temporal Logic and Tree Automata
------------------------------------------------

In temporal-logic model checking, we verify the correctness of a
program with respect to a desired behavior by checking whether a
structure that models the program satisfies a temporal logic formula
that specifies this behavior. 
The close connection between linear-time temporal logics and the
theory of automata on infinite words has been an active area of
research. In particular, automata-theoretic techniques have proven to
be an effective approach to linear-time model checking. On the other
hand, for branching-time temporal logics, current automata-theoretic
techniques involve an exponential blow up, making them essentially
useless for model-checking. In this paper we present an
automata-theoretic framework for branching-time model checking. 
We introduce simultaneous trees and associate with every structure a  
simultaneous tree that enables an automaton to visit different
nodes on the same path of the structure simultaneously. 
With every formula f we associate an automaton that accepts exactly
these simultaneous trees that originate from structures that satisfy
f. This enables to use the automaton for model checking which is
reduced to the membership problem. 

We demonstrate our framework with the branching-time temporal logic
CTL and show that it yields a linear automata-based model-checking
algorithm, matching the known bound. This is the first time that a
model-checking algorithm for a branching-time temporal logic is placed
in the automata-theoretic framework.