Deciding Well-Specification in Population Protocols via Presburger Arithmetic and PetriNet Theory
Javier Esparza, Pierre Ganty, Jerome Leroux, Rupak Majumdar
Progress in Machines and Systems, Vol. 14, No. 2, 2025.
DOI: https://doi.org/10.6025/pms/2025/14/2/47-61
Link: https://www.dline.info/pms/fulltext/v14n2/pmsv14n2_1.pdf
Abstract:
This paper establishes the decidability of the well-specification problem for population protocols, a model of distributed computation by anonymous, finite-state agents. A protocol is well-specified if all fair executions from any initial configuration stabilize to the same consensus value. The authors prove decidability by characterizing well-specification through the existence of a &quot;witness&quot;: a tuple of four Presburgerdefinable, inductive sets of configurations and a bounded language that together guarantee convergence. This characterization leverages deep results from Petri net theory, including the Presburger-definability of mutual reachability and separators for unreachable markings. The same techniques also show decidability for the correctness problem (verifying if a protocol computes a given Presburger predicate) and yield a new decidability result for the home space problem in Petri nets under specific finiteness conditions.