Sciweavers

CAV
2004
Springer

Global Model-Checking of Infinite-State Systems

13 years 7 months ago
Global Model-Checking of Infinite-State Systems
Abstract. We extend the automata-theoretic framework for reasoning about infinitestate sequential systems to handle also the global model-checking problem. 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 a two-way automaton that navigates through the tree. The framework is known for local model checking. For branching time properties, the framework uses two-way alternating automata. For linear time properties, the framework uses two-way path automata. In order to solve the global model-checking problem we show that for both types of automata, given a regular tree, we can construct a nondeterministic word automaton that accepts all the nodes in the tree from which an accepting run of the automaton can start.
Nir Piterman, Moshe Y. Vardi
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2004
Where CAV
Authors Nir Piterman, Moshe Y. Vardi
Comments (0)