6 Search Results for "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
Invited Talk
DOI: 10.4230/LIPIcs.FSTTCS.2021.2
State Complexity of Population Protocols (Invited Talk)

Authors: Javier Esparza

Published in: LIPIcs, Volume 213, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)

Abstract
Population protocols were introduced by Angluin et al. in 2004 to study the theoretical properties of networks of mobile sensors with very limited computational resources. They have also been proposed as a natural computing model, with molecules, cells, or microorganisms playing the role of sensors. In a population protocol an arbitrary number of indistinguishable, finite-state agents interact randomly in pairs to collectively decide if their initial global configuration satisfies a given property. The property is formalized as a predicate that maps each initial configuration to an output, 0 or 1. Starting from an initial configuration, the agents eventually agree to the correct output almost surely, and continue producing it forever. The protocol is said to stabilize to the correct output. It is well known that population protocols can decide exactly the semilinear predicates, or, equivalently, the predicates expressible in Presburger arithmetic. Current research concentrates on investigating the amount of resources needed to decide a given predicate. The standard resources, time and memory, translate for population protocols into expected time to stabilization, usually called parallel runtime, and number of states of each agent. In this talk we concentrate on the latter. A variant of population protocols allows for a leader, a distinguished finite-state agent that is added to the initial configuration and, intuitively, helps the other agents to organize the computation. In the last years my collaborators and I have obtained upper and lower bounds for the state complexity of population protocols with and without a leader. Define the state complexity of a predicate as the minimal number of states of a protocol that decides the predicate, and STATE(η) as the maximum state complexity of the predicates of size at most η, where predicates are encoded as quantifier-free formulas of Presburger arithmetic with coefficients written in binary. Using techniques from the theory of Petri nets and Vector Addition Systems, we have shown that STATE(η) is polynomially bounded, even for leaderless protocols; this improves on the exponential bound given in 2004 by Angluin and collaborators. We have also proved that STATE(η) ∈ Ω(log log η) for leaderless protocols, even for those deciding very simple predicates of the form x ≥ c for some constant c. In the talk I report on these results, and on two very recent, still unpublished results. Modulo the pending peer-review confirmation, the first result shows the existence of leaderless protocols with a polynomial number of states and linear parallel runtime, and the second, due to Leroux, gives a Ω((log log η)^{1/3}) lower bound for protocols with a leader.
Cite as

Javier Esparza. State Complexity of Population Protocols (Invited Talk). In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{esparza:LIPIcs.FSTTCS.2021.2,
  author =	{Esparza, Javier},
  title =	{{State Complexity of Population Protocols}},
  booktitle =	{41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)},
  pages =	{2:1--2:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-215-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{213},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Chekuri, Chandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2021.2},
  URN =		{urn:nbn:de:0030-drops-155139},
  doi =		{10.4230/LIPIcs.FSTTCS.2021.2},
  annote =	{Keywords: Population protocols, state complexity, Petri nets}
}
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}
}
  • Refine by Author
  • 5 Czerner, Philipp
  • 3 Esparza, Javier
  • 2 Guttenberg, Roland
  • 1 Fischer, Vincent
  • 1 Helfrich, Martin
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 2 population protocols
  • 2 state complexity
  • 1 Compact Routing
  • 1 Competitive Analysis
  • 1 Distributed computing
  • Show More...

  • Refine by Type
  • 6 document

  • Refine by Publication Year
  • 3 2024
  • 1 2020
  • 1 2021
  • 1 2022

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