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:

Research

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

Publications

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

Dagstuhl Seminar 16031 Well Quasi-Orders in Computer Science, 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 shall discuss 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 will be based on the article Complexity hierarchies beyond Elementary to appear in ToCT.
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.
LICS 2015, 11:15am, July 6th, 2015, Kyoto, Japan.
I presented the article Demystifying Reachability in Vector Addition Systems written with J. Leroux. Here are the slides.
DIMAP Logic Day 2015, 9am, June 1st, 2015, University of Warwick, Warwick, UK.
I presented the recent joint work with J. Leroux on deriving complexity upper bounds for the reachability problem 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

Contact

Export in vCard format

Sylvain Schmitz
Address
LSV, CNRS & ENS de Cachan
61, avenue du Président Wilson
94235 CACHAN Cedex, France
Office
RH-B-102
Phone
+33 (0)1 47 40 75 42
Fax
+33 (0)1 47 40 75 21
Secr.
+33 (0)1 47 40 75 20
E-Mail
Sylvain.Schmitz@lsv.ens-cachan.fr

Funding