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é:   
The Vector Addition System Reachability Problem
du groupe Modélisation et Verification

Date 2010-09-30  11:30-12:45
TitreThe Vector Addition System Reachability Problem 
RésuméThe reachability problem for Vector Addition Systems (VASs) is a central problem of net theory. The general problem is known decidable by algorithms exclusively based on the classical Kosaraju-Lambert-Mayr-Sacerdote-Tenney decomposition. Recently from this decomposition, we deduced that a final configuration is not reachable from an initial one if and only if there exists a Presburger inductive invariant that contains the initial configuration but not the final one. Since we can decide if a Preburger formula denotes an inductive invariant, we deduce from this result that there exist checkable certificates of non-reachability. In particular, there exists a simple algorithm for deciding the general VAS reachability problem based on two semi-algorithms. A first one that tries to prove the reachability by enumerating finite sequences of actions and a second one that tries to prove the non-reachability by enumerating Presburger formulas. In this presentation we provide the first proof of the VAS reachability problem that is not based on the classical Kosaraju-Lambert-Mayr-Sacerdote-Tenney decomposition. The new proof is based on the notion of productive sequences inspired from Hauschildt that directly provides the existence of Presburger inductive invariants. 
LieuSalle 076, LaBRI, Rez-de-chaussée 
OrateurJérôme Leroux 
Emailleroux@labri.fr 
UrlLaBRI 



Aucun document lié à cet événement.

Retour
Retour à l'index