@inproceedings{schmitz-dlt06,
  address = {Santa Barbara, California, USA},
  month = jun,
  year = 2006,
  volume = 4036,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Dang, Zhe and Ibarra, Oscar H.},
  acronym = {{DLT}'06},
  booktitle = {{P}roceedings of the 10th {I}nternational
               {C}onference on {D}evelopments in {L}anguage {T}heory
               ({DLT}'06)},
  author = {Schmitz, Sylvain},
  title = {Noncanonical {LALR}(1) Parsing},
  pages = {95-107},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/schmitz-dlt06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/schmitz-dlt06.pdf},
  doi = {10.1007/11779148_10},
  abstract = {This paper addresses the longstanding problem of the recognition
                  limitations of classical LALR(1) parser generators by
                  proposing the usage of noncanonical parsers. To this end, we
                  present a definition of noncanonical LALR(1) parsers,
                  NLALR(1). The class of grammars accepted by NLALR(1) parsers
                  is a proper superclass of the NSLR(1) and LALR(1) grammar
                  classes. Among the recognized languages are some
                  nondeterministic languages. The proposed parsers retain many
                  of the qualities of canonical LALR(1) parsers: they are
                  deterministic, easy to construct, and run in linear time. We
                  argue that they could provide the basis for a range of
                  powerful noncanonical parsers.}
}
@inproceedings{FSF-ciaa06,
  address = {Taipei, Taiwan},
  month = aug,
  year = 2006,
  volume = 4094,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  editor = {Ibarra, Oscar H. and Yen, Hsu-Chun},
  acronym = {{CIAA}'06},
  booktitle = {{P}roceedings of the 11th {I}nternational 
           {C}onference on {I}mplementation and
           {A}pplication of {A}utomata
           ({CIAA}'06)},
  author = {Fortes G{\'a}lvez, Jos{\'e} and Schmitz, Sylvain
                 and Farr{\'e}, Jacques},
  title = {Shift-Resolve Parsing: Simple, Linear Time,
                 Unbounded Lookahead},
  pages = {253-264},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FSF-ciaa06.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FSF-ciaa06.pdf},
  doi = {10.1007/11812128_24},
  abstract = {This paper introduces a mechanism for combining unbounded
                  lookahead exploration with linear time complexity in a
                  deterministic parser. The idea is to use a resolve parsing
                  action in place of the classical reduce. The construction of
                  shift-resolve parsers is presented as a two-step algorithm,
                  from the grammar to a finite nondeterministic automaton, and
                  from this automaton to the deterministic parser. Grammar
                  classes comparisons are provided.}
}
@techreport{Schmitz-rri3s06,
  author = {Sylvain Schmitz},
  title = {Modular Syntax Demands Verification},
  institution = {Laboratoire {I3S}, Universit{\'e} de Nice-Sophia Antipolis, France},
  month = oct,
  year = 2006,
  number = {I3S/RR-2006-32-FR},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/schmitz-RR0632.pdf},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/schmitz-RR0632.pdf},
  abstract = {Modular grammatical formalisms provide an essential step
                  towards improved grammar engineering practices. However, as
                  we depart from traditional deterministic models, some
                  intrinsic static checks are lost. The paper shows why
                  grammar verification is necessary for reliable uses of
                  context-free grammars (CFGs) and parsing expression grammars
                  (PEGs) as modular syntax definitions. Simple conservative
                  verification procedures are presented for each formalism.}
}
@inproceedings{Schmitz-ldta07,
  address = {Braga, Portugal},
  month = apr,
  year = 2008,
  number = 2,
  volume = 203,
  series = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier Science Publishers},
  editor = {Sloane, Anthony and Johnstone, Adrian},
  acronym = {{LDTA}'07},
  booktitle = {{P}roceedings of the 7th {W}orkshop on {L}anguage {D}escriptions,
                  {T}ools, and {A}pplications ({LDTA}'07)},
  author = {Sylvain Schmitz},
  title = {An Experimental Ambiguity Detection Tool},
  pages = {69-84},
  url = {http://hal.archives-ouvertes.fr/hal-00436398},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Schmitz-ldta07.pdf},
  doi = {10.1016/j.entcs.2008.03.045},
  abstract = {Although programs convey an unambiguous meaning, the grammars
                  used in practice to describe their syntax are often
                  ambiguous, and completed with disambiguation rules. Whether
                  these rules achieve to remove all the ambiguities while
                  preserving the original intended language can be difficult
                  to ensure. We present an experimental ambiguity detection
                  tool for GNU Bison, and illustrate how it can assist a
                  grammatical development for a subset of Standard ML.}
}
@inproceedings{Schmitz-icalp07,
  address = {Wroc{\l}aw, Poland},
  month = jul,
  year = 2007,
  volume = 4596,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Arge, Lars and Cachin, {\relax Ch}ristian and Jurdzi{\'n}ski, Tomasz
	 	and Tarlecki, Andrzej},
  acronym = {{ICALP}'07},
  booktitle = {{P}roceedings of the 34th {I}nternational 
               {C}olloquium on {A}utomata, {L}anguages and 
               {P}rogramming ({ICALP}'07)},
  author = {Sylvain Schmitz},
  title = {Conservative Ambiguity Detection in Context-Free Grammars},
  pages = {692-703},
  url = {http://hal.archives-ouvertes.fr/hal-00610222},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Schmitz-icalp07.pdf},
  futureslides = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/SLIDES/
		Schmitz-icalp07-slides.pdf},
  doi = {10.1007/978-3-540-73420-8_60},
  abstract = {The ability to detect ambiguities in context-free grammars is
                  vital for their use in several fields, but the problem is
                  undecidable in the general case. We present a safe,
                  conservative approach, where approximations cannot result in
                  overlooked ambiguous cases. We analyze the complexity of its
                  use, and compare it with other ambiguity detection methods.}
}
@phdthesis{phd-Schmitz07,
  author = {Sylvain Schmitz},
  title = {Approximating Context-Free Grammars for Parsing and
                 Verification},
  month = sep,
  year = 2007,
  school = {Laboratoire {I3S}, Universit{\'e} de Nice-Sophia Antipolis, France},
  type = {Th{\`e}se de doctorat},
  url = {http://tel.archives-ouvertes.fr/tel-00271168},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/phd-schmitz07.pdf},
  abstract = {Programming language developers are blessed with the
    availability of efficient, powerful tools for parser generation. But even
    with automated help, the implementation of a parser often remains overly
    complex.\par
    Although programs should convey an unambiguous meaning, the parsers
    produced for their syntax, specified by a context-free grammar, are most
    often nondeterministic, and even ambiguous. Facing the limitations of
    traditional deterministic parsers, developers have embraced general
    parsing techniques, capable of exploring every nondeterministic choice,
    but offering no unambiguity warranty. The real challenge in parser
    development lies then in the proper identification and treatment of
    ambiguities---but these issues are undecidable.\par
    The grammar approximation technique discussed in the thesis is applied to
    nondeterminism and ambiguity issues in two different ways. The first
    application is the generation of noncanonical parsers, less prone to
    nondeterminism, mostly thanks to their ability to exploit an unbounded
    context-free language as right context to guide their decision. Such
    parsers enforce the unambiguity of the grammar, and furthermore warrant a
    linear time parsing complexity. The second application is ambiguity
    detection in itself, with the insurance that a grammar reported as
    unambiguous is actually so, whatever level of approximation we might
    choose.}
}
@inproceedings{SLR-tagp08,
  address = {T{\"u}bingen, Germany},
  month = jun,
  year = 2008,
  editor = {Gardent, Claire and Sarkar, Anoop},
  acronym = {{TAG+}'08},
  booktitle = {{P}roceedings of the 9th {I}nternational {W}orkshop on {T}ree
                  {A}djoining {G}rammars and {R}elated {F}ormalisms ({TAG+}'08)},
  author = {Schmitz, Sylvain and Le{~}Roux, Joseph},
  title = {Feature Unification in {TAG} Derivation Trees},
  pages = {141-148},
  url = {http://arxiv.org/abs/0804.4584},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SLR-tag+08.pdf},
  abstract = {Compared to derived trees, the derivation trees of a tree
                  adjoining grammar provide a first insight into the sentence
                  semantics, and are thus prime targets for generation
                  systems. We define a formalism, feature based regular tree
                  grammars, that produces derivation trees that account for
                  the feature structures found in a tree adjoining grammar. We
                  provide an optimized translation from tree adjoining
                  grammars into this formalism.}
}
@article{schmitz-scp10,
  publisher = {Elsevier Science Publishers},
  journal = {Science of Computer Programming},
  author = {Sylvain Schmitz},
  title = {An Experimental Ambiguity Detection Tool},
  volume = 75,
  number = {1-2},
  pages = {71-84},
  month = jan,
  year = 2010,
  doi = {10.1016/j.scico.2009.07.002},
  url = {http://hal.archives-ouvertes.fr/hal-00436398},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/schmitz-scp10.pdf},
  abstract = {Although programs convey an unambiguous meaning, the grammars
   used in practice to describe their syntax are often ambiguous, and
   completed with disambiguation rules. Whether these rules achieve the
   removal of all the ambiguities while preserving the original intended
   language can be difficult to ensure. We present an experimental ambiguity
   detection tool for GNU Bison, and illustrate how it can assist a
   grammatical development for a subset of Standard~ML.}
}
@inproceedings{HNS-ciaa09,
  address = {Sydney, Australia},
  month = jul,
  year = 2009,
  volume = 5642,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  editor = {Maneth, Sebastian},
  acronym = {{CIAA}'09},
  booktitle = {{P}roceedings of the 14th {I}nternational 
           {C}onference on {I}mplementation and
           {A}pplication of {A}utomata
           ({CIAA}'09)},
  author = {H{\'e}am, Pierre-Cyrille and Nicaud, Cyril and Schmitz, Sylvain},
  title = {Random Generation of Deterministic Tree (Walking) Automata},
  pages = {115-124},
  doi = {10.1007/978-3-642-02979-0_15},
  url = {http://hal.inria.fr/inria-00408316},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HNS-ciaa09.pdf},
  abstract = {Uniform random generators deliver a simple empirical means to
    estimate the average complexity of an algorithm. We present a general
    rejection algorithm that generates sequential letter-to-letter transducers
    up to isomorphism. We tailor this general scheme to randomly generate
    deterministic tree walking automata and deterministic top-down tree
    automata. We apply our implementation of the generator to the estimation
    of the average complexity of a deterministic tree walking automata to
    nondeterministic top-down tree automata construction we also implemented.}
}
@inproceedings{Schmitz-acl10,
  address = {Uppsala, Sweden},
  month = jul,
  year = 2010,
  publisher = {Association for Computational Linguistics},
  acronym = {{ACL}'10},
  booktitle = {{P}roceedings of the 48th {A}nnual {M}eeting of the 
  	   {A}ssociation for {C}omputational {L}inguistics ({ACL}'10)},
  author = {Schmitz, Sylvain},
  title = {On the Computational Complexity of Dominance Links
                 in Grammatical Formalisms},
  pages = {514-524},
  url = {http://hal.archives-ouvertes.fr/hal-00482396},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Schmitz-acl10.pdf},
  abstract = {Dominance links were introduced in grammars to model long
    distance scrambling phenomena, motivating the definition of multiset-valued
    linear indexed grammars (MLIGs) by Rambow~(1994b), and inspiring quite a
    few recent formalisms. It~turns out that MLIGs have since been
    rediscovered and reused in a variety of contexts, and that the complexity
    of their emptiness problem has become the key to several open questions in
    computer science. We survey complexity results and open issues on MLIGs
    and related formalisms, and provide new complexity bounds for some
    linguistically motivated restrictions.}
}
@article{HNS-tcs10,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {H{\'e}am, Pierre-Cyrille and Nicaud, Cyril and
                 Schmitz, Sylvain},
  title = {Parametric Random Generation of Deterministic Tree
                 Automata},
  year = 2010,
  volume = 411,
  number = {38-39},
  pages = {3469-3480},
  month = aug,
  url = {http://hal.inria.fr/inria-00511450},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HNS-tcs10.pdf},
  doi = {10.1016/j.tcs.2010.05.036},
  abstract = {Uniform random generators deliver a simple empirical means to
    estimate the average complexity of an algorithm. We present a general
    rejection algorithm that generates sequential letter-to-letter transducers
    up to isomorphism. We~also propose an original parametric random
    generation algorithm to produce sequential letter-to-letter transducers
    with a fixed number of transitions. We~tailor this general scheme to
    randomly generate deterministic tree walking automata and deterministic
    top-down tree automata. We~apply our implementation of the generator to
    the estimation of the average complexity of a deterministic tree walking
    automata to nondeterministic top-down tree automata construction we also
    implemented.}
}
@inproceedings{ltc-GardentPPS11,
  address = {Pozna\'n, Poland},
  month = nov,
  year = 2014,
  volume = {8387},
  series = {Lecture Notes in Artificial Intelligence},
  publisher = {Springer},
  editor = {Vetulani, Zygmunt and Mariani, Joseph},
  acronym = {{LTC}'11},
  booktitle = {{P}roceedings of the 5th {L}anguage {\&} {T}echnology
                  {C}onference ({LTC}'11)},
  author = {Gardent, Claire and Perrier, Guy and Parmentier, Yannick
                  and Schmitz, Sylvain},
  title = {Lexical Disambiguation in {LTAG} using Left Context},
  nopages = {},
  url = {http://hal.archives-ouvertes.fr/hal-00629902/},
  abstract = {In this paper, we present an automaton-based lexical
                  disambiguation process for Lexicalized Tree-Adjoining
                  Grammar (LTAG).  This process builds on previous work
                  of Bonfante \textit{et~al.}~(2004), and extends it by
                  computing a polarity-based abstraction, which
                  contains information about left context.  This
                  extension allows for a faster lexical disambiguation
                  by reducing the filtering automaton.}
}
@inproceedings{Schmitz-fsmnlp11,
  address = {Blois, France},
  month = jul,
  year = 2011,
  publisher = {ACL Press},
  editor = {Maletti, Andreas},
  acronym = {{FSMNLP}'11},
  booktitle = {{P}roceedings of the 9th {I}nternational {W}orkshop on
                  {F}inite-{S}tate {M}ethods and {N}atural {L}anguage
                  {P}rocessing ({FSMNLP}'11)},
  author = {Sylvain Schmitz},
  title = {A~Note on Sequential Rule-Based {POS} Tagging},
  pages = {83-87},
  url = {http://hal.archives-ouvertes.fr/hal-00600260/},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Schmitz-fsmnlp11.pdf},
  abstract = {Brill's part-of-speech tagger is defined through a cascade of
    leftmost rewrite rules. We revisit the compilation of such rules into a
    single sequential transducer given by Roche and Schabes (\textit{Comput.
    Ling.}~1995) and provide a direct construction of the minimal sequential
    transducer for each individual rule.}
}
@inproceedings{BS-mfcs11,
  address = {Warsaw, Poland},
  month = aug,
  year = 2011,
  volume = 6907,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Murlak, Filip and Sankowski, Piotr},
  acronym = {{MFCS}'11},
  booktitle = {{P}roceedings of the 36th
               {I}nternational {S}ymposium on
               {M}athematical {F}oundations of 
               {C}omputer {S}cience
               ({MFCS}'11)},
  author = {Blockelet, Michel and Schmitz, Sylvain},
  title = {Model-Checking Coverability Graphs of Vector Addition Systems},
  pages = {108-119},
  url = {http://hal.archives-ouvertes.fr/hal-00600077/},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-mfcs11.pdf},
  doi = {10.1007/978-3-642-22993-0_13},
  abstract = {A large number of properties of a vector addition system---for
    instance coverability, boundedness, or regularity---can be decided using its
    coverability graph, by looking for some characteristic pattern. We propose
    to unify the known exponential-space upper bounds on the complexity of
    such problems on vector addition systems, by seeing them as instances of
    the model-checking problem for a suitable extension of computation tree
    logic, which allows to check for the existence of these patterns. This
    provides new insights into what constitutes a {"}coverability-like{"}
    property.}
}
@inproceedings{SS-icalp11,
  address = {Z{\"u}rich, Switzerland},
  month = jul,
  year = 2011,
  volume = 6756,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Aceto, Luca and Henzinger, Monika and Sgall, Jir{\'\i}},
  acronym = {{ICALP}'11},
  booktitle = {{P}roceedings of the 38th {I}nternational 
               {C}olloquium on {A}utomata, {L}anguages and 
               {P}rogramming ({ICALP}'11)~-- {P}art~{II}},
  author = {Schmitz, Sylvain and Schnoebelen, {\relax Ph}ilippe},
  title = {Multiply-Recursive Upper Bounds with {H}igman's Lemma},
  pages = {441-452},
  url = {http://arxiv.org/abs/1103.4399},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SS-icalp11.pdf},
  doi = {10.1007/978-3-642-22012-8_35},
  abstract = {We develop a new analysis for the length of controlled
                  bad sequences in well-quasi-orderings based on
                  Higman's Lemma. This leads to tight
                  multiply-recursive upper bounds that readily apply
                  to several verification algorithms for
                  well-structured systems.}
}
@inproceedings{CFS-atpn2011,
  address = {Newcastle upon Tyne, UK},
  month = jun,
  year = 2011,
  volume = {6709},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Kristensen, Lars M. and Petrucci, Laure},
  acronym = {{PETRI~NETS}'11},
  booktitle = {{P}roceedings of the 32nd
               {I}nternational {C}onference on
               {A}pplications and {T}heory of {P}etri {N}ets
               ({PETRI~NETS}'11)},
  author = {Chambart, Pierre and Finkel, Alain and Schmitz, Sylvain},
  title = {Forward Analysis and Model Checking for Trace Bounded {WSTS}},
  nopages = {49-68},
  url = {http://arxiv.org/abs/1004.2802},
  doi = {10.1007/978-3-642-21834-7_4},
  abstract = {We investigate a subclass of well-structured transition
    systems~(WSTS), the bounded---in the sense of Ginsburg and Spanier (Trans.
    AMS 1964)---complete deterministic ones, which we claim provide an
    adequate basis for the study of forward analyses as developed by Finkel
    and Goubault-Larrecq (ICALP~2009). Indeed, we prove that, unlike other
    conditions considered previously for the termination of forward analysis,
    boundedness is decidable. Boundedness turns out to be a valuable
    restriction for WSTS verification, as we show that it further allows to
    decide all \(\omega\)-regular properties on the set of infinite traces of
    the system.}
}
@inproceedings{FFSS-lics2011,
  address = {Toronto, Canada},
  month = jun,
  year = 2011,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{LICS}'11},
  booktitle = {{P}roceedings of the 26th
               {A}nnual {IEEE} {S}ymposium on
               {L}ogic in {C}omputer {S}cience
               ({LICS}'11)},
  author = {Figueira, Diego and Figueira, Santiago and Schmitz, Sylvain and
  	   Schnoebelen,  {\relax Ph}ilippe},
  title = {{A}ckermannian and Primitive-Recursive Bounds with {D}ickson's Lemma},
  pages = {269-278},
  url = {http://arxiv.org/abs/1007.2989},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FFSS-lics11.pdf},
  doi = {10.1109/LICS.2011.39},
  abstract = {Dickson's Lemma is a simple yet powerful tool widely used in
    decidability proofs, especially when dealing with counters or related data
    structures in algorithmics, verification and model-checking, constraint
    solving, logic, etc. While Dickson's Lemma is well-known, most computer
    scientists are not aware of the complexity upper bounds that are entailed
    by its use. This is mainly because, on this issue, the existing literature
    is not very accessible.\par
    We propose a new analysis of the length of bad sequences over
    \((\mathbb{N}^{k},\leq)\), improving on earlier results and providing
    upper bounds that are essentially tight. This analysis is complemented by
    a {"}user guide{"} explaining through practical examples how to easily
    derive complexity upper bounds from Dickson's Lemma.}
}
@unpublished{aawqot,
  author = {Sylvain Schmitz and {\relax Ph}ilippe Schnoebelen},
  title = {Algorithmic Aspects of {WQO} Theory},
  month = aug,
  year = 2012,
  note = {Lecture Notes},
  url = {http://cel.archives-ouvertes.fr/cel-00727025},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SS-esslli12.pdf}
}
@inproceedings{HSS-lics2012,
  address = {Dubrovnik, Croatia},
  month = jun,
  year = 2012,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{LICS}'12},
  booktitle = {{P}roceedings of the 27th
               {A}nnual {IEEE} {S}ymposium on
               {L}ogic in {C}omputer {S}cience
               ({LICS}'12)},
  author = {Haddad, Serge and Schmitz, Sylvain and Schnoebelen, {\relax Ph}ilippe},
  title = {The Ordinal-Recursive Complexity of Timed-Arc {P}etri
                     Nets, Data Nets, and Other Enriched Nets},
  pages = {355-364},
  url = {http://hal.archives-ouvertes.fr/hal-00793811},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HSS-lics12.pdf},
  doi = {10.1109/LICS.2012.46},
  abstract = {We show how to reliably compute fast-growing functions
                  with timed-arc Petri nets and data nets. This
                  construction provides ordinal-recursive lower bounds
                  on the complexity of the main decidable properties
                  (safety, termination, regular simulation,~etc.) of
                  these models. Since these new lower bounds match the
                  upper bounds that one can derive from wqo theory,
                  they precisely characterise the computational power
                  of these so-called {"}enriched{"} nets.}
}
@inproceedings{SS-concur13,
  address = {Buenos Aires, Argentina},
  month = aug,
  year = 2013,
  volume = 8052,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {D'Argenio, Pedro R. and Melgratti, Hern{\'a}n)},
  acronym = {{CONCUR}'13},
  booktitle = {{P}roceedings of the 24th
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'13)},
  author = {Schmitz, Sylvain and Schnoebelen, {\relax Ph}ilippe},
  title = {The Power of Well-Structured Systems},
  pages = {5-24},
  url = {http://arxiv.org/abs/1402.2908},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/SS-concur13.pdf},
  doi = {10.1007/978-3-642-40184-8_2},
  abstract = {Well-structured systems, aka WSTS, are computational models
    where the set of possible configurations is equipped with a
    well-quasi-ordering which is compatible with the transition relation
    between configurations. This structure supports generic decidability
    results that are important in verification and several other fields. This
    paper recalls the basic theory underlying well-structured systems and
    shows how two classic decision algorithms can be formulated as an
    exhaustive search for some {"}bad{"} sequences. This lets us describe new
    powerful techniques for the complexity analysis of WSTS algorithms.
    Recently, these techniques have been successful in precisely
    characterizing the power, in a complexity-theoretical sense, of several
    important WSTS models like unreliable channel systems, monotonic counter
    machines, or networks of timed systems.}
}
@inproceedings{HSS-concur13,
  address = {Buenos Aires, Argentina},
  month = aug,
  year = 2013,
  volume = 8052,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {D'Argenio, Pedro R. and Melgratti, Hern{\'a}n)},
  acronym = {{CONCUR}'13},
  booktitle = {{P}roceedings of the 24th
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'13)},
  author = {Haase, Christoph and Schmitz, Sylvain and Schnoebelen,
                  {\relax Ph}ilippe},
  title = {The Power of Priority Channel Systems},
  pages = {319-333},
  url = {http://arxiv.org/abs/1301.5500},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HSS-corr13.pdf},
  arxivpdf = {http://arxiv.org/pdf/1301.5500},
  doi = {10.1007/978-3-642-40184-8_23},
  abstract = {We introduce Priority Channel Systems, a new natural class of
    channel systems where messages carry a numeric priority and where
    higher-priority messages can supersede lower-priority messages preceding
    them in the fifo communication buffers. The decidability of safety and
    inevitability properties is shown via the introduction of a \emph{priority
    embedding}, a~well-quasi-ordering that has not previously been used in
    well-structured systems. We then show how Priority Channel Systems can
    compute Fast-Growing functions and prove that the aforementioned
    verification problems are \(F_{\epsilon_{0}}\)-complete.}
}
@inproceedings{BS-lics13,
  address = {New-Orleans, Louisiana, USA},
  month = jun,
  year = 2013,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{LICS}'13},
  booktitle = {{P}roceedings of the 28th
               {A}nnual {IEEE} {S}ymposium on
               {L}ogic in {C}omputer {S}cience
               ({LICS}'13)},
  author = {Boral, Anudhyan and Schmitz, Sylvain},
  title = {Model Checking Parse Trees},
  pages = {153-162},
  url = {http://arxiv.org/abs/1211.5256},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BS-lics13.pdf},
  arxivpdf = {http://arxiv.org/pdf/1211.5256},
  doi = {10.1109/LICS.2013.21},
  abstract = {Parse trees are fundamental syntactic structures in both
    computational linguistics and compilers construction. We argue in this
    paper that, in both fields, there are good incentives for model-checking
    sets of parse trees for some word according to a context-free grammar. We
    put forward the adequacy of propositional dynamic logic (PDL) on trees in
    these applications, and study as a sanity check the complexity of the
    corresponding model-checking problem: although complete for exponential
    time in the general case, we find natural restrictions on grammars for our
    applications and establish complexities ranging from nondeterministic
    polynomial time to polynomial space in the relevant cases.}
}
@inproceedings{BNS-cc13,
  address = {Rome, Italy},
  month = mar,
  year = 2013,
  volume = {7791},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {De{~}Bosschere, Koen and Jhala, Ranjit},
  acronym = {{CC}'13},
  booktitle = {{P}roceedings of the 22nd {I}nternational {C}onference on {C}ompiler
                  {C}onstruction ({CC}'13)},
  author = {Eberhard Bertsch and Mark-Jan Nederhof and Sylvain
                  Schmitz},
  title = {On {LR} Parsing with Selective Delays},
  pages = {244-263},
  url = {http://hal.archives-ouvertes.fr/hal-00769668},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BNS-cc13.pdf},
  doi = {10.1007/978-3-642-37051-9_13},
  abstract = {The paper investigates an extension of LR parsing that allows
                  the delay of parsing decisions until a sufficient amount
                  of context has been processed. We provide two
                  characterizations for the resulting class of grammars, one
                  based on grammar transformations, the other on the direct
                  construction of a parser. We also report on experiments with
                  a grammar collection.}
}
@inproceedings{KS-fossacs13,
  address = {Rome, Italy},
  month = mar,
  year = 2013,
  volume = {7794},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Pfenning, Frank},
  acronym = {{FoSSaCS}'13},
  booktitle = {{P}roceedings of the 16th {I}nternational
               {C}onference on {F}oundations of {S}oftware {S}cience
               and {C}omputation {S}tructures
               ({FoSSaCS}'13)},
  author = {Karandikar, Prateek and Schmitz, Sylvain},
  title = {The Parametric Ordinal-Recursive Complexity of {P}ost
                  Embedding Problems},
  pages = {273-288},
  url = {http://arxiv.org/abs/1211.5259},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/KS-fossacs13.pdf},
  doi = {10.1007/978-3-642-37075-5_18},
  abstract = {Post Embedding Problems are a family of decision problems based
    on the interaction of a rational relation with the subword embedding
    ordering, and are used in the literature to prove non multiply-recursive
    complexity lower bounds. We refine the construction of Chambart and
    Schnoebelen (LICS~2008) and prove parametric lower bounds depending on the
    size of the alphabet.}
}
@article{HSS-lmcs14,
  journal = {Logical Methods in Computer Science},
  author = {Haase, Christoph and Schmitz, Sylvain and Schnoebelen, {\relax Ph}ilippe},
  title = {The Power of Priority Channel Systems},
  year = {2014},
  month = dec,
  volume = 10,
  number = {4:4},
  nopages = {},
  url = {http://arxiv.org/abs/1301.5500},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HSS-lmcs14.pdf},
  doi = {10.2168/LMCS-10(4:4)2014},
  abstract = {We introduce Priority Channel Systems, a new class of channel
    systems where messages carry a numeric priority and where higher-priority
    messages can supersede lower-priority messages preceding them in the fifo
    communication buffers. The decidability of safety and inevitability
    properties is shown via the introduction of a priority embedding, a
    well-quasi-ordering that has not previously been used in well-structured
    systems. We then show how Priority Channel Systems can compute
    Fast-Growing functions and prove that the aforementioned verification
    problems are \(\mathbf{F}_{\epsilon_{0}}\)-complete.}
}
@inproceedings{schmitz-rp14,
  address = {Oxford, UK},
  month = sep,
  year = 2014,
  volume = {8762},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Ouaknine, Jo{\"e}l and Potapov, Igor and Worrell, James},
  acronym = {{RP}'14},
  booktitle = {{P}roceedings of the 8th {W}orkshop
           on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'14)},
  author = {Schmitz, Sylvain},
  title = {Complexity Bounds for Ordinal-Based Termination},
  pages = {1-19},
  url = {http://arxiv.org/abs/1407.5896},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/schmitz-rp14.pdf},
  doi = {10.1007/978-3-319-11439-2_1},
  abstract = {`What more than its truth do we know if we have a proof of a
    theorem in a given formal system?' We examine Kreisel's question in the
    particular context of program termination proofs, with an eye to deriving
    complexity bounds on program running times.\par
    Our main tool for this are length function theorems, which provide
    complexity bounds on the use of well quasi orders. We illustrate how to
    prove such theorems in the simple yet until now untreated case of
    ordinals. We show how to apply this new theorem to derive complexity
    bounds on programs when they are proven to terminate thanks to a ranking
    function into some ordinal.}
}
@inproceedings{CS-mfcs14,
  address = {Budapest, Hungary},
  month = aug,
  year = 2014,
  volume = {8634},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {{\'E}sik, Zolt{\'a}n and Csuhaj{-}Varj{\'u}, Erzs{\'e}bet and 
                 Dietzfelbinger, Martin},
  acronym = {{MFCS}'14},
  booktitle = {{P}roceedings of the 39th
               {I}nternational {S}ymposium on
               {M}athematical {F}oundations of 
               {C}omputer {S}cience
               ({MFCS}'14)~-- {P}art~{I}},
  author = {Courtois, Jean-Baptiste and Schmitz, Sylvain},
  title = {Alternating Vector Addition Systems with States},
  pages = {220-231},
  url = {http://hal.inria.fr/hal-00980878},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/CS-mfcs14.pdf},
  doi = {10.1007/978-3-662-44522-8_19},
  abstract = {Alternating vector addition systems are obtained by equipping
    vector addition systems with states (VASS) with 'fork' rules, and provide
    a natural setting for infinite-arena games played over a VASS. Initially
    introduced in the study of propositional linear logic, they have more
    recently gathered attention in the guise of \emph{multi-dimensional
    energy} games for quantitative verification and synthesis.\par
    We show that establishing who is the winner in such a game with a state
    reachability objective is 2-ExpTime-complete. As a further application, we
    show that the same complexity result applies to the problem of whether a
    VASS is simulated by a finite-state system.}
}
@inproceedings{Schmitz-rta14,
  address = {Vienna, Austria},
  month = jul,
  year = 2014,
  volume = {8560},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Dowek, Gilles},
  acronym = {{RTA\slash TLCA}'14},
  booktitle = {{P}roceedings of the {J}oint 25th {I}nternational {C}onference on
                  {R}ewriting {T}echniques and {A}pplications and 12th
                  {I}nternational {C}onference on {T}yped {L}ambda-{C}alculi
                  and {A}pplications ({RTA\slash TLCA}'14)},
  author = {Schmitz, Sylvain},
  title = {Implicational Relevance Logic is 2-{E}xp{T}ime-Complete},
  pages = {395-409},
  url = {http://arxiv.org/abs/1402.0705},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Schmitz-rta14.pdf},
  doi = {10.1007/978-3-319-08918-8_27},
  abstract = {We show that provability in the implicational fragment of
                  relevance logic is complete for doubly exponential time,
                  using reductions to and from coverability in branching
                  vector addition systems.}
}
@inproceedings{LS-csllics14,
  address = {Vienna, Austria},
  month = jul,
  year = 2014,
  publisher = {ACM Press},
  acronym = {{CSL\slash LICS}'14},
  booktitle = {{P}roceedings of the Joint Meeting of the 23rd {EACSL} {A}nnual {C}onference on
  	    {C}omputer {S}cience {L}ogic and the 29th {A}nnual {ACM\slash
            IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({CSL\slash LICS}'14)},
  author = {Lazi{\'c}, Ranko and Schmitz, Sylvain},
  title = {Non-Elementary Complexities for Branching {VASS},
                  {MELL}, and Extensions},
  nopages = {},
  chapter = 61,
  url = {http://arxiv.org/abs/1401.6785},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-csllics14.pdf},
  doi = {10.1145/2603088.2603129},
  abstract = {We study the complexity of reachability problems on branching
                  extensions of vector addition systems, which allows us to
                  derive new non-elementary complexity bounds for fragments
                  and variants of propositional linear logic. We show that
                  provability in the multiplicative exponential fragment is
                  Tower-hard already in the affine case---and hence
                  non-elementary. We match this lower bound for the full
                  propositional affine linear logic, proving its
                  Tower-completeness. We also show that provability in
                  propositional contractive linear logic is
                  Ackermann-complete.}
}
@inproceedings{LS-rp15,
  address = {Warsaw, Poland},
  month = sep,
  year = 2015,
  volume = {9328},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Boja{\'n}czyk, Miko{\l}aj and Lasota, S{\l}awomir and Potapov, Igor},
  acronym = {{RP}'15},
  booktitle = {{P}roceedings of the 9th {W}orkshop
           on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'15)},
  author = {Lazi{\'c}, Ranko and Schmitz, Sylvain},
  title = {The Ideal View on {R}ackoff's Coverability Technique},
  pages = {76-88},
  url = {https://hal.inria.fr/hal-01176755},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-rp15.pdf},
  doi = {10.1007/978-3-319-24537-9_8},
  abstract = {Rackoff's small witness property for the coverability problem
    is the standard means to prove tight upper bounds in vector addition
    systems (VAS) and many extensions. We show how to derive the same bounds
    directly on the computations of the VAS instantiation of the generic
    backward coverability algorithm. This relies on a dual view of the
    algorithm using ideal decompositions of downwards-closed sets, which
    exhibits a key structural invariant in the VAS case. The same reasoning
    readily generalises to several VAS extensions.}
}
@inproceedings{JLS-icalp15,
  address = {Kyoto, Japan},
  month = jul,
  year = 2015,
  volume = {9135},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Halld{\'o}rsson, Magnus M. and Iwama, Kazuo and Kobayashi,
                  Naoki and Speckmann, Bettina},
  acronym = {{ICALP}'15},
  booktitle = {{P}roceedings of the 42nd {I}nternational 
               {C}olloquium on {A}utomata, {L}anguages and 
               {P}rogramming ({ICALP}'15)~-- {P}art~{II}},
  author = {Jurdzi{\'n}ski, Marcin and Lazi{\'c}, Ranko and Schmitz, Sylvain},
  title = {Fixed-Dimensional Energy Games are in Pseudo Polynomial Time},
  pages = {260-272},
  url = {http://arxiv.org/abs/1502.06875},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JLS-arxiv15.pdf},
  doi = {10.1007/978-3-662-47666-6_21},
  abstract = {We generalise the hyperplane separation technique (Chatterjee
    and Velner,~2013) from multi-dimensional mean-payoff to energy games, and
    achieve an algorithm for solving the latter whose running time is
    exponential only in the dimension, but not in the number of vertices of
    the game graph. This answers an open question whether energy games with
    arbitrary initial credit can be solved in pseudo-polynomial time for fixed
    dimensions~\(3\) or larger (Chaloupka,~2013). It~also improves the complexity
    of solving multi-dimensional energy games with given initial credit from
    non-elementary (Br\'azdil, Jan\v{c}ar, and Ku\v{c}era,~2010) to 2EXPTIME,
    thus establishing their 2EXPTIME-completeness.}
}
@inproceedings{LS-lics15,
  address = {Kyoto, Japan},
  month = jul,
  year = 2015,
  publisher = {{IEEE} Press},
  acronym = {{LICS}'15},
  booktitle = {{P}roceedings of the 30th {A}nnual {ACM\slash
            IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'15)},
  author = {Leroux, J{\'e}r{\^o}me and Schmitz, Sylvain},
  title = {Demystifying Reachability in Vector Addition Systems},
  pages = {56-67},
  url = {http://arxiv.org/abs/1503.00745},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-arxiv15.pdf},
  doi = {10.1109/LICS.2015.1},
  abstract = {More than 30 years after their inception, the decidability
    proofs for reachability in vector addition systems (VAS) still retain much
    of their mystery. These proofs rely crucially on a decomposition of runs
    successively refined by Mayr, Kosaraju, and Lambert, which appears rather
    magical, and for which no complexity upper bound is known.\par
    We first offer a justification for this decomposition technique, by
    showing that it emerges naturally in the study of the ideals of a well
    quasi ordering of VAS runs. In a second part, we apply recent results on
    the complexity of termination thanks to well quasi orders and well orders
    to obtain fast-growing complexity upper bounds for the decomposition
    algorithms, thus providing the first known upper bounds for general VAS
    reachability.}
}
@article{LS-tocl15,
  publisher = {ACM Press},
  journal = {ACM Transactions on Computational Logic},
  author = {Lazi{\'c}, Ranko and Schmitz, Sylvain},
  title = {Non-Elementary Complexities for Branching~{VASS}, {MELL}, and Extensions},
  volume = {16},
  number = {3:20},
  nopages = {},
  month = jul,
  year = 2015,
  url = {http://arxiv.org/abs/1401.6785},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/LS-tocl15.pdf},
  doi = {10.1145/2733375},
  abstract = {We study the complexity of reachability problems on branching
    extensions of vector addition systems, which allows us to derive new
    non-elementary complexity bounds for fragments and variants of
    propositional linear logic. We show that provability in the multiplicative
    exponential fragment is Tower-hard already in the affine case---and hence
    non-elementary. We match this lower bound for the full propositional
    affine linear logic, proving its Tower-completeness. We also show that
    provability in propositional contractive linear logic is
    Ackermann-complete.}
}
@article{Schmitz-jsl15,
  publisher = {Association for Symbolic Logic},
  journal = {Journal of Symbolic Logic},
  author = {Schmitz, Sylvain},
  title = {Implicational Relevance Logic is \(2\)-{ExpTime}-Complete},
  volume = {81},
  number = {2},
  pages = {641-661},
  month = jun,
  year = 2016,
  url = {http://arxiv.org/abs/1402.0705},
  pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/Schmitz-jsl15.pdf},
  doi = {10.1017/jsl.2015.7},
  abstract = {We show that provability in the implicational fragment of
    relevance logic is complete for doubly exponential time, using reductions
    to and from coverability in branching vector addition systems.}
}
@inproceedings{BLS-hal15,
  address = {Marseille, France},
  month = sep,
  year = 2016,
  volume = {62},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Regnier, Laurent and Talbot, Jean-Marc},
  acronym = {{CSL}'16},
  booktitle = {{P}roceedings of the 25th {A}nnual {EACSL} {C}onference on
                  {C}omputer {S}cience {L}ogic ({CSL}'16)},
  author = {Baelde, David and Lunel, Simon and Schmitz, Sylvain},
  title = {A~Sequent Calculus for a Modal Logic on Finite Data
                  Trees},
  pages = {32:1-32:16},
  url = {https://hal.inria.fr/hal-01191172},
  doi = {10.4230/LIPIcs.CSL.2016.32},
  abstract = {We investigate the proof theory of a modal fragment of XPath
                  equipped with data (in)equality tests over finite data
                  trees, i.e. over finite unranked trees where nodes are
                  labelled with both a symbol from a finite alphabet and a
                  single data value from an infinite domain.  We present a
                  sound and complete sequent calculus for this logic, which
                  yields the optimal PSPACE complexity bound for its validity
                  problem.}
}
@inproceedings{GLS-icalp16,
  address = {Rome, Italy},
  month = jul,
  year = 2016,
  volume = {55},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Chatzigiannakis, Ioannis and Mitzenmacher,
                  Michael and Rabani, Yuval and Sangiorgi, Davide},
  acronym = {{ICALP}'16},
  booktitle = {{P}roceedings of the 43rd {I}nternational 
               {C}olloquium on {A}utomata, {L}anguages and 
               {P}rogramming ({ICALP}'16)},
  author = {Goubault{-}Larrecq, Jean and Schmitz, Sylvain},
  title = {Deciding Piecewise Testable Separability for Regular
                  Tree Languages},
  pages = {97:1-97:15},
  url = {https://hal.inria.fr/hal-01276119/},
  optpdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLS-icalp16.pdf},
  doi = {10.4230/LIPIcs.ICALP.2016.97},
  abstract = {The piecewise testable separability problem asks, given
    two input languages, whether there exists a piecewise testable
    language that contains the first input language and is disjoint from
    the second. We prove a general characterisation of piecewise
    testable separability on languages in a well-quasi-order, in terms
    of ideals of the ordering. This subsumes the known characterisations
    in the case of finite words. In the case of finite ranked trees
    ordered by homeomorphic embedding, we show using effective
    representations for tree ideals that it entails the decidability of
    piecewise testable separability when the input languages are
    regular. A~final byproduct is a new proof of the decidability of
    whether an input regular language of ranked trees is piecewise
    testable, which was first shown in the unranked case by Boja{\'n}czyk,
    Segoufin, and Straubing (Log.~Meth. in Comput.~Sci.,~8(3:26),
    2012).}
}
@inproceedings{LS-lics16,
  address = {New York City, USA},
  month = jul,
  year = 2016,
  publisher = {ACM Press},
  editor = {Grohe, Martin and Koskinen, Eric and Shankar, Natarajan},
  acronym = {{LICS}'16},
  booktitle = {{P}roceedings of the 31st {A}nnual {ACM\slash
            IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'16)},
  author = {Ranko Lazi{\'c} and Sylvain Schmitz},
  title = {The Complexity of Coverability in {{\(\nu\)}}-{P}etri Nets},
  pages = {467-476},
  url = {https://hal.inria.fr/hal-01265302},
  doi = {10.1145/2933575.2933593},
  abstract = {We show that the coverability problem in nu-Petri
                  nets is complete for `double Ackermann' time, thus
                  closing an open complexity gap between an Ackermann
                  lower bound and a hyper-Ackermann upper bound. The
                  coverability problem captures the verification of
                  safety properties in this nominal extension of Petri
                  nets with name management and fresh name
                  creation. Our completeness result establishes
                  nu-Petri nets as a model of intermediate power among
                  the formalisms of nets enriched with data, and
                  relies on new algorithmic insights brought by the
                  use of well-quasi-order ideals.}
}
@comment{{B-arxiv16,
  author =		Bollig, Benedikt, 
  affiliation = 	aff-LSVmexico,
  title =    		One-Counter Automata with Counter Visibility, 
  institution = 	Computing Research Repository, 
  number =    		1602.05940, 
  month = 		feb, 
  nmonth =     		2,
  year = 		2016, 
  type = 		RR, 
  axeLSV = 		mexico,
  NOcontrat = 		"",
  
  url =			http://arxiv.org/abs/1602.05940, 
  PDF =			"http://www.lsv.fr/Publis/PAPERS/PDF/B-arxiv16.pdf",
  lsvdate-new =  	20160222,
  lsvdate-upd =  	20160222,
  lsvdate-pub =  	20160222,
  lsv-category = 	"rapl",
  wwwpublic =    	"public and ccsb",
  note = 		18~pages, 

  abstract = "In a one-counter automaton (OCA), one can read a letter
    from some finite alphabet, increment and decrement the counter by
    one, or test it for zero. It is well-known that universality and
    language inclusion for OCAs are undecidable. We consider here OCAs
    with counter visibility: Whenever the automaton produces a letter,
    it outputs the current counter value along with~it. Hence, its
    language is now a set of words over an infinite alphabet. We show
    that universality and inclusion for that model are in PSPACE, thus
    no harder than the corresponding problems for finite automata, which
    can actually be considered as a special case. In fact, we show that
    OCAs with counter visibility are effectively determinizable and
    closed under all boolean operations. As~a~strict generalization, we
    subsequently extend our model by registers. The general nonemptiness
    problem being undecidable, we impose a bound on the number of
    register comparisons and show that the corresponding nonemptiness
    problem is NP-complete.",
}}
@inproceedings{LS-stacs16,
  address = {Orl{\'e}ans, France},
  month = feb,
  year = 2016,
  volume = {47},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Ollinger, Nicolas and Vollmer, Heribert},
  acronym = {{STACS}'16},
  booktitle = {{P}roceedings of the 33rd {A}nnual
               {S}ymposium on {T}heoretical {A}spects of
               {C}omputer {S}cience
               ({STACS}'16)},
  author = {Leroux, J{\'e}r{\^o}me and Schmitz, Sylvain},
  title = {Ideal Decompositions for Vector Addition Systems},
  pages = {1:1-1:13},
  url = {http://drops.dagstuhl.de/opus/volltexte/2016/5702},
  doi = {10.4230/LIPIcs.STACS.2016.1},
  abstract = {Vector addition systems, or equivalently Petri nets, are one of
    the most popular formal models for the representation and the analysis of
    parallel processes. Many problems for vector addition systems are known to
    be decidable thanks to the theory of well-structured transition systems.
    Indeed, vector addition systems with configurations equipped with the
    classical point-wise ordering are well-structured transition systems.
    Based on this observation, problems like coverability or termination can
    be proven decidable.\par
    However, the theory of well-structured transition systems does not explain
    the decidability of the reachability problem. In this presentation, we
    show that runs of vector addition systems can also be equipped with a well
    quasi-order. This observation provides a unified understanding of the data
    structures involved in solving many problems for vector addition systems,
    including the central reachability problem.}
}
@article{siglog16-Schmitz,
  publisher = {ACM Press},
  journal = {SIGLOG News},
  author = {Schmitz, Sylvain},
  title = {Automata column: The~complexity of reachability in
                  vector addition systems},
  volume = 3,
  number = 1,
  pages = {3-21},
  year = 2016,
  month = jan,
  url = {https://hal.inria.fr/hal-01275972},
  doi = {10.1145/2893582.2893585},
  annote = {Invited column},
  abstract = {The program of the 30th Symposium on Logic in Computer Science
    held in 2015 in Kyoto included two contributions on the computational
    complexity of the reachability problem for vector addition systems:
    Blondin, Finkel, G{\"o}ller, Haase, and McKenzie~[2015] attacked the
    problem by providing the first tight complexity bounds in the case of
    dimension-2 systems with states, while Leroux and Schmitz~[2015] proved
    the first complexity upper bound in the general case. The purpose of this
    column is to present the main ideas behind these two results, and more
    generally survey the current state of affairs.}
}
@article{CFS-tcs16,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Chambart, Pierre and Finkel, Alain and Schmitz, Sylvain},
  title = {Forward Analysis and Model Checking for Trace
                  Bounded~{WSTS}},
  year = 2016,
  volume = {637},
  pages = {1-29},
  month = jul,
  url = {http://arxiv.org/abs/1004.2802},
  doi = {10.1016/j.tcs.2016.04.020},
  abstract = {We investigate a subclass of well-structured transition
     systems~(WSTS), the bounded---in the sense of Ginsburg and Spanier
     (Trans.~AMS, 1964)---complete deterministic ones, which we claim provide
     an adequate basis for the study of forward analyses as developed by
     Finkel and Goubault-Larrecq (ICALP~2009). Indeed, we prove that, unlike
     other conditions considered previously for the termination of forward
     analysis, boundedness is decidable. Boundedness turns out to be a
     valuable restriction for WSTS verification, as we show that it further
     allows to decide all {{\(\omega\)}}-regular properties on the set of infinite
     traces of the system.}
}
@article{toct-Schmitz13,
  publisher = {ACM Press},
  journal = {ACM Transactions on Computation Theory},
  author = {Schmitz, Sylvain},
  title = {Complexity Hierarchies Beyond {E}lementary},
  volume = {8},
  number = {1:3},
  nopages = {},
  year = 2016,
  month = feb,
  url = {http://arxiv.org/abs/1312.5686},
  doi = {10.1145/2858784},
  abstract = {We introduce a hierarchy of fast-growing complexity classes and
     show its suitability for completeness statements of many non elementary
     problems. This hierarchy allows the classification of many decision
     problems with a non-elementary complexity, which occur naturally in
     logic, combinatorics, formal languages, verification, etc., with
     complexities ranging from simple towers of exponentials to Ackermannian
     and beyond.}
}
@inproceedings{HLLLST-fossacs16,
  address = {Eindhoven, The~Netherlands},
  month = apr,
  year = 2016,
  volume = {9634},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Jacobs, Bart and L{\"o}ding, Christof},
  acronym = {{FoSSaCS}'16},
  booktitle = {{P}roceedings of the 19th {I}nternational
               {C}onference on {F}oundations of {S}oftware {S}cience
               and {C}omputation {S}tructures
               ({FoSSaCS}'16)},
  author = {Hofman, Piotr and Lasota, S{\l}awomir and Lazi{\'c}, Ranko and
                  Leroux, J{\'e}r{\^o}me and Schmitz, Sylvain and Totzke, Patrick},
  title = {Coverability Trees for {P}etri Nets with Unordered Data},
  pages = {445-461},
  url = {https://hal.inria.fr/hal-01252674},
  doi = {10.1007/978-3-662-49630-5_26},
  abstract = {We study an extension of classical Petri nets where tokens carry
    values from a countable data domain, that can be tested for equality upon
    firing transitions. These Unordered Data Petri Nets (UDPN) are
    well-structured and therefore allow generic decision procedures for
    several verification problems including coverability and boundedness. We
    show how to construct a finite representation of the coverability set in
    terms of its ideal decomposition. This not only provides an alternative
    method to decide coverability and boundedness, but is also an important
    step towards deciding the reachability problem. This also allows to answer
    more precise questions about the reachability set, for instance whether
    there is a bound on the number of tokens on a given place (place
    boundedness), or if such a bound exists for the number of different data
    values carried by tokens (place width boundedness). We provide matching
    Hyper-Ackermann bounds on the size of cover-ability trees and on the
    running time of the induced decision procedures.}
}
@phdthesis{schmitz-hdr2017,
  author = {Schmitz, Sylvain},
  title = {Algorithmic Complexity of Well-Quasi-Orders},
  school = {{\'E}cole Normale Sup{\'e}rieure Paris-Saclay, France},
  type = {M{\'e}moire d'habilitation},
  year = 2017,
  month = nov,
  url = {http://tel.archives-ouvertes.fr/tel-01663266}
}
@inproceedings{CJLS-lics17,
  address = {Reykjavik, Iceland},
  month = jun,
  publisher = {{IEEE} Press},
  editor = {Ouaknine, Jo{\"e}l},
  acronym = {{LICS}'17},
  booktitle = {{P}roceedings of the 32nd {A}nnual {ACM\slash
            IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'17)},
  author = {Colcombet, {\relax Th}omas and Jurdzi{\'n}ski,
                   Marcin and Lazi{\'c}, Ranko and Schmitz, Sylvain},
  title = {Perfect Half Space Games},
  pages = {1--11},
  year = {2017},
  doi = {10.1109/LICS.2017.8005105},
  url = {http://arxiv.org/abs/1704.05626},
  abstract = {We introduce perfect half space games,
in which the goal of Player 2
is to make the sums of encountered multi-dimensional weights diverge in 
a direction which is consistent with a chosen sequence of perfect half spaces (chosen dynamically by Player 2).
We establish that the bounding games of
Jurdzinski et al. (ICALP 2015) can be reduced to perfect half space games, which in turn can be translated to the lexicographic
energy games of Colcombet and Niwinski, and are positionally determined in a strong sense (Player 2 can play without knowing the current perfect half space).
We finally show how perfect half space games and bounding games can be employed
to solve multi-dimensional energy parity games in pseudo-polynomial time 
when both the numbers of energy dimensions and of priorities are fixed, regardless of whether the initial credit is given as part of the input or existentially quantified.  This also yields an optimal 2EXP complexity 
with given initial credit, where the best known upper bound was non-elementary.}
}
@inproceedings{BHSS-pn17,
  address = {Zaragoza, Spain},
  month = jun,
  volume = {10258},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {van der Aalst, Wifred and Best, Eike},
  acronym = {{PETRI~NETS}'17},
  booktitle = {{P}roceedings of the 38th
               {I}nternational {C}onference on
               {A}pplications and {T}heory of {P}etri {N}ets
               ({PETRI~NETS}'17)},
  author = {B{\'e}rard, B{\'e}atrice and Haar, Stefan and
                  Schmitz, Sylvain and Schwoon, Stefan},
  title = {The Complexity of Diagnosability and Opacity
                  Verification for {P}etri Nets},
  pages = {200-220},
  year = {2017},
  doi = {10.1007/978-3-319-57861-3_13},
  url = {https://hal.inria.fr/hal-01484476},
  abstract = {Diagnosability and opacity are two well-studied problems in discrete-event systems.  We revisit these two problems with respect to expressiveness and complexity issues.  We first relate different notions of diagnosability and opacity.  We consider in particular fairness issues and extend the definition of Germanos et al. [ACM TECS, 2015] of weakly fair diagnosability for safe Petri nets to general Petri nets and to opacity questions.  Second, we provide a global picture of complexity results for the verification of diagnosability and opacity.  We show that diagnosability is NL-complete for finite state systems, PSPACE-complete for safe Petri nets (even with fairness), and EXPSPACE-complete for general Petri nets without fairness, while non diagnosability is inter-reducible with reachability when fault events are not weakly fair.  Opacity is ESPACE-complete for safe Petri nets (even with fairness) and undecidable for general Petri nets already without fairness.}
}
@inproceedings{BLS-fsttcs18,
  address = {Ahmedabad, India},
  month = dec,
  year = 2018,
  volume = {122},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Sumit Ganguly and Paritosh Pandya},
  acronym = {{FSTTCS}'18},
  booktitle = {{P}roceedings of the 38th {C}onference on
               {F}oundations of {S}oftware {T}echnology and
               {T}heoretical {C}omputer {S}cience
               ({FSTTCS}'18)},
  author = {Baelde, David and Lick, Anthony and Schmitz, Sylvain},
  title = {A Hypersequent Calculus with Clusters for Tense Logic over Ordinals},
  pages = {15:1-15:19},
  url = {http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=9914},
  pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/9914/pdf/LIPIcs-FSTTCS-2018-15.pdf},
  doi = {10.4230/LIPIcs.FSTTCS.2018.15},
  abstract = {Prior's tense logic forms the core of linear temporal logic, with both past-and future-looking modalities.  We present a sound and complete proof system for tense logic over ordinals.  Technically, this is a hypersequent system, enriched with an ordering, clusters, and annotations. The system is designed with proof search algorithms in mind, and yields an optimal coNP complexity for the validity problem.  It entails a small model property for tense logic over ordinals: every satisfiable formula has a model of order type at most \(\omega^2\).  It also allows to answer the validity problem for ordinals below or exactly equal to a given one.}
}
@inproceedings{BLS-pods19,
  address = {Amsterdam, Netherlands},
  month = jun # {-} # jul,
  publisher = {ACM Press},
  editor = {Christoph Koch},
  acronym = {{PODS}'19},
  booktitle = {{P}roceedings of the 38th {A}nnual 
	  {ACM} {SIGACT}-{SIGMOD}-{SIGART} {S}ymposium 
	  on {P}rinciples of {D}atabase {S}ystems
	  ({PODS}'19)},
  author = {Baelde, David and Lick, Anthony and Schmitz, Sylvain},
  title = {Decidable {XP}ath Fragments in the Real World},
  pages = {285-302},
  year = 2019,
  doi = {10.1145/3294052.3319685},
  url = {https://hal.inria.fr/hal-01852475},
  abstract = {XPath is arguably the most popular query language for selecting elements in XML documents.  Besides query evaluation, query satisfiability and containment are the main computational problems for XPath; they are useful, for instance, to detect dead code or validate query optimisations.  These problems are undecidable in general, but several fragments have been identified over time for which satisfiability (or query containment) is decidable: CoreXPath 1.0 and 2.0 without so-called data joins, fragments with data joins but limited navigation, etc.  However, these fragments are often given in a simplified syntax, and sometimes wrt. a simplified XPath semantics.  Moreover, they have been studied mostly with theoretical motivations, with little consideration for the practically relevant features of XPath.  To investigate the practical impact of these theoretical fragments, we design a benchmark compiling thousands of real-world XPath queries extracted from open-source projects.  These queries are then matched against syntactic fragments from the literature.  We investigate how to extend these fragments with seldom-considered features such as free variables, data tests, data joins, and the last() and id() functions, for which we provide both undecidability and decidability results.  We analyse the coverage of the original and extended fragments, and further provide a glimpse at which other practically-motivated features might be worth investigating in the future.}
}
@inproceedings{BLS-aiml18,
  address = {Bern, Switzerland},
  month = aug,
  year = 2018,
  publisher = {College Publications},
  editor = {Guram Bezhanishvili and Giovanna D'Agostino and
                  George Metcalfe and Thomas Studer},
  acronym = {{AiML}'18},
  booktitle = {{P}roceedings of the 10th
           {C}onference on {A}dvances in {M}odal {L}ogics
           ({AiML}'18)},
  author = {Baelde, David and Lick, Anthony and Schmitz, Sylvain},
  title = {A Hypersequent Calculus with Clusters for Linear Frames},
  pages = {36-55},
  url = {https://hal.inria.fr/hal-01756126},
  abstract = {The logic Kt4.3 is the basic modal logic of linear frames. Along with its extensions, it is found at the core of linear-time temporal logics and logics on words.  In this paper, we consider the problem of designing proof systems for these logics, in such a way that proof search yields decision procedures for validity with an optimal complexity---coNP in this case.  In earlier work, Indrzejczak has proposed an ordered hypersequent calculus that is sound and complete for Kt4.3 but does not yield any decision procedure.  We refine his approach, using a hypersequent structure that corresponds to weak rather than strict total orders, and using annotations that reflect the model-theoretic insights given by small models for Kt4.3.  We obtain a sound and complete calculus with an associated coNP proof search algorithm.  These results extend naturally to the cases of unbounded and dense frames, and to the complexity of the two-variable fragment of first-order logic over total orders.}
}
@article{BHSS-fi18,
  publisher = {{IOS} Press},
  journal = {Fundamenta Informaticae},
  author = {B{\'e}atrice B{\'e}rard and Stefan Haar and Sylvain Schmitz and Stefan Schwoon},
  title = {{The Complexity of Diagnosability and Opacity Verification for Petri Nets}},
  volume = 161,
  number = 4,
  year = 2018,
  pages = {317-349},
  doi = {10.3233/FI-2018-1706},
  url = {https://hal.inria.fr/hal-01852119},
  abstract = {Diagnosability and opacity are two well-studied problems in discrete-event systems. We revisit these two problems with respect to expressiveness and complexity issues.
\par
We first relate different notions of diagnosability and opacity. We consider in particular fairness issues and extend the definition of Germanos et al. [ACM TECS, 2015] of weakly fair diagnosability for safe Petri nets to general Petri nets and to opacity questions.
\par
Second, we provide a global picture of complexity results for the verification of diagnosability and opacity. We show that diagnosability is NL-complete for finite state systems, PSPACE-complete for safe convergent Petri nets (even with fairness), and EXPSPACE-complete for general Petri nets without fairness, while non diagnosability is inter-reducible with reachability when fault events are not weakly fair. Opacity is ESPACE-complete for safe Petri nets (even with fairness) and undecidable for general Petri nets already without fairness.}
}
@inproceedings{SZ-rp19,
  address = {Brussels, Belgium},
  month = sep,
  volume = {11674},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Rapha{\"e}l Jungers and Emmanuel Fillot and Igor Potapov},
  acronym = {{RP}'19},
  booktitle = {{P}roceedings of the 13th {W}orkshop
           on {R}eachability {P}roblems in {C}omputational {M}odels ({RP}'19)},
  author = {Sylvain Schmitz and Georg Zetzsche},
  title = {Coverability Is Undecidable in One-Dimensional Pushdown Vector Addition Systems with Resets},
  year = 2019,
  pages = {193-201},
  pdf = {https://arxiv.org/pdf/1906.07069.pdf},
  url = {https://arxiv.org/abs/1906.07069},
  doi = {10.1007/978-3-030-30806-3_15},
  abstract = {We consider the model of pushdown vector addition systems with resets.
  These consist of vector addition systems that have access to a pushdown stack and have
  instructions to reset counters. For this model, we study the coverability problem. In
  the absence of resets, this problem is known to be decidable for one-dimensional pushdown
  vector addition systems, but decidability is open for general pushdown vector addition
  systems. Moreover, coverability is known to be decidable for reset vector addition
  systems without a pushdown stack. We show in this note that the problem is undecidable
  for one-dimensional pushdown vector addition systems with resets.}
}
@inproceedings{Schmitz-icalp19,
  address = {Patras, Greece},
  month = jul,
  volume = {132},
  series = {Leibniz International Proceedings in Informatics},
  publisher = {Leibniz-Zentrum f{\"u}r Informatik},
  editor = {Chatzigiannakis, Ioannis and Merelli, Emanuela},
  acronym = {{ICALP}'19},
  booktitle = {{P}roceedings of the 46th {I}nternational 
               {C}olloquium on {A}utomata, {L}anguages and 
               {P}rogramming ({ICALP}'19)},
  author = {Schmitz, Sylvain},
  title = {The Parametric Complexity of Lossy Counter Machines},
  year = 2019,
  pages = {129:1-129:15},
  doi = {10.4230/LIPIcs.ICALP.2019.129},
  pdf = {https://hal.archives-ouvertes.fr/hal-02020728v2/document},
  url = {http://drops.dagstuhl.de/opus/volltexte/2019/10705/},
  abstract = {The reachability problem in lossy counter machines is
  the best-known ACKERMANN-complete problem and has been used to establish
  most of the ACKERMANN-hardness statements in the literature. This hides
  however a complexity gap when the number of counters is fixed. We close
  this gap and prove F_d-completeness for machines with d counters, which
  provides the first known uncontrived problems complete for the fast-growing
  complexity classes at levels 3 < d < omega. We develop for this an approach
  through antichain factorisations of bad sequences and analysing the length
  of controlled antichains.}
}
@inproceedings{LS-lics19,
  address = {Vancouver, Canada},
  month = jun,
  publisher = {{IEEE} Press},
  editor = {Bouyer, Patricia},
  acronym = {{LICS}'19},
  booktitle = {{P}roceedings of the 34th {A}nnual {ACM\slash
            IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'19)},
  author = {J{\'e}r{\^o}me Leroux and Schmitz, Sylvain},
  title = {Reachability in Vector Addition Systems is
                  Primitive-Recursive in Fixed Dimension},
  pages = {1-13},
  year = 2019,
  doi = {10.1109/LICS.2019.8785796},
  url = {https://arxiv.org/abs/1903.08575},
  abstract = {The reachability problem in vector addition systems
                  is a central question, not only for the static
                  verification of these systems, but also for many
                  inter-reducible decision problems occurring in
                  various fields. The currently best known upper bound
                  on this problem is not primitive-recursive, even
                  when considering systems of fixed dimension. We
                  provide significant refinements to the classical
                  decomposition algorithm of Mayr, Kosaraju, and
                  Lambert and to its termination proof, which yield an
                  ACKERMANN upper bound in the general case, and
                  primitive-recursive upper bounds in fixed
                  dimension. While this does not match the currently
                  best known TOWER lower bound for reachability, it is
                  optimal for related problems.}
}
@article{LS-icomp19,
  publisher = {Elsevier Science Publishers},
  journal = {Information and Computation},
  author = {Ranko Lazi\'c and Sylvain Schmitz},
  title = {The Ideal View on {R}ackoff's Coverability
                  Technique},
  url = {https://hal.inria.fr/hal-01176755},
  year = 2019,
  note = {To appear},
  abstract = {Well-structured transition systems form a large
                  class of infinite-state systems, for which safety
                  verification is decidable thanks to a generic
                  backward coverability algorithm.  However, for
                  several classes of systems, the generic upper bounds
                  one can extract from the algorithm are far from
                  optimal.  In particular, in the case of vector
                  addition systems (VAS) and several of their
                  extensions, the known tight upper bounds were rather
                  derived thanks to ad-hoc arguments based on
                  Rackoff's small witness property.  We show how to
                  derive the same bounds directly on the computations
                  of the VAS instantiation of the generic backward
                  coverability algorithm.  This relies on a dual view
                  of the algorithm using ideal decompositions of
                  downwards-closed sets, which exhibits a key
                  structural invariant in the VAS case.  This reasoning
                  offers a uniform setting for all well-structured
                  transition systems, including branching ones, and we
                  further apply it to several VAS extensions: we
                  derive optimal upper bounds for coverability in
                  branching and alternating VAS, matching the
                  previously known results from the literature.}
}
@inproceedings{JS-lics19,
  address = {Vancouver, Canada},
  month = jun,
  publisher = {{IEEE} Press},
  editor = {Bouyer, Patricia},
  acronym = {{LICS}'19},
  booktitle = {{P}roceedings of the 34th {A}nnual {ACM\slash
            IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'19)},
  author = {Jan{\v c}ar, Petr and Schmitz, Sylvain},
  title = {Bisimulation Equivalence of First-Order Grammars is
                  {ACKERMANN}-Complete},
  pages = {1-12},
  year = 2019,
  doi = {10.1109/LICS.2019.8785848},
  url = {https://arxiv.org/abs/1901.07170},
  abstract = {Checking whether two pushdown automata with
                  restricted silent actions are weakly bisimilar was
                  shown decidable by S{\'e}nizergues (1998, 2005). We
                  provide the first known complexity upper bound for
                  this famous problem, in the equivalent setting of
                  first-order grammars. This ACKERMANN upper bound is
                  optimal, and we also show that strong bisimilarity
                  is primitive-recursive when the number of states of
                  the automata is fixed.}
}
@incollection{DSS-til2020,
  volume = 53,
  series = {Trends In Logic},
  publisher = {Springer},
  booktitle = {Well-Quasi Orders in Computation, Logic, Language and Reasoning},
  editor = {Schuster, Peter M. and Seisenberger, Monika and Weiermann, Andreas},
  author = {D{\v{z}}amonja, Mirna and Schmitz, Sylvain and Schnoebelen, {\relax Ph}ilippe},
  title = {On Ordinal Invariants in Well Quasi Orders and Finite Antichain Orders},
  pages = {2-54},
  year = 2020,
  doi = {10.1007/978-3-030-30229-0_2}
}

This file was generated by bibtex2html 1.98.