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

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.