Proving probabilistic correctness statements
Isaac Saias · 1992
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 issue involved in this type of analysis, we focus on Rabin's randomized distributed algorithm for mutual exclusion [6].