Verification of Population Protocols with Unordered Data

TL;DR

This work studies verification for population protocols that carry unordered data (PPUD) and its immediate-observation subclass (IOPPUD). It proves that well-specification is undecidable for PPUD, while GRE emptiness for IOPPUD is decidable in $EXPSPACE$ and, in fact, admits a $coNEXPTIME$ lower bound. Central to the results are generalised reachability expressions (GRE), the translation to container representations (boxes and containers), and structural run-bounding lemmas that limit observed data and agents. The approach unifies reachability, safety, and parameterised verification problems under GRE, providing a tractable decision framework for IOPPUD while highlighting inherent hardness barriers for the data-augmented model. The work advances understanding of how data values influence the decidability and complexity of distributed protocol verification.

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.

Figures (7)

• Figure 1: For simplicity, we use Petri net notation: circles are states, rectangles are Petri net transitions. To encode this into our protocols, we split each transition into pairwise interactions.
• Figure 2: An example of a "run" with six steps on a protocol with two states $q_1,q_2$. $\mathsf{a},\mathsf{b},\mathsf{c},\mathsf{d},\mathsf{e}$ denote agents; $\mathsf{a},\mathsf{b},\mathsf{c}$ have the same datum and $\mathsf{d},\mathsf{e}$ have the same datum. Dashed lines are observations.
• Figure 3: How a configuration is mapped to a $(4,2)$-container. Here, the protocol has five states $q_0, \dots, q_4$. Five distinct data appear in the configuration, and they are represented using symbols.
• Figure 4: Partial depiction of the protocol constructed in \ref{['nexptime-hardness']}.
• Figure 5: The part of $\mathcal{P}$ encoding the tiling and checking for duplicates.

Theorems & Definitions (65)

• definition 1
• theorem 1
• definition 2
• theorem 2: BL23, Theorem 18 and Corollary 29
• remark 1
• definition 3
• theorem 3
• proposition 1
• proof
• theorem 3