This case study concerns modeling and verifying the shared coin protocol of the randomised consensus algorithm of Aspnes and Herlihy [AH90] using the RML language.
This case study was taken from the Prism case studies here.
Sponsors
Statistical Model-Checker