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:

Research

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

Publications

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...

Talks

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.
LAAG Reading Group, 10:30am, December 19th, 2013, room 4068, U. Paris Diderot, Paris, France.
A whiteboard presentation of non-elementary complexity classes and problems, mostly on subrecursive hierarchies with a few words on length function theorems for well-quasi-orderings. Some background material for this talk can be found in this paper and in these lecture notes.
Theory Seminar, 11am, December 11th, 2013, room CS:404, Queen Mary, London, UK.
I presented recent work on non-elementary complexity classes and problems. Here are the slides and associated paper.
68nqrt Seminar, 2:30pm, November 7th, 2013, Markov room, IRISA, France.
I presented a survey and some work in progress with J.-B. Courtois on vector addition games. See the slides.

More talks...

Other activities

Teaching

(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

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