A Verification Technique for Self-Stabilizing Algorithms based on Ljapunov's ``Second Method''

Oliver Theel

To appear at Nineteenth Annual ACM SIGACT-SIGOPS Symposium on PRINCIPLES OF DISTRIBUTED COMPUTING (PODC 2000), Portland, Oregon, 16-19 July 2000


Abstract

A particularly suitable design strategy for constructing a robust distributed algorithm is to endow it with a self-stabilization property. Such a property guarantees that the system will always return to and stay within a specified set of legal states within bounded time regardless of its initial state. A self-stabilizing application therefore has the potential of recovering from the effects of arbitrary transient failures. However, to actually verify that an application self-stabilizes can be quite tedious with current proof methodologies and is non-trivial. The self-stabilizing property of distributed algorithms exhibits interesting analogies to stabilizing control circuits used in various engineering domains. In this brief announcement we would like to draw attention to the fact that methodologies from control theory, namely Ljapunov's ``Second Method'' can be used to more easily verify the self-stabilization property of distributed algorithms.