Verification of orbitally self-stabilizing distributed algorithms using Lyapunov functions and Poincare maps

Self-stabilization is a novel method for achieving fault tolerance in distributed applications. A self-stabilizing algorithm will reach a legal set of states, regardless of the starting state or states adopted due to the effects of transient faults, infinite time. However, proving self-stabilization is a difficult task. In this paper, we present a method for showing self-stabilization of a class of non-silent distributed algorithms, namely orbitally self-stabilizing algorithms. An algorithm of this class is modeled as a hybrid feedback control system. We then employ the control theoretic methods of Poincare maps and Lyapunov functions to show convergence to an orbit cycle