Actualités
  Période
semaine
ou mois
aucune période


  Thèmes:
Thèses
Colloques
Autres
Groupes
Tous les thèmes

   
  Liens:
Voir les thèses

Voir les colloques

Voir les autres événements

Voir la page des groupes

Accéder à l'intranet

Intitulé:   
Forward Analysis for WSTS : Beyond Regular Accelerations
du 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