2001 | OriginalPaper | Chapter
Verification of Randomized Distributed Algorithms
Author : Roberto Segala
Published in: Lectures on Formal Methods and PerformanceAnalysis
Publisher: Springer Berlin Heidelberg
Included in: Professional Book Archive
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.