Search Results

Documents authored by Guttenberg, Roland

Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.141
Flattability of Priority Vector Addition Systems

Authors: Roland Guttenberg

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

Abstract
Vector addition systems (VAS), also known as Petri nets, are a popular model of concurrent systems. Many problems from many areas reduce to the reachability problem for VAS, which consists of deciding whether a target configuration of a VAS is reachable from a given initial configuration. One of the main approaches to solve the problem on practical instances is called flattening, intuitively removing nested loops. This technique is known to terminate for semilinear VAS due to [Jérôme Leroux, 2013]. In this paper, we prove that also for VAS with nested zero tests, called Priority VAS, flattening does in fact terminate for all semilinear reachability relations. Furthermore, we prove that Priority VAS admit semilinear inductive invariants. Both of these results are obtained by defining a well-quasi-order on runs of Priority VAS which has good pumping properties.
Cite as

Roland Guttenberg. Flattability of Priority Vector Addition Systems. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 141:1-141:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{guttenberg:LIPIcs.ICALP.2024.141,
  author =	{Guttenberg, Roland},
  title =	{{Flattability of Priority Vector Addition Systems}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{141:1--141:20},
  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.141},
  URN =		{urn:nbn:de:0030-drops-202848},
  doi =		{10.4230/LIPIcs.ICALP.2024.141},
  annote =	{Keywords: Priority Vector Addition Systems, Semilinear, Inductive Invariants, Geometry, Flattability, Almost Semilinear, Transformer Relation}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.156
Verification of Population Protocols with Unordered Data

Authors: Steffen van Bergerem, Roland Guttenberg, Sandra Kiefer, Corto Mascle, Nicolas Waldburger, and Chana Weil-Kennedy

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

Abstract
Population protocols are a well-studied model of distributed computation in which a group of anonymous finite-state agents communicates via pairwise interactions. Together they decide whether their initial configuration, i. e., the initial distribution of agents in the states, satisfies a property. As an extension in order to express properties of multisets over an infinite data domain, Blondin and Ladouceur (ICALP'23) introduced population protocols with unordered data (PPUD). In PPUD, each agent carries a fixed data value, and the interactions between agents depend on whether their data are equal or not. Blondin and Ladouceur also identified the interesting subclass of immediate observation PPUD (IOPPUD), where in every transition one of the two agents remains passive and does not move, and they characterised its expressive power. We study the decidability and complexity of formally verifying these protocols. The main verification problem for population protocols is well-specification, that is, checking whether the given PPUD computes some function. We show that well-specification is undecidable in general. By contrast, for IOPPUD, we exhibit a large yet natural class of problems, which includes well-specification among other classic problems, and establish that these problems are in ExpSpace. We also provide a lower complexity bound, namely coNExpTime-hardness.
Cite as

Steffen van Bergerem, Roland Guttenberg, Sandra Kiefer, Corto Mascle, Nicolas Waldburger, and Chana Weil-Kennedy. Verification of Population Protocols with Unordered Data. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 156:1-156:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{vanbergerem_et_al:LIPIcs.ICALP.2024.156,
  author =	{van Bergerem, Steffen and Guttenberg, Roland and Kiefer, Sandra and Mascle, Corto and Waldburger, Nicolas and Weil-Kennedy, Chana},
  title =	{{Verification of Population Protocols with Unordered Data}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{156:1--156:20},
  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.156},
  URN =		{urn:nbn:de:0030-drops-202993},
  doi =		{10.4230/LIPIcs.ICALP.2024.156},
  annote =	{Keywords: Population protocols, Parameterized verification, Distributed computing, Well-specification}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2023.6
Geometry of Reachability Sets of Vector Addition Systems

Authors: Roland Guttenberg, Mikhail Raskin, and Javier Esparza

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

Abstract
Vector Addition Systems (VAS), aka Petri nets, are a popular model of concurrency. The reachability set of a VAS is the set of configurations reachable from the initial configuration. Leroux has studied the geometric properties of VAS reachability sets, and used them to derive decision procedures for important analysis problems. In this paper we continue the geometric study of reachability sets. We show that every reachability set admits a finite decomposition into disjoint almost hybridlinear sets enjoying nice geometric properties. Further, we prove that the decomposition of the reachability set of a given VAS is effectively computable. As a corollary, we derive a new proof of Hauschildt’s 1990 result showing the decidability of the question whether the reachability set of a given VAS is semilinear. As a second corollary, we prove that the complement of a reachability set, if it is infinite, always contains an infinite linear set.
Cite as

Roland Guttenberg, Mikhail Raskin, and Javier Esparza. Geometry of Reachability Sets of Vector Addition Systems. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{guttenberg_et_al:LIPIcs.CONCUR.2023.6,
  author =	{Guttenberg, Roland and Raskin, Mikhail and Esparza, Javier},
  title =	{{Geometry of Reachability Sets of Vector Addition Systems}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{6:1--6:16},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.6},
  URN =		{urn:nbn:de:0030-drops-190005},
  doi =		{10.4230/LIPIcs.CONCUR.2023.6},
  annote =	{Keywords: Vector Addition System, Petri net, Reachability Set, Almost hybridlinear, Partition, Geometry}
}
Document
DOI: 10.4230/LIPIcs.SAND.2022.11
Fast and Succinct Population Protocols for Presburger Arithmetic

Authors: Philipp Czerner, Roland Guttenberg, Martin Helfrich, and Javier Esparza

Published in: LIPIcs, Volume 221, 1st Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2022)

Abstract
In their 2006 seminal paper in Distributed Computing, Angluin et al. present a construction that, given any Presburger predicate as input, outputs a leaderless population protocol that decides the predicate. The protocol for a predicate of size m (when expressed as a Boolean combination of threshold and remainder predicates with coefficients in binary) runs in 𝒪(m ⋅ n² log n) expected number of interactions, which is almost optimal in n, the number of interacting agents. However, the number of states of the protocol is exponential in m. This is a problem for natural computing applications, where a state corresponds to a chemical species and it is difficult to implement protocols with many states. Blondin et al. described in STACS 2020 another construction that produces protocols with a polynomial number of states, but exponential expected number of interactions. We present a construction that produces protocols with 𝒪(m) states that run in expected 𝒪(m⁷ ⋅ n²) interactions, optimal in n, for all inputs of size Ω(m). For this, we introduce population computers, a carefully crafted generalization of population protocols easier to program, and show that our computers for Presburger predicates can be translated into fast and succinct population protocols.
Cite as

Philipp Czerner, Roland Guttenberg, Martin Helfrich, and Javier Esparza. Fast and Succinct Population Protocols for Presburger Arithmetic. In 1st Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 221, pp. 11:1-11:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{czerner_et_al:LIPIcs.SAND.2022.11,
  author =	{Czerner, Philipp and Guttenberg, Roland and Helfrich, Martin and Esparza, Javier},
  title =	{{Fast and Succinct Population Protocols for Presburger Arithmetic}},
  booktitle =	{1st Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2022)},
  pages =	{11:1--11:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-224-2},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{221},
  editor =	{Aspnes, James and Michail, Othon},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAND.2022.11},
  URN =		{urn:nbn:de:0030-drops-159535},
  doi =		{10.4230/LIPIcs.SAND.2022.11},
  annote =	{Keywords: population protocols, fast, succinct, population computers}
}
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact