Analysing randomized distributed algorithms

Randomization is of paramount importance in practical applications and randomized algorithms are used widely, for example in co-ordinating distributed computer networks, message routing and cache management. The appeal of randomized algorithms is their simplicity and elegance. However, this comes at a cost: the analysis of such systems become very complex, particularly in the context of distributed computation. This arises through the interplay between probability and nondeterminism. To prove a randomized distributed algorithm correct one usually involves two levels: classical, assertion-based reasoning, and a probabilistic analysis based on a suitable probability space on computations. In this paper we describe a number of approaches which allows us to verify the correctness of randomized distributed algorithms.