An exercise in proving self-stabilization with a variant function

DOI10.1016/0020-0190(88)90131-7MaRDI QIDQ1115172zbMATH OpenOpenAlexFDO

Authors Joep L. W. Kessels

Publication date 1988

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0020-0190(88)90131-7

zbMATH Keywords

bound functiondistributed processingself-stabilizationtoken passingvariant function

Mathematics Subject Classification ID

Theory of operating systems (68N25) Theory of software (68N99) Specification and verification (program logics, model checking, etc.) (68Q60)

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.

Recommendations

• Probabilistic self-stabilization
• A self-stabilizing algorithm for constructing breadth-first trees
• A belated proof of self-stabilization
• scientific article; zbMATH DE number 2226803
• Self-stabilization

Cites work

• A belated proof of self-stabilization
• scientific article; zbMATH DE number 3740740 (Why is no real title available?)
• Self-stabilizing systems in spite of distributed control

Cited in

(18)

• A belated proof of self-stabilization
• A self-stabilizing algorithm for constructing spanning trees
• A self-stabilizing algorithm for constructing breadth-first trees
• A self-stabilizing algorithm for maximal matching
• A self-stabilizing distributed algorithm to find the median of a tree graph
• Self-stabilizing depth-first token circulation on networks
• A self-stabilizing algorithm for coloring bipartite graphs
• A self-stabilizing distributed algorithm to construct an arbitrary spanning tree of a connected graph
• Monotonic self-stabilization and its application to robust and adaptive pattern formation
• Self-stabilizing local k-placement of replicas with local minimum variance
• A SELF-STABILIZING DISTRIBUTED ALGORITHM TO FIND THE CENTER OF A TREE GRAPH
• On the Performance of Beauquier and Debas’ Self-stabilizing Algorithm for Mutual Exclusion
• A Self-stabilizing Algorithm with Tight Bounds for Mutual Exclusion on a Ring
• Tiara: a self-stabilizing deterministic skip list and skip graph
• A SELF-STABILIZING DISTRIBUTED ALGORITHM FOR ALL-PAIRS SHORTEST PATH PROBLEM
• Self-stabilizing token circulation in uniform networks
• Proving convergence of self-stabilizing systems using first-order rewriting and regular languages
• On the performance of Dijkstra's third self-stabilizing algorithm for mutual exclusion and related algorithms

This page was built for publication: An exercise in proving self-stabilization with a variant function

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1115172)