An exercise in proving convergence through transfer functions

Self-stabilizing algorithms must fulfill two requirements generally called closure and convergence. We are interested in the convergence property and discuss a new method for proving it. Usually proving the convergence of self-stabilizing algorithms requires a well foundedness argument: briefly spoken it involves exhibiting a convergence function which is shown to decrease with every transition of the algorithm, starting in an illegal state. Devising such a convergence function can be difficult task, since it must bear in itself the essence of stabilization which lies within the algorithm. We explore how to utilize results from control theory to proving the stability of self-stabilizing algorithms. We define a simple stabilization task and adapt stability criteria for linear control circuits to construct a self-stabilizing algorithm which solves the task. In contrast to the usual procedure in which finding a convergence function is an afterthought of algorithm design, our approach can be seen as starting with a convergence function which is implicitly given through a so-called transfer function. Then, we construct an algorithm around it. It turns out that this methodology seems to adapt well to those settings which are quite difficult to handle by the traditional methodologies of self-stabilization