Sylvain Schmitz

Assistant professor

Complexity Hierarchies Beyond Elementary

Get paper from arXiv

Don't Panic!

I've been busy these last few years trying to get a clear picture of the complexity of problems that arise from the use of well-quasi-orders and well-structured transition systems. Here is some of the material I co-authored on the subject:


Verification, infinite systems, well quasi orders, formal languages, parsing, computational linguistics


Most recent work:

A Sequent Calculus for a Modal Logic on Finite Data Trees
Joint work with David Baelde from LSV and Simon Lunel and based on Simon's Master Thesis. As a first dive into proof systems for data-aware logics, in the context of the ANR Prodaq project, we propose a sequent calculus for a modal fragment of DataXPath. We further show that proof search in this calculus can be performed in PSPACE, which is optimal for the logic.
The Ideal View on Rackoff's Coverability Technique
Joint work with R. Lazić from U. Warwick. We re-prove Bozzelli & Ganty's 2EXP upper bound on the backward coverability algorithm for VAS using ideal representations of downwards-closed sets. This yields a generic means of proving complexity upper bounds for coverability in WSTS. Presented at RP 2015.
Fixed-dimensional Energy Games are in Pseudo-polynomial Time
Joint work with M. Jurdziński and R. Lazić from U. Warwick. We show that multi-dimensional energy games can be solved in pseudo-polynomial time when the dimension is fixed, answering an open question of Chaloupka (2013). This entails a 2EXP upper bound for multidimensional energy games when both the dimension and the initial credit are part of the input, answering an open question of Brázdil et al. (2010), and closes the gap with 2EXP hardness proven last year with J.-B. Courtois. Presented at ICALP 2015.
Demystifying Reachability in Vector Addition Systems
Joint work with J. Leroux from LaBRI. The decidability of reachability in vector addition systems (VAS), or equivalently in Petri nets, is arguably one of the landmark results in theoretical computer science. The first proof by Mayr (1981) and its further simplifications by Kosaraju (1982) and Lambert (1992) are extremely complex on two accounts.
  1. First, on a conceptual side, they rely on a somewhat magical decomposition technique. We expose the tricks involved in this construction, by showing that this decomposition technique can be recast as the computation of an ideal decomposition of the set of runs, for an appropriately chosen well-quasi-ordering on runs.
  2. Second, on a complexity side, no upper bounds were known until now for the decomposition algorithms. Using recent results on the complexity of algorithms that terminate thanks to well-quasi-orderings, we provide the first known upper bound on the VAS reachability problem: it belongs to F ω 3 , a non primitive-recursive complexity class, among the lowest multiply-recursive complexites.
Presented at LICS 2015.

Full BibTeX

More publications...

Recent Talks

Séminaire de l'équipe Méthodes Formelles, 11am, March 8th, 2016, LaBRI, Bordeaux.
I presented a joint work with R. Lazić on the complexity of coverability in ν-Petri nets, an extension of Petri nets with data management and creation capabilities. Here are the preprint and the slides.
Dagstuhl Seminar 16031 Well Quasi-Orders in Computer Science, 4:30pm, January 21st, 2016, Schloss Dagstuhl, Germany.
Well-quasi-orders provide termination or finiteness arguments for many algorithms, and miniaturised versions can furthermore be employed to prove complexity upper bounds for those algorithms. We have however an issue with these bounds: they go way beyond the familiar complexity classes used in complexity theory. I discussed a definition of complexity classes suitable for the task. In particular, unlike the subrecursive classes they are based on, those classes support the usual notions of reduction and completeness. The talk was based on the article Complexity hierarchies beyond Elementary.
Reading Group on Logic, Automata, Algebra and Games, 10:30am, January 7th, 2016, Université Paris-Diderot.
Chalk talk on ideals in VAS reachability. The decidability of the reachability problem for vector addition systems is a notoriously difficult result. First shown by Mayr in 1981 after a decade of unsuccessful attempts and partial results, its proof has been simplified and refined several times, by Kosaraju and Lambert, and re-proven by very different techniques by Leroux in 2011. The principles behind the original proof remained however obscure. In this seminar, I presented the ideas behind the algorithms of Mayr, Kosaraju, and Lambert (the KLM algorithm) in the light of ideals of well-quasi-orders. The interest here is that ideals provide a semantics to the structures manipulated in the KLM algorithm, bringing some new understanding to its proof of correctness. This approach is based on a joint work with Jérôme Leroux (LaBRI) presented at LICS'15.
Reading Group on Logic, Automata, Algebra and Games, 10:30am, December 3rd, 2015, Université Paris-Diderot.
Chalk talk on ideals of well-quasi-orders. These irreducible downwards-closed sets of elements were first invented in the 1970's but rediscovered in recent years in the theory of well-structured transition systems, notably by Finkel and Goubault-Larrecq. Ideals provide indeed finite effective representations of downwards-closed sets, in the same way as bases of minimal elements provide representations of upwards-closed sets. After defining ideals and establishing some of their properties, I illustrated their use in a concrete setting. I presented some recent results by Czerwiński, Martens, van Rooijen, and Zeitoun (FCT'15) on the decidability of piecewise-testable separability in the light of ideals. This seminar was also a warm-up for the next seminar on reachability in vector addition systems.

More talks...

Other activities

Teaching (2015–2016)

ESSLLI 2016, Bolzano-Bozen
Course on Algorithmic Aspects of WQO Theory together with Ph. Schnoebelen.
MPRI, Paris
First half of the logical and computational structures for linguistic modelling course.
First half of the initiation to verification course.
Computer science option of the French "agrégation de mathématiques", ENS Cachan
Courses on formal languages and automata.
Bachelor of computer science, ENS Cachan
Labs for the second half of the computability and complexity course.
Labs for the formal languages course.

Further documents and course pages related to my older teaching activities can be found in my teaching activities page.

About LSV


Export in vCard format

Sylvain Schmitz
LSV, CNRS & ENS de Cachan
61, avenue du Président Wilson
94235 CACHAN Cedex, France
+33 (0)1 47 40 75 42
+33 (0)1 47 40 75 21
+33 (0)1 47 40 75 20