Search Results

Documents authored by Schmitz, Sylvain

Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.153
On the Length of Strongly Monotone Descending Chains over ℕ^d

Authors: Sylvain Schmitz and Lia Schütze

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
A recent breakthrough by Künnemann, Mazowiecki, Schütze, Sinclair-Banks, and Węgrzycki (ICALP 2023) bounds the running time for the coverability problem in d-dimensional vector addition systems under unary encoding to n^{2^{O(d)}}, improving on Rackoff’s n^{2^{O(dlg d)}} upper bound (Theor. Comput. Sci. 1978), and provides conditional matching lower bounds. In this paper, we revisit Lazić and Schmitz' "ideal view" of the backward coverability algorithm (Inform. Comput. 2021) in the light of this breakthrough. We show that the controlled strongly monotone descending chains of downwards-closed sets over ℕ^d that arise from the dual backward coverability algorithm of Lazić and Schmitz on d-dimensional unary vector addition systems also enjoy this tight n^{2^{O(d)}} upper bound on their length, and that this also translates into the same bound on the running time of the backward coverability algorithm. Furthermore, our analysis takes place in a more general setting than that of Lazić and Schmitz, which allows to show the same results and improve on the 2EXPSPACE upper bound derived by Benedikt, Duff, Sharad, and Worrell (LICS 2017) for the coverability problem in invertible affine nets.
Cite as

Sylvain Schmitz and Lia Schütze. On the Length of Strongly Monotone Descending Chains over ℕ^d. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 153:1-153:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{schmitz_et_al:LIPIcs.ICALP.2024.153,
  author =	{Schmitz, Sylvain and Sch\"{u}tze, Lia},
  title =	{{On the Length of Strongly Monotone Descending Chains over \mathbb{N}^d}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{153:1--153:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.153},
  URN =		{urn:nbn:de:0030-drops-202964},
  doi =		{10.4230/LIPIcs.ICALP.2024.153},
  annote =	{Keywords: Vector addition system, coverability, well-quasi-order, order ideal, affine net}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2021.3
Branching in Well-Structured Transition Systems (Invited Talk)

Authors: Sylvain Schmitz

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract
The framework of well-structured transition systems has been highly successful in providing generic algorithms to show the decidability of verification problems for infinite-state systems. In some of these applications, the executions in the system at hand are actually trees, and need to be "lifted" to executions over sets of configurations in order to fit in the framework. The downside of this approach is that we might lose precision when analysing the computational complexity of the algorithms, compared to reasoning over branching executions.
Cite as

Sylvain Schmitz. Branching in Well-Structured Transition Systems (Invited Talk). In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 3:1-3:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{schmitz:LIPIcs.CSL.2021.3,
  author =	{Schmitz, Sylvain},
  title =	{{Branching in Well-Structured Transition Systems}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{3:1--3:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.3},
  URN =		{urn:nbn:de:0030-drops-134377},
  doi =		{10.4230/LIPIcs.CSL.2021.3},
  annote =	{Keywords: fast-growing complexity, well-structured transition system}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2019.129
The Parametric Complexity of Lossy Counter Machines (Track B: Automata, Logic, Semantics, and Theory of Programming)

Authors: Sylvain Schmitz

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

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.
Cite as

Sylvain Schmitz. The Parametric Complexity of Lossy Counter Machines (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 129:1-129:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{schmitz:LIPIcs.ICALP.2019.129,
  author =	{Schmitz, Sylvain},
  title =	{{The Parametric Complexity of Lossy Counter Machines}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{129:1--129:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.129},
  URN =		{urn:nbn:de:0030-drops-107056},
  doi =		{10.4230/LIPIcs.ICALP.2019.129},
  annote =	{Keywords: Counter machine, well-structured system, well-quasi-order, antichain, fast-growing complexity}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2018.15
A Hypersequent Calculus with Clusters for Tense Logic over Ordinals

Authors: David Baelde, Anthony Lick, and Sylvain Schmitz

Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)

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.
Cite as

David Baelde, Anthony Lick, and Sylvain Schmitz. A Hypersequent Calculus with Clusters for Tense Logic over Ordinals. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 15:1-15:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{baelde_et_al:LIPIcs.FSTTCS.2018.15,
  author =	{Baelde, David and Lick, Anthony and Schmitz, Sylvain},
  title =	{{A Hypersequent Calculus with Clusters for Tense Logic over Ordinals}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{15:1--15:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Ganguly, Sumit and Pandya, Paritosh},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.15},
  URN =		{urn:nbn:de:0030-drops-99143},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.15},
  annote =	{Keywords: modal logic, proof system, hypersequent}
}
Document
DOI: 10.4230/LIPIcs.CSL.2016.32
A Sequent Calculus for a Modal Logic on Finite Data Trees

Authors: David Baelde, Simon Lunel, and Sylvain Schmitz

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

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.
Cite as

David Baelde, Simon Lunel, and Sylvain Schmitz. A Sequent Calculus for a Modal Logic on Finite Data Trees. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 32:1-32:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{baelde_et_al:LIPIcs.CSL.2016.32,
  author =	{Baelde, David and Lunel, Simon and Schmitz, Sylvain},
  title =	{{A Sequent Calculus for a Modal Logic on Finite Data Trees}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{32:1--32:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.32},
  URN =		{urn:nbn:de:0030-drops-65720},
  doi =		{10.4230/LIPIcs.CSL.2016.32},
  annote =	{Keywords: XPath, proof systems, modal logic, complexity}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2016.97
Deciding Piecewise Testable Separability for Regular Tree Languages

Authors: Jean Goubault-Larrecq and Sylvain Schmitz

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

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-quasiorder, 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 Bojanczyk, Segoufin, and Straubing [Log. Meth. in Comput. Sci., 8(3:26), 2012].
Cite as

Jean Goubault-Larrecq and Sylvain Schmitz. Deciding Piecewise Testable Separability for Regular Tree Languages. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 97:1-97:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{goubaultlarrecq_et_al:LIPIcs.ICALP.2016.97,
  author =	{Goubault-Larrecq, Jean and Schmitz, Sylvain},
  title =	{{Deciding Piecewise Testable Separability for Regular Tree Languages}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{97:1--97:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.97},
  URN =		{urn:nbn:de:0030-drops-62321},
  doi =		{10.4230/LIPIcs.ICALP.2016.97},
  annote =	{Keywords: Well-quasi-order, ideal, tree languages, first-order logic}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.STACS.2016.1
Ideal Decompositions for Vector Addition Systems (Invited Talk)

Authors: Jérôme Leroux and Sylvain Schmitz

Published in: LIPIcs, Volume 47, 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)

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. 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.
Cite as

Jérôme Leroux and Sylvain Schmitz. Ideal Decompositions for Vector Addition Systems (Invited Talk). In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 1:1-1:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{leroux_et_al:LIPIcs.STACS.2016.1,
  author =	{Leroux, J\'{e}r\^{o}me and Schmitz, Sylvain},
  title =	{{Ideal Decompositions for Vector Addition Systems}},
  booktitle =	{33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)},
  pages =	{1:1--1:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-001-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{47},
  editor =	{Ollinger, Nicolas and Vollmer, Heribert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.1},
  URN =		{urn:nbn:de:0030-drops-57024},
  doi =		{10.4230/LIPIcs.STACS.2016.1},
  annote =	{Keywords: Petri net, ideal, well-quasi-order, reachability, verification}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact