TY - GEN
T1 - Towards efficient verification of population protocols
AU - Blondin, Michael
AU - Esparza, Javier
AU - Jaax, Stefan
AU - Meyer, Philipp J.
N1 - Publisher Copyright:
© 2017 Association for Computing Machinery.
PY - 2017/7/26
Y1 - 2017/7/26
N2 - 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 EXPSPACE-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 problem for WS3 reduces to solving boolean combinations of linear constraints over N. This allowed us to develop the first software able to automatically prove well-specification for all of the infinitely many possible inputs.
AB - 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 EXPSPACE-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 problem for WS3 reduces to solving boolean combinations of linear constraints over N. This allowed us to develop the first software able to automatically prove well-specification for all of the infinitely many possible inputs.
KW - Automated verification
KW - Population protocols
KW - Termination
UR - http://www.scopus.com/inward/record.url?scp=85027872993&partnerID=8YFLogxK
U2 - 10.1145/3087801.3087816
DO - 10.1145/3087801.3087816
M3 - Conference contribution
AN - SCOPUS:85027872993
T3 - Proceedings of the Annual ACM Symposium on Principles of Distributed Computing
SP - 423
EP - 430
BT - PODC 2017 - Proceedings of the ACM Symposium on Principles of Distributed Computing
PB - Association for Computing Machinery
T2 - 36th ACM Symposium on Principles of Distributed Computing, PODC 2017
Y2 - 25 July 2017 through 27 July 2017
ER -