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.
Implicational Relevance Logic is 2-ExpTime-Complete
Building 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. The result extends all the way up to intuitionistic contractive multiplicative exponential linear logic (IMELLC). Will be presented at RTA-TLCA 2014 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. Will be 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.
Model Checking Parse Trees
Joint work with A. Boral from CMI. We consider a variant of the satisfiability of PDL formulae on trees (or equivalently of Regular XPath), in presence of a tree language. The main originality is that the tree languages we consider are the set of parse trees (or parse forest) of a given word according to a context-free grammar. We show that this problem has applications in computational linguistics and for declarative syntactic specifications of programming languages, and study its computational complexity. Was presented at LICS 2013.

Full BibTeX

More publications...

Talks

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

MPRI 2013–2014
First half of the logical and computational structures for linguistic modeling course.
Practical sessions for the initiation to verification course.
Preparation to agregation 2013–2014
Courses in formal languages and automata for the computer science option of the French "agrégation de mathématiques".

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