19 Search Results for "Leroux, Jérôme"


Volume

LIPIcs, Volume 272

48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

MFCS 2023, August 28 to September 1, 2023, Bordeaux, France

Editors: Jérôme Leroux, Sylvain Lombardy, and David Peleg

Document
New Lower Bounds for Reachability in Vector Addition Systems

Authors: Wojciech Czerwiński, Ismaël Jecker, Sławomir Lasota, Jérôme Leroux, and Łukasz Orlikowski

Published in: LIPIcs, Volume 284, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)


Abstract
We investigate the dimension-parametric complexity of the reachability problem in vector addition systems with states (VASS) and its extension with pushdown stack (pushdown VASS). Up to now, the problem is known to be F_d-hard for VASS of dimension 3d+2 (the complexity class F_d corresponds to the kth level of the fast-growing hierarchy), and no essentially better bound is known for pushdown VASS. We provide a new construction that improves the lower bound for VASS: F_d-hardness in dimension 2d+3. Furthermore, building on our new insights we show a new lower bound for pushdown VASS: F_d-hardness in dimension d/2 + 6. This dimension-parametric lower bound is strictly stronger than the upper bound for VASS, which suggests that the (still unknown) complexity of the reachability problem in pushdown VASS is higher than in plain VASS (where it is Ackermann-complete).

Cite as

Wojciech Czerwiński, Ismaël Jecker, Sławomir Lasota, Jérôme Leroux, and Łukasz Orlikowski. New Lower Bounds for Reachability in Vector Addition Systems. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 35:1-35:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.FSTTCS.2023.35,
  author =	{Czerwi\'{n}ski, Wojciech and Jecker, Isma\"{e}l and Lasota, S{\l}awomir and Leroux, J\'{e}r\^{o}me and Orlikowski, {\L}ukasz},
  title =	{{New Lower Bounds for Reachability in Vector Addition Systems}},
  booktitle =	{43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)},
  pages =	{35:1--35:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-304-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{284},
  editor =	{Bouyer, Patricia and Srinivasan, Srikanth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2023.35},
  URN =		{urn:nbn:de:0030-drops-194088},
  doi =		{10.4230/LIPIcs.FSTTCS.2023.35},
  annote =	{Keywords: vector addition systems, reachability problem, pushdown vector addition system, lower bounds}
}
Document
The Semilinear Home-Space Problem Is Ackermann-Complete for Petri Nets

Authors: Petr Jančar and Jérôme Leroux

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)


Abstract
A set of configurations H is a home-space for a set of configurations X of a Petri net if every configuration reachable from (any configuration in) X can reach (some configuration in) H. The semilinear home-space problem for Petri nets asks, given a Petri net and semilinear sets of configurations X, H, if H is a home-space for X. In 1989, David de Frutos Escrig and Colette Johnen proved that the problem is decidable when X is a singleton and H is a finite union of linear sets with the same periods. In this paper, we show that the general (semilinear) problem is decidable. This result is obtained by proving a duality between the reachability problem and the non-home-space problem. In particular, we prove that for any Petri net and any linear set of configurations L we can effectively compute a semilinear set C of configurations, called a non-reachability core for L, such that for every set X the set L is not a home-space for X if, and only if, C is reachable from X. We show that the established relation to the reachability problem yields the Ackermann-completeness of the (semilinear) home-space problem. For this we also show that, given a Petri net with an initial marking, the set of minimal reachable markings can be constructed in Ackermannian time.

Cite as

Petr Jančar and Jérôme Leroux. The Semilinear Home-Space Problem Is Ackermann-Complete for Petri Nets. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 36:1-36:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{jancar_et_al:LIPIcs.CONCUR.2023.36,
  author =	{Jan\v{c}ar, Petr and Leroux, J\'{e}r\^{o}me},
  title =	{{The Semilinear Home-Space Problem Is Ackermann-Complete for Petri Nets}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{36:1--36:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.36},
  URN =		{urn:nbn:de:0030-drops-190300},
  doi =		{10.4230/LIPIcs.CONCUR.2023.36},
  annote =	{Keywords: Petri nets, home-space property, semilinear sets, Ackermannian complexity}
}
Document
Complete Volume
LIPIcs, Volume 272, MFCS 2023, Complete Volume

Authors: Jérôme Leroux, Sylvain Lombardy, and David Peleg

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)


Abstract
LIPIcs, Volume 272, MFCS 2023, Complete Volume

Cite as

48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 1-1302, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@Proceedings{leroux_et_al:LIPIcs.MFCS.2023,
  title =	{{LIPIcs, Volume 272, MFCS 2023, Complete Volume}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{1--1302},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023},
  URN =		{urn:nbn:de:0030-drops-185332},
  doi =		{10.4230/LIPIcs.MFCS.2023},
  annote =	{Keywords: LIPIcs, Volume 272, MFCS 2023, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Jérôme Leroux, Sylvain Lombardy, and David Peleg

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)


Abstract
Front Matter, Table of Contents, Preface, Conference Organization

Cite as

48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{leroux_et_al:LIPIcs.MFCS.2023.0,
  author =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{0:i--0:xviii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.0},
  URN =		{urn:nbn:de:0030-drops-185349},
  doi =		{10.4230/LIPIcs.MFCS.2023.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Reachability in Two-Dimensional Vector Addition Systems with States: One Test Is for Free

Authors: Jérôme Leroux and Grégoire Sutre

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)


Abstract
Vector addition system with states is an ubiquitous model of computation with extensive applications in computer science. The reachability problem for vector addition systems is central since many other problems reduce to that question. The problem is decidable and it was recently proved that the dimension of the vector addition system is an important parameter of the complexity. In fixed dimensions larger than two, the complexity is not known (with huge complexity gaps). In dimension two, the reachability problem was shown to be PSPACE-complete by Blondin et al. in 2015. We consider an extension of this model, called 2-TVASS, where the first counter can be tested for zero. This model naturally extends the classical model of one counter automata (OCA). We show that reachability is still solvable in polynomial space for 2-TVASS. As in the work Blondin et al., our approach relies on the existence of small reachability certificates obtained by concatenating polynomially many cycles.

Cite as

Jérôme Leroux and Grégoire Sutre. Reachability in Two-Dimensional Vector Addition Systems with States: One Test Is for Free. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 37:1-37:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{leroux_et_al:LIPIcs.CONCUR.2020.37,
  author =	{Leroux, J\'{e}r\^{o}me and Sutre, Gr\'{e}goire},
  title =	{{Reachability in Two-Dimensional Vector Addition Systems with States: One Test Is for Free}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{37:1--37:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.37},
  URN =		{urn:nbn:de:0030-drops-128498},
  doi =		{10.4230/LIPIcs.CONCUR.2020.37},
  annote =	{Keywords: Counter machine, Vector addition system, Reachability problem, Formal verification, Infinite-state system}
}
Document
Flatness and Complexity of Immediate Observation Petri Nets

Authors: Mikhail Raskin, Chana Weil-Kennedy, and Javier Esparza

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)


Abstract
In a previous paper we introduced immediate observation (IO) Petri nets, a class of interest in the study of population protocols and enzymatic chemical networks. In the first part of this paper we show that IO nets are globally flat, and so their safety properties can be checked by efficient symbolic model checking tools using acceleration techniques, like FAST. In the second part we study Branching IO nets (BIO nets), whose transitions can create tokens. BIO nets extend both IO nets and communication-free nets, also called BPP nets, a widely studied class. We show that, while BIO nets are no longer globally flat, and their sets of reachable markings may be non-semilinear, they are still locally flat. As a consequence, the coverability and reachability problem for BIO nets, and even a certain set-parameterized version of them, are in PSPACE. This makes BIO nets the first natural net class with non-semilinear reachability relation for which the reachability problem is provably simpler than for general Petri nets.

Cite as

Mikhail Raskin, Chana Weil-Kennedy, and Javier Esparza. Flatness and Complexity of Immediate Observation Petri Nets. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 45:1-45:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{raskin_et_al:LIPIcs.CONCUR.2020.45,
  author =	{Raskin, Mikhail and Weil-Kennedy, Chana and Esparza, Javier},
  title =	{{Flatness and Complexity of Immediate Observation Petri Nets}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{45:1--45:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.45},
  URN =		{urn:nbn:de:0030-drops-128574},
  doi =		{10.4230/LIPIcs.CONCUR.2020.45},
  annote =	{Keywords: Petri Nets, Reachability Analysis, Parameterized Verification, Flattability}
}
Document
Reachability in Fixed Dimension Vector Addition Systems with States

Authors: Wojciech Czerwiński, Sławomir Lasota, Ranko Lazić, Jérôme Leroux, and Filip Mazowiecki

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)


Abstract
The reachability problem is a central decision problem in verification of vector addition systems with states (VASS). In spite of recent progress, the complexity of the reachability problem remains unsettled, and it is closely related to the lengths of shortest VASS runs that witness reachability. We obtain three main results for VASS of fixed dimension. For the first two, we assume that the integers in the input are given in unary, and that the control graph of the given VASS is flat (i.e., without nested cycles). We obtain a family of VASS in dimension 3 whose shortest runs are exponential, and we show that the reachability problem is NP-hard in dimension 7. These results resolve negatively questions that had been posed by the works of Blondin et al. in LICS 2015 and Englert et al. in LICS 2016, and contribute a first construction that distinguishes 3-dimensional flat VASS from 2-dimensional ones. Our third result, by means of a novel family of products of integer fractions, shows that 4-dimensional VASS can have doubly exponentially long shortest runs. The smallest dimension for which this was previously known is 14.

Cite as

Wojciech Czerwiński, Sławomir Lasota, Ranko Lazić, Jérôme Leroux, and Filip Mazowiecki. Reachability in Fixed Dimension Vector Addition Systems with States. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 48:1-48:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.CONCUR.2020.48,
  author =	{Czerwi\'{n}ski, Wojciech and Lasota, S{\l}awomir and Lazi\'{c}, Ranko and Leroux, J\'{e}r\^{o}me and Mazowiecki, Filip},
  title =	{{Reachability in Fixed Dimension Vector Addition Systems with States}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{48:1--48:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.48},
  URN =		{urn:nbn:de:0030-drops-128605},
  doi =		{10.4230/LIPIcs.CONCUR.2020.48},
  annote =	{Keywords: reachability problem, vector addition systems, Petri nets}
}
Document
Invited Talk
Finkel Was Right: Counter-Examples to Several Conjectures on Variants of Vector Addition Systems (Invited Talk)

Authors: Ranko Lazić

Published in: LIPIcs, Volume 150, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)


Abstract
Studying one-dimensional grammar vector addition systems has long been advocated by Alain Finkel. In this presentation, we shall see how research on those systems has led to the recent breakthrough tower lower bound for the reachability problem on vector addition systems, obtained by Czerwiński et al. In fact, we shall look at how appropriate modifications of an underlying technical construction can lead to counter-examples to several conjectures on one-dimensional grammar vector addition systems, fixed-dimensional vector addition systems, and fixed-dimensional flat vector addition systems.

Cite as

Ranko Lazić. Finkel Was Right: Counter-Examples to Several Conjectures on Variants of Vector Addition Systems (Invited Talk). In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{lazic:LIPIcs.FSTTCS.2019.3,
  author =	{Lazi\'{c}, Ranko},
  title =	{{Finkel Was Right: Counter-Examples to Several Conjectures on Variants of Vector Addition Systems}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  pages =	{3:1--3:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-131-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{150},
  editor =	{Chattopadhyay, Arkadev and Gastin, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019.3},
  URN =		{urn:nbn:de:0030-drops-115653},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.3},
  annote =	{Keywords: Petri nets, vector addition systems, reachability}
}
Document
Distance Between Mutually Reachable Petri Net Configurations

Authors: Jérôme Leroux

Published in: LIPIcs, Volume 150, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)


Abstract
Petri nets are a classical model of concurrency widely used and studied in formal verification with many applications in modeling and analyzing hardware and software, data bases, and reactive systems. The reachability problem is central since many other problems reduce to reachability questions. In 2011, we proved that a variant of the reachability problem, called the reversible reachability problem is exponential-space complete. Recently, this problem found several unexpected applications in particular in the theory of population protocols. In this paper we revisit the reversible reachability problem in order to prove that the minimal distance in the reachability graph of two mutually reachable configurations is linear with respect to the Euclidean distance between those two configurations.

Cite as

Jérôme Leroux. Distance Between Mutually Reachable Petri Net Configurations. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 47:1-47:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{leroux:LIPIcs.FSTTCS.2019.47,
  author =	{Leroux, J\'{e}r\^{o}me},
  title =	{{Distance Between Mutually Reachable Petri Net Configurations}},
  booktitle =	{39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)},
  pages =	{47:1--47:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-131-3},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{150},
  editor =	{Chattopadhyay, Arkadev and Gastin, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2019.47},
  URN =		{urn:nbn:de:0030-drops-116094},
  doi =		{10.4230/LIPIcs.FSTTCS.2019.47},
  annote =	{Keywords: Petri nets, Vector addition systems, Formal verification, Reachability problem}
}
Document
Invited Talk
Petri Net Reachability Problem (Invited Talk)

Authors: Jérôme Leroux

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)


Abstract
Petri nets, also known as vector addition systems, are a long established model of concurrency with extensive applications in modelling and analysis of hardware, software and database systems, as well as chemical, biological and business processes. The central algorithmic problem for Petri nets is reachability: whether from the given initial configuration there exists a sequence of valid execution steps that reaches the given final configuration. The complexity of the problem has remained unsettled since the 1960s, and it is one of the most prominent open questions in the theory of verification. In this presentation, we overview decidability and complexity results over the last fifty years about the Petri net reachability problem.

Cite as

Jérôme Leroux. Petri Net Reachability Problem (Invited Talk). In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 5:1-5:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{leroux:LIPIcs.MFCS.2019.5,
  author =	{Leroux, J\'{e}r\^{o}me},
  title =	{{Petri Net Reachability Problem}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{5:1--5:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.5},
  URN =		{urn:nbn:de:0030-drops-109493},
  doi =		{10.4230/LIPIcs.MFCS.2019.5},
  annote =	{Keywords: Petri net, Reachability problem, Formal verification, Concurrency}
}
Document
Reachability for Two-Counter Machines with One Test and One Reset

Authors: Alain Finkel, Jérôme Leroux, and Grégoire Sutre

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


Abstract
We prove that the reachability relation of two-counter machines with one zero-test and one reset is Presburger-definable and effectively computable. Our proof is based on the introduction of two classes of Presburger-definable relations effectively stable by transitive closure. This approach generalizes and simplifies the existing different proofs and it solves an open problem introduced by Finkel and Sutre in 2000.

Cite as

Alain Finkel, Jérôme Leroux, and Grégoire Sutre. Reachability for Two-Counter Machines with One Test and One Reset. 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. 31:1-31:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{finkel_et_al:LIPIcs.FSTTCS.2018.31,
  author =	{Finkel, Alain and Leroux, J\'{e}r\^{o}me and Sutre, Gr\'{e}goire},
  title =	{{Reachability for Two-Counter Machines with One Test and One Reset}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{31:1--31:14},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.31},
  URN =		{urn:nbn:de:0030-drops-99305},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.31},
  annote =	{Keywords: Counter machine, Vector addition system, Reachability problem, Formal verification, Presburger arithmetic, Infinite-state system}
}
Document
Polynomial Vector Addition Systems With States

Authors: Jérôme Leroux

Published in: LIPIcs, Volume 107, 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)


Abstract
The reachability problem for vector addition systems is one of the most difficult and central problems in theoretical computer science. The problem is known to be decidable, but despite intense investigation during the last four decades, the exact complexity is still open. For some sub-classes, the complexity of the reachability problem is known. Structurally bounded vector addition systems, the class of vector addition systems with finite reachability sets from any initial configuration, is one of those classes. In fact, the reachability problem was shown to be polynomial-space complete for that class by Praveen and Lodaya in 2008. Surprisingly, extending this property to vector addition systems with states is open. In fact, there exist vector addition systems with states that are structurally bounded but with Ackermannian large sets of reachable configurations. It follows that the reachability problem for that class is between exponential space and Ackermannian. In this paper we introduce the class of polynomial vector addition systems with states, defined as the class of vector addition systems with states with size of reachable configurations bounded polynomially in the size of the initial ones. We prove that the reachability problem for polynomial vector addition systems is exponential-space complete. Additionally, we show that we can decide in polynomial time if a vector addition system with states is polynomial. This characterization introduces the notion of iteration scheme with potential applications to the reachability problem for general vector addition systems.

Cite as

Jérôme Leroux. Polynomial Vector Addition Systems With States. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 107, pp. 134:1-134:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{leroux:LIPIcs.ICALP.2018.134,
  author =	{Leroux, J\'{e}r\^{o}me},
  title =	{{Polynomial Vector Addition Systems With States}},
  booktitle =	{45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)},
  pages =	{134:1--134:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-076-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{107},
  editor =	{Chatzigiannakis, Ioannis and Kaklamanis, Christos and Marx, D\'{a}niel and Sannella, Donald},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2018.134},
  URN =		{urn:nbn:de:0030-drops-91387},
  doi =		{10.4230/LIPIcs.ICALP.2018.134},
  annote =	{Keywords: Vector additions system with states, Reachability problem, Formal verification, Infinite state system, Linear algebra, Kosaraju-Sullivan algorithm}
}
Document
Polynomial-Space Completeness of Reachability for Succinct Branching VASS in Dimension One

Authors: Diego Figueira, Ranko Lazic, Jérôme Leroux, Filip Mazowiecki, and Grégoire Sutre

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)


Abstract
Whether the reachability problem for branching vector addition systems, or equivalently the provability problem for multiplicative exponential linear logic, is decidable has been a long-standing open question. The one-dimensional case is a generalisation of the extensively studied one-counter nets, and it was recently established polynomial-time complete provided counter updates are given in unary. Our main contribution is to determine the complexity when the encoding is binary: polynomial-space complete.

Cite as

Diego Figueira, Ranko Lazic, Jérôme Leroux, Filip Mazowiecki, and Grégoire Sutre. Polynomial-Space Completeness of Reachability for Succinct Branching VASS in Dimension One. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 119:1-119:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{figueira_et_al:LIPIcs.ICALP.2017.119,
  author =	{Figueira, Diego and Lazic, Ranko and Leroux, J\'{e}r\^{o}me and Mazowiecki, Filip and Sutre, Gr\'{e}goire},
  title =	{{Polynomial-Space Completeness of Reachability for Succinct Branching VASS in Dimension One}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{119:1--119:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.119},
  URN =		{urn:nbn:de:0030-drops-74374},
  doi =		{10.4230/LIPIcs.ICALP.2017.119},
  annote =	{Keywords: branching vector addition systems, reachability problem}
}
Document
Model Checking Population Protocols

Authors: Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)


Abstract
Population protocols are a model for parameterized systems in which a set of identical, anonymous, finite-state processes interact pairwise through rendezvous synchronization. In each step, the pair of interacting processes is chosen by a random scheduler. Angluin et al. (PODC 2004) studied population protocols as a distributed computation model. They characterized the computational power in the limit (semi-linear predicates) of a subclass of protocols (the well-specified ones). However, the modeling power of protocols go beyond computation of semi-linear predicates and they can be used to study a wide range of distributed protocols, such as asynchronous leader election or consensus, stochastic evolutionary processes, or chemical reaction networks. Correspondingly, one is interested in checking specifications on these protocols that go beyond the well-specified computation of predicates. In this paper, we characterize the decidability frontier for the model checking problem for population protocols against probabilistic linear-time specifications. We show that the model checking problem is decidable for qualitative objectives, but as hard as the reachability problem for Petri nets - a well-known hard problem without known elementary algorithms. On the other hand, model checking is undecidable for quantitative properties.

Cite as

Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar. Model Checking Population Protocols. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 27:1-27:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.FSTTCS.2016.27,
  author =	{Esparza, Javier and Ganty, Pierre and Leroux, J\'{e}r\^{o}me and Majumdar, Rupak},
  title =	{{Model Checking Population Protocols}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{27:1--27:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.27},
  URN =		{urn:nbn:de:0030-drops-68628},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.27},
  annote =	{Keywords: parameterized systems, population protocols, probabilistic model checking, probabilistic linear-time specifications, decidability}
}
  • Refine by Author
  • 16 Leroux, Jérôme
  • 4 Sutre, Grégoire
  • 3 Esparza, Javier
  • 2 Czerwiński, Wojciech
  • 2 Finkel, Alain
  • Show More...

  • Refine by Classification
  • 8 Theory of computation → Logic and verification
  • 4 Theory of computation → Concurrency
  • 3 Theory of computation
  • 3 Theory of computation → Verification by model checking
  • 2 Mathematics of computing
  • Show More...

  • Refine by Keyword
  • 5 Formal verification
  • 5 Petri nets
  • 5 Reachability problem
  • 3 reachability problem
  • 3 vector addition systems
  • Show More...

  • Refine by Type
  • 18 document
  • 1 volume

  • Refine by Publication Year
  • 5 2023
  • 3 2019
  • 3 2020
  • 2 2016
  • 2 2018
  • Show More...

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