2010 | OriginalPaper | Chapter
An Automata-Theoretic Approach to Infinite-State Systems
Authors : Orna Kupferman, Nir Piterman, Moshe Y. Vardi
Published in: Time for Verification
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
In this paper we develop an automata-theoretic framework for reasoning about 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 a system satisfies a temporal property can then be done by an alternating two-way tree automaton that navigates through the tree. We show how this framework can be used to solve the model-checking problem for
μ
-calculus and LTL specifications with respect to pushdown and prefix-recognizable systems. In order to handle model checking of linear-time specifications, we introduce and study
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.
As has been the case with finite-state systems, the automata-theoretic framework is quite versatile. We demonstrate it by solving the realizability and synthesis problems for
μ
-calculus specifications with respect to prefix-recognizable environments, and extending our framework to handle systems with
regular labeling
regular fairness constraints
and
μ
-calculus with
backward modalities
.