Uniform approaches to the verification of finite state systems
Sandeep K. Shukla · 1997
Research in formal verification mainly entails the following activities: development of appropriate formal models for systems; design of specification formalisms for describing desirable properties; inventing algorithmic techniques to establish the conformance of systems to the desired properties; analyzing complexity bounds for various algorithmic problems arising in these contexts; and characterization of classes of problems which have efficient algorithmic solutions. The contributions of this thesis are in three of these areas, the main emphasis being on the development of uniform techniques. In the area of algorithmic techniques, we develop a uniform methodology that enables us to derive polynomial time algorithms for a number of problems arising in various approaches to the verification of finite state systems. We consider two well known models for finite state systems, namely process algebraic and automata theoretic. The specification formalism for the former is also process algebraic and for the latter, it is based on various modal logics. The notion of conformance is given in terms of appropriate relations (such as bisimulation, simulation, nested simulation, etc.) between processes or in terms of model checking. However, the main hurdle towards achieving feasible algorithmic approach based on these models is the formidable complexity lower bounds. Thus pragmatic considerations demand that the algorithms should be on-the-fly, local and incremental. Our methodology not only allows us to derive polynomial time algorithms with these desirable properties, we can also generate diagnostic information without any additional complexity overhead. Our approach is based on propositional satisfiability problems for Horn clauses and their variants. In the area of complexity lower bounds, we establish uniform lower bounds for classes of relational problems for some natural succinct representations of systems. We show the tightness of our uniform lower bounds by establishing matching upper bounds in several cases. In the area of characterization of subclasses of verificational problems, we establish two sets of results. First, we develop a game theoretic approach to characterize process algebraic relations for polynomial time decidability. Second, our uniform approach leads to characterizations of subclasses of verificational problems that are amenable to efficient parallel algorithms.