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.

翻译：人口协议是一种经过深入研究的分布式计算模型，其中一组匿名的有限状态智能体通过成对交互进行通信。它们共同决定其初始配置（即智能体在状态中的初始分布）是否满足某个属性。为了表达无限数据域上多重集的属性，Blondin 和 Ladouceur (ICALP'23) 引入了带有无序数据的人口协议（PPUD）。在 PPUD 中，每个智能体携带一个固定的数据值，且智能体之间的交互取决于其数据是否相等。Blondin 和 Ladouceur 还识别出一个有趣的子类——即时观察 PPUD（IOPPUD），其中每次转换中两个智能体之一保持被动且不移动，并刻画了其表达能力。我们研究了这些协议形式化验证的可判定性与复杂度。人口协议的主要验证问题是良规定性（well-specification），即检查给定 PPUD 是否计算了某个函数。我们证明良规定性在一般情况下是不可判定的。相比之下，对于 IOPPUD，我们展示了一个包含良规定性及其他经典问题在内的广泛而自然的问题类，并证明这些问题属于 EXPSPACE。我们还提供了一个下界复杂度，即 coNEXPTIME 困难性。