2010 | OriginalPaper | Buchkapitel
An Automata-Theoretic Approach to Infinite-State Systems
verfasst von : Orna Kupferman, Nir Piterman, Moshe Y. Vardi
Erschienen in: Time for Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. 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
.