REGULAR MODEL CHECKINGAhmed Bouajjani Bengt Jonsson Marcus Nilsson Tayssir TouiliAbstract We present REGULAR MODEL CHECKING, a framework for algorithmic verification of infinitestate 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 lengthpreserving relation on strings. Major problems in the verification of parameterized and infinitestate systems is to compute the set of states that are reachable from some set of initial state, or to compute the transitive closure of the transition relation. We present two complementary techniques for these problems. One is a direct automatatheoretic construction, and the other is based on widening. Both techniques are incomplete in general, but we give sufficient conditions under which they work. We also present a method for verifying $\omega$regular properties of parameterized systems, by computation of the transitive closure of a transition relation. ASTEC seminar
