Model Checking Linear Properties of Prefix-Recognizable Systems
Orna Kupferman, Nir Piterman, Moshe Y. Vardi · 2002
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.