Licentiate thesis 2000-008

Regular Model Checking

Marcus Nilsson

December 2000

Abstract:
We present regular model checking, a framework for algorithmic verification of infinite-state systems with, e.g., queues, stacks, integers, or a parameterized linear topology. States are represented by strings over a finite alphabet and the transition relation by a regular length-preserving relation on strings. Both sets of states and the transition relation are represented by regular sets. Major problems in the verification of parameterized and infinite-state systems are to compute the set of states that are reachable from some set of initial states, and to compute the transitive closure of the transition relation. We present an automata-theoretic construction for computing a non-finite composition of regular relations, e.g., the transitive closure of a relation. The method is incomplete in general, but we give sufficient conditions under which it works. We show how to reduce model checking of omega-regular properties of parameterized systems into a non-finite composition of regular relations. We also report on an implementation of regular model checking, based on a new package for non-deterministic finite automata.

Available as PDF (412 kB) and compressed Postscript (288 kB)

Download BibTeX entry.