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.
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.