This case study is based on Herman's self-stabilising algorithm [Her90].

For more information, see: http://www.prismmodelchecker.org/casestudies/self-stabilisation.php

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

[Her90]
T. Herman
Probabilistic self-stabilization
In Information Processing Letters, 35(2):63-67, 1990