Verification of Randomized Distributed Algorithms

Appears: Lectures on Formal Methods and Performance Analysis, First EEF/Euro Summer School on Trends in Computer Science, LNCS 2090, pages 232-260, 2001.

Abstract: 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.
When the nondeterminism is factored out, the analysis of an algorithm has several pieces that are in common with the area of performance evaluation. Thus, the techniques that we describe are likely to constitute a bridge to export typical performance evaluation techniques to the area of concurrent nondeterministic systems and, vice versa, to understand alternative ways for handling nondeterminism when it arises.

Download:
Download the full paper from the publisher.

Download an author-created copy of the paper (© Springer-Verlag).