Sylvain Schmitz

"The complexity of reachability in vector addition systems"

( MPI-SWS talk in Kooperation mit dem Fachbereich Informatik)

The last few years have seen a surge of decision problems with an astronomical, non primitive-recursive complexity, in logic,verification, and games. While the existence of such uncontrived problems is known since the early 1980s, the field has matured with techniques for proving complexity lower and upper bounds and the definition of suitable complexity classes. This framework has been especially successful for analysing so-called `well-structured systems'---i.e., transition systems endowed with a well-quasi-order, which underly most of these astronomical problems---, but it turns out to be applicable to other decision problems that resisted analysis, including two famous problems: reachability in vector addition systems and bisimilarity of pushdown automata. In this talk, I will explain how some of these techniques apply to reachability in vector addition systems, yielding tight Ackermannian upper bounds for the decomposition algorithm initially invented by Mayr, Kosaraju, and Lambert; this will be based on joint work with Jérôme Leroux.

Bio: Sylvain Schmitz is an assistant professor (maître de conférences) at École Normale Supérieure Paris-Saclay since 2008 and a junior member of Institut Universitaire de France since 2018. He received his Ph.D. degree in Computer Science from Université Nice-Sophia Antipolis in 2007 and his habilitation from École Normale Supérieure Paris-Saclay in 2017. His research interests are in logic, verification, and complexity.