# REGULAR MODEL CHECKING

## Ahmed Bouajjani Bengt Jonsson Marcus Nilsson Tayssir Touili

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.

Major problems in the verification of parameterized and infinite-state 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 automata-theoretic 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 September 5, 2000

### Place: Information technology, Uppsala University Room: 1549 Time: 13.15 - 15.00

Room 1549 is in Building 1, Floor 5, room 49
(in the northern part of the building).

Help on how get here and MIC campus drawing.

There will be an extended period for discussions after the seminar.

Speakers are encouraged to give an short (5 min) introduction to the subject at the begining of the talk.
Listeners are excused if they have to leave after 1 hour.

Updated 27-Apr-2006 17:30 by Roland Grönroos
e-mail: info -at- astec.uu.se    Location: http://www.astec.uu.se/Seminars/sem000905.shtml