Sylvain Schmitz
Assistant professor
Get paper from arXiv
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
wellquasiorders and wellstructured transition systems. Here
is some of the material I coauthored on the subject:
Research
 Keywords
 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 dataaware 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 reprove Bozzelli & Ganty's 2EXP upper bound on the backward coverability algorithm for VAS using ideal representations of downwardsclosed sets. This yields a generic means of proving complexity upper bounds for coverability in WSTS. Presented at RP 2015.
 Fixeddimensional Energy Games are in Pseudopolynomial Time
 Joint work with M. Jurdziński and R. Lazić from U. Warwick. We show that multidimensional energy games can be solved in pseudopolynomial 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.
 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 wellquasiordering on runs.  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 wellquasiorderings, we provide the first known upper bound on the VAS reachability problem: it belongs to ${\mathbf{F}}_{{\omega}^{3}}$, a non primitiverecursive complexity class, among the lowest multiplyrecursive complexites.
Presented at LICS 2015.
 Implicational Relevance Logic is 2EXPTIMEComplete
 Building on the complexity of root coverability in branching VASSs, which was shown 2EXPcomplete by Demri et al., I show that the same complexity holds for provability in the implicational fragment of relevance logic, a problem open for almost 25 years. The result extends all the way up to intuitionistic contractive multiplicative exponential linear logic (IMELLC). Was presented at RTATLCA 2014 where it received the Best Paper Award during the Vienna Summer of Logic. Extended version accepted for publication in JSL.
 NonElementary Complexities for Branching VASS, MELL, and Extensions
 Joint work with R. Lazić from U. Warwick. We investigate the complexity of decision problems in substructural logics and branching variants of vector addition systems. Concretely, we define alternating branching vector addition systems with states (ABVASS) and provide reductions in both directions between their reachability problem and provability in propositional linear logic. These reductions carry over for fragments of linear logic and restricted ABVASS, and furthermore carry over in presence of structural weakening when considering lossy ABVASS and in presence of structural contraction when considering expansive ABVASS. For these two relaxations, we provide optimal complexity bounds on reachability, and thus on provability on the associated substructural logics: Towercomplete in the lossy case, and Ackermanncomplete in the expansive case. The former entails a new Tower lower bound on BVASS reachability and MELL provability. Was presented at CSLLICS 2014 during the Vienna Summer of Logic. Extended version published in ToCL.
Full BibTeX
More publications...
 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.
 DIMAP
Seminar, 4pm, May 26th, 2015, University of Warwick, Warwick,
UK.

I gave a lecture (on the blackboard) on complexity classes beyond
Elementary. Using the case of reachability in lossy counter
machines as a running example, I sketched the proofs of the
complexity lower and upper bounds, and motivated the need for
fastgrowing complexity classes. The lecture was based
mainly on the complexity classes paper.
 Oxford
Verification Seminar, 11am, May 6th, 2015, University of Oxford, Oxford,
UK.

I gave a lecture on ideal decompositions of downwardclosed
sets, and in particular on how they provide a new
understanding of the structures and computations defined in
the reachability algorithms for VAS developped by Mayr (1981), Kosaraju (1982), and Lambert
(1992).
The lecture is based on a joint paper with J. Leroux. Here are the
slides.
 Theory Seminar, 11am, April 28th, 2015, Queen Mary University of London, London, UK.
 I gave a lecture on the complexity of provability in systems of substructural logic, more precisely affine or contractive variants of linear logic. The main message is that a lot of insights into algorithmic complexity can be gained through interreductions with reachability problems in extensions of vector addition systems. The lecture is based on a joint paper with R. Lazić. Here are the slides.
 ACTS 2015, 11:45am, February 11, 2015, CMI, Chennai, India.
 I gave a chalk talk on the blackboard on the recent complexity upper bounds obtained with J. Leroux for the reachability problem in vector addition systems. Here are some mostly unreadable (guess you had to be there) slides compiled from photos (many thanks to A. Sangnier for taking these!).
More talks...