An exercise in proving self-stabilization with a variant function
type: Item
instance of: scholarly article
title: An exercise in proving self-stabilization with a variant function
zbMATH Open document ID: 0663.68010
DOI: 10.1016/0020-0190(88)90131-7
published in: Information Processing Letters
publication date: 1988-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 68N99
Mathematics Subject Classification ID: 68N25
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 4084977
zbMATH Keywords: distributed processing
zbMATH Keywords: token passing
zbMATH Keywords: bound function
zbMATH Keywords: variant function
zbMATH Keywords: self-stabilization
author: Joep L. W. Kessels
MaRDI profile type: Publication
full work available at URL: 0020-0190(88)90131-7
OpenAlex ID: W1970730976
cites work: Self-stabilizing systems in spite of distributed control
cites work: A belated proof of self-stabilization
cites work: Q3925859
description: scientific article; zbMATH DE number 4084977