An Automata-Theoretic Approach to Sequential Infinite-State Systems
Nir Piterman

Abstract:
We develop an automata-theoretic framework for reasoning about
infinite-state sequential systems. As in the automata-theoretic
approach to model-checking finite-state systems,
we reduce branching-time model checking to the membership problem of
alternating tree automata and linear-time model checking to the
emptiness problem of nondeterministic word automata. As we start with
pushdown systems we end up with pushdown tree and word automata.

We show that membership and emptiness of pushdown automata can be
reduced to questions about two-way finite tree automata. The
solution is based on the observation that the state of such automata,
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.
In order to reason about nondeterministic word automata we
introduce 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.

Our framework also handles prefix-recognizable systems, global model
checking, and systems with regular labeling. In fact
we show that model-checking with respect to pushdown systems with
regular labeling is intereducible with model-checking with respect to
prefix-recognizable systems with simple labeling.

(Joint work with O. Kupferman and M.Y. Vardi.)