on the extremely fair treatment of probabilistic algorithms
A proof system based on linear temporal logic for the qualitative verification of concurrent probabilistic programs is proposed. The concept of extreme fairness is introduced as an approximation to the notion of probabilistic executions. The proof system proposed is shown to be relatively complete with respect to validity over all extremely fair computations. The proof methodology is demonstrated by proving correctness of a new probabilistic algorithm for solving the mutual exclusion problem ([CLP]).
fairness probabilistic algorithm systems temporal logic verification concurrency program concept approximation completeness validation methodology correctness mutual exclusion