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 measure 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 system. In contrast we propose here a simple method for proving convergence, which regards self-stabilizing systems as string rewrite systems, and adapts a procedure initially designed by Dershowitz for proving termination of string rewrite systems. In order to make the method terminate more often, we also propose an adapted procedure that manipulates "schemes", i.e. regular sets of words, and incorporates a process of scheme generalization. The interest of the method is illustrated on several nontrivial examples.
Introduction
Introduced by Dijkstra, with three mutual exclusion algorithms on a ring of processes
[11], the notion of self-stabilization has been largely studied for the last
ten years (see [29,31] for surveys). In this paper, we consider a system which
consists of a ring of machines controlled by a "central demon". Its configuration
is the concatenation of the component local states and it is characterized by
a set S of transitions defined over configurations. The system is self-stabilizing
with respect to a subset L of legitimate configurations when, regardless of the
initial configuration and regardless of the transition selected at each step by the
central demon, it is guaranteed to reach a configuration of L within a finite number
of steps. The set L is assumed to have a closure property: from a legitimate
configuration in L, the system persistently remains in L. It is also frequent to
This paper is a revised and extended version of a communication given by the three
first authors, at Symp. DISC'99, under the title "A new rewrite method for proving
convergence of self-stabilizing systems" (LNCS 1693, Springer-Verlag, pp. 240-253).
assume that there is no-deadlock. With these two hypotheses, it is easy to show
that a system is self-stabilizing iff it has the no-cycle property: there is no cyclic
sequence of transitions which contains some configuration w 62 L. This property
is often proved by exhibiting a norm function defined over the set of configu-
rations, whose value strictly decreases after each transition (or each bounded
sequence of transitions) as long as the configuration is not legitimate [31]. Since
such a measure is usually very specific to the considered system, finding one is
very difficult and requires a deep understanding of this system (see e.g.[23,14,4]).
We propose here a new approach for proving the absence of cycle. Configurations
are viewed as words of a formal language, transitions of S as rewrite
rules, and the no-cycle property as a variant of the nontermination property for
rewrite rules. The absence of infinite sequences will be shown by refining the generation
procedure of reduction chains 1 , first proposed by Dershowitz for proving
string rewriting termination [8]. The method proposed here is new in that: 1) it
uses a general technique of string-rewriting to deal with self-stabilization; 2) it
does not consider all the possible rewrite derivations, but only "representative"
ones, using a restricted first-order rewriting strategy. A generalization strategy,
replacing sequences of words with regular languages, is also incorporated in the
method in order to improve its termination.
Related work on self-stabilization proofs. [11] is without proof. In [12], a
correctness proof is given for the third (3-state) algorithm of [11], by showing
properties of executions using behavioral reasoning. As already pointed out, almost
all further proof methods (cf. [31]) are based on norm functions (see an
example in [19]) but, as expressed by Gouda in [15]: "It has been my experience
that the ratio of time to design a stabilizing system to the time to verify its stabilization
is about one to ten". For simplifying proof process, general paradigms
have been proposed: various protocol compositions making proofs modular [3,16],
attractor or staircase methods [15,29], automatic transformations into stabilizing
systems [2]. The idea of representing sets of configurations as regular languages
is used in [18], but, only at a "ground" level (without use of 1st-order variables).
Note that, recently, some works were done for proving convergence without appealing
to a norm function: [32] uses techniques borrowed from control theory
and [1] induction techniques over the set of configurations.
Related work on rewrite techniques applied to distributed systems. Although
viewing transitions as rewrite rules is rather natural, the application of
general rewrite techniques for proving properties of distributed systems has not
been explored to our knowledge, except in [25-27] where graph rewriting techniques
(with priorities) are used to prove the correctness of various distributed
algorithms (election, spanning-tree construction,. However this work does not
address the issue of self-stabilization.
1 also called forward closures in [9].
Plan of the paper. Section 2 explains how self-stabilization can be viewed
as a property of string rewriting systems. In section 3, we give a basic pro-
cedure, inspired from Dershowitz, that, when it terminates, allows to decide
self-stabilization. In order to make the procedure terminate more often, we incorporate
a process of generalization into it (section 4). Section 5 shows application
of the method on detailed examples and section 6 concludes with final remarks
and perspectives.
Self-stabilizing systems as string rewrite systems
We first recall some basic definitions from (string) rewrite systems [10,5]. The
words considered here are generally delimited by a leftmost and rightmost special
'#'. The symbols appearing between them belong to a finite alphabet
\Sigma or a set of variable symbols. A string is an element of
\Sigma   , with " for the empty string. A ground word is an element of #\Sigma   # and a
(1st-order) word is an element of #(\Sigma [ V)   #. A substitution is a mapping '
from V to (\Sigma [V)   with '(W almost everywhere except on a finite set of
variables denoted by Dom('). This mapping extends trivially to words and the
result '(w) is called an instance of the word w. A substitution ' is represented by
a finite set of pairs of the form fW='(W )g W2Dom(') . A substitution ' is ground
when '(W ) is in \Sigma   , for all W 2 Dom(').
2.1 String rewrite systems.
The string rewrite systems S considered here contain length-preserving rules,
divided into three subsets: top rules in Top S are applied to the rightmost part
of words; bottom rules in Bottom S are applied to the leftmost part of words
(or simultaneously at both ends); the rest of rules in Middle S are called middle
rules. More precisely, let '; r (resp. ' be nonempty strings of \Sigma
of the same length, and X;Y variables,
Middle S is made of rules of the form: #X'Y #XrY #
TopS is made of rules of the form: #X'#Xr#
Bottom S is made of rules of the form:
#'X#rX# or #' 1 X' 2 #r 1 Xr 2 #.
We are going to apply these rules either to ground words or to 1st-order words
of the form #uW v# where u; v are strings over \Sigma   , and W is a variable.
Example.
Consider the following rules from Beauquier-Debas algorithm (see section 5):
is a bottom-rule.
is a top-rule.
are middle rules.
These rules are used throughout the next sections to illustrate the notions which
are defined, as well as the method we propose. Note that, strictly speaking, rules
can be applied only if Y 6= ". For example, M 1 should correspond
to 3 rules of the form #X10aY #X01aY # with a 2 f0; 1; 2g. For the sake
of conciseness, we neglect such a restrictive condition of application (except at
section 5).
2.2 Ground reduction.
A ground word w is reducible via a rule of the form #X' 1 Y #Xr 1 Y # iff
One also says that w is an instance of
the rule lefthand side via the ground substitution fX=u; Y=vg. The reduced form
of w is w Reduction via a rule of the form #' 1 X' 2 #r 1 Xr 2 #
is defined in a similar way.
A ground word w reduces to w 0 via S, written w !S w 0 (or sometimes simply
is the reduced form of w via some rule of S. We say that S is
non terminating iff there exists an infinite sequence of reductions via S starting
from some ground word w. Otherwise, S is said to be terminating.
Example. Consider #2X1#1X2#. The ground word
is an instance of the lefthand side, using the substitution fX=01g. Replacement
with the righthand side, yields the reduced form w
Reduction of a ground word w using a middle rule R : X'Y ! XrY merely
consists in searching for a substring ' of R, and replacing it with r. Note that
reduction can occur in various places (corresponding to all the possible positions
where ' occurs as a substring of w). It is well-known (see, e.g., [24]) that such
an operation can be simulated by a finite transducer, say TR , associated with
R, so that: w reduces to w 0 if and only if the pair hw; w 0 i is accepted by TR .
For example, the transducer TM1 associated with rule #X10Y #X01Y #
is represented in figure 1. A similar simulation is possible for top and bottom
rules.
Fig. 1. Transducer TM 1
for rule M1 : #X10Y #X01Y #
2.3 Self-stabilization.
We are now able to give a formal definition of self-stabilization for a system
modeled as a string rewrite system S. From now on, configurations are regarded
as ground words. Writing LN for the set of legitimate configurations in a system
with N machines, we define the global set of legitimitate configurations, as
N2 LN .
Definition 1. A rewrite system S is self-stabilizing with respect to set L iff
Each ground word is reducible via S.
(1) L is closed via S, i.e: w
words w; w 0 .
(2) There is no ground cyclic derivation of the form w
with
Statement (0) expresses a no-deadlock property, (1) a closure property for L, and
(2) a no-cycle property. It easily follows from this definition that any "maximal"
derivation is infinite and reaches the set L: this corresponds to a convergence
property (also called no-livelock property in [6]).
Note that assuming (1), an equivalent version for (2) is:
There is no infinite ground derivation \Delta via S, such that
3 A first-order characterization of cycles
Assuming now that S satisfies (0) and (1), we will focus on the problem of proving
the no-cycle property, stated under form (2 0 ). Our method relies on a first-order
characterization of cycles: we will show that an infinite ground derivation via S
(as mentioned in (2 0 )) is actually an instance of an infinite derivation at the "first-
level. In order to state our main result, we need the notion of reduction
chains, which is transposed from [8] in our particular context.
3.1 Minimal reductions and chains.
We now deal with one-variable words t of the form #uW v#, with u; v 2 \Sigma
and W 2 V. The notion of ground reduction defined in section 2.2, extends
trivially to such one-variable words: it suffices to consider W as a new constant
(i.e., to extend \Sigma with fWg). We say in this case that reduction is done using
substitution Given a first-order word t and a rewrite rule R, it is
also possible to consider nontrivial instantiations of W (oe 6= id), that make t
reducible. This problem is a particular case of the unification problem: finding
common instances of t and . The general unification problem for words is
complex, and was solved by Makanin [28]. However our particular unification
problem here is simple, because t and  do not share variables, and are "lin-
(i.e. contain at most one occurrence of the same variable). In such a case
there exists a complete set of minimal unifiers that is finite: roughly speaking,
it suffices to consider all the manners in which t and  overlap depending on the
possible instantiations of their variables (see, e.g., [21]). Assume given a minimal
complete set of unifiers  k), each instance t i of
t reduces to r i However, we disregard unifiers  j which instantiate
t at a "variable position" (replacing variable W of t with a subword of the form
which will turn out to be unnecessary in our context
(see remark, section 3.2). Such an operation of minimal reduction (at nonvari-
able position) is an adaptation of the operation of "narrowing" [30,13,20] in our
context (one-variable words rather than 1st-order terms).
Example.
Consider the rule #X11Y #X22Y #. The word t : #1W1# unifies with
lefthand side #X11Y # via most general unifiers:
1g.
The last unifier  4 (with the associated reduction) is discarded because it corresponds
to a unification taking place at a variable position of t. The minimal
reductions of t corresponding to  1 are: #11W 0 1#22W 0 1#,
Let us now define in a formal and constructive manner the operation of
minimal reduction (at nonvariable position). We distinguish two basic cases, depending
on wether the involved substitution is identity not. Suppose
that we are given a middle rule R : #X'Y #XrY # where ' is of the form
an (with a i 2 \Sigma ). The substitutions oe 6= id involved in minimal reductions
via R form the set
- AR is the set of substitutions ff
- BR is the set of substitutions
- CR is the set of (ground) substitutions
(with the convention that fl i;j is fW="g if
A similar set of substitutions DR can be defined for a top or bottom rule R.
Definition 2. A word t is minimally reducible to u via rule R : using
substitution oe 2 DR [ fidg (written: toe !R u, or more simply toe ! u) iff:
is an instance of , and u is the corresponding instance of ae.
ffl For a middle rule R : #X'Y #XrY # with an , and a word
begins with string a an (for some 1  i
is obtained from t by replacing Wa an with W 0 r.
ends with string a 1 and u is
obtained from t by replacing a 1
begins with a j+1 \Delta \Delta \Delta an and t 1 ends with a 1
and u is obtained from t by replacing
an with r.
ffl For a top or bottom rule R, minimal reduction of t (using oe 6= id), is defined
similarly to the case of a middle rule.
Example.
For rule there is a
single substitution ff 1 : fW=W 0 1g that yields minimal reduction. This gives
For there are two
possible instantiations which yields the
following minimal reductions: #W 0 10003#W 0 11003# and #W 0 1003# !
As seen in section 2.2, the reduction of a ground word t via a rule R can
be performed by applying a transducer to t. When t is a 1st-order word of
the form #t 1 W t 2 #, minimal reduction for can be simulated in the
same manner, by considering W as "frozen" (i.e., extending \Sigma withfWg). We
R;id the associated transducer. Similarly, for oe 2 DR , we can define a
transducer, say T R;oe , which performs minimal reduction via R using oe. For
example in the case of a substitution oe of the form ff g, the
transducer searches a string of the form Wa an within the word given as
an input and if such a strings exists, replaces it with W 0 r. This is illustrated in
figure 2 for rule
(The transducer TM1 ;ff 1
searches for string Wa 2 , and replaces it with W 0 r, with
Therefore, for any rule R and any
substitution oe 2 DR [fidg, it is always possible to define a transducer T R;oe such
accepted by T R;oe . Such a definition via transducers will
subsequently allow us to extend minimal reduction from words to "schemes", in
a straightforward manner (see section 4).
Fig. 2. Transducer TM 1 ;ff 1
We can now define the notion of "minimal reduction chains". They are direct
transpositions of definitions or properties of [8] in our particular context.
Definition 3. The minimal top reduction chains of a rewrite system S form a
set of derivations inductively defined as follows:
Every top rule of S is a minimal top reduction chain.
is a top minimal reduction chain and R is a rule of S
such that t n oe ! u via R, then t reduction
chain, called a successor of C via R using oe.
The transitive closure of the successor relation is called "iterated successor".
Henceforth, we will simply say "top chain" instead of "top minimal reduction
chain".
Example. Consider the rule viewed as a chain. Its
successor via using fW=2W 0 g is
In the definition above, we require that chains start with a top rule, instead
of an arbitrary rule of S. This requirement is new with respect to Dershowitz's
definition [8] (where chains can start with arbitrary rules). The advantage of
focusing on top chains, is to restrict the number of possible chains that will
have to be considered for determining self-stabilization (see Theorem 5). This
restriction will not endanger the correctness of our characterization, because we
further assume that system S \Gamma Top S is terminating (see section 3.2).
Recall that in all rules  ! ae of the string rewrite systems considered here,
the substring ' of  is replaced by substring r of ae, which has the same length.
Therefore, a chain is such that either all the words
are ground and of the same length, or each t i is of the form #u
where the u i s and v i s are strings of \Sigma   of same length. For the same reason
of length preservation, there must exist 1
any infinite top chain (ground or not). This explains the use of the following
definition.
Definition 4. A top chain (resp. ground derivation)
quasi-cyclic if t
3.2 A characterization of self-stabilization.
We can now state our main result:
Theorem 5. Let be a rewrite system and let
L be a set of configurations. If
(0) each ground word is reducible via S,
(1) L is closed via S, and
Then S is self-stabilizing w.r.t. L iff there is no quasi-cyclic top chain
via S, such that t 0
2 L for some ground instance t 0
n of t n .
This result is an adaptation of Dershowitz's theorem ([8], p. 454) characterizing
nonterminating string rewrite systems as those having at least one cycling
chain (or infinitely many noncycling infinite chains, which cannot happen in
our case). The proof of theorem 5 relies on properties involving the notions of
"active" or "inactive" steps within infinite ground derivations, as introduced by
Dershowitz [8].
Definition 6. The active area of a ground word w i in a ground derivation
wn is the part of w i that has been created by the nonvariable
portions of the righthand sides of the rules that have been applied. Only the top
letter (i.e., the rightmost letter) of the initial word w 1 is considered active.
More precisely, suppose that a rule of the form #X' 1 Y #Xr 1 Y # (resp.
#) is applied to a ground word w of the form #u
#) to obtain a ground word w 0 of the form #u 1 r 1
#). Then, in w 0 , all the letters of r 1 (resp. r 1 and r 2 ) are active if at
least one letter of ' 1 (resp. ' 1 or ' 2 ) was active; besides, all the letters of u
that were already active in w remain active in w 0 . We say that a ground word is
active if its top letter is.
Definition 7. An active ground derivation via S (resp. inactive ground derivation
via S) is a ground derivation w wn in which rules of S are
applied only in the active area (resp. inactive area) of words.
We denote by act
\Gamma\Gamma! (resp. inact
\Gamma\Gamma\Gamma!) an application of a rule at an active area (resp.
inactive area) of a ground word.
In the derivations, we start with a single active top letter and the successive
reductions will increase the active part in the words. Active letters will be put
in bold.
Example. Starting from the ground word #2012# and applying successively
top rule at
active area, we obtain the following active ground derivation act
\Gamma\Gamma!
act
\Gamma\Gamma! #1022#.
The following property is the counterpart of the relation between reduction
sequences and narrowing sequences in first-order term theory [20]. The proof is
analogous, therefore omitted.
Lemma 8 (lifting lemma). For all active ground derivation
act
act
\Gamma\Gamma! wn via S, there exists a top chain
which has \Delta as an instance (i.e. such that w
some ground substitution ').
Remark.
The lemma states that any ground derivation is an instance of some 1st-order
top chain. Such a chain is obtained by using a sequence of minimal instantiations
is of the form fW=uW 0 g, fW=W 0 ug or fW=ug.
This 1st-order covering holds in spite of the fact that instantiations oe of the
are discarded by definition. This justifies a posteriori
our focus on minimal reductions at nonvariable positions.
Example. The active ground derivation (see above)
act
\Gamma\Gamma! T4 #2021# act
\Gamma\Gamma! B1 #1022#
is an instance (via the ground substitution fW 0 =0g) of the top chain
We will use the following property (as did Dershowitz in a more general
context [8]):
Lemma 9 (semi-commutation lemma). Let w words such
that w 1
act
inact
\Gamma\Gamma\Gamma! w 3 . Then there exists a ground word w 0
2 such that
inact
\Gamma\Gamma\Gamma! w 0act
\Gamma\Gamma! w 3 .
Example. Starting from the word #1012#, consider the following derivation
via T 4 then act
\Gamma\Gamma! T4 #1021# inact
\Gamma\Gamma\Gamma! M1 #0121#. The order of rule
application can be permuted to get: #1012# inact
\Gamma\Gamma\Gamma! M1 #0112# act
\Gamma\Gamma! T4 #0121#.
Therefore inactive steps can always be switched with active steps, and pushed
upwards. It remains to show that the number of inactive steps in infinite ground
derivations is necessarily finite.
Proposition 10. Let S be a rewrite sytem such that S \Gamma Top S is terminating.
Then any infinite ground derivation via S has only a finite number of inactive
steps.
Proof. Consider an infinite ground derivation
S. Applying a rule at an active area of a ground word cannot create any new
inactive letters, while applying a rule at an inactive area only replaces a certain
portion of inactive area by another inactive portion of the same length. Therefore
either (a) all the inactive subareas of \Delta disappear after a finite number of steps,
or (b) at least one of them remains, but between two fixed positions. In case
(b), there is a subpart \Delta 0 of \Delta of the form w
every wn is of the form xn vn yn , all the xn 's (resp. vn 's, wn 's) have the same
length, and the vn 's always remain inactive. Since the active application of rules
over subparts of xn or y n do not involve the inactive portion v n , one can extract
from \Delta 0 an infinite inactive ground derivation \Delta 00 affecting only the vn 's. This
infinite derivation \Delta 00 never makes use of a top rule since the top letter is active.
This is in contradiction with assumption that S \Gamma Top S is terminating. The only
possible case is therefore (a): all the inactive subareas disappear after a finite
number of steps.
Finally, all inactive steps from an infinite ground derivation can be pushed
upwards, thus yielding a purely active suffix, which is an instance of a top chain.
Proposition 11. Suppose that S \Gamma Top S is terminating, and L is closed via S.
Then there is an infinite ground derivation via S containing no word in L if and
only if there is a quasi-cyclic top chain via S, starting from a word t such that
t' 62 L for some ground substitution '.
Proof. The if part is obvious. To prove the only-if part, consider an infinite
ground derivation \Delta not in L. By property 10 (since
ing), this infinite derivation contains only a finite number of inactive steps. Applying
iteratively the semi-commutation lemma (9), one can push back these
inactive steps to the beginning of the derivation, thus obtaining a reordered infinite
ground derivation \Delta 0 . From some point on, there are only active steps in
derivation active infinite ground
part of derivation not in L. Since the rules are length-preserving, there is an
initial part of \Delta 00 of the form w wn such that w wn
and w p 6= w q for all n. By the lifting lemma (8), there is a chain
In particular t are either both ground or of
the form #u j Wv j # and #unWvn# with ju
follows from t j are distinct since
their instances w p , w q via ' are distinct. Therefore t
a quasi-cyclic chain, ending at t n with t n wn 62 L.
Remark.
In order to mechanically check point (3) of theorem 5, i.e. termination of S \Gamma
Top S , one can use classical well-founded orderings used in rewriting theory [10].
One can also use Dershowitz's chain test: generate all the general chains until either
one "cycles" in the sense of [8] (non-termination detection) or all terminate
(termination proof). Dershowitz's procedure can also be refined if one knows
that in order to prove termination
of suffices to generate only the "bottom" chains via
i.e. chains that start from a bottom rule, and check that none of them has a
cycle. (Of course, in this case, one has to check additionally the termination of
but this is generally easier.)
theorem 5 directly results from proposition 11 and the definition of
self-stabilization.
3.3 Chain generation
Theorem 5 suggests to prove self-stabilization by the following procedure:
- Generate all top chains
- If the only infinite chains generated are of the form t
t i with all instances of t n in L, then S is self-stabilizing. Otherwise, S is not
self-stabilizing.
In order to prove self-stabilization, it is then (necessary and) sufficient to
generate only 1st-order sequences that extend top rules,
instead of blindly generating all the possible ground derivations, starting from
arbitrary ground words. The generation procedure is limited because the procedure
is first-order and manipulates one-variable words of the form #uWv#,
instead of all the (infinite) sets of their ground instances. It is also limited by
the fact that sequences always start with the left-hand side of a top rule.
3.4 An optimization of the procedure.
Our basic theorem, and the associated generation procedure, can be refined by
exploiting a measure, say ', over words which ``never increases'' when applying
a rule, i.e., such that:
This is a relaxed assumption, with respect to norms that, as required in traditional
self-stabilization proof methods, must "always decrease" (i.e., roughly
speaking, norms / such that w
In addition with such a non-increasing measure ', we assume given a rewrite
system S 0 such
Now in any infinite derivation via S, all the rewrite steps, after a finite number
of them, are necessarily '-preserving (because of the non-increasing property),
and may be viewed as rewrite steps via S 0 . In order to prove self-stabilization
of S, it becomes necessary and sufficient to show the absence of quasi-cyclic top
chains (except those ending with an instance of L) via S 0 , instead of S. More
precisely, in theorem 5, we may replace:
"S is self-stabilizing w.r.t. L iff there is no quasi-cyclic top chain via S ",
"S is self-stabilizing w.r.t. L iff there is no quasi-cyclic top chain via S 0 ".
Henceforth, when given a measure ' and an associated system S 0 , we implicitly
focus on the generation of top chains via S 0 .
Example.
Consider the middle rules of Ghosh's algorithm (see Section 5 for details):
and '+' is addition modulo 4.
The convergence proof uses a norm function (Br; Ds) such that either Br or
Ds strictly decreases at each step, but individually Br and Ds are only non-increasing
functions. While Ds is a very subtle function, Br is simply the number
of breaks, i.e. the number of neighbouring states q, q 0 of the string which
differ by at least one unit. In contrast, our method proves the convergence, with
the help of measure Br only: we will focus on Br-preserving infinite derivations,
i.e. infinite derivations which preserve the number of breaks. Since Br is non-increasing
and bounded, any infinite derivation has an infinite Br-preserving
suffix, so there is no loss of generality.
To obtain the system S 0 , we modify the rules above into Br-preserving rules as
follows:
Remark.
It is sometimes convenient to use a measure ' that is ``never decreasing'', instead
of never increasing. The enhanced theorem still holds, because, again, in
any infinite derivation via S, all the steps, after a finite number of them, must
be '-preserving (provided that ' is bounded upward, e.g., by the number N
of machines the ring is made of). Such a reasoning is used by Burns and Pachl
(see [6], p. 339), who focus on infinite derivations preserving the number of "dy-
namic segments" of configurations. We use ourselves a non-decreasing measure
' in section 5.3.
The '-refinement will allow us to restrict even more the number of generated
chains. However, in practice, in spite of focusing on top chains and using a '-
preserving system S 0 , the generation procedure does not terminate and produces
an infinite number of word sequences. To solve this problem, we introduce in
section 4 a notion of chains over regular sets of words (instead of simply words)
and apply a notion of "generalization".
Compositionality
It is interesting to relate compositionality results obtained in the context of
self-stabilizing systems with those obtained in the context of rewrite systems.
Similarly to what Dershowitz proved w.r.t. composition of terminating systems
(see theorem in [8], p.456), one can derive from theorem 5 sufficient conditions
for self-stabilization of the combination of two self-stabilizing systems.
Theorem 12. Assume that:
self-stabilizing w.r.t. L 1 .
self-stabilizing w.r.t. L 2 when starting from L 1 . 2
- there is no overlap between lefthand sides of S 1 and righthand sides of S 2 .
all executions are fair w.r.t. both S 1 and S 2 . 3
self-stabilizing w.r.t. L 2 .
This can be seen as a version of Herman's compositionality result [17] in our
context.
4 A sufficient condition for self-stabilization
As mentioned earlier, top chains, when generated in a brute manner, are frequently
in infinite number. However it is often possible to discover some recurrent
forms for words t n appearing at the end of chains. Consider again the subset
of rules S 4 g from Beauquier-Debas system:
"when starting from L1 " means that condition (0) is replaced with "(0 0 ) Each ground
word of L1 is reducible via S2 " in definition 1 of self-stabilization for S2 w.r.t. L2 .
3 See, e.g., [31], p. 476, for a formal definition of "fairness".
Starting from T 4 , and applying iteratively rule M 4 , one generates chains of the
These chains are in infinite number, but all of them (except the first one) end
with words of the form #W20 j 1# with j ? 0. It is then convenient to generalize
words of the form #W20 j 1# by the regular set #W20 + 1#, and replace first-order
derivations over words by first-order derivations over regular sets. Such
regular sets are called "schemes" in the following. Derivations over schemes are
then defined in such a manner that they "cover" all the possible top chains
over words (overapproximation). These generalized derivations may be represented
under the compact form of paths along the nodes of a symbolic graph,
each node corresponding to a scheme. Absence of infinite derivations (i.e., self-
stabilization) is then shown by checking that every path of the graph uses only
a bounded number of top rules. (This exploits the assumption of termination
section 4.3.) We claim that such a process of generalization
improves the convergence of the method of top chain generation.
Remark.
This idea of integrating a generalization process (or overapproximation) is similar
to the idea of using "widening" in the context of Abstract Interpretation in order
to accelerate the convergence of fixed-point computations over abstract domains
(see [7]). The idea of reasoning with derivations over regular languages is used
by Hoepman [18] in the context of self-stabilizing systems. Note however that
Hoepman, in contrast with us, only reason at the ground level, and does not
exploit the notion of first-order variables.
4.1 Replacing words by schemes
We are now going to define the notion of "schemes", an appropriate form of
regular languages that contain sets of words considered before. We extend accordingly
our notion of reduction chains by manipulating schemes instead of
words.
Definition 13. A first-order scheme S is a language of the form #LWM#
are (nonempty) regular languages over \Sigma   , and W a first-order
variable. A ground scheme S is a language of the form #L# where L is a regular
language over \Sigma   . A scheme is either a 1st-order or a ground scheme.
In the following we assume that the set of legitimate configurations L is expressed
as a ground scheme.
Note that any first-order word of the form #uWv# (with strings u; v) can
be seen as a special first-order scheme with fvg. Likewise any
ground word is a special ground scheme.
4.2 Minimal reductions of schemes and generalization
As shown earlier, it is possible to define minimal reduction over words using the
notion of transducers (soe !R t iff hs; ti is accepted by T R;oe ). This allows us to
define minimal reduction over schemes in a straightforward manner.
Definition 14. Let S be a scheme, R a rule, oe a substitution of DR [ fidg and
T R;oe the transducer associated with R and oe. Then the reduced form of S via
R using oe is the scheme S 0 defined by:
such that hs; s 0 i is accepted by T R;oe g.
This is written Soe !R S 0 .
Note that if A is a finite automaton accepting S, then S 0 is the output of T R;oe
with input filtered by A. It follows immediately from the definition that the
output S 0 associated with S is itself a scheme.
Example. For rule #, the scheme
minimally reduces to S 0g. The reduction
is written
Generalization over 1st-order schemes is an overapproximation of the regular
languages surrounding the 1st-order variable of a scheme. More precisely,
a 1st-order scheme is a generalization of a 1st-order scheme
. Note that the names of variables
appearing in T and S (viz., W and W 0 ) do not matter. Henceforth, without
loss of generality, we always rename first-order variables W 0 appearing
in schemes, to W . In particular a substitution of the form fW=W 0 ug is simply
fW=Wug. With this convention, a generalization T of 1st-order scheme
S is just a 1st-order scheme that contains S, i.e., such
we say that a ground scheme T is a generalization of a ground scheme S iff S ' T .
In the following, we interleave the generalization process with minimal re-
duction. Given a rule R, and a substitution oe 2 DR [fidg, we say that a scheme
T is a generalized successor of scheme S, and write Soe %R T (or more simply
Example. For rule
We can thus
write Soe % S. So S is its own generalized successor via R using oe.
We now express formally the correspondence between relation % at the
scheme level and ! at the word level. We have:
Lemma 15. Given a rule R and a substitution oe 2 DR [fidg, we have, for any
scheme S and any word s 2 S:
soe !R t implies Soe %R T for some scheme T such that t 2 T .
We now give formally the notion of "generalized top chain".
Definition 16. The generalized minimal top chains of a rewrite system S form
a set inductively defined as follows:
Every top rule t g.
is a generalized minimal top chain and R is a rule of
S such that is a generalized
minimal top chain called generalized successor of G (via R using oe).
Lemma 15 generalizes as follows:
Lemma 17. Given a top chain over words,
via rules R of S, using substitutions oe
that there is a top chain over schemes,
using the same substitutions, such that t
This lemma states that any top chain at the word level is "covered" by a
corresponding top chain at the scheme level. Hereafter, we describe a procedure
of chain generation at the scheme level. This procedure has a top rule t
as input and \Gamma denotes the set of chains for which the successors remain to be
computed.
Generalized chain
g.
While
do
1. Select
2. Compute the finite set of generalized successors, say fS
new
(Soe
new for some rule R 2 S and some oe 2 DR [ fidg).
3. For all i, add S i
new to \Gamma unless S i
new ' S old for some S old in \Gamma .
od
Note that test S i
new ' S old is decidable since it deals with inclusion of regular
languages. An optimization of the above procedure (that will be implicit
consists in computing successors of S only if S is not a subset of L.
This is justified, since we are only interested in detecting the existence of infinite
chains that do not intersect with L (cf: criterion (2 0 ), Section 2.3).
Example. As already seen above for Beauquier-Debas system, the righthand
side #W21# of top rule T 4 minimally reduces via M 4 to scheme S
which is its own generalized successor via M 4 using fW=W0g.
On the other hand, scheme minimally reducible via B 1 (using
fW=2Wg) to Scheme U is itself minimally reducible via M 1
(using fW=0Wg) in an iterative way, which yields #01W20
Scheme U can be thus generalized as
A generalized successor of S 1 via B 1 (using fW=2Wg) is thus S 2 . The latter
scheme is minimally reducible via M 4 (resp. M 1 ), but this yields only the subset
2#) of S 2 . Therefore S 2 is its own generalized
successor via M 4 (using fW=W0g) and via M 1 (using fW=0Wg).
4.3 Graph construction
It is convenient to represent a minimal reduction of the form S 1 oe 1
the form of an edge, labelled (R 1 ; oe 1 ), from S 1 to S 2 . Likewise, a chain of the
represented as an edge (labelled (R
from S 1 to S 2 , followed by an edge (labelled (R 2 ; oe 2 )) from S 2 to S 3 (see the
graph on the left in figure 3).
If additionally, schemes are represented as labels of nodes and structure sharing
is used in order to merge the representation of nodes associated with identical
schemes, then the generation of scheme successors corresponds to the construction
of a graph, where paths between nodes represent chains over schemes. For
example, the graph on the right in figure 3 corresponds to the minimal reduction
Soe %R S and represents under a compact form an infinite number of chains
Fig. 3. Graphs for reductions
The process of graph construction, described below, takes a top rule t
as an input and builds iteratively generalized successors under the form of growing
paths. Each node N of the graph is labelled with a scheme S, and referred
to as pair (N; S). Each generalized top chain using substitutions oe
the form (U represented as a path of the graph
of the form h(N 1 labels the edge from N i to
Formally, the procedure is as follows:
Graph construction
While Q 6= f;g
do
1. Select (N; S) 2 Q
2. Compute the finite set of successors, say fS
new
(Soe
new for some rule R 2 S and some oe 2 DR [ fidg).
3. For all i:
3a. If S i
new ' S old for some node (N old ; S old add an edge, labelled with
(R; oe), from (N; S) to (N old ; S old ).
3b. Otherwise, add node (N i
new
new ) to Q, and edge, labelled (R; oe), from
(N; S) to (N i
new
new ).
4. Q
od
According to the optimization mentioned previously, successors of S, at step
2, are implicitly computed only if S is not a subset of L. Therefore in the graph,
no edge exits from nodes labelled with (subsets of) L. Another obvious optimization
consists in skipping step 3a in case an edge, labelled oe, already exists
from (N; S) to (N old ; S old ).
Example. Figure 4 shows the complete graph corresponding to generalized chain
generation for Beauquier-Debas system S 0 , with T 4 as an input.
From the construction of the graph, we have:
Proposition 18. Suppose that during the scheme chain generation, there is a
generated chain from U to Un via R using oe
there is a path from (N 1 ; ft 1 g) to
a node of the form (N; Un ) via edges labeled (R
This gives a sufficient condition for self-stabilization:
Theorem 19. If, for each top rule t as an input, there is no path in
the associated graph, that uses Top S infinitely often (apart from paths passing
by L), then S is self-stabilizing.
Proof. Suppose there is no path using Top S infinitely often (except paths passing
by L). Then, by proposition 18, there is no chain over schemes using Top S
infinitely often (except chains reaching L). Now, by lemma 17, there is no chain
over words using TopS infinitely often (except chains reaching L). Finally, using
the fact that S \Gamma TopS terminates, there is no infinite chain over words (except
those reaching L), hence no quasi-cyclic chain t
Therefore, S is self-stabilizing.
In contrast with theorem 5, the condition above is no longer necessary, and
we cannot deduce non self-stabilization in case an infinite chain is produced.
On the other hand, we claim that the procedure terminates more often than its
counterpart over words, thus allowing to prove self-stabilization in more cases.
This is illustrated by examples in the next section.
Fig. 4. The graph construction for T4
5 Examples
5.1 Beauquier-Debas algorithm
This system originates from [4], and is an adaptation of Dijkstra's third (3-state)
algorithm [11]. In our formalism, it corresponds to the following system S:
Top
Middle
L is defined as: #0   20   1#0   10   2# .
In this example, it is assumed that the sum of the elements of the initial configuration
is null, modulo 3. This property is preserved when applying the rules
of S. It is easy to check that any ground word (with a null sum of elements)
is reducible via S, and that L is closed via S (see [4]). Therefore, S is self-stabilizing
iff there is no ground cyclic derivation via S containing an element
As remarked in [4], one can see that T are applied at most once.
As a consequence S is self-stabilizing iff there is no ground cyclic derivation via
containing an element w 62 L. The measure ' over a word
defined as the number of nonnull elements contained by t. Ob-
viously, ' is non-increasing with S 0 and compatible with substitution. Besides,
among rules of S 0 only rules preserve the number of nonnull ele-
ments. The '-refinement of the basic procedure thus consists in generating top
chains via S instead of S 0 .
The graph constructed in figure 4 gives a complete picture of the situation
illustrated in the previous examples. Since there is no infinite path using Top
(T 4 is used at most once), it follows that there is no quasi-cyclic top chain
n of t n . Self-stabilization
is thus proved for Beauquier-Debas's variant of Dijkstra's 3-state
algorithm.
5.2 Ghosh's 4-state algorithm
Self-stabilization of Ghosh's algorithm [14], a variant of Dijkstra's 4-state al-
gorithm, can be proved formally along the same lines. The system consists of
a parametric number N of machines (0; which have four states:
except the top machine machine 0) which has
only two states: f0; 2g (resp. f1; 3g). As explained in Section 2, the configuration
of the system is the string of all machine states, delimited by special end
symbols '#'. Writing X;Y for string variables, the transitions correspond to the
following system of rewrite rules.
Middle
and '+' is addition modulo 4.
Top
Bottom
L is defined as #f1; 3g
As mentioned in section 3.4, Ghosh proves the convergence by considering a
norm function (Br; Ds) such that either Br or Ds strictly decreases at each
step. Recall that Br and Ds are non-increasing functions: Br is the number
of breaks, i.e. the number of neighbouring states q, q 0 of the string which differ
by at least one unit and Ds measures the sum of distances between pairs of
neighbouring breaks of the string. All the difficulty of Ghosh's proof comes from
the discovery of such a measure Ds, while our method uses measure Br only
and focus on Br-preserving infinite derivations. For instance, the two following
reductions (with underlines indicating positions of a substring to be reduced)
are discarded because they decrease Br by one:
We thus consider the system S 0 where the middle rules are replaced by:
The graph construction is illustrated in figure 5 in the case of initial rule
#W32#W30#. Similarly, another representative graph can be obtained,
starting from the other top chain T 2 , with righthand side #W12#. To make the
figure more readable, some details have been omitted:
substitutions oe 0 and oe 0
are respectively fW=W0g and fW=W03g,
- the edges labelled by M 1 without a substitution correspond to
most schemes appearing in the figure are closed by (generalized) application
of the rule M 1 with should have a loop which is not represented.
The important point is that, in both graphs, all the pathes make use of the
top rule a finite number of times (at most once). It follows by theorem 19 that
the system is self-stabilizing.
or oe 0
or oe 0
or oe 0
M1 oe 0 or oe 0M1 oe 1 or oe 0M1 oe 2 or oe 0M1 oe 3 or oe 0100
Fig. 5. First-order generation of chain for
5.3 Hoepman's ring orientation algorithm
We finally sketch out how our method adapts to uniform algorithms (algorithms
without distinguished top, bottom or middle rules). We take as an example the
self-stabilizing ring orientation algorithm presented by Hoepman in [18]. In this
context, our underlying assumptions about the existence of distinguished top
rules Top and the termination of S \Gamma Top, do not hold any longer. Instead, an
assumption of fairness (also used in [18]) is used in the convergence proof: any
infinite sequence of rules modifies infinitely often the state of every machine of
the ring.
Hoepman's algorithm is based on 16 rules applied to words over the alphabet
and uses the following notations:
and I
g.
The corresponding rewriting system S transforms a subword pqr in pq 0 r,
where q 0 is given by the following tables:
rule
a
rule
rule
rule
These rules can be applied at any position of the configuration. Formally,
every transformation of pqr into pq 0 r corresponds to 3 rules: #XpqrY # !
so that these
rules can be applied at any position of the configuration. Hoepman proves that
the system converges on L 2 in two steps: first, he exhibits a measure that strictly
decreases when applied to a ground configuration of L 0 , unless this ground configuration
belongs to the subset L 1 . Then, he exhibits another measure that
strictly decreases when applied to a ground configuration of L 1 , unless it belongs
to L 2 . (He also proves that the system converges from L 2 to a third set
3 , but this is beyond the scope of this presentation.) In contrast, our method
gives a direct proof for the convergence to L 2 , viewed here as set L of legitimate
configurations, and does not appeal to any strictly decreasing measure.
In a preliminary step, we transform Hoepman's system into a simpler set of
rules. We first use a '-refinement in order to disregard rules (a) and (c). Our
measure ' counts the number of maximal subsequences of same value (either
or 1), inside a word (assuming the leftmost and rightmost elements to be
contiguous). For example, the measure ' for #000100W1100# is 4. All the
rules preserve this number, except rules (a) and (c), which strictly increase it by
2. Therefore, (a) and (c) can only be used a finite number of times (' is bounded
upward with N ), and we can focus on infinite derivations via cg. The
remaining rules are themselves merged to form the simple new system S
given by the table below.
rule
Note that each transformation is now a shorthand for 4 rules. For example
transforms As before, every transformation
of pqr into p 0 q 0 r 0 corresponds to 3 rules: #XpqrY #Xp 0 q 0 r 0 Y #,
#, depending on the position
where it is applied. It is easy to see that any sequence via S \Gamma fa; cg can be
simulated by a sequence via S g.
In order to prove self-stabilization via S, it is thus necessary and sufficient
to prove that there is no infinite sequence of derivations via S 0 (apart from
sequences ending at L 2 ). We thus focus on chains starting from a rule E (or
F , F 0 ). Since the system is uniform, we can actually focus on chains starting
with rule E applied at an arbitrary position, e.g., the rightmost one. We thus
as a starting rule and we show that there is no
infinite derivation from E by first-order rewriting via S 0 (regardless of sequences
going to L 2 ). This is done in two steps: first we build the graph associated with
E, then we explain why there is no infinite path in this graph (except those
going to L 2 ).
This graph can be found in figure 6. Only the edges corresponding to non
trivial substitutions (oe 6= id) are represented. All nodes should have in addition
a self-loop labeled by id. For the sake of readability, the substitutions
labeling the edges of the figure are also omitted. For example, consider the upmost
node its three outgoing edges labeled
respectively
- The substitution corresponding to rule E is
which gives generalized as \Sigma
- The substitution for rule E 0 is
which gives generalized as \Sigma
- The substitution for rule F 0 is fW=W0g,
which gives
generalized as
F
F
F
F
F
F
Fig. 6. First-order graph generation for E
Also note that the two edges leading to L 2 (our set of legitimate configurations)
are implicitly labeled by fW="g.
Considering this graph, we see that there are three kinds of nodes. The first
one corresponds to a first order scheme LWM , the second one to the legitimate
scheme L 2 and the third one to ground schemes containing either 0+
This observation is summarized in figure 7.
oe 6= id
Fig. 7. A reduced form for the graph in figure 6
A simple analysis of the new synthetic graph leads us to conclude that no
infinite path exists (except those passing in L 2 ), for the following reasons:
- There is no infinite loop over the nodes which contain the patterns 0+
and no rule can rewrite the central letter which is in contradiction
with the fairness assumption.
- There is no infinite loop with a substitution oe 6= id because W represents a
finite word and then cannot be instanciated infinitely often.
- There is no infinite loop with label because otherwise, the string represented
by W could never be modified at its extremities which contradicts
fairness.
Similar constructions and explanations hold for rules This achieves our
proof of self-stabilization.
6 Conclusion and perspectives
In contrast with methods relying on the existence of a strictly decreasing norm
function [4,14,19,23], our method requires only little specific knowledge and proposes
a uniform framework for the full proof of several non trivial examples,
as shown here on Ghosh's 4-state algorithm [14] and Beauquier-Debas's 3-state
algorithm [4]. These examples are simple ones, which allow us to give a clear
view of the procedure.
Our procedure is inspired by Dershowitz's chain generation procedure [8],
and proves convergence of self-stabilizing algorithms much in the same way than
Dershowitz proves the termination of rewrite systems. Following Hoepman [18],
we enhanced the basic method by incorporating a generalization process from
words to regular languages, and defining rewriting over "schemes". The method
is not fully automatic: we need in particular to infer by hand generic schemes
of configurations from words produced recurrently throughout derivations. The
main differences with traditional proof methods of self-stabilization, which use
strictly decreasing measures over ground configurations, come from:
1. focusing on derivations originating from top-configurations instead of derivations
starting from arbitrary configurations.
2. reasoning with 1st-order variables, and deriving new configurations through
a restricted strategy of reduction (top chain generation) instead of considering
all the possible ground configurations, and all their possible ground
successors.
3. reasoning with regular languages (including 1st-order variables), and integrating
a generalization process.
We have also given a natural counterpart of Herman's compositionality result
in our framework. We believe that our method easily adapts to the case of
uniform rings, as sketched out for Hoepman's ring-orientation protocol. We are
currently investigating extensions of the method in two directions. We first want
to consider more realistic token ring algorithms, like different versions of the IBM
token ring or FDDI protocols, involving a change from the state reading model to
the message passing model. In this case, channel states must be modeled and the
hypotheses must be slightly modified to consider self-stabilization. The second
natural extension concerns algorithms running on arbitrary (non-ring) networks.
In this framework, strings must be replaced by graphs. We would then have to
use graph rewriting techniques, as proposed in [25-27] for other properties of
distributed systems.

Acknowledgement

We would like to thank Nachum Dershowitz for his encouragement and pointing
out reference [32].



--R

"A Self-Stabilizing Leader Election Algorithm for Tree Graphs"
"Memory efficient self stabilizing protocols for general networks"
"Composite routing protocols"
"An optimal self-stabilizing algorithm for mutual exclusion on uniform bidirectional rings"

"Uniform Self-Stabilizing Rings"
"Abstract interpretation: a unified lattice model for static analysis of programs"
"Termination of Linear Rewriting Systems"
"Topics in termination"
"Rewrite Systems"
"Self-stabilizing systems in spite of distributed control"
"A Belated Proof of Self-stabilization"
"First-order unification in an equational theory"
"An Alternative Solution to a Problem on Self-Stabilization"
"The triumph and tribulation of system stabilization"
"Adaptative programming"
Adaptativity through distributed convergence.
"Self-Stabilizing Ring-Orientation Using Constant Space"
"A self-stabilizing algorithm for maximal matching"
"Canonical Forms and Unification"
"Minimal and Complete Word Unification"
"Self-stabilizing extensions for message-passing systems"
"An Exercise in proving self-stabilization with a variant function"
"Symbolic Model-Checking with Rich Assertional Languages"
"Computing with Graph Rewriting Systems with Pri- orities"
"Different Local Controls for Graph Relabeling Systems"
"On the Recognition of Families of Graphs with Local Computations"
"The problem of solvability of equations in a free semigroup"
"Self-Stabilization"
"Automated Theorem-Proving for Theories with Simplifiers, Commu- tativity, and Associativity."
Introduction to Distributed Algorithms.
"An Exercise in Proving Convergence through Transfer Functions"
--TR
A belated proof of self-stabilization
An exercise in proving self-stabilization with a variant function
Uniform self-stabilizing rings
Minimal and complete word unification
Memory-efficient self stabilizing protocols for general networks
Rewrite systems
Adaptive Programming
String-rewriting systems
A self-stabilizing algorithm for maximal matching
Adaptivity through distributed convergence
Self-stabilization
An alternative solution to a problem on self-stabilization
Computing with graph rewriting systems with priorities
Introduction to distributed algorithms
On the recognition of families of graphs with local computations
A self-stabilizing leader election algorithm for tree graphs
Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
Self-stabilizing systems in spite of distributed control
Uniform Deterministic Self-Stabilizing Ring-Orientation on Odd-Length Rings
Termination of Linear Rewriting Systems (Preliminary Version)
Topics in Termination
Symbolic Model Checking with Rich ssertional Languages
Canonical Forms and Unification
The Triumph and Tribulation of System Stabilization
An exercise in proving convergence through transfer functions
self-stabilization;rewriting systems