Proving probabilistic correctness statements: the case of Rabin's algorithm for mutual exclusion
| dc.creator | Saias, Isaac | |
| dc.date | 1994-09-19 | |
| dc.date.accessioned | 2026-07-07T10:19:54Z | |
| dc.date.available | 2026-07-07T10:19:54Z | |
| dc.description | The correctness of most randomized distributed algorithms is expressed by a statement of the form ``some predicate of the executions holds with high probability, regardless of the order in which actions are scheduled''. In this paper, we present a general methodology to prove correctness statements of such randomized algorithms. Specifically, we show how to prove such statements by a series of refinements, which terminate in a statement independent of the schedule. To demonstrate the subtlety of the issues involved in this type of analysis, we focus on Rabin's randomized distributed algorithm for mutual exclusion [Rabin 82]. Surprisingly, it turns out that the algorithm does not maintain one of the requirements of the problem under a certain schedule. In particular, we give a schedule under which a set of processes can suffer lockout for arbitrary long periods. | |
| dc.description | 12 pages | |
| dc.identifier | https://arxiv.org/abs/math/9409219 | |
| dc.identifier | http://arxiv.org/abs/math/9409219 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/174680 | |
| dc.subject | Combinatorics | |
| dc.subject | Computational Complexity | |
| dc.subject | 68Q22 | |
| dc.title | Proving probabilistic correctness statements: the case of Rabin's algorithm for mutual exclusion | |
| dc.type | text |