Document Open Access Logo

Succinct Population Protocols for Presburger Arithmetic

Authors Michael Blondin , Javier Esparza , Blaise Genest , Martin Helfrich , Stefan Jaax



PDF
Thumbnail PDF

File

LIPIcs.STACS.2020.40.pdf
  • Filesize: 0.59 MB
  • 15 pages

Document Identifiers

Author Details

Michael Blondin
  • Département d'informatique, Université de Sherbrooke, Sherbrooke, Canada
Javier Esparza
  • Fakultät für Informatik, Technische Universität München, Garching bei München, Germany
Blaise Genest
  • Univ Rennes, CNRS, IRISA, France
Martin Helfrich
  • Fakultät für Informatik, Technische Universität München, Garching bei München, Germany
Stefan Jaax
  • Fakultät für Informatik, Technische Universität München, Garching bei München, Germany

Cite AsGet 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)
    0
    PDF Downloads

References

  1. 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. Google Scholar
  2. 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.
  3. 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.
  4. 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. Google Scholar
  5. 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.
  6. Dana Angluin, James Aspnes, and David Eisenstat. Fast computation by population protocols with a leader. Distributed Computing, 21(3):183-199, 2008. Google Scholar
  7. 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.
  8. 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.
  9. David Doty and David Soloveichik. Stable leader election in population protocols requires linear time. Distributed Computing, 31(4):257-271, 2018. Google Scholar
  10. Robert Elsässer and Tomasz Radzik. Recent results in population protocols for exact majority and leader election. Bulletin of the EATCS, 126, 2018. Google Scholar
  11. 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.
  12. Christoph Haase. A survival guide to Presburger arithmetic. SIGLOG News, 5(3):67-82, 2018. Google Scholar
  13. 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. Google Scholar
  14. David Soloveichik, Matthew Cook, Erik Winfree, and Jehoshua Bruck. Computation with finite stochastic chemical reaction networks. Natural Computing, 7(4):615-633, 2008. Google Scholar
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