LIPIcs.STACS.2020.40.pdf
- Filesize: 0.59 MB
- 15 pages
Document
Succinct Population Protocols for Presburger Arithmetic
Authors
Michael Blondin 
,
Javier Esparza ,
Blaise Genest ,
Martin Helfrich ,
Stefan Jaax
-
Part of:
Volume:
37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Symposium on Theoretical Aspects of Computer Science (STACS) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2020-03-04
File
Document Identifiers
Author Details
- Fakultät für Informatik, Technische Universität München, Garching bei München, Germany
- Fakultät für Informatik, Technische Universität München, Garching bei München, Germany
Cite As Get BibTex
Michael Blondin, Javier Esparza, Blaise Genest, Martin Helfrich, and Stefan Jaax. Succinct Population Protocols for Presburger Arithmetic. In 37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 154, pp. 40:1-40:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.STACS.2020.40
Abstract
In [Dana Angluin et al., 2006], Angluin et al. proved that population protocols compute exactly the predicates definable in Presburger arithmetic (PA), the first-order theory of addition. As part of this result, they presented a procedure that translates any formula φ of quantifier-free PA with remainder predicates (which has the same expressive power as full PA) into a population protocol with 2^?(poly(|φ|)) states that computes φ. More precisely, the number of states of the protocol is exponential in both the bit length of the largest coefficient in the formula, and the number of nodes of its syntax tree. In this paper, we prove that every formula φ of quantifier-free PA with remainder predicates is computable by a leaderless population protocol with ?(poly(|φ|)) states. Our proof is based on several new constructions, which may be of independent interest. Given a formula φ of quantifier-free PA with remainder predicates, a first construction produces a succinct protocol (with ?(|φ|³) leaders) that computes φ; this completes the work initiated in [Michael Blondin et al., 2018], where we constructed such protocols for a fragment of PA. For large enough inputs, we can get rid of these leaders. If the input is not large enough, then it is small, and we design another construction producing a succinct protocol with one leader that computes φ. Our last construction gets rid of this leader for small inputs.
Subject Classification
ACM Subject Classification
- Theory of computation → Distributed computing models
- Theory of computation → Automata over infinite objects
- Theory of computation → Logic and verification
Keywords
- Population protocols
- Presburger arithmetic
- state complexity
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
Dan Alistarh, James Aspnes, David Eisenstat, Rati Gelashvili, and Ronald L. Rivest. Time-space trade-offs in population protocols. In Proc. Twenty-Eighth Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pages 2560-2579. SIAM, 2017.
- Dan Alistarh and Rati Gelashvili. Recent algorithmic advances in population protocols. SIGACT News, 49(3):63-73, 2018. URL: https://doi.org/10.1145/3289137.3289150.
- Dana Angluin, James Aspnes, Zoë Diamadi, Michael J. Fischer, and René Peralta. Computation in networks of passively mobile finite-state sensors. In Proc. 23^rd Annual ACM Symposium on Principles of Distributed Computing (PODC), pages 290-299, 2004. URL: https://doi.org/10.1145/1011767.1011810.
-
Dana Angluin, James Aspnes, Zoë Diamadi, Michael J. Fischer, and René Peralta. Computation in networks of passively mobile finite-state sensors. Distributed Computing, 18(4):235-253, 2006.
- Dana Angluin, James Aspnes, and David Eisenstat. Stably computable predicates are semilinear. In Proc. 25^th Annual ACM Symposium on Principles of Distributed Computing (PODC), pages 292-299, 2006. URL: https://doi.org/10.1145/1146381.1146425.
-
Dana Angluin, James Aspnes, and David Eisenstat. Fast computation by population protocols with a leader. Distributed Computing, 21(3):183-199, 2008.
- Michael Blondin, Javier Esparza, Blaise Genest, Martin Helfrich, and Stefan Jaax. Succinct population protocols for Presburger arithmetic, 2019. URL: http://arxiv.org/abs/1910.04600.
- Michael Blondin, Javier Esparza, and Stefan Jaax. Large flocks of small birds: On the minimal size of population protocols. In Proc. 35^th Symposium on Theoretical Aspects of Computer Science (STACS), pages 16:1-16:14, 2018. URL: https://doi.org/10.4230/LIPIcs.STACS.2018.16.
-
David Doty and David Soloveichik. Stable leader election in population protocols requires linear time. Distributed Computing, 31(4):257-271, 2018.
-
Robert Elsässer and Tomasz Radzik. Recent results in population protocols for exact majority and leader election. Bulletin of the EATCS, 126, 2018.
- Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar. Verification of population protocols. Acta Informatica, 54(2):191-215, 2017. URL: https://doi.org/10.1007/s00236-016-0272-3.
-
Christoph Haase. A survival guide to Presburger arithmetic. SIGLOG News, 5(3):67-82, 2018.
-
Mojżesz Presburger. Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. Comptes rendus du I^er Congrès des mathématiciens des pays slaves, pages 192-201, 1929.
-
David Soloveichik, Matthew Cook, Erik Winfree, and Jehoshua Bruck. Computation with finite stochastic chemical reaction networks. Natural Computing, 7(4):615-633, 2008.