Unavoidable Configurations of Parameterized Rings of Processes
Marie Duflot, Laurent Fribourg, Ulf J. Nilsson, Marie Du Ot, Laurent Fribourg, Ulf Nilsson · 2000
Rewrite systems over words are often used for modeling distributed algorithms over linear networks (or rings) of N processes, where N is a parameter. Here we are interested in constructing a regular set of configurations G which is unavoidable, i.e., such that any infinite derivation intersects G. We give some sufficient conditions of the rewrite system that allow us to construct an unavoidable set G using Caucal's algorithm of prefix rewriting. This construction is used to show the convergence property of distributed algorithms to closed subsets of configurations. The method is useful for proving the correctness of self-stabilizing algorithms and the liveness property of termination detection algorithms. It has been implemented, and successfully applied to several signficant examples, treated in a uniform mechanical way for the first time.