Complexity Issues in Automata Theoretic Verification

Abstract

We discuss the complexity theoretic issues that arise in the automata theoretic approach to linear time based verification methodology. In this paradigm, computations of a system are viewed as a set of linear sequences of events. Hence, we refer to the ensuing models as linear time in contrast with branching time models. The COSPAN¹ tool has been developed specifically to cope with the computational complexity associated with the algorithmic analysis of finite-state linear time models. Various refinement and abstraction techniques as well as heuristics for decomposition and algorithms for localizations have been essential parts of the COSPAN verification tool. As a result, to appreciate the problems related to the computational complexity in automated verification and methods to circumvent them, it will be a great exercise to understand the methodologies and background of this specific tool.

This material is based on R. P. Kurshan’s lectures in the DIMACS summer school on Automated Verification, which was repeated (and now first published) in this NATO school. It is a tutorial introduction to the material presented and only loosely follows the sequence of the lectures. For more information, the reader is referred to Computer-Aided Verification of Coordinating Processes: The Automata Theoretic Approach by Robert P. Kurshan (Princeton University Press, 1994) and the bibliographic references therein. We acknowledge the contributions of Oleg Sokolsky and Kathy Fisler in the preparation of these notes.

COSPAN may be licensed without Charge for academic purposes (apply to k@research.bell-labs.com) .