JUCS - Journal of Universal Computer Science 12(8): 981-1006, doi: 10.3217/jucs-012-08-0981
Variations on Itai-Rodeh Leader Election for Anonymous Rings and their Analysis in PRISM
expand article infoWan Fokkink‡, Jun Pang§
‡ Vrije Universiteit, Netherlands§ Universitat Oldenburg, Germany

Corresponding author: Wan Fokkink ( wanf@cs.vu.nl )

© Wan Fokkink, Jun Pang.
This article is freely available under the J.UCS Open Content License.
Citation: Fokkink W, Pang J (2006) Variations on Itai-Rodeh Leader Election for Anonymous Rings and their Analysis in PRISM. JUCS - Journal of Universal Computer Science 12(8): 981-1006. https://doi.org/10.3217/jucs-012-08-0981
Open Access
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.
Keywords
distributed computing, leader election, anonymous networks, probabilistic algorithms, formal verification, model checking