2026-07-24T11:30:41Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20299 2024-07-02T07:52:57Z ddc:004 open_access

Verification of Population Protocols with Unordered Data van Bergerem, Steffen Guttenberg, Roland Kiefer, Sandra Mascle, Corto Waldburger, Nicolas Weil-Kennedy, Chana Population protocols Parameterized verification Distributed computing Well-specification 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Steffen van Bergerem and Roland Guttenberg and Sandra Kiefer and Corto Mascle and Nicolas Waldburger and Chana Weil-Kennedy 2024 Is Part Of LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2024.156 urn:nbn:de:0030-drops-202993 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.156 eng https://creativecommons.org/licenses/by/4.0/legalcode