Paper Info
Title
Towards efficient verification of population protocols
Abstract
Population protocols are a well established model of computation by anonymous, identical finite-state agents. A protocol is well-specified if from every initial configuration, all fair executions of the protocol reach a common consensus. The central verification question for population protocols is the well-specification problem: deciding if a given protocol is well-specified. Esparza et al. have recently shown that this problem is decidable, but with very high complexity: it is at least as hard as the Petri net reachability problem, which is TOWER-hard, and for which only algorithms of non-primitive recursive complexity are currently known. In this paper we introduce the class WS3 of well-specified strongly-silent protocols and we prove that it is suitable for automatic verification. More precisely, we show that WS3 has the same computational power as general well-specified protocols, and captures standard protocols from the literature. Moreover, we show that the membership and correctness problems for WS3 reduce to solving boolean combinations of linear constraints over N. This allowed us to develop the first software able to automatically prove correctness for all of the infinitely many possible inputs.
Year
DOI
Venue
2021
10.1007/s10703-021-00367-3
FORMAL METHODS IN SYSTEM DESIGN
Keywords
DocType
Volume
Population protocols, Automated verification, Termination
Journal
57
Issue
ISSN
Citations 
3
0925-9856
0
PageRank 
References 
Authors
0.34
0
4
Name
Order
Citations
PageRank
Michael Blondin1279.06
Javier Esparza277060.33
Stefan Jaax3101.51
Philipp Meyer4294.72