Symbolic Techniques for Parametric Reasoning about Counter and
Liafa - University of Paris 7
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
(1) expressive symbolic representation structures called Parametric
(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
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.
June 07, 2000
Place: Information technology, Uppsala University
Room 1549 is in Building 1, Floor 5, room 49
Time: 14.15 (+ coffee and discussion)
(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 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.
Updated 07-Jun-2000 14:48 by Roland Grönroos
e-mail: info -at- astec.uu.se