Search Results

Documents authored by Czerner, Philipp

Document
DOI: 10.4230/LIPIcs.DISC.2024.17
Breaking Through the Ω(n)-Space Barrier: Population Protocols Decide Double-Exponential Thresholds

Authors: Philipp Czerner

Published in: LIPIcs, Volume 319, 38th International Symposium on Distributed Computing (DISC 2024)

Abstract
Population protocols are a model of distributed computation in which finite-state agents interact randomly in pairs. A protocol decides for any initial configuration whether it satisfies a fixed property, specified as a predicate on the set of configurations. A family of protocols deciding predicates φ_n is succinct if it uses 𝒪(|φ_n|) states, where φ_n is encoded as quantifier-free Presburger formula with coefficients in binary. (All predicates decidable by population protocols can be encoded in this manner.) While it is known that succinct protocols exist for all predicates, it is open whether protocols with o(|φ_n|) states exist for any family of predicates φ_n. We answer this affirmatively, by constructing protocols with 𝒪(log|φ_n|) states for some family of threshold predicates φ_n(x) ⇔ x ≥ k_n, with k₁,k₂,... ∈ ℕ. (In other words, protocols with 𝒪(n) states that decide x ≥ k for a k ≥ 2^2ⁿ.) This matches a known lower bound. Moreover, our construction for threshold predicates is the first that is not 1-aware, and it is almost self-stabilising.
Cite as

Philipp Czerner. Breaking Through the Ω(n)-Space Barrier: Population Protocols Decide Double-Exponential Thresholds. In 38th International Symposium on Distributed Computing (DISC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 319, pp. 17:1-17:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{czerner:LIPIcs.DISC.2024.17,
  author =	{Czerner, Philipp},
  title =	{{Breaking Through the \Omega(n)-Space Barrier: Population Protocols Decide Double-Exponential Thresholds}},
  booktitle =	{38th International Symposium on Distributed Computing (DISC 2024)},
  pages =	{17:1--17:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-352-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{319},
  editor =	{Alistarh, Dan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2024.17},
  URN =		{urn:nbn:de:0030-drops-212438},
  doi =		{10.4230/LIPIcs.DISC.2024.17},
  annote =	{Keywords: Distributed computing, population protocols, state complexity}
}
Document
Brief Announcement
DOI: 10.4230/LIPIcs.DISC.2024.44
Brief Announcement: The Expressive Power of Uniform Population Protocols with Logarithmic Space

Authors: Philipp Czerner, Vincent Fischer, and Roland Guttenberg

Published in: LIPIcs, Volume 319, 38th International Symposium on Distributed Computing (DISC 2024)

Abstract
Population protocols are a model of computation in which indistinguishable mobile agents interact in pairs to decide a property of their initial configuration. Originally introduced by Angluin et. al. in 2004 with a constant number of states, research nowadays focuses on protocols where the space usage depends on the number of agents. The expressive power of population protocols has so far however only been determined for protocols using o(log n) states, which compute only semilinear predicates, and for Ω(n) states. This leaves a significant gap, particularly concerning protocols with Θ(log n) or Θ(polylog n) states, which are the most common constructions in the literature. In this paper we close the gap and prove that for any ε > 0 and f ∈ Ω(log n) ∩ 𝒪(n^{1-ε}), both uniform and non-uniform population protocols with Θ(f(n)) states can decide exactly NSPACE(f(n) log n).
Cite as

Philipp Czerner, Vincent Fischer, and Roland Guttenberg. Brief Announcement: The Expressive Power of Uniform Population Protocols with Logarithmic Space. In 38th International Symposium on Distributed Computing (DISC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 319, pp. 44:1-44:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{czerner_et_al:LIPIcs.DISC.2024.44,
  author =	{Czerner, Philipp and Fischer, Vincent and Guttenberg, Roland},
  title =	{{Brief Announcement: The Expressive Power of Uniform Population Protocols with Logarithmic Space}},
  booktitle =	{38th International Symposium on Distributed Computing (DISC 2024)},
  pages =	{44:1--44:7},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-352-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{319},
  editor =	{Alistarh, Dan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2024.44},
  URN =		{urn:nbn:de:0030-drops-212726},
  doi =		{10.4230/LIPIcs.DISC.2024.44},
  annote =	{Keywords: Population Protocols, Uniform, Expressive Power}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2024.19
Computing Inductive Invariants of Regular Abstraction Frameworks

Authors: Philipp Czerner, Javier Esparza, Valentin Krasotin, and Christoph Welzel-Mohr

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
Regular transition systems (RTS) are a popular formalism for modeling infinite-state systems in general, and parameterised systems in particular. In a CONCUR 22 paper, Esparza et al. introduce a novel approach to the verification of RTS, based on inductive invariants. The approach computes the intersection of all inductive invariants of a given RTS that can be expressed as CNF formulas with a bounded number of clauses, and uses it to construct an automaton recognising an overapproximation of the reachable configurations. The paper shows that the problem of deciding if the language of this automaton intersects a given regular set of unsafe configurations is in EXPSPACE and PSPACE-hard. We introduce regular abstraction frameworks, a generalisation of the approach of Esparza et al., very similar to the regular abstractions of Hong and Lin. A framework consists of a regular language of constraints, and a transducer, called the interpretation, that assigns to each constraint the set of configurations of the RTS satisfying it. Examples of regular abstraction frameworks include the formulas of Esparza et al., octagons, bounded difference matrices, and views. We show that the generalisation of the decision problem above to regular abstraction frameworks remains in EXPSPACE, and prove a matching (non-trivial) EXPSPACE-hardness bound. EXPSPACE-hardness implies that, in the worst case, the automaton recognising the overapproximation of the reachable configurations has a double-exponential number of states. We introduce a learning algorithm that computes this automaton in a lazy manner, stopping whenever the current hypothesis is already strong enough to prove safety. We report on an implementation and show that our experimental results improve on those of Esparza et al.
Cite as

Philipp Czerner, Javier Esparza, Valentin Krasotin, and Christoph Welzel-Mohr. Computing Inductive Invariants of Regular Abstraction Frameworks. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{czerner_et_al:LIPIcs.CONCUR.2024.19,
  author =	{Czerner, Philipp and Esparza, Javier and Krasotin, Valentin and Welzel-Mohr, Christoph},
  title =	{{Computing Inductive Invariants of Regular Abstraction Frameworks}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{19:1--19:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.19},
  URN =		{urn:nbn:de:0030-drops-207919},
  doi =		{10.4230/LIPIcs.CONCUR.2024.19},
  annote =	{Keywords: Regular model checking, abstraction, inductive invariants}
}
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}
}
Document
DOI: 10.4230/LIPIcs.ESA.2020.36
Compact Oblivious Routing in Weighted Graphs

Authors: Philipp Czerner and Harald Räcke

Published in: LIPIcs, Volume 173, 28th Annual European Symposium on Algorithms (ESA 2020)

Abstract
The space-requirement for routing-tables is an important characteristic of routing schemes. For the cost-measure of minimizing the total network load there exist a variety of results that show tradeoffs between stretch and required size for the routing tables. This paper designs compact routing schemes for the cost-measure congestion, where the goal is to minimize the maximum relative load of a link in the network (the relative load of a link is its traffic divided by its bandwidth). We show that for arbitrary undirected graphs we can obtain oblivious routing strategies with competitive ratio 𝒪̃(1) that have header length 𝒪̃(1), label size 𝒪̃(1), and require routing-tables of size 𝒪̃(deg(v)) at each vertex v in the graph. This improves a result of Räcke and Schmid who proved a similar result in unweighted graphs.
Cite as

Philipp Czerner and Harald Räcke. Compact Oblivious Routing in Weighted Graphs. In 28th Annual European Symposium on Algorithms (ESA 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 173, pp. 36:1-36:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{czerner_et_al:LIPIcs.ESA.2020.36,
  author =	{Czerner, Philipp and R\"{a}cke, Harald},
  title =	{{Compact Oblivious Routing in Weighted Graphs}},
  booktitle =	{28th Annual European Symposium on Algorithms (ESA 2020)},
  pages =	{36:1--36:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-162-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{173},
  editor =	{Grandoni, Fabrizio and Herman, Grzegorz and Sanders, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2020.36},
  URN =		{urn:nbn:de:0030-drops-129024},
  doi =		{10.4230/LIPIcs.ESA.2020.36},
  annote =	{Keywords: Oblivious Routing, Compact Routing, Competitive Analysis}
}
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 About DROPS Imprint Privacy Contact