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