Verification of multiprocess probabilistic protocols (Q1079944)

In this paper we demonstrate the utility of temporal logic to the formal verification of probabilistic distributed programs. The approach taken is to represent the quantitative notion of probabilistic computations by the qualitative abstraction of extreme fairness. The method is illustrated first on the dining philosophers problem and then on a new probabilistic symmetric solution to the n-processes mutual exclusion problem. Two related solutions are presented corresponding to different assumptions about the granularity of a compound test.