@article{4563,
  author = {Javier Esparza, Pierre Ganty, Jerome Leroux, Rupak Majumdar},
  title = {Deciding Well-Specification in Population Protocols via Presburger Arithmetic and PetriNet Theory},
  journal = {Progress in Machines and Systems},
  year = {2025},
  volume = {14},
  number = {2},
  doi = {https://doi.org/10.6025/pms/2025/14/2/47-61},
  url = {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 "witness": 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.},
}