Verification of the Randomized Consensus Algorithm of Aspnes and Herlihy: a Case Study*
| dc.contributor.author | Pogosyants, Anna | en_US |
| dc.contributor.author | Segala, Roberto | en_US |
| dc.contributor.author | Lynch, Nancy A. | en_US |
| dc.date.accessioned | 2023-03-29T14:40:05Z | |
| dc.date.available | 2023-03-29T14:40:05Z | |
| dc.date.issued | 1997-06 | |
| dc.identifier.uri | https://hdl.handle.net/1721.1/149263 | |
| dc.description.abstract | The Probabilistic I/O Automaton model of [20] is used as the basis for a formal presentation and proof of the randomized consensus algorithm of Aspnes and Herlihy. The algorithm guarantees termination within expected polynomial time. The Aspnes-Herlihy algorithm is a rather complex algorithm. Processes move through a succesion of asynchronous rounds, attempting to agree at each round. At each round, the agreement attempt involves a distributed random walk. | en_US |
| dc.relation.ispartofseries | MIT-LCS-TM-555 | |
| dc.title | Verification of the Randomized Consensus Algorithm of Aspnes and Herlihy: a Case Study* | en_US |
