Model Checking Linear Properties of Prefix-Recognizable Systems
===============================================================
We develop an automata-theoretic framework for reasoning about linear
properties of 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 automaton that
navigates through the tree. For branching properties, the framework
is known and the two-way alternating automaton is a tree
automaton. Applying the framework for linear properties results in
algorithms that are not optimal. Indeed, the fact that a tree
automaton can split to copies and simultaneously read all the paths of
the tree has a computational price and is irrelevant for linear
properties. We introduce {\em 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. In particular, {\em
two-way\/} nondeterministic path automata enable exactly the type of
navigation that is required in order to check linear properties of
infinite-state sequential systems.
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 LTL specifications and
prefix-recognizable systems. Our algorithm is exponential in both the
size of (the description of) the system and the size of the LTL
specification, and we prove a matching lower bound. This is the first
optimal algorithm for solving the LTL model-checking problem for
prefix recognizable systems. Our framework also handles systems with
regular labeling, and in fact we show that LTL model checking with
respect to pushdown systems with regular labeling is intereducible
with LTL model checking with respect to prefix-recognizable systems
with simple labeling.