Modular population protocols
Michael Raskin
TL;DR
The paper extends population protocols with a modular design framework based on input–output specifications that operate on multisets of inputs and outputs, together with a shutdown and reconfiguration mechanism. A protocol implements a specification $(\varphi,\psi)$ if fair executions eventually stabilize outputs that satisfy the specification alongside compatible input–output pairs, even as agents are added or removed. It then presents a completely mechanical method for sequentially composing two protocols to realize the composition of their specifications, and proves that the set of implementable specifications is exactly the semilinear (Presburger-definable) ones, thereby preserving a tractable expressive power. While these constructions generalize predicate computation to richer output distributions, they may be inefficient in practice, motivating future work on faster, succinct semilinear protocols. The framework enables modular, dynamic role assignment and multiphase computations in distributed settings, with potential applications in fleet management and other adaptive systems.
Abstract
Population protocols are a model of distributed computation intended for the study of networks of independent computing agents with dynamic communication structure. Each agent has a finite number of states, and communication opportunities occur nondeterministically, allowing the agents involved to change their states based on each other's states. Population protocols are often studied in terms of reaching a consensus on whether the input configuration satisfied some predicate. A desirable property of a computation model is modularity, the ability to combine existing simpler computations in a straightforward way. In the present paper we present a more general notion of functionality implemented by a population protocol in terms of multisets of inputs and outputs. This notion allows to design multiphase protocols as combinations of independently defined phases. The additional generality also increases the range of behaviours that can be captured in applications (e.g. maintaining the role distribution in a fleet of servers). We show that composition of protocols can be performed in a uniform mechanical way, and that the expressive power is essentially semilinear, similar to the predicate expressive power in the original population protocol setting.