Abstract

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 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, 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) th