Towards Efficient Verification of Population Protocols

11:00 24th May 2017 ( week 5, Trinity Term 2017 )Room 051, Wolfson Building, Parks Road
Population protocols are a model of computation by anonymous and identical finite state agents. A protocol is wellspecified if from every initial configuration, all fair executions reach a common consensus. The central verification question for population protocols is the wellspecification problem: deciding if a given protocol is wellspecified. 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 wellspecified stronglysilent protocols and I will show that it is suitable for automatic verification. More precisely, WS³ has the same computational power as general wellspecified 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 wellspecification for all of the infinitely many possible inputs.
This talk is based on joint work with Stefan Jaax, Javier Esparza and Philipp J. Meyer.