Verification of Population Protocols with Unordered Data
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917655675404288 |
|---|---|
| author | van Bergerem, Steffen Guttenberg, Roland Kiefer, Sandra Mascle, Corto Waldburger, Nicolas Weil-Kennedy, Chana |
| author_facet | van Bergerem, Steffen Guttenberg, Roland Kiefer, Sandra Mascle, Corto Waldburger, Nicolas Weil-Kennedy, Chana |
| contents | 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, that is, 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_00921 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Verification of Population Protocols with Unordered Data van Bergerem, Steffen Guttenberg, Roland Kiefer, Sandra Mascle, Corto Waldburger, Nicolas Weil-Kennedy, Chana Distributed, Parallel, and Cluster Computing Logic in Computer Science Multiagent Systems 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, that is, 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. |
| title | Verification of Population Protocols with Unordered Data |
| topic | Distributed, Parallel, and Cluster Computing Logic in Computer Science Multiagent Systems |
| url | https://arxiv.org/abs/2405.00921 |