We present two probabilistic leader election algorithms for anonymous unidirectional rings with FIFO channels, based on an algorithm from Itai and Rodeh. 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.

, ,
, , , ,
Software Engineering [SEN]
Software Analysis and Transformation

Fokkink, W.J, & Pang, J. (2004). Simplifying Itai-Rodeh leaderelection for anonymous rings. Software Engineering [SEN]. CWI.