Verification of Immediate Observation Population Protocols

Authors Javier Esparza , Pierre Ganty , Rupak Majumdar, Chana Weil-Kennedy



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2018.31.pdf
  • Filesize: 0.53 MB
  • 16 pages

Document Identifiers

Author Details

Javier Esparza
  • Technische Universität München, Munich, Germany
Pierre Ganty
  • IMDEA Software Institute, Madrid, Spain
Rupak Majumdar
  • MPI-SWS, Kaiserslautern, Germany
Chana Weil-Kennedy
  • Technische Universität München, Munich, Germany

Cite AsGet BibTex

Javier Esparza, Pierre Ganty, Rupak Majumdar, and Chana Weil-Kennedy. Verification of Immediate Observation Population Protocols. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 31:1-31:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.CONCUR.2018.31

Abstract

Population protocols (Angluin et al., PODC, 2004) 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 satisfying a strong fairness constraint. A population protocol is well-specified if for every initial configuration C of devices, and every computation starting at C, all devices eventually agree on a consensus value depending only on C. If a protocol is well-specified, then it is said to compute the predicate that assigns to each initial configuration its consensus value. In a previous paper we have shown that the problem whether a given protocol is well-specified and the problem whether it computes a given predicate are decidable. However, in the same paper we prove that both problems are at least as hard as the reachability problem for Petri nets. Since all known algorithms for Petri net reachability have non-primitive recursive complexity, in this paper we restrict attention to immediate observation (IO) population protocols, a class introduced and studied in (Angluin et al., PODC, 2006). We show that both problems are solvable in exponential space for IO protocols. This is the first syntactically defined, interesting class of protocols for which an algorithm not requiring Petri net reachability is found.

Subject Classification

ACM Subject Classification
  • Theory of computation → Distributed computing models
Keywords
  • Population protocols
  • Immediate Observation
  • Parametrized verification

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Parosh A. Abdulla and Aletta Nylén. Better is better than well: on efficient verification of infinite-state systems. In LICS\:'00. IEEE Comput. Soc, 2000. URL: http://dx.doi.org/10.1109/lics.2000.855762.
  2. Dana Angluin, James Aspnes, Zoë Diamadi, Michael J. Fischer, and René Peralta. Computation in networks of passively mobile finite-state sensors. In PODC\:'04, pages 290-299. ACM, 2004. URL: http://dx.doi.org/10.1145/1011767.1011810.
  3. 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. URL: http://dx.doi.org/10.1007/s00446-005-0138-3.
  4. Dana Angluin, James Aspnes, David Eisenstat, and Eric Ruppert. The computational power of population protocols. Distributed Computing, 20(4):279-304, 2007. URL: http://dx.doi.org/10.1007/s00446-007-0040-2.
  5. Michael Blondin, Javier Esparza, and Stefan Jaax. Large flocks of small birds: on the minimal size of population protocols. In STACS\:'18, volume 96, pages 16:1-16:14. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2018. URL: http://dx.doi.org/10.4230/LIPIcs.STACS.2018.16.
  6. Laura Bozzelli and Pierre Ganty. Complexity analysis of the backward coverability algorithm for vass. In RP\:'11, volume 6945 of LNCS, pages 96-109. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-24288-5_10.
  7. Ioannis Chatzigiannakis, Othon Michail, and Paul G. Spirakis. Algorithmic verification of population protocols. In SSS\:'10, volume 6366 of LNCS, pages 221-235. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-16023-3_19.
  8. Allan Cheng, Javier Esparza, and Jens Palsberg. Complexity results for 1-safe nets. Theoretical Computer Science, 147(1&2):117-136, 1995. URL: http://dx.doi.org/10.1016/0304-3975(94)00231-7.
  9. Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar. Verification of population protocols. In CONCUR\:'15, volume 42 of LIPIcs, pages 470-482. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2015.470.
  10. Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar. Model checking population protocols. In FSTTCS\:'16, volume 65. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2016. URL: http://dx.doi.org/10.4230/lipics.fsttcs.2016.27.
  11. Neil D. Jones, Lawrence H. Landweber, and Y. Edmund Lien. Complexity of some problems in petri nets. Theoretical Computer Science, 4(3):277-299, 1977. URL: http://dx.doi.org/10.1016/0304-3975(77)90014-7.
  12. Saket Navlakha and Ziv Bar-Joseph. Distributed information processing in biological and computational systems. Commun. ACM, 58(1):94-102, 2014. URL: http://dx.doi.org/10.1145/2678280.
  13. Christos H. Papadimitriou. Computational complexity. Academic Internet Publ., 2007. Google Scholar
  14. Charles Rackoff. The covering and boundedness problems for vector addition systems. Theoretical Computer Science, 6(2):223-231, 1978. URL: http://dx.doi.org/10.1016/0304-3975(78)90036-1.
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