Distributed program checking: a paradigm for building self-stabilizing distributed protocols

The notion of distributed program checking as a means of making a distributed algorithm self-stabilizing is explored. A compiler that converts a deterministic synchronous protocol π for static networks into a self-stabilizing version of π for dynamic networks is described. If T_π is the time complexity of π and D is a bound on the diameter of the final network, the compiled version of π stabilizes in time O(D+T _π) and has the same space complexity as π. The general method achieves efficient results for many specific noninteractive tasks. For instance, solutions for the shortest paths and spanning tree problems take O(D) to stabilize, an improvement over the previous best time of O(D² )