An exercise in proving self-stabilization with a variant function (Q1115172)

A ring of machines is called self-stabilizing if, from any (initial) state and regardless of the possible nondeterminacy, it is bound to become stabilized within a finite number of transitions. A variant function is a function mapping the system states on a well-founded set, i.e., an ordered set without an infinitely decreasing sequence. A straightforward way of proving that the system can always make a transition and then giving a variant function whose value decreases for each transition as long as the system is not stabilized. This implies that the function value is minimal only if the system is in a stabilized state. In this paper, the self-stabilization property of the system is proved in much the same way as loop termination is normally being proved, i.e., by means of a variant function. An attractive property of a self-stabilization proof based on a variant function is that such a proof is rather calculational: the invariant function reduces the verification of the design to a number of simple and independent calculations. In this respect, the role of the variant function in a self-stabilization proof is similar to that of an invariant predicate in a safety proof.