An Automata-Theoretic Approach to Reasoning about Infinite-State Systems

Orna Kupferman

Abstract

An important research topic over the past decade has been the application of formal methods to infinite-state systems. The automata-theoretic approach uses the theory of automata as a unifying paradigm for system specification, verification, and synthesis. The approach is very powerful for reasoning about finite-state systems. It has long been thought that the automata-theoretic approach is inapplicable for effective reasoning about infinite-state systems. 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. 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 \mu-calculus specifications and prefix-recognizable systems, and by solving the realizability and synthesis problems for \mu-calculus specifications with respect to prefix-recognizable environments.

Joint work with Moshe Vardi.

Orna Kupferman, and Moshe Y. Vardi. An Automata-Theoretic Approach to Reasoning about Infinite-State Systems. Proceedings of the 12th International Conference on Computer Aided Verification (CAV 2000) Lecture Notes in Computer Science, Springer-Verlag, 2000.
Contact 
©2002-2018 U.C. Regents