Document Open Access Logo

Verification of Population Protocols

Authors Javier Esparza, Pierre Ganty, Jérôme Leroux, Rupak Majumdar

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2015.470.pdf
  • Filesize: 462 kB
  • 13 pages

Document Identifiers

Subject Classification

Keywords
  • Population protocols
  • Petri nets
  • parametrized verification

Metrics

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

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.

While the predicates computable by well-specified protocols have been extensively studied, the two basic verification problems remain open: is a given protocol well-specified? Does a protocol compute a given predicate? We prove that both problems are decidable. Our results also prove decidability of a natural question about home spaces of Petri nets.

Cite As Get BibTex

Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar. Verification of Population Protocols. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 470-482, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CONCUR.2015.470

Author Details

Javier Esparza
Pierre Ganty
Jérôme Leroux
Rupak Majumdar

References

  1. Benjamin Aminof, Tomer Kotek, Sasha Rubin, Francesco Spegni, and Helmut Veith. Parameterized model checking of rendezvous systems. In CONCUR'14, volume 8704 of LNCS, pages 109-124. Springer, 2014. Google Scholar
  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. Google Scholar
  3. Dana Angluin, James Aspnes, and David Eisenstat. Fast computation by population protocols with a leader. In DISC'06, volume 4167 of LNCS, pages 61-75. Springer, 2006. Google Scholar
  4. Dana Angluin, James Aspnes, and David Eisenstat. Stably computable predicates are semilinear. In PODC'06, pages 292-299. ACM, 2006. Google Scholar
  5. Krzysztof R. Apt and Dexter C. Kozen. Limits for automatic verification of finite-state concurrent systems. Information Processing Letters, 22(6):307-309, 1986. Google Scholar
  6. J. Clement, C. Delporte-Gallet, H. Fauconnier, and M. Sighireanu. Guidelines for the verification of population protocols. In ICDCS'11, pages 215-224, 2011. Google Scholar
  7. Z. Diamadi and Michael J. Fischer. A simple game for the study of trust in distributed systems. Wuhan University Journal of Natural Sciences, 6(1–2):72-82, 2001. Google Scholar
  8. David Frutos-Escrig and C. Johnen. Decidability of home space property. Technical Report 503, LRI, Université de Paris-Sud. Centre d'Orsay., 1989. Google Scholar
  9. Steven M. German and A. Prasad Sistla. Reasoning about systems with many processes. Journal of ACM, 39(3):675-735, 1992. Google Scholar
  10. Seymour Ginsburg. The Mathematical Theory of Context-Free Languages. McGraw-Hill, Inc., New York, NY, USA, 1966. Google Scholar
  11. Jérôme Leroux. The general vector addition system reachability problem by presburger inductive invariants. In LICS'09, pages 4-13. IEEE Computer Society, 2009. Google Scholar
  12. Jérôme Leroux. Vector addition system reversible reachability problem. In CONCUR'11, volume 6901 of LNCS, pages 327-341. Springer, 2011. Google Scholar
  13. Jérôme Leroux. Vector addition systems reachability problem (a simpler solution). In Turing-100: The Alan Turing Centenary Conference, volume 10 of EPiC Series, pages 214-228. EasyChair, 2012. Google Scholar
  14. Jérôme Leroux. Presburger vector addition systems. In LICS'13, pages 23-32. IEEE Computer Society, 2013. Google Scholar
  15. Saket Navlakha and Ziv Bar-Joseph. Distributed information processing in biological and computational systems. Commun. ACM, 58(1):94-102, December 2014. 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
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact