FoSSaCS Invited Speaker Jérôme Leroux
Jérôme Leroux is a CNRS senior researcher, member and former director of the Formal Methods team of the computer science laboratory of Bordeaux (LaBRI) in France. He defended his PhD in 2003 on the model-checking of counter machines at ENS Paris-Saclay (ex Cachan). Over the past twenty years, he has been involved in several national and international research projects in the areas of the formal verification of infinite state systems, supported by several research grants from governmental research agencies. He worked on relations between automata and Presburger formulas for solving Presburger arithmetic up to 2006 before he started a new research project on the reachability problem for Petri nets. In 2009, he provided a new approach for solving that problem based on Presburger inductive invariants. Recently, he provided with several coauthors and teams the exact complexity of the reachability problem for Petri nets, closing a 40 years old open problem.
Talk
The Vector Addition System Reachability Problem
Wednesday, 9:00
Room: Europe A
Vector addition systems, or equivalently Petri nets are a long-established model of concurrency with extensive applications. The reachability problem that asks whether from a given initial configuration there exists a sequence of valid execution steps that reaches a given final configuration, is central. In fact, many problems, not necessarily related to this model, can be reduced or are even equivalent to the vector addition system reachability problem.
The complexity of the problem has remained unsettled between the 1960s and 2021. In fact, for many years no-complexity upper-bound was known, and the expspace-hardness result introduced by Richard Lipton in 1976 remained the state of the art in terms of complexity lower-bound. In 2019, with my colleague Sylvain Schmitz, we find a way to derive an Ackermannian complexity upper-bound. While this complexity was far away from the expspace complexity lower-bound, with my colleagues Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, and Filip Mazowiecki, we find a way the same year to improve the Lipton result by providing a Tower-hardness complexity lower-bound. Finally, in 2021 two groups, Wojciech Czerwinski and Lukasz Orlikowski on one side, and myself on the other side, independently find a way to show that the problem is in fact Ackermannian-complete.
In this presentation, we focus on the central ideas that provided a way to settle this long-standing open problem.