Verification of Population Protocols with Unordered Data
arXiv (Cornell University)(2024)
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, 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.
MoreTranslated text
Key words
population protocols,unordered data,verification
AI Read Science
Must-Reading Tree
Example
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined