文章基本信息

标题：Variations on Itai-Rodeh Leader Election for Anonymous Rings and their Analysis in PRISM
本地全文：下载
作者：W. Fokkink, J. Pang
期刊名称：Journal of Universal Computer Science
印刷版ISSN：0948-6968
出版年度：2006
卷号：12
期号：8
页码：981-981
出版社：Graz University of Technology and Know-Center
摘要：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.
关键词：anonymous networks, distributed computing, formal verification, leader election, model checking, probabilistic algorithms