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

Простая страница элемента
dc.creatorFokkink,Wan
dc.creatorPang,Jun
dc.date2006
dc.date.accessioned2024-02-06T12:54:40Z
dc.date.available2024-02-06T12:54:40Z
dc.descriptionWe 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.
dc.formattext/html
dc.identifierhttps://doi.org/10.3217/jucs-012-08-0981
dc.identifierhttps://lib.jucs.org/article/28645/
dc.identifier.urihttps://openrepository.mephi.ru/handle/123456789/9104
dc.languageen
dc.publisherJournal of Universal Computer Science
dc.relationinfo:eu-repo/semantics/altIdentifier/eissn/0948-6968
dc.relationinfo:eu-repo/semantics/altIdentifier/pissn/0948-695X
dc.rightsinfo:eu-repo/semantics/openAccess
dc.rightsJ.UCS License
dc.sourceJUCS - Journal of Universal Computer Science 12(8): 981-1006
dc.subjectdistributed computing
dc.subjectleader election
dc.subjectanonymous networks
dc.subjectprobabilistic algorithms
dc.subjectformal verification
dc.subjectmodel checking
dc.titleVariations on Itai-Rodeh Leader Election for Anonymous Rings and their Analysis in PRISM
dc.typeResearch Article
Файлы
Коллекции