[FP06] W. Fokkink and J. Pang. Variations on Itai-Rodeh Leader Election for Anonymous Rings and their Analysis in PRISM. Journal of Universal Computer Science, 12(8), pages 981--1006. 2006. [bib] http://www.jucs.org/jucs_12_8/variations_on_itai_rodeh
Downloads:  bib bib
Abstract. We present two probabilistic leader election algorithms for anonymous unidirectional rings with FIFO channels, based on an algorithm from Itai and Rodeh [Itai and Rodeh 1981]. In contrast to the Itai-Rodeh algorithm, our algorithms are finite-state. So they can be analyzed using explicit state space exploration; we used the probabilistic model checker PRISM to verify, for rings up to size four, that eventually a unique leader is elected with probability one. Furthermore, we give a manual correctness proof for each algorithm.