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. 
LieuSalle 076, LaBRI, Rez-de-chaussée 
OrateurRémi Bonnet 
Emailremi.bonnet@lsv.ens-cachan.fr 
UrlLSV 



Aucun document lié à cet événement.

Retour
Retour à l'index