Document Open Access Logo

Verification of Population Protocols with Unordered Data

Authors Steffen van Bergerem , Roland Guttenberg , Sandra Kiefer , Corto Mascle, Nicolas Waldburger , Chana Weil-Kennedy

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICALP.2024.156.pdf
  • Filesize: 1.09 MB
  • 20 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Verification by model checking
  • Theory of computation → Distributed computing models
Keywords
  • Population protocols
  • Parameterized verification
  • Distributed computing
  • Well-specification

Metrics

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

Abstract

Population protocols are a well-studied model of distributed computation in which a group of anonymous finite-state agents communicates via pairwise interactions. Together they decide whether their initial configuration, i. e., the initial distribution of agents in the states, satisfies a property. As an extension in order to express properties of multisets over an infinite data domain, Blondin and Ladouceur (ICALP'23) introduced population protocols with unordered data (PPUD). In PPUD, each agent carries a fixed data value, and the interactions between agents depend on whether their data are equal or not. Blondin and Ladouceur also identified the interesting subclass of immediate observation PPUD (IOPPUD), where in every transition one of the two agents remains passive and does not move, and they characterised its expressive power.
We study the decidability and complexity of formally verifying these protocols. The main verification problem for population protocols is well-specification, that is, checking whether the given PPUD computes some function. We show that well-specification is undecidable in general. By contrast, for IOPPUD, we exhibit a large yet natural class of problems, which includes well-specification among other classic problems, and establish that these problems are in ExpSpace. We also provide a lower complexity bound, namely coNExpTime-hardness.

Cite As Get BibTex

Steffen van Bergerem, Roland Guttenberg, Sandra Kiefer, Corto Mascle, Nicolas Waldburger, and Chana Weil-Kennedy. Verification of Population Protocols with Unordered Data. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 156:1-156:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.ICALP.2024.156

Author Details

Steffen van Bergerem
  • Humboldt-Universität zu Berlin, Germany
Roland Guttenberg
  • Technische Universität München, Germany
Sandra Kiefer
  • University of Oxford, UK
Corto Mascle
  • LaBRI, Université de Bordeaux, France
Nicolas Waldburger
  • IRISA, Université de Rennes, France
Chana Weil-Kennedy
  • IMDEA Software Institute, Madrid, Spain

Funding

  • van Bergerem, Steffen: This work was funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - project number 431183758 (gefördert durch die Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 431183758).
  • Kiefer, Sandra: This research was supported by the Glasstone Benefaction, University of Oxford [Violette and Samuel Glasstone Research Fellowships in Science 2022] as well as Jesus College in Oxford, UK.
  • Weil-Kennedy, Chana: This work was supported by the grant PID2022-138072OB-I00, funded by MCIN, FEDER, UE and partially supported by PRODIGY Project (TED2021-132464B-I00) funded by MCIN and the European Union NextGeneration.

Acknowledgements

This project started at and has benefitted substantially from the research camp Autobóz 2023 in Kassel, Germany. We would like to thank the host, sponsors, and organisers of the research camp for bringing us together.

References

  1. Dan Alistarh, James Aspnes, David Eisenstat, Rati Gelashvili, and Ronald L. Rivest. Time-space trade-offs in population protocols. In 28th Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2017, pages 2560-2579, 2017. URL: https://doi.org/10.1137/1.9781611974782.169.
  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 33rd Annual ACM Symposium on Principles of Distributed Computing, PODC 2004, pages 290-299. ACM, 2004. URL: https://doi.org/10.1145/1011767.1011810.
  4. Dana Angluin, James Aspnes, David Eisenstat, and Eric Ruppert. The computational power of population protocols. Distributed Comput., 20(4):279-304, 2007. URL: https://doi.org/10.1007/S00446-007-0040-2.
  5. A. R. Balasubramanian, Lucie Guillou, and Chana Weil-Kennedy. Parameterized analysis of reconfigurable broadcast networks. In Foundations of Software Science and Computation Structures - 25th International Conference, FoSSaCS 2022, pages 61-80, 2022. URL: https://doi.org/10.1007/978-3-030-99253-8_4.
  6. A. R. Balasubramanian and Chana Weil-Kennedy. Reconfigurable broadcast networks and asynchronous shared-memory systems are equivalent. In 12th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2021, pages 18-34, 2021. URL: https://doi.org/10.4204/EPTCS.346.2.
  7. Steffen van Bergerem, Roland Guttenberg, Sandra Kiefer, Corto Mascle, Nicolas Waldburger, and Chana Weil-Kennedy. Verification of population protocols with unordered data. CoRR, abs/2405.00921, 2024. URL: https://arxiv.org/abs/2405.00921.
  8. Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, and Josef Widder. Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2015. URL: https://doi.org/10.2200/S00658ED1V01Y201508DCT013.
  9. Michael Blondin, Javier Esparza, Stefan Jaax, and Philipp J. Meyer. Towards efficient verification of population protocols. Formal Methods Syst. Des., 57(3):305-342, 2021. URL: https://doi.org/10.1007/S10703-021-00367-3.
  10. Michael Blondin and François Ladouceur. Population protocols with unordered data. In 50th International Colloquium on Automata, Languages, and Programming, ICALP 2023, pages 115:1-115:20, 2023. URL: https://doi.org/10.4230/LIPICS.ICALP.2023.115.
  11. Patricia Bouyer, Nicolas Markey, Mickael Randour, Arnaud Sangnier, and Daniel Stan. Reachability in networks of register protocols under stochastic schedulers. In 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, pages 106:1-106:14, 2016. URL: https://doi.org/10.4230/LIPICS.ICALP.2016.106.
  12. Philipp Czerner, Roland Guttenberg, Martin Helfrich, and Javier Esparza. Fast and succinct population protocols for Presburger arithmetic. J. Comput. Syst. Sci., 140:103481, 2024. URL: https://doi.org/10.1016/J.JCSS.2023.103481.
  13. Wojciech Czerwinski and Lukasz Orlikowski. Reachability in vector addition systems is Ackermann-complete. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, pages 1229-1240, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00120.
  14. Robert Elsässer and Tomasz Radzik. Recent results in population protocols for exact majority and leader election. Bull. EATCS, 126, 2018. URL: http://bulletin.eatcs.org/index.php/beatcs/article/view/549/546.
  15. Javier Esparza. Keeping a crowd safe: On the complexity of parameterized verification (invited talk). In 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014), STACS 2014, March 5-8, 2014, Lyon, France, pages 1-10, 2014. URL: https://doi.org/10.4230/LIPICS.STACS.2014.1.
  16. Javier Esparza. Population protocols: Beyond runtime analysis. In Reachability Problems - 15th International Conference, RP 2021, pages 28-51, 2021. URL: https://doi.org/10.1007/978-3-030-89716-1_3.
  17. 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.
  18. Javier Esparza, Stefan Jaax, Mikhail A. Raskin, and Chana Weil-Kennedy. The complexity of verifying population protocols. Distributed Comput., 34(2):133-177, 2021. URL: https://doi.org/10.1007/S00446-021-00390-X.
  19. Javier Esparza, Mikhail A. Raskin, and Chana Weil-Kennedy. Parameterized analysis of immediate observation Petri nets. In Application and Theory of Petri Nets and Concurrency - 40th International Conference, PETRI NETS 2019, pages 365-385, 2019. URL: https://doi.org/10.1007/978-3-030-21571-2_20.
  20. Lucie Guillou, Corto Mascle, and Nicolas Waldburger. Parameterized broadcast networks with registers: from NP to the frontiers of decidability. In Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, pages 250-270, 2024. URL: https://doi.org/10.1007/978-3-031-57231-9_12.
  21. Petr Jancar. Undecidability of bisimilarity for Petri nets and some related problems. Theor. Comput. Sci., 148(2):281-301, 1995. URL: https://doi.org/10.1016/0304-3975(95)00037-W.
  22. Petr Jancar and Jérôme Leroux. The semilinear home-space problem is Ackermann-complete for Petri nets. In 34th International Conference on Concurrency Theory, CONCUR 2023, pages 36:1-36:17, 2023. URL: https://doi.org/10.4230/LIPICS.CONCUR.2023.36.
  23. Ranko Lazic, Thomas Christopher Newcomb, Joël Ouaknine, A. W. Roscoe, and James Worrell. Nets with tokens which carry data. In 28th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, ICATPN 2007, pages 301-320, 2007. URL: https://doi.org/10.1007/978-3-540-73094-1_19.
  24. Jérôme Leroux. The reachability problem for Petri nets is not primitive recursive. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, pages 1241-1252, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00121.
  25. Jérôme Leroux and Sylvain Schmitz. Reachability in vector addition systems is primitive-recursive in fixed dimension. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, pages 1-13, 2019. URL: https://doi.org/10.1109/LICS.2019.8785796.
  26. Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, Inc., 1967. Google Scholar
  27. Fernando Rosa-Velardo and David de Frutos-Escrig. Decidability and complexity of Petri nets with unordered data. Theor. Comput. Sci., 412(34):4439-4451, 2011. URL: https://doi.org/10.1016/J.TCS.2011.05.007.
  28. François Schwarzentruber. The complexity of tiling problems. CoRR, abs/1907.00102, 2019. URL: https://arxiv.org/abs/1907.00102.
  29. Chana Weil-Kennedy. Observation Petri Nets. PhD thesis, Technical University of Munich, Germany, 2023. URL: https://nbn-resolving.org/urn:nbn:de:bvb:91-diss-20230320-1691161-1-3.
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