Verifying Self-stabilizing Population Protocols with Coq
Yuxin Deng and Jean-Francois Monin
Population protocols are an elegant model recently introduced for
distributed algorithms running in large and unreliable networks of
tiny mobile agents. Correctness proofs of such protocols involve
subtle arguments on infinite sequences of events. We propose a
general formalization of self-stabilizing population protocols with
the Coq proof assistant. It is used in reasoning about a concrete
protocol for leader election in complete graphs. The protocol is
formally proved to be correct for networks of arbitrarily large
size. To this end we develop an appropriate theory of infinite
sequences, including results for reasoning on abstractions. In
addition, we provide a constructive correctness proof for a leader
election protocol in directed rings. An advantage of using a
constructive setting is that we get more informative proofs on the
scenarios that converge to the desired configurations.