LIPIcs.CONCUR.2018.33.pdf
- Filesize: 0.62 MB
- 16 pages
Document
Automatic Analysis of Expected Termination Time for Population Protocols
Authors
Michael Blondin 
,
Javier Esparza ,
Antonín Kucera
-
Part of:
Volume:
29th International Conference on Concurrency Theory (CONCUR 2018)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Concurrency Theory (CONCUR) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2018-08-31
File
Document Identifiers
Author Details
Cite AsGet BibTex
Michael Blondin, Javier Esparza, and Antonín Kucera. Automatic Analysis of Expected Termination Time for Population Protocols. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 33:1-33:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.CONCUR.2018.33
https://doi.org/10.4230/LIPIcs.CONCUR.2018.33
Abstract
Population protocols are a formal model of sensor networks consisting of identical mobile devices. Two devices can interact and thereby change their states. Computations are infinite sequences of interactions in which the interacting devices are chosen uniformly at random.
In well designed population protocols, for every initial configuration of devices, and for every computation starting at this configuration, all devices eventually agree on a consensus value. We address the problem of automatically computing a parametric bound on the expected time the protocol needs to reach this consensus. We present the first algorithm that, when successful, outputs a function f(n) such that the expected time to consensus is bound by O(f(n)), where n is the number of devices executing the protocol. We experimentally show that our algorithm terminates and provides good bounds for many of the protocols found in the literature.
Subject Classification
ACM Subject Classification
- Theory of computation → Distributed computing models
- Theory of computation → Probabilistic computation
- Theory of computation → Logic and verification
Keywords
- population protocols
- performance analysis
- expected termination time
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. 28^th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pages 2560-2579, 2017. URL: http://dx.doi.org/10.1137/1.9781611974782.169.
- Dan Alistarh, Rati Gelashvili, and Milan Vojnović. Fast and exact majority in population protocols. In Proc. ACM Symposium on Principles of Distributed Computing (PODC), pages 47-56, 2015. URL: http://dx.doi.org/10.1145/2767386.2767429.
- 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: http://dx.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, jan 2006. URL: http://dx.doi.org/10.1007/s00446-005-0138-3.
- Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. How long, O bayesian network, will I sample thee? - A program analysis perspective on expected sampling times. In Proc. 27^th European Symposium on Programming (ESOP), pages 186-213. Springer, 2018. URL: http://dx.doi.org/10.1007/978-3-319-89884-1_7.
- Amanda Belleville, David Doty, and David Soloveichik. Hardness of computing and approximating predicates and functions with leaderless population protocols. In Proc. 44^th International Colloquium on Automata, Languages, and Programming (ICALP), pages 141:1-141:14, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.ICALP.2017.141.
- 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: http://dx.doi.org/10.4230/LIPIcs.STACS.2018.16.
- Michael Blondin, Javier Esparza, Stefan Jaax, and Philipp J. Meyer. Towards efficient verification of population protocols. In Proc. 36^th ACM Symposium on Principles of Distributed Computing (PODC), pages 423-430, 2017. URL: http://dx.doi.org/10.1145/3087801.3087816.
- Michael Blondin, Javier Esparza, and Antonín Kučera. Automatic analysis of expected termination time for population protocols. ArXiv e-prints, 2018. URL: http://arxiv.org/abs/1807.00331.
- Krishnendu Chatterjee, Hongfei Fu, and Aniket Murhekar. Automated recurrence analysis for almost-linear expected-runtime bounds. In Proc. 29^th International Conference on Computer Aided Verification (CAV), pages 118-139, 2017. URL: http://dx.doi.org/10.1007/978-3-319-63387-9_6.
- Ho-Lin Chen, Rachel Cummings, David Doty, and David Soloveichik. Speed faults in computation by chemical reaction networks. Distributed Computing, 30(5):373-390, 2017. URL: http://dx.doi.org/10.1007/s00446-015-0255-6.
- Julien Clément, Carole Delporte-Gallet, Hugues Fauconnier, and Mihaela Sighireanu. Guidelines for the verification of population protocols. In Proc. 31^st International Conference on Distributed Computing Systems (ICDCS), pages 215-224, 2011. URL: http://dx.doi.org/10.1109/ICDCS.2011.36.
- Leonardo Mendonça de Moura and Nikolaj Bjørner. Z3: an efficient SMT solver. In Proc. 14^th International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 337-340, 2008. URL: http://dx.doi.org/10.1007/978-3-540-78800-3_24.
- David Doty and David Soloveichik. Stable leader election in population protocols requires linear time. In Proc. 29^th International Symposium on Distributed Computing (DISC), pages 602-616, 2015. URL: http://dx.doi.org/10.1007/978-3-662-48653-5_40.
- Moez Draief and Milan Vojnović. Convergence speed of binary interval consensus. In Proc. 29^th IEEE International Conference on Computer Communications (INFOCOM), pages 1792-1800, 2010. URL: http://dx.doi.org/10.1109/INFCOM.2010.5461999.
- Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar. Verification of population protocols. Acta Informatica, 54(2):191-215, 2017. URL: http://dx.doi.org/10.1007/s00236-016-0272-3.
- Philippe Flajolet, Bruno Salvy, and Paul Zimmermann. Automatic average-case analysis of algorithm. Theoretical Computer Science, 79(1):37-109, 1991. URL: http://dx.doi.org/10.1016/0304-3975(91)90145-R.
-
Stefan Jaax. Personal communication, April 2018.
- Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. Weakest precondition reasoning for expected run-times of probabilistic programs. In Proc. 25^th European Symposium on Programming (ESOP), pages 364-389. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-662-49498-1_15.
- Othon Michail and Paul G. Spirakis. Elements of the theory of dynamic networks. Communications of the ACM, 61(2):72, 2018. URL: http://dx.doi.org/10.1145/3156693.
- Saket Navlakha and Ziv Bar-Joseph. Distributed information processing in biological and computational systems. Communications of the ACM, 58(1):94-102, 2015. URL: http://dx.doi.org/10.1145/2678280.
- Van Chan Ngo, Quentin Carbonneaux, and Jan Hoffmann. Bounded expectations: resource analysis for probabilistic programs. In Proc. 39^th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 496-512, 2018. URL: http://dx.doi.org/10.1145/3192366.3192394.
- Etienne Perron, Dinkar Vasudevan, and Milan Vojnović. Using three states for binary consensus on complete graphs. In Proc. 28^th IEEE International Conference on Computer Communications (INFOCOM), pages 2527-2535, 2009. URL: http://dx.doi.org/10.1109/INFCOM.2009.5062181.