Le séminaire du LSV

Le séminaire du LSV a lieu le mardi à 11h00. Le lieu habituel est la salle de conférences au Pavillon des Jardins (plan d'accès). Pour être informé par email des prochains séminaires, contacter Stéphane Le Roux and Matthias Fuegger.

Le séminaire du LSV est public et ne nécessite aucune inscription préalable.

Séminaires passés

An Easy Algorithm For The General Vector Addition System Reachability Problem

Visiter le site web pour cet événement | Exporter cet événement au format iCalendar

Date
Le mardi 09 décembre 2008 à 11:00
Lieu
Salle de Conférence (Pavillon des Jardins)
Orateur
Jérôme Leroux (LaBRI, Bordeaux)

The reachability problem for Vector Addition Systems (VAS) or equivalently for Petri Nets 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 (KLMST) decomposition. This decomposition is difficult and it just has a non-primitive recursive upper-bound complexity. In this paper, we prove that if a final configuration is not reachable from an initial one, there exists a pair of Presburger formulas denoting an inductive separator proving this property. Since we can decide with any decision procedure for the Presburger arithmetic if pairs of Presburger formulas denote inductive separators, we deduce that there exist checkable certificates of non-reachability. In particular, there exists an easy algorithm for deciding the general VAS reachability problem based on two semi-algorithms. A first one that tries to prove the reachability by fairly enumerating finite sequence of actions and a second one that tries to prove the non-reachability by fairly enumerating pairs of Presburger formulas. Even if the KLMST decomposition is used for proving the termination, this algorithm is the very first one that can be implemented without using it.


À propos du LSV

Agenda des séminaires

Exporter l'agenda au format iCalendar | Les séminaires précédents

mar. 19 février

Les séminaires précédents