In temporal-logic model checking, we verify the correctness of a progr
am with respect to a desired behavior by checking whether a structure
that models the program satisfies a temporal logic formula that specif
ies this behavior. The close connection between linear-time temporal l
ogics and the theory of automata on infinite words has been an active
area of research, In particular, automata-theoretic techniques have pr
oven to be an effective approach to linear-time model checking. On the
other hand, for branching-time temporal logics, current automata-theo
retic techniques involve an exponential blow-up, making them essential
ly useless for model-checking. In this paper we present an automata-th
eoretic framework for branching-time model checking. We introduce simu
ltaneous 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 psi we associate an
automaton that accepts exactly these simultaneous trees that originate
from structures that satisfy psi. This enables to use the automaton f
or model checking which is reduced to the membership problem. We demon
strate our framework with the branching-time temporal logic CTL and sh
ow that it yields a linear automata-based model-checking algorithm, ma
tching the known bound. This is the first time that a model-checking a
lgorithm for a branching-time temporal logic has been placed in the au
tomata-theoretic framework. (C) 1996 Academic Press, Inc.