
An AutomataTheoretic Approach to Reasoning about InfiniteState SystemsOrna Kupferman AbstractAn important research topic over the past decade has been the application of formal methods to infinitestate systems. The automatatheoretic approach uses the theory of automata as a unifying paradigm for system specification, verification, and synthesis. The approach is very powerful for reasoning about finitestate systems. It has long been thought that the automatatheoretic approach is inapplicable for effective reasoning about infinitestate systems. We develop an automatatheoretic framework for reasoning about infinitestate 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 finitestate automata. As has been the case with finitestate systems, the automatatheoretic framework is quite versatile. We demonstrate it by solving several versions of the modelchecking problem for \mucalculus specifications and prefixrecognizable systems, and by solving the realizability and synthesis problems for \mucalculus specifications with respect to prefixrecognizable environments.Joint work with Moshe Vardi. Orna Kupferman, and Moshe Y. Vardi. An AutomataTheoretic Approach to Reasoning about InfiniteState Systems. Proceedings of the 12th International Conference on Computer Aided Verification (CAV 2000) Lecture Notes in Computer Science, SpringerVerlag, 2000. 
You are not logged in 
Contact 
©20022017 U.C. Regents 