Sylvain Schmitz
Assistant professor on leave at INRIA
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
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
Most recent work:
- 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...
- 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...