Towards Efficient Verification of Population Protocols

Population protocols are a model of computation by anonymous and identical finite state agents. A protocol is well-specified if from every initial configuration, all fair executions 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.

In this talk, I will introduce the class WS³ of well-specified strongly-silent protocols and I will show that it is suitable for automatic verification. More precisely, WS³ has the same computational power as general well-specified protocols and captures standard protocols from the literature. Moreover, the membership problem for WS³ 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.

This talk is based on joint work with Stefan Jaax, Javier Esparza and Philipp J. Meyer.