Joint work with Aurore Annichini and Eugene Asarin (Verimag - Grenoble)

We address the problem of automatic analysis of parametric counter and clock automata. We propose a semi-algorithmic approach based on using
(1) expressive symbolic representation structures called Parametric DBM's,and
(2) accurate extrapolation techniques allowing to speed up the reachability analysis and help its termination. The extrapolation techniques we propose consist in guessing automatically the effect of iterating a control loop an arbitray number of times, and in checking that this guess is exact.

Our approach can deal uniformly with systems that generate linear or nonlinear sets of configurations. We have implemented our techniques and experimented them on nontrivial examples such as a parametric timed version of the Bounded Retransmission Protocol.

ASTEC seminar
June 07, 2000

Place: Information technology, Uppsala University
Room: 1549
Time: 14.15 (+ coffee and discussion)

Help on how get here and MIC campus drawing.

There will be an extended period for discussions after the seminar nourished by cookies and coffee.

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.