# LSV Seminar

The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue).
If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.

The seminar is open to public and does not require any form of registration.

## Past Seminars

### An Easy Algorithm For The General Vector Addition System Reachability Problem

- Date
- Tuesday, December 09 2008 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- 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.