Formal Verification of Timed Properties for Randomized Distributed Algorithms

Appears: Proceedings of the 14th Annual ACM Symposium on Principles of Distributed Computing (PODC), Ottawa. Ontario, Canada, pages 174-183, August 1995.

Abstract: In [LSS94] a method for the analysis of the expected time complexity of a randomized distributed algorithm is presented. The method consists of proving auxiliary probabilistic time bound statements of the form U-{t,p}->U', which mean that whenever the algorithm begins in a state in set U, it will reach a state in set U' within time t with probability at least p. However, [LSS94] does not provide a formal methodology to prove the validity of a specific probabilistic time bound statement from scratch: each statement is proved by means of ad hoc operational arguments. Unfortunately, operational reasoning is generally error-prone and difficult to check. In this paper we overcome the problem by developing a new technique to prove probabilistic time bound statements, which consists of reducing the analysis of a time bound statement to the analysis of a statement that does not involve probability. As a consequence, several existing techniques for non-randomized algorithms can be applied, and correctness proofs can be verified mechanically.

Download:

Download the paper from the publisher.

Download an author-created copy of the paper.