Sciweavers

JUCS
2006

Variations on Itai-Rodeh Leader Election for Anonymous Rings and their Analysis in PRISM

13 years 12 months ago
Variations on Itai-Rodeh Leader Election for Anonymous Rings and their Analysis in PRISM
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. Key Words: distributed computing, leader election, anonymous networks, probabilistic algorithms, formal verification, model checking Category: C.2.4, D.2.4, F.3.1
Wan Fokkink, Jun Pang
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2006
Where JUCS
Authors Wan Fokkink, Jun Pang
Comments (0)