Reference

[PnueliZ86] Pnueli, A. and Zuck, L. Verification of Multiprocess Probabilistic Protocols. In Distrib. Comput., 1: 53-72, 1986.
Downloads: bibAbstract. A new probabilistic symmetric solution to the n processes mutual exclusion problem is presented. The algorithm is verified formally using the extreme fairness approach to probabilistic verification.