Sylvain Schmitz

Assistant professor
Leverhulme Visiting Professor at the University of Warwick

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:

Fixed-dimensional Energy Games are in Pseudo-polynomial Time
Joint work with M. Jurdziński and R. Lazić from U. Warwick. We show that multi-dimensional energy games can be solved in pseudo-polynomial time when the dimension is fixed, answering an open question of Chaloupka (2013). This entails a 2-ExpTime 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 2-ExpTime hardness proven last year with J.-B. Courtois.
Reachability in Vector Addition Systems Demystified
Joint work with J. Leroux from LaBRI. The deciddability 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.
  1. 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 well-quasi-ordering on runs.
  2. 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 well-quasi-orderings, we provide the first known upper bound on the VAS reachability problem: it belongs to F ω 3 , a non primitive-recursive complexity class, among the lowest multiply-recursive complexites.
    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. Extended version accepted for publication in JSL.
    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. Extended version accepted for publication in ToCL.

    Full BibTeX

    More publications...

    Talks

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

    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