Abstract
We consider parameterized systems which typically consist of networks with an arbitrary number of components. The goal is to verify the correctness of the system regardless of the number of components.

Examples of parameterized systems include mutual exclusion protocols, cache coherence protocols, and broadcast protocols.

First, we consider systems where each component is a finite-state process.We show how to capture the behaviour of such a system using a Petri net. Then, we show how to generalize the results to parameterized systems of timed processes using Timed Petri Nets.

In a timed Petri net, each token is equipped with a real-valued clock representing the ``age'' of the token. Each arc in the net is provided with a subinterval of the natural numbers, restricting the ages of the tokens traveling through the arc. Timed Petri nets are strictly more powerful than timed automata, since they operate on an unbounded number of real-valued clocks.

ASTEC seminar
November 27, 2001

Place: Information technology, Uppsala University
Room: 1113
Time: 15.15-16.15 (+ discussions)

Room 1113 is in building 1, floor 1, room 13 (in the southern part of the building).

Help on how to find ASTEC Seminars.

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 16.15