Regular Model Checking

Sammanfattning: A major current challenge in the area of program verification is to extend its applicability to infinite-state systems. A system can be infinite-state because it operates on unbounded data structures, such as queues, stacks, integers, etc., or because its description is parameterized by the number of components inside the system.In this thesis, we apply the framework of regular model checking for algorithmic verification of infinite-state systems. In regular model checking, system states are represented by words over a finite alphabet and the transition relation by a regular length-preserving relation on words. The contributions can be divided into three categories: acceleration techniques, specification, and implementation.The aim of acceleration techniques is to consider arbitrarily long execution sequences. This is usually done by computing the transitive closure: the effect of applying a transition relation an arbitrary number of times. We give several novel algorithms for computing the transitive closure. The algorithms are general in the sense that they are not dependent on the type of data structure or if a parameterized system is considered. Hence, they unify several previous techniques based on regular sets. We develop a theoretical framework to explain the algorithms and prove their correctness. Using the new algorithms, we can automatically verify several examples of parameterized and infinite-state systems. While computing transitive closures is not possible in general, we give a sufficient condition under which our algorithms terminate.We extend the so-called automata-theoretic approach and define the logic LTL(MSO) used for specification of systems. The logic is an extension of propositional linear temporal logic with the added ability to reason about words of arbitrary length. We show how to transform formulas in this extended logic into a suitable form for the verification algorithms. Using the logic, we can express parameterized fairness and liveness properties.Finally, we describe in detail an implementation of regular model checking. It includes an automata package implemented using BDDs, a symbolic representation of finite sets. We evaluate the algorithms for computing transitive closures by verifying several examples of parameterized and infinite-state systems.