An Automata-Theoretic Approach to Reasoning about Infinite-State Systems
========================================================================

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 the system satisfies a temporal property can
then be done by an alternating two-way tree automaton that navigates
through the tree.  As has been the case with finite-state systems, the
automata-theoretic framework is quite versatile.  We demonstrate it by
solving several versions of the model-checking problem for
$\mu$-calculus specifications and prefix-recognizable systems, and by
solving the realizability and synthesis problems for $\mu$-calculus
specifications with respect to prefix-recognizable environments.