Sylvain Schmitz

Assistant professor, ENS Cachan

Research

Keywords: Verification, infinite systems, wqo, formal languages, parsing, computational linguistics

Publications

Most recent work:

The Ordinal-Recursive Complexity of Timed-Arc Petri Nets, Data Nets, and Other Enriched Nets: Joint work with S. Haddad and Ph. Schnoebelen. We prove the completeness of the coverability and termination problems for timed-arc Petri nets (and other classes of coloured Petri nets) for $F_{ω^{ω^{ω}}}$ . Will be presented at LICS 2012.
Model-Checking Coverability Graphs of Vector Addition Systems: Joint work with Michel Blockelet, based on his MSc. Thesis at MPRI. We propose a different unifying framework for expressing properties on VAS using their coverability graph. We introduce for this an extension of CTL allowing to express such properties, and show decidability and even ExpSpace-completeness for the VAS model-checking problem of some fragments. Presented at MFCS 2011.
Multiply-Recursive Bounds with Higman's Lemma: Joint work with Philippe Schnoebelen on complexity upper bounds derivable from the use of Higman's Lemma, a new milestone in our work on complexity bounds for wqo-based termination arguments, started with Dickson's Lemma. Presented at ICALP 2011.
Ackermannian and Primitive-Recursive Bounds with Dickson's Lemma: Joint work with Diego Figueira, Santiago Figueira, and Philippe Schnoebelen on complexity upper bounds derivable from the use of Dickson's Lemma. Presented at LICS 2011.
Forward Analysis and Model Checking for Bounded WSTS: Joint work with Pierre Chambart and Alain Finkel. We identify a recursive subclass of WSTS, for which action-based LTL properties are decidable. Presented at Petri Nets 2011.
A Note on Sequential Rule-Based POS Tagging: An alternative proof that the contextual rules of the Brill POS tagger can be implemented as a sequential function. I wrote this as part of the lecture notes for the MPRI course 2-27-1 before extracting this short note. Presented at FSMNLP 2011.