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

Recent Publications

Th. Colcombet, M. Jurdziński, R. Lazić and S. SchmitzPerfect Half Space GamesIn LICS'17. IEEE Press, June 2017. To appear. BibTeX )
B. Bérard, S. Haar, S. Schmitz and S. SchwoonThe Complexity of Diagnosability and Opacity Verification for Petri NetsIn PETRI NETS'17, LNCS. Springer, June 2017. To appear. Web page | BibTeX )
J. Goubault-Larrecq and S. SchmitzDeciding Piecewise Testable Separability for Regular Tree LanguagesIn ICALP'16, Leibniz International Proceedings in Informatics 55, pages 97:1-97:15. Leibniz-Zentrum für Informatik, July 2016. Web page | BibTeX )
R. Lazić and S. SchmitzThe Complexity of Coverability in ν-Petri NetsIn LICS'16, pages 467-476. ACM Press, July 2016. Web page | BibTeX )
D. Baelde, S. Lunel and S. SchmitzA Sequent Calculus for a Modal Logic on Finite Data TreesIn CSL'16, Leibniz International Proceedings in Informatics 62, pages 32:1-32:16. Leibniz-Zentrum für Informatik, September 2016. Web page | BibTeX )

Full BibTeX

More publications...

Recent Talks

Verification Seminar, 11am, November 2nd, 2016, Department of Computer Science, Oxford University, Oxford, UK
I presented the paper The Complexity of Coverability in ν-Petri Nets written with R. Lazić. Here are the slides.
Verification Seminar, 11am, October 24th, 2016, IRIF, Paris, France
I presented the applications of ideals of well-quasi-orders for the verification of vector addition systems, based on the papers Demystifying Reachability in Vector Addition Systems and Ideal Decompositions for Vector Addition Systems with J. Leroux. Here are the slides.
Highlights 2016, 14:51pm, September 8th, 2016, Université libre de Bruxelles, Brussels, Belgium.
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 papaer and the slides.
ICALP 2016, 11:45am, July 12th, 2016, Sapienza University, Rome, Italy.
I presented the paper Deciding Piecewise Testable Separability for Regular Tree Languages written with J. Goubault-Larrecq. Here are the slides.
LICS 2016, 16:11pm, July 6th, 2016, Columbia University, New York, USA.
I presented the joint paper 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.
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.

More talks...

Other activities

Teaching (2016–2017)

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 lectures.
Tree automata, techniques and applications lectures.
Computer science option of the French "agrégation de mathématiques", ENS Cachan
Lectures on formal languages and automata.
Second half of the lectures on logic.
Bachelor of computer science, ENS Cachan
Lectures in formal languages.
Department of doctoral studies, ENS Cachan
Tutorial on searching and publishing on the web

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