A self-stabilizing distributed algorithm to construct an arbitrary spanning tree of a connected graph

The authors propose a simple self-stabilizing distributed algorithm that maintains an arbitrary spanning tree in a connected graph. In proving the correctness of the algorithm, they develop a new technique without using a bounded function (which is customary for proving correctness of self-stabilizing algorithms); the new approach is simple and can be potentially applied to proving correctness of other self-stabilizing algorithms.