Proving convergence of self-stabilizing systems using first-order rewriting and regular languages

摘要

In the framework of self-stabilizing systems, the convergence proof is generally done by exhibiting a mea- sure that strictly decreases until a legitimate configuration is reached. The discovery of such a measure is very specific and requires a deep understanding of the studied transition sys- tem.