|
Evènement pour le groupe Modélisation et Verification
Date | 2012-04-05 11:30-12:45 |
Titre | Forward Analysis for WSTS : Beyond Regular Accelerations |
Résumé | The well-known Karp and Miller algorithm constructs the
coverability tree of a Vector Addition System, obtaining a finite representation
of the cover (the downward closure of the reachability set).
The series "Forward analysis in WSTS" aims to generalize this procedure for
arbitrary well-ordered state spaces. I'll first recall the earlier works by Finkel
and Goubbault-Larrecq, that introduced the notion of complete WSTS, in
which a finite representation of the cover as set of maximal elements exists.
Then, i'll present our formalization of acceleration strategy and a parameterized Karp Miller procedure that relies on these strategy in order to compute this
set of maximal elements.
As an illustration of these ideas, I'll present an acceleration strategy for
Vector Addition Systems with two resets that allows the previously defined
procedure to terminate, effectively computing the finite representation of the cover.
This is joint work with Alain Finkel. |
Lieu | Salle 076, LaBRI, Rez-de-chaussée |
Orateur | Rémi Bonnet |
Email | remi.bonnet@lsv.ens-cachan.fr |
Url | LSV |
Aucun document lié à cet événement. RetourRetour à l'index
| |