Verification of Randomized Distributed Algorithms
Author: R. Segala.
Appears: Lectures on Formal Methods and Performance Analysis, First EEF/Euro Summer School on Trends in Computer Science, LNCS 2090, pages 232-260, 2001.
We describe modular verification techniques for randomized
distributed algorithms as extensions of techniques for ordinary,
non randomized, distributed algorithms. The main difficulty to
overcome arises from the subtle interplay between probability and
nondeterminism, where probability is due to the random choices that
occur within an algorithm, and nondeterminism is
due to the unknown speeds and scheduling policies of the
processes. The techniques that we introduce are based on separation
of probability from nondeterminism.