This case study is based on the shared coin protocol from the randomised consensus algorithm of Aspnes and Herlihy [AH90].

For more information, see: http://www.prismmodelchecker.org/casestudies/consensus_prism.php

=====================================================================================

[AH90]
J. Aspnes and M. Herlihy.
Fast randomized consensus using shared memory.
Journal of Algorithms, 15(1):441-460, 1990.