Sylvain Schmitz

Assistant professor on leave at INRIA

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:

Alternating Vector Addition Systems with States
Joint work with J.-B. Courtois, based on his 2013 MSc. Thesis. Originally motivated by the study of the complexity of deciding whether a vector addition system with states (VASS) simulates a finite-state system, or vice versa, we investigate a formalism of alternating VASS. We show that the state reachability (aka leaf coverability) problem for AVASS is 2ExpTime-complete, and derive new compexity bounds for the simulation problems. Presented at MFCS 2014.
Implicational Relevance Logic is 2-ExpTime-Complete
Best Paper Award at RTA-TLCA 2014Building on the complexity of root coverability in branching VASSs, which was shown 2-ExpTime-complete 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 RTA-TLCA 2014 where it received the Best Paper Award during the Vienna Summer of Logic.
Non-Elementary 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: Tower-complete in the lossy case, and Ackermann-complete in the expansive case. The former entails a new Tower lower bound on BVASS reachability and MELL provability. Was presented at CSL-LICS 2014 during the Vienna Summer of Logic.
The Power of Priority Channel Systems
Joint work with C. Haase and Ph. Schnoebelen. We introduce priority channel systems, a new class of channel systems where messages carry a numeric priority, and where higher priority messages can supercede lower priority ones preceding them in the fifo communication buffers. Such systems can be used to model differentiated service protocols, where packet dropping policies in congested networks rely on priorities to maintain the quality of service for important messages. We prove that safety and inevitability properties are decidable in priority channel systems, and that their computational complexity is complete for Fε0. Presented at Concur 2013.

Full BibTeX

More publications...


Groupe de travail Modélisation et Vérification, 11:00am, December 4, 2014, LaBRI, Bordeaux, France.
Séminaire Automates, 2:30pm, November 14, 2014, LIAFA, Paris, France.
A survey of the many guises under which alternating vector addition systems with states have been (re)invented, along with a few complexity results together with J.-B. Courtois, M. Jurdziński, and R. Lazić. Here are the slides.
Groupe de travail Sémantique, 2pm, October 22, 2014, PPS, Paris, France.
A talk based on the paper Implicational Relevance Logic is 2-EXPTIME-Complete. Here are the slides.
Chocola Seminar, 10:30am, October 16, 2014, ENS Lyon, France.
A chalk talk based on the paper Non-Elementary Complexities for Branching VASS, MELL, and Extensions with R. Lazić.
RP 2014, 2pm, September 22nd, 2014, University of Oxford, UK.
Invited talk on the complexity of programs proven to terminate thanks to a ranking function into some ordinal. See the supporting paper, and the slides, which contain a bonus application: the first complexity upper bounds on the reachability problem in vector addition systems!
MFCS 2014, 5pm, August 26th, 2014, Budapest, Hungary.
I presented the paper Alternating Vector Addition Systems with States written with J.-B. Courtois. Here are the slides.
RTA-TLCA 2014, Vienna Summer of Logic, 10:45am, July 14th, 2014, Informatikhörsaal, TU Vienna, Austria.
I presented the paper Implicational Relevance Logic is 2-ExpTime-Complete. Here are the slides.
Dagstuhl Seminar 14141 Reachability Problems for Infinite-State Systems, 9am, April 1st, 2014, Schloss Dagstuhl, Germany.
I presented a one-hour survey on non-elementary complexity classes. See the paper for in-depth material.
Groupe de travail modélisation et vérification, 11am, March 13th, 2014, room 076, LaBRI, Bordeaux, France.
I presented a joint work with C. Haase and Ph. Schnoebelen on priority channel systems. Here are the slides.

More talks...

Other activities


(On partial leave at INRIA in 2013—2015.)

MPRI 2014–2015
Second half of the logical and computational structures for linguistic modeling course.
Computer science option of the French "agrégation de mathématiques"
Courses on formal languages and automata.

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