Notes:
The original publication is available at link.springer.com.

Abstract.
Herman's selfstabilisation algorithm provides a simple randomised solution to the problem of recovering from faults in an Nprocess token ring. However, a precise analysis of the algorithm's maximum execution time proves to be surprisingly difficult. McIver and Morgan have conjectured that the worstcase behaviour results from a ring configuration of three evenly spaced tokens, giving an expected time of approximately 0.15N^{2}. However, the tightest upper bound proved to date is 0.64N^{2}. We apply probabilistic verification techniques, using the probabilistic model checker PRISM, to analyse the conjecture, showing it to be correct for all sizes of the ring that can be exhaustively analysed. We furthermore demonstrate that the worstcase execution time of the algorithm can be reduced by using a biased coin.
