
Evènement pour le groupe Modélisation et Verification
Date  20100930 11:3012:45 
Titre  The 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 KosarajuLambertMayrSacerdoteTenney 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 nonreachability. In particular, there exists a simple algorithm for deciding the general VAS reachability problem based on two semialgorithms. A first one that tries to prove the reachability by enumerating finite sequences of actions and a second one that tries to prove the nonreachability by enumerating Presburger formulas. In this presentation we provide the first proof of the VAS reachability problem that is not based on the classical KosarajuLambertMayrSacerdoteTenney decomposition. The new proof is based on the notion of productive sequences inspired from Hauschildt that directly provides the existence of Presburger inductive invariants. 
Lieu  Salle 076, LaBRI, Rezdechaussée 
Orateur  Jérôme Leroux 
Email  leroux@labri.fr 
Url  LaBRI 
Aucun document lié à cet événement. RetourRetour à l'index
 