Synthesizing self-stabilization through superposition and backtracking

While the design of self-stabilization is known to be a hard problem, several sound (but incomplete) heuristics exist for algorithmic design of self-stabilization. This paper presents a sound and complete method for algorithmic design of self-stabilizing network protocols. The essence of the proposed approach is based on variable superposition and backtracking search. We have validated the proposed method by creating both a sequential and a parallel implementation in the context of a software tool, called Protocon. Moreover, we have used Protocon to automatically design self-stabilizing protocols for the problems that all existing heuristics fail to solve