Go home now Header Background Image
Submission Procedure
share: |
Follow us
Volume 12 / Issue 8

available in:   PDF (239 kB) PS (189 kB)
Similar Docs BibTeX   Write a comment
Links into Future
DOI:   10.3217/jucs-012-08-0981


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

Wan Fokkink (Vrije Universiteit, The Netherlands)

Jun Pang (Universitat Oldenburg, Germany)

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: anonymous networks, distributed computing, formal verification, leader election, model checking, probabilistic algorithms

Categories: C.2.4, D.2.4, F.3.1