Formal verification of timed properties of randomized distributed algorithms

Abstract

In [11] 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, [11] 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 a non-randomized algorithms can be applied, and correctness proofs can be verified mechanically.