Abstract.
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.