Laboratoire Bordelais de Recherche en Informatique (LaBRI)
Equipe Méthodes Formelles (MF)
Domaine Universitaire
351 cours de la liberation
33405 Talence Cedex

Phone :+33 54000 3509
Fax :+33 54000 6669
E-Mail : jerome DOT leroux AT labri DOT fr
Office : 264

Postdoc position for 2 years in the BraVAS project.
Research Interests

The Vector Addition System Reachability Problem
Petri Nets is one of the most popular formal models for the representation and the analysis of parallel processes. The reachability problem is central since many computational problems (even outside the realm of parallel processes) reduce to this problem. The reachability problem is difficult and its decidability remained open during 20 years. Sacerdote and Tenney provided in 1977 a partial proof of decidability. The proof was completed in 1981 by Mayr and simplified by Kosaraju in 1982. Ten years later, Lambert provided a further simplified version based on the Kosaraju paper. Nowadays, no decision procedure are implemented. In fact the known algorithm is conceptually difficult (to be understood and to be implemented) and with high computational complexity bound (Ackermann). Since the proof of decidability of the reachability problem in the early 80's, very few results improved the original solution except the book of Reutenauer and the Lambert's structures. Recently in 2009 we obtained a significant progress by introducing a simple algorithm for deciding the reachability problem based on inductive invariants definable in the Presburger arithmetic that separate unreachable configurations. Whereas these invariants are obtained from the Lambert's structure in the proof published in 2009, we provided in 2011 a new shorter direct proof of the existence of these inductive invariants. This new proof introduces the central notion of almost semilinear sets, a class of sets inspired by the characterization of Presburger sets by semilinear sets. The class of almost semilinear sets provides a simple way to capture the reachability sets of vector addition systems, and in particular those with reachability sets not definable in the Presburger arithmetic. These results open many research problems. Very recently, a new proof that darmatically simplify the one publised in 2011 was published in the proceedings of ``The Alan Turing Centenary Conference, Manchester, UK, June 22-25, 2012''. This paper received a best paper award.

Recent paper: This research is founded by the ANR BraVAS. It was previously founded by the ANR Reachard
Related tool:

Arithmetic automata and Presburger arithmetic
Finite state automata provide a simple way for deciding the satisfiability of a Presburger formula. Since 1962 we know that for the positional notation of natural numbers and vectors of natural numbers, the solutions of Presburger formulas are encoded by regular languages that can be effectively represented by finite state automata. Whereas there exist efficient algorithms computing arithmetic automata from Presburger formulas, the inverse problem of decoding arithmetic automata to Presburger formulas is much more difficult. Since in general an arithmetic automaton may encode a set that is not definable in the Presburger arithmetic (for instance the power of the basis of decomposition), the decoding problem is linked to deciding if an arithmetic automaton represents a Presburger set. The decidability of this problem was first established by Muchnik in 1991 with a 4-exponential time algorithm. In a book published in 2003, Jean-Paul Allouche and Jeffrey Shallit conjectured that the problem in dimension one should be solvable in polynomial time. In 2004, Louis Latour and Denis Lugiez provides exponential time and double-exponential time algorithm for deciding the membership of sets encoded by arithmetic automata into some subclasses of Presburger sets. In 2005, we solved the general problem with a polynomial time algorithm. More precisely we introduced a polynomial time criterion for deciding if an arithmetic automaton encodes a set of vectors definable in the Presburger arithmetic. Moreover, in the positive case we showed how to decode in polynomial time an arithmetic automaton to a Presburger formula. We spent the 2006 year to improve the solution in order to get efficient algorithms in practice. In a 134 pages long internal report, we provided the complete solution in full detail. The algorithm is based on many algorithmic solutions to difficult problems and a surprising application of the Stallings' folding process to extract periodicities from the strongly connected components of arithmetic automata. During the year 2007, with Gérald Point (LaBRI, Bordeaux), we implemented these algorithms in the tool BATOF. This tool is very efficient ! In fact the decoding of an arithmetic automaton with more than 100k states takes less than one minute on a standard computer. BATOF is the unique tool that implements a decoding algorithm. By combining BATOF with a tool computing arithmetic automata from Presburger formulas we obtain the unique implementation of a simplification and normalization procedure for Presburger formulas based on the minimization procedure for automata. These encouraging results were published in 2009 and provide a framework for solving the Presburger arithmetic with hybrid representations combining formulas and automata.

Recent papers: Related tools:


Ph.D. proposals Ph.D students and postdocs