Verification of Population Protocols with Unordered Data

TL;DR

This paper investigates the verification problem for population protocols with unordered data, showing undecidability in general but EXPSPACE decidability and coNEXPTIME-hardness for a natural subclass called IOPPUD.

Contribution

It establishes the decidability and complexity bounds for verifying population protocols with unordered data, especially focusing on the IOPPUD subclass.

Findings

Well-specification is undecidable for general PPUD.

Verification for IOPPUD is in EXPSPACE.

Verification for IOPPUD is coNEXPTIME-hard.

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.