In this paper we develop an automata-theoretic framework for reasoning about
infinite-state sequential systems. Our framework is based on the
observation that states of such systems, which carry a finite but
unbounded amount of information, can be viewed as nodes in an infinite
tree, and transitions between states can be simulated by finite-state
automata. Checking that a system satisfies a temporal property can
then be done by an alternating two-way tree automaton that navigates
through the tree. We show how this framework can be used to solve the
model-checking problem for mu-calculus and LTL specifications with
respect to pushdown and prefix-recognizable systems. In order to
handle model checking of linear-time specifications, we introduce and
study path automata on trees. The input to a path automaton is a
tree, but the automaton cannot split to copies and it can read only a
single path of the tree.
As has been the case with finite-state systems, the automata-theoretic
framework is quite versatile. We demonstrate it by solving the
realizability and synthesis problems for mu-calculus specifications
with respect to prefix-recognizable environments, and extending our
framework to handle systems with regular labeling, regular
fairness constraints, and mu-calculus with backward
modalities.