|
Evènement pour le groupe Modélisation et Verification
Date | 2010-09-30 11:30-12: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 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. |
Lieu | Salle 076, LaBRI, Rez-de-chaussée |
Orateur | Jérôme Leroux |
Email | leroux@labri.fr |
Url | LaBRI |
Aucun document lié à cet événement. RetourRetour à l'index
| |