Variations on Itai-Rodeh Leader Election for Anonymous Rings and their Analysis in PRISM
Дата
Авторы
Fokkink,Wan
Pang,Jun
Journal Title
Journal ISSN
Volume Title
Издатель
Journal of Universal Computer Science
Аннотация
Описание
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.
Ключевые слова
distributed computing , leader election , anonymous networks , probabilistic algorithms , formal verification , model checking