Full text of DOI:10.1007/PL00008931

Distrib. Comput. (2001) 14: 83–95
c
ꢀ Springer-Verlag 2001
Proving convergence of self-stabilizing systems
using first-order rewriting and regular languages
J. Beauquier1, B. Be´rard2, L. Fribourg2, F. Magniette1
1
LRI, CNRS URA 410, Universite´ Paris-Sud 91405 Orsay cedex, France (e-mail: {jb,magniett}@lri.fr)
2
LSV, CNRS UMR 8643, ENS de Cachan, 61 av. du Pre´s. Wilson, 94235 Cachan cedex, France (e-mail: {berard,fribourg}@lsv.ens-cachan.fr)
Received: January 2000 / Accepted: November 2000
Summary. 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. 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 sev-
eralnontrivialexamples.
iff it has the no-cycle property: there is no cyclic sequence
of transitions which contains some configuration w ∈ L. This
property is often proved by exhibiting a norm function defined
over the set of configurations, 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,5]).
We propose here a new approach for proving the absence
of cycle. Configurations are viewed as words of a formal lan-
guage, transitions of S as rewrite rules, and the no-cycle prop-
erty 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 chains1, first
proposed by Dershowitz for proving string rewriting termi-
nation [8]. The method proposed here is new in that: 1) it
uses a generaltechnique of string-rewriting to dealwith 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, replac-
ing sequences of words with regular languages, is also incor-
porated in the method in order to improve its termination.
Key words: Self-stabilization – Rewriting systems
1 Introduction
Introduced by Dijkstra, with three mutual exclusion algo-
rithms on a ring of processes [11], the notion of self-stabiliza-
tion 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 con-
figuration 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 centraldemon, 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 con-
figuration in L, the system persistently remains in L. It is al so
frequent to assume that there is no-deadlock. With these two
hypotheses, it is easy to show that a system is self-stabilizing
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 stabi-
lizing system to the time to verify its stabilization is about one
to ten”. For simplifying proof process, general paradigms have
been proposed: various protocolcompositions making proofs
modular [3,16], attractor or staircase methods [15,29], auto-
matic 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 func-
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).
1
also called forward closures in [9].

84
J. Beauquier et al.
tion: [32] uses techniques borrowed from controltheory and
[1] induction techniques over the set of configurations.
Example. Consider the following rules from Beauquier-
Debas algorithm (see Sect.5):
B1 : #2X1# → #1X2# is a bottom-rule.
T4 : #X12# → #X21# is a top-rule.
M1 : #X10Y # → #X01Y # and
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 prov-
ing 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 con-
struction,...). However this work does not address the issue of
self-stabilization.
M4 : #X02Y # → #X20Y # are middle rules.
These rules are used throughout the next sections to illus-
trate the notions which are defined, as well as the method we
propose.
Note that, strictly speaking, rules M1 and M4 can be ap-
plied only if Y = ε. For example, M1 should correspond to
3 rules of the form #X10aY # → #X01aY # with a ∈
{0, 1, 2}. For the sake of conciseness, we neglect such a re-
strictive condition of application (except at Sect.5).
Plan of the paper. Section 2 explains how self-stabilization
can be viewed as a property of string rewriting systems. In
Sect.3, we give a basic procedure, inspired from Dershowitz,
that, when it terminates, allows to decide self-stabilization. In
order to make the procedure terminate more often, we incor-
porate a process of generalization into it (Sect.4). Section 5
shows application of the method on detailed examples and
Sect.6 concludes with final remarks and perspectives.
Ground reduction. A ground word w is reducible via a rule
of the form #Xꢀ1Y # → #Xr1Y # iff w = #uꢀ1v# for
some strings u, v ∈ Σ∗. One also says that w is an instance of
the rule lefthand side via the ground substitution {X/u, Y/v}.
The reduced form of w is wꢀ = #ur1v#. Reduction via a rule
of the form #ꢀ1Xꢀ2# → #r1Xr2# is defined in a similar
way.
2 Self-stabilizing systems as string rewrite systems
A ground word w reduces to wꢀ via S, written w →S wꢀ
(or sometimes simply w → wꢀ), if wꢀ 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.
We first recall some basic definitions from (string) rewrite
systems [10,6]. The words considered here are generally de-
limited by a leftmost and rightmost special symbol ‘#’. The
symbols appearing between them belong to a finite alphabet
Σ or a set V = {W, X, Y . . . } of variable symbols. A string
is an element of Σ∗, with ε for the empty string. A ground
word is an element of #Σ∗# and a (1st-order) word is an
element of #(Σ ∪ V)∗#. A substitution is a mapping θ from
V to (Σ ∪ V)∗ with θ(W) = 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 in-
stance of the word w.A substitution θ is represented by a finite
set of pairs of the form {W/θ(W)}W ∈Dom(θ). A substitution
θ is ground when θ(W) is in Σ∗, for all W ∈ Dom(θ).
Example. Consider B1 : #2X1# → #1X2#. The ground
word w = #2011# is an instance of the lefthand side, using
the substitution {X/01}.
Replacement with the righthand side yields the reduced form
wꢀ = #1012#.
Reduction of a ground word w using a middle rule R :
XꢀY → XrY merely consists in searching for a substring ꢀ
of w, 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).
2.1 String rewrite systems
2.2 Self-stabilization
The string rewrite systems S considered here contain length-
preserving rules, divided into three subsets: top rules in Top
S
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 ma-
are applied to the rightmost part of words; bottom rules in
Bottom are applied to the leftmost part of words (or simul-
S
taneously at both ends); the rest of rules in Middle are called
S
middle rules. More precisely, let ꢀ, r (resp. ꢀi, ri for i = 1, 2)
be nonempty strings of Σ∗ of the same length, and X, Y vari-
ables,
chines, we define the global set of legitimate configurations,
ꢀ
as L =
LN .
N≥2
Definition 1. A rewrite system S is self-stabilizing with re-
Middle is made of rules of the form:
S
spect to set L iff
#XꢀY # → #XrY #
(0) Each ground word is reducible via S.
(1) L is closed via S, i.e: w ∈ L ∧ w →S wꢀ ⇒ wꢀ ∈ L,
for all ground words w, wꢀ.
Top is made of rules of the form:
S
#Xꢀ# → #Xr#
Bottom is made of rules of the form:
S
(2) There is no ground cyclic derivation of the form w1 →S
#ꢀX# → #rX# or #ꢀ1Xꢀ2# → #r1Xr2#.
· · · →S wn = w1 with w1 ∈ L.
We are going to apply these rules either to ground words or to
1st-order words of the form #uWv# where u, v are strings
over Σ∗, and W is a variable.
Statement (0) expresses a no-deadlock property, (1) a closure
property for L, and (2) a no-cycle property. It easily follows

Rewrite systems for self-stabilization proofs
85
from this definition that any “maximal” derivation is infinite
and reaches the set L: this corresponds to a convergence prop-
erty (also called no-livelock property in [7]).
to µ1, µ2, µ3 are:
#11Wꢀ1# → #22Wꢀ1#,
Note that assuming (1), an equivalent version for (2) is:
#1Wꢀ11# → #1Wꢀ22# and
#11# → #22#.
(2ꢀ) There is no infinite ground derivation ∆ via S,
such that ∆ ∩ L = ∅.
Let us now define in a formaland constructive manner the
operation of minimalreduction (at nonvariable position). We
distinguish two basic cases, depending on wether the involved
substitution is identity (σ = id) or not. Suppose that we are
given a middle rule R : #XꢀY # → #XrY # where ꢀ is of
the form a1 · · · an (with ai ∈ Σ). The substitutions σ = id
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ꢀ). Our method relies on a first-order characterization of cy-
cles: we will show that an infinite ground derivation via S (as
mentioned in (2ꢀ)) is actually an instance of an infinite deriva-
tion at the “first-order” level. In order to state our main result,
we need the notion of reduction chains, which is transposed
from [8] in our particular context.
involved in minimal reductions via R form the set DR
AR ∪ BR ∪ CR, with:
=
• AR is the set of substitutions αi : {W/Wꢀa1 · · · ai} for
1 ≤ i ≤ n − 1,
• BR is the set of substitutions βi : {W/ai+1 · · · anWꢀ} for
1 ≤ i ≤ n − 1,
• CR is the set of (ground) substitutions
γi,j : {W/ai+1 · · · aj} for 1 ≤ i ≤ j ≤ n − 1 (with the
convention that γi,j is {W/ε} if i = j).
3.1 Minimal reductions and chains
A similar set of substitutions DR can be defined for a top or
bottom rule R.
We now dealwith one-variable words t of the form #uWv#,
with u, v ∈ Σ∗ and W ∈ V. The notion of ground re-
duction defined in Sect.2.1, extends trivially to such one-
variable words: it suffices to consider W as a new constant
(i.e., to extend Σ with {W}), and reduce the word using a
rule R : λ → ρ, as in Sect.2.1. We say in this case that reduc-
tion is done using substitution σ = id. Given a first-order word
t and a rewrite rule R, it is also possible to consider nontriv-
ialinstantiations of W (σ = id), that make t reducible. This
problem is a particular case of the unification problem: finding
common instances of t and λ. The generalunification problem
for words is complex, and was solved by Makanin [28]. How-
ever our particular unification problem here is simple, because
t and λ do not share variables, and are “linear” (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 µ1, ..., µk (tµi = λµi for i = 1, ..., k), each
instance tµi of t reduces to ꢀµi (tµi → ꢀµi). However, we
disregard unifiers µj which instantiate t at a “variable posi-
tion” (replacing variable W of t with a subword of the form
#uWꢀv# with u, v = ε), which will turn out to be unneces-
sary in our context (see remark, Sect.3.3). Such an operation
of minimalreduction (at nonvariabel position) is an adapta-
tion of the operation of “narrowing” [30,13,20] in our context
(one-variable words rather than 1st-order terms).
Definition 2. A word t is minimally reducible to u via rule
R : λ → ρ using substitution σ ∈ DR ∪ {id} (written:
tσ →R u, or more simply tσ → u) iff:
• σ = id, t is an instance of λ, and u is the corresponding
instance of ρ.
• For a middle rule R : #XꢀY # → #XrY # with ꢀ =
a1 · · · an, and a word t = #t1Wt2#:
- t2 begins with string ai+1 · · · an (for some 1 ≤ i ≤
n − 1), σ = αi, and u is obtained from t by replacing
Wai+1 · · · an with Wꢀr.
- t1 ends with string a1 · · · ai (for some 1 ≤ i ≤ n −
1), σ = βi, and u is obtained from t by replacing
a1 · · · aiW with rWꢀ.
- t2 begins with aj+1 · · · an and t1 ends with a1 · · · ai
(for some 1 ≤ i ≤ j ≤ n − 1), σ = γi,j, and u
is obtained from t by replacing a1 · · · aiWaj+1 · · · an
with r.
• For a top or bottom rule R, minimal reduction of t (using
σ = id), is defined similarly to the case of a middle rule.
Example. For rule M1 : #X10Y # → #X01Y # and word
t1 = #W02#, there is a single substitution α1 : {W/Wꢀ1}
that yields a minimal reduction.
This gives #Wꢀ102# → #Wꢀ012#.
For rule R : #X100Y # → #X110Y # and word
t2
= #W003#, there are two possible instantiations
Example. Consider the rule #X11Y # → #X22Y #. The
word t : #1W1# unifies with lefthand side #X11Y # via
most generalunifiers:
α1 : {W/Wꢀ10} and α2 : {W/Wꢀ1}, which yield respec-
tively the following minimal reductions: #Wꢀ10003# →
#Wꢀ11003# and #Wꢀ1003# → #Wꢀ1103#.
µ1 : {W/1Wꢀ} ∪ {X/ε, Y/Wꢀ1},
µ2 : {W/Wꢀ1} ∪ {X/1Wꢀ, Y/ε},
µ3 : {W/ε} ∪ {X/ε, Y/ε} and
We can now define the notion of “minimalreduction
chains”. They are direct transpositions of definitions or prop-
erties of [8] in our particular context.
µ4 : {W/W111W2} ∪ {X/1W1, Y/W21}.
The last unifier µ4 (with the associated reduction) is discarded
because it corresponds to a unification taking place at a vari-
able position of t. The minimalreductions of t corresponding
Definition 3. The minimaltop reduction chains of a rewrite
system S form a set of derivations inductively defined as fol-
lows:

86
J. Beauquier et al.
• Every top rule of S is a minimal top reduction chain.
Theorem 5. Let S = Middle ∪ Top ∪ Bottom be a
S
S
S
• If C : t0 → · · · → tn is a top minimal reduction chain
and R is a rule of S such that tnσ → u via R, then
t0σ → · · · tnσ → u is a top minimal reduction chain,
called a successor of C via R using σ.
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
(3) S − Top is terminating.
S
The transitive closure of the successor relation is called “iter-
ated successor”. Henceforth, we will simply say “top chain”
instead of “top minimalreduction chain”.
Then S is self-stabilizing w.r.t. L iff there is no quasi-cyclic
top chain t1 → · · · → tn via S, such that un ∈/ L for some
ground instance un of tn.
Example. Consider the rule T4
viewed as a chain. Its successor via
:
#W12# → #W21#
Example. Let us illustrate Theorem 5 on the system T of the
example above. First, it is easy to see that T and L satisfy
properties (0), (1) and (3). From the existence of quasi-cyclic
top chain t1 → · · · → t9 with t1 = t9 = #0101# ∈ L,
it now follows by Theorem 5 that T is not self-stabilizing
w.r.t. L.
B1 : #2X1# → #1X2# using {W/2Wꢀ} is:
C1 : #2Wꢀ12# → #2Wꢀ21# → #1Wꢀ22#.
Recall that in all rules λ → ρ of the string rewrite systems
considered here, the substring ꢀ of λ is replaced by substring
r of ρ, which has the same length. Therefore, a chain t1 →
t2 → ... → tn . . . is such that either all the words t1, ..., tn
are ground and of the same length, or each ti is of the form
#uiWvi# where the uis and vis are strings of Σ∗ of same
length. For the same reason of length preservation, there must
exist 1 ≤ i < j such that ti = tj, within any infinite top
chain (ground or not). This explains the use of the following
definition.
Theorem 5 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).
Remark. InTheorem 5, we require the termination property of
S −Top (condition (3)). This condition is new w.r.t. original
S
Dershowitz’s framework of [8]. Condition (3) allows us to re-
fine Dershowitz’s method and to focus on top chains (instead
of chains starting with arbitrary rules), so that the number of
chains generated is further restricted. In practice, condition (3)
is often satisfied when dealing with stabilizing systems hav-
ing infinite executions, that means solving dynamical prob-
lems (like token circulation, networks traversal, resource allo-
cation), because these systems, from their very specification,
have to be fair in the following sense (cf, e.g., [31]): any infi-
nite execution involves any process (and in particular the top
process) an infinite number of times. It is easy to see that a fair
system always satisfies (3). Details about how to mechanically
check (3), are given in [4].
Definition 4. A top chain (resp. ground derivation)
t1 → · · · → · · · → tn
is quasi-cyclic if ti = tn for some i < n, and tp = tq for all
distinct p, q less than n.
Example. Consider the alphabet Σ = {0, 1} and the follow-
ing system T :
Bottom C0 :
C1 :
#0X0# → #1X0#
#1X1# → #0X1#
#X01# → #X00#
#X10# → #X11#
3.3 Proof of Theorem 5
Top
U0 :
U1 :
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].
Middle N0 : #X01Y # → #X00Y # ( with Y = ε)
N1 : #X10Y # → #X11Y # ( with Y = ε)
Let L be: #0+1+# ∪ #1+0+# ∪ #11+# ∪ #00+#
and consider the top rule U0 : #W01# → #W00# viewed
asachain. ItssuccessorviaN1 using{W/Wꢀ1}is:#Wꢀ101#
→ #Wꢀ100# → #Wꢀ110#. The successor via N0 us-
ing {Wꢀ/Wꢀꢀ0} is then: #Wꢀꢀ0101# → #Wꢀꢀ0100# →
#Wꢀꢀ0110# → #Wꢀꢀ0010#. Now the successor via B0 us-
ing {Wꢀꢀ/ε} is: t1 = #0101# → t2 = #0100# → t3 =
#0110# → t4 = #0010# → t5 = #1010#. Note that this
last chain is ground. It is easy to see that it can be prolonged
by the following sequence of reductions: t5 = #1010# →
t6 = #1011# → t7 = #1001# → t8 = #1101# → t9 =
#0101#. A quasi-cyclic chain t1 → · · · → t9 = t1 has thus
been obtained.
Definition 6. The active area of a ground word wi in a ground
derivation w1 → w2 → · · · → wn is the part of wi that has
beencreatedbythenonvariableportionsoftherighthandsides
of the rules that have been applied. Only the top letter (i.e., the
rightmost letter) of the initial word w1 is considered active.
More precisely, suppose that a rule of the form:
#Xꢀ1Y # → #Xr1Y #
(resp. #ꢀ1Xꢀ2# → #r1Xr2#)
is applied to a ground word w of the form #u1ꢀ1u2# (resp.
#ꢀ1u1ꢀ2#)toobtainagroundwordwꢀ oftheform#u1r1u2#
(resp. #r1u1r2#). Then, in wꢀ, all the letters of r1 (resp. r1
and r2) are active if at least one letter of ꢀ1 (resp. ꢀ1 or ꢀ2)
was active; besides, all the letters of u1, u2 that were already
active in w remain active in wꢀ. We say that a ground word is
active if its top letter is.
3.2 A characterization of self-stabilization
We can now state our main result:

Rewrite systems for self-stabilization proofs
87
Definition 7. An active ground derivation via S (resp. inactive
ground derivation via S) is a ground derivation w1 → w2 →
· · · → wn in which rules of S are applied only in the active
area (resp. inactive area) of words.
Therefore inactive steps can always be switched with ac-
tive steps, and pushed upwards. It remains to show that the
number of inactive steps in infinite ground derivations is nec-
essarily finite.
act
inact
We denote by −−→ (resp. −−−→) an application of a rule at an
Proposition 10. Let S be a rewrite sytem such that S −Top
S
active area (resp. inactive area) of a ground word.
is terminating. Then any infinite ground derivation via S has
only a finite number of inactive steps.
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.
Proof. Consider an infinite ground derivation ∆ : w1
→
· · · → wn → · · · via S. Applying a rule at an active area of a
ground word cannot create any new inactive letters, while ap-
plying 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 ∆ disappear
after a finite number of steps, or (b) at least one of them re-
mains, but between two fixed positions. In case (b), there is a
subpart ∆ꢀ of ∆ of the form wi → · · · → wn → · · · , such that
every wn is of the form xnvnyn, 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 yn
do not involve the inactive portion vn, one can extract from
∆ꢀ an infinite inactive ground derivation ∆ꢀꢀ affecting only
the vn’s. This infinite derivation ∆ꢀꢀ never makes use of a top
rule since the top letter is active. This is in contradiction with
Example. Starting from the ground word #2012# and ap-
plying successively top rule T4 : #X12# → #X21# and
bottom rule B1 : #2X1# → #1X2# at active area, we ob-
tain the following active ground derivation:
act
act
∆ : #2012# −−→ #2021# −−→ #1022#.
Thefollowingpropertyisthecounterpartoftherelationbe-
tween reduction sequences and narrowing sequences in first-
order term theory [20]. The proof is analogous, therefore omit-
ted.
Lemma 8 (lifting lemma). For all active ground derivation
act
act
act
∆ : w1 −−→ w2 −−→ · · · −−→ wn via S, there exists a top
chain C : t1 → t2 → · · · → tn via S which has ∆ as an
instance (i.e. such that w1 = t1θ, w2 = t2θ, ..., wn = tnθ for
some ground substitution θ).
assumption that S − Top is terminating. The only possible
S
case is therefore (a): all the inactive subareas disappear after
a finite number of steps.
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 minimalinstantiations {σ1, · · · , σn},
where σi is of the form {W/uWꢀ}, {W/Wꢀu} or {W/u}.
This 1st-order covering holds in spite of the fact that instanti-
ations σ of the form {W/uWꢀv} with u, v = ε are discarded
by definition. This justifies a posteriori our focus on minimal
reductions at nonvariable positions.
Finally, allinactivestepsfromaninfinitegroundderivation
can be pushed upwards, thus yielding a purely active suffix,
which is an instance of a top chain. Formally:
Proposition 11. Suppose that S −Top is terminating and L
S
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θ ∈ L for
some ground substitution θ.
Example. The active ground derivation (see above)
Proof. The if part is obvious. To prove the only-if part, con-
sider an infinite ground derivation ∆ not in L. By property 10
act
act
∆ : #2012# −−→T #2021# −−→B #1022#
4
1
(since S − Top is terminating), this infinite derivation con-
S
is an instance (via the ground substitution {Wꢀ/0}) of the top
tains only a finite number of inactive steps. Applying itera-
tively 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 ∆ꢀ. From
some point on, there are only active steps in derivation ∆ꢀ.
chain
C1 : #2Wꢀ12# → #2Wꢀ21# → #1Wꢀ22#.
Let ∆ꢀꢀ
:
wi → wi+1 → · · · denote this active infinite
Finally we will use the following property (also used by
Dershowitz in a more generalcontext [8]):
ground part of derivation not in L. Since the rules are length-
preserving, there is an initialpart of ∆ꢀꢀ of the form wi →
· · · → wj → · · · → wn such that wj = wn and wp = wq
for all p < q < n. By the lifting lemma (8), there is a chain
C : ti → · · · → tj → · · · → tn with Cθ = ∆ꢀꢀ, for some
ground substitution θ. In particular tjθ = wj = wn = tnθ.
But tj and tn are either both ground or of the form #ujWvj#
and #unWvn# with |uj| = |un| and |vj| = |vn|. So tj = tn
follows from tjθ = tnθ. Besides, for all p < q < n, tp and
tq are distinct since their instances wp, wq via θ are distinct.
Therefore ti → · · · → tj → · · · → tn is a quasi-cyclic chain,
ending at tn with tnθ = wn ∈ L.
Lemma 9 (semi-commutation lemma). Let w1, w2, w3 be
act
inact
ground words such that w1 −−→ w2 −−−→ w3. Then there
inact
act
exists a ground word w2ꢀ such that w1 −−−→ w2ꢀ −−→ w3.
Example. Starting from the word #1012#, consider the fol-
lowing derivation via T4 then M1:
act
inact
#1012# −−→T #1021# −−−→M #0121#.
4
1
The order of rule application can be permuted to get:
Now, Theorem 5 directly results from Proposition 11 and
the definition of self-stabilization.
inact
act
#1012# −−−→M #0112# −−→T #0121#.
1
4

88
J. Beauquier et al.
3.4 Basic procedure and ϕ-refinement
breaks, i.e. the number of neighbouring states q, qꢀ 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ꢀ, we modify the rules above into Br-
preserving rules as follows:
Theorem5suggeststoproveself-stabilizationbythefollowing
basic procedure:
• Generate all top chains t1 → · · · → tn via S, until tn = ti
for some i < n.
• If the only infinite chains generated are of the form t1 →
· · · → ti → · · · tn = ti with all instances of tn 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 t1
· · · → ti → · · · tn that extend top rules, instead of blindly
generating all the possible ground derivations, starting from
arbitrary ground words. The generation procedure is restric-
tive because the procedure is first-order and manipulates one-
variable words of the form #uWv#, instead of all the (infi-
nite) sets of their ground instances. It is also restricted by the
fact that sequences always start with the left-hand side of a top
rule.
M1: #X(q + 1)qqY # → #X(q + 1)(q + 1)qY #
M2: #Xqq(q + 1)Y # → #Xq(q + 1)(q + 1)Y #
→
It is easy to show that Sꢀ is a Br-preserving version of S
(w →S wꢀ iff w →S wꢀ ∧ Br(w) = Br(wꢀ)) and that
ꢀ
Sꢀ − Top is terminating.
ꢀ
S
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
numberN ofmachinestheringismadeof). Suchareasoningis
used by Burns and Pachl(see [7], p. 339), who focus on infinite
derivations preserving the number of “dynamic segments” of
configurations. We also use a non-decreasing mesure ϕ in the
example of Sect.5.3.
Theorem 5, and the associated procedure, can be refined
by exploiting a measure, say ϕ, over words, which “never
increases” when applying a rule i.e. such that: w → wꢀ ⇒
ϕ(w) ≥ ϕ(wꢀ). 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 → wꢀ ⇒ ψ(w) > ψ(wꢀ)). In addition
with such a non-increasing mesure ϕ, we assume given a ϕ-
ꢀ
Henceforth, when given a measure ϕ and an associated
system Sꢀ, we implicitly focus on the generation of top chains
via Sꢀ instead of S. This allows us to restrict even more the
number of generated chains. However, in practice, in spite of
this refinement, the generation procedure does not terminate,
but yields infinitely many chains. To solve this problem, we
introduce in Sect.4 a notion of chains over regular sets of
words (instead of simply words) combined with a notion of
“generalization”.
preserving version Sꢀ of S, that is a system Sꢀ = Middle
∪
S
Bottom ∪ Top such that: w →S wꢀ iff w →S wꢀ ∧
ꢀ
ꢀ
ꢀ
S
ϕ(w) =Sϕ(wꢀ). 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ꢀ. 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ꢀ (instead of S) as far as Sꢀ −Top
ꢀ
S
(instead of S − Top ) is terminating. More precisely, Theo-
S
4 A sufficient condition for self-stabilization
rem 5 becomes:
Theorem 12. Let S = Middle ∪ Top ∪ Bottom be a
S
S
S
As mentioned earlier, top chains, when generated in a brute
manner, are frequently in infinite number. However it is of-
ten possible to discover some recurrent forms for words tn
appearing at the end of chains. Consider again the subset of
rules Sꢀ = {T4, B1, M1, M4} from Beauquier-Debas system:
rewrite system and L a set of configurations. Let ϕ be a non-
increasing mesure and Sꢀ = Middle ∪ Top ∪ Bottom
ꢀ
ꢀ
ꢀ
S
S
S
a ϕ-preserving version of S. If
(0) each ground word is reducible via S,
(1) L is closed via S, and
(3’) Sꢀ − Top is terminating.
ꢀ
S
T4 : #X12# → #X21#,
B1 : #2X1# → #1X2#,
M1 : #X01Y # → #X10Y #,
M4 : #X02Y # → #X20Y #.
Then S is self-stabilizing w.r.t. L iff there is no quasi-cyclic
top chain t1 → · · · → tn via Sꢀ, such that un ∈/ L for some
ground instance un of tn.
Example. ConsiderthemiddlerulesofGhosh’salgorithm(see
Sect.5 for details):
Starting from T4, and applying iteratively rule M4, one gen-
erates chains of the form:
M1: #X(q + 1)qY # → #X(q + 1)(q + 1)Y #
M2: #Xq(q + 1)Y # → #X(q + 1)(q + 1)Y #
where q ∈ {0, 1, 2, 3} and ‘+’ is addition modulo 4.
#W12# → #W21#,
The convergence proof uses a norm function (Br, Ds) such
that either Br or Ds strictly decreases at each step, but indi-
vidually Br and Ds are only non-increasing functions. While
Ds is a very subtle function, Br is simply the number of
#W012# → #W021# → #W201#,
#W0012# → #W0021# → #W0201# → #W2001#,
· · ·

Rewrite systems for self-stabilization proofs
89
These chains are in infinite number, but all of them (except
the first one) end with words of the form #W20j1# with
j > 0. It is then convenient to generalize words of the form
#W20j1# 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
of variables appearing in T and S (viz., W and Wꢀ) do not mat-
ter. Henceforth, without loss of generality, we always rename
first-order variables Wꢀ, Wꢀꢀ, · · · appearing in schemes, to W.
In particular a substitution of the form {W/Wꢀu} is simply
written {W/Wu}. With this convention, a generalization T of
1st-order scheme S is just a 1st-order scheme that contains S,
i.e., such that: S ⊆ T. Likewise, 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 minimalreduction. Given a ruel R, and a substitution
σ ∈ DR ∪ {id}, we say that a scheme T is a generalized
successor of scheme S, and write Sσ ꢁR T (or more simply
Sσ ꢁ T), iff Sσ →R Sꢀ and Sꢀ ⊆ T.
Example. For rule M4 : #X20Y # → #X02Y # and
schemes S = #W20+1# and Sꢀ = #W200+1#, we have
Sσ → Sꢀ ⊆ S (with σ : {W/W0}). We can thus write
Sσ ꢁ S. So S is its own generalized successor via M4
using σ.
termination for S − Top , see Sect.4.3.) We claim that such
S
a process of generalization improves the convergence of the
method of top chain generation.
4.1 Replacing words by schemes
We now express formally the correspondence between re-
lation ꢁ at the scheme level and → at the word level. We
have:
We are now going to define the notion of “schemes”, an ap-
propriate form of regular languages that contain sets of words
considered before. We extend accordingly our notion of re-
duction chains by manipulating schemes instead of words.
Lemma 15. GivenaruleR andasubstitutionσ ∈ DR∪{id},
we have, for any scheme S and any word s ∈ S: sσ →R
t implies Sσ ꢁR T for some scheme T such that t ∈ T.
We now give formally the notion of “generalized top
chain”.
Definition 13. A first-order scheme S is a language of the
form #LWM# where L, M are (nonempty) regular lan-
guages over Σ∗, and W a first-order variable. A ground
scheme S is a language of the form #L# where L is a regular
language over Σ∗. A scheme is either a 1st-order or a ground
scheme.
Definition 16. The generalized minimal top chains of a re-
write system S form a set inductively defined as follows:
• Every top rule t0 → t1 of S is a generalized chain, written
In the following we assume that the set of legitimate configu-
rations L is expressed as a ground scheme.
{t0} ꢁ {t1}.
• If G : T0 ꢁ · · · ꢁ Tn is a generalized minimal top
chain and R is a rule of S such that Tnσ ꢁ Tn+1, then
T0σ ꢁ · · · ꢁ Tnσ ꢁ Tn+1 is a generalized minimal top
chain called generalized successor of G (via R using σ).
Note that any first-order word of the form #uWv# (with
strings u, v) can be seen as a specialfirst-order scheme with
L = {u} and M = {v}. Likewise any ground word is a
specialground scheme.
Lemma 15 generalizes as follows:
4.2 Minimal reductions of schemes and generalization
Lemma 17. Given a top chain over words,
t0σ1 . . . σn →R · · · →R
t
n−1σn →R tn,
1
n
via rules R1, . . . , Rn of S, nu−si1ng substitutions σ1, . . . , σn,
and a scheme T0 such that t0 ∈ T0, there is a top chain over
schemes,
The notion of minimal reduction over words extends naturally
over schemes. Formally:
Definition 14. Let S be a scheme, R a rule and σ a substitu-
tion of DR ∪{id}. The reduced form of S via R using σ is the
scheme Sꢀ defined by:
T0σ1 . . . σn ꢁR · · · ꢁR
T
n−1σn ꢁR Tn,
1
n−1
n
Sꢀ = {sꢀ | ∃s ∈ S such that sσ →R sꢀ}.
This is written Sσ →R Sꢀ.
using the same substitutions, such that ti
i = 1, . . . , n.
∈
Ti for
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 t0 → t1 as input
and Γ denotes the set of schemes for which the successors
remain to be computed.
Example. For rule M4 : #X02Y # → #X20Y #, the
scheme S = #W20+1# minimally reduces via M4 to Sꢀ =
#Wꢀ200+1# using σ : {W/Wꢀ0}. The reduction is written
Sσ = #Wꢀ020+1# → #Wꢀ200+1#.
Generalization over 1st-order schemes is an overapprox-
imation of the regular languages surrounding the 1st-order
variable of a scheme. More precisely, a 1st-order scheme T :
#M1WM2# is a generalization of a 1st-order scheme S :
#L1WꢀL2# iff L1 ⊆ M1 and L2 ⊆ M2. Note that the names
Generalized chain generation (t0 → t1)
Initially: Γ = {t1}.
While Γ = ∅

90
J. Beauquier et al.
do
1. Select S ∈ Γ.
2. Compute the finite set of generalized successors,
say {Sni ew}i, of S
(Sσ ꢁR Sni ew for some rule R ∈ S and some σ ∈ DR
{id}).
∪
Fig. 1. Graphs for reductions S1σ1σ2 ꢁR S2σ2 ꢁR S3 and
1
2
Sσ ꢁR
S
3. For all i, add Sni ew to Γ unless Sni ew ⊆ Sold for some Sold
in Γ.
The process of graph construction, described below, takes
a top rule t0 → t1 as an input and builds iteratively gen-
eralized successors under the form of growing paths. Each
node N of the graph is labelled with a scheme S, and re-
ferred to as pair (N, S). Each generalized top chain using
substitutions σ1, . . . , σn, of the form (U0 ꢁR ) U1 ꢁR
4. Γ := Γ − {S}.
od
Note that test Sni ew ⊆ Sold is decidable since it deals
with inclusion of regular languages. An optimization of the
above procedure (that will be implicit henceforth) 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ꢀ), Sect.2.2).
1
2
· · · ꢁR Un, is represented as a path of the graph of the form
n
ꢂ(N1, S1), . . . , (Nn, Sn)ꢃ, where (Ri, σi) labels the edge
from Ni to Ni+1 (1 ≤ i ≤ n − 1), such that Siσi · · · σn
=
Ui (1 ≤ i ≤ n − 1) and Sn = Un. Formally, the procedure is
as follows:
Example. As already seen above for Beauquier-Debas sys-
tem, the righthand side #W21# of top rule T4 minimally
reduces via M4 to scheme S1 = #W20+1#, which is its
own generalized successor via M4 using {W/W0}. On the
other hand, scheme S1 = #W20+1# is minimally reducible
via B1 (using {W/2W}) to
Graph construction (t0 → t1)
Initially: Q = {(N1, {t1})}.
While Q = ∅
do
1. Select (N, S) ∈ Q
2. Compute the finite set of successors of S, say {Sni ew}i,
(Sσ ꢁR Sni ew for some rule R ∈ S
and some σ ∈ DR ∪ {id}).
3. For all i:
U = #1W20+2#.
Scheme U is itself minimally reducible via M1 (using
{W/0W}) in an iterative way, which yields
#01W20+2#, #001W20+2#, #0001W20+2#, etc.
Scheme U can be thus generalized as
S2 = #0∗1W20+2#,
3a. If Sni ew ⊆ Sold for some node (Nold, Sold) ∈ Q,
add an edge, labelled with (R, σ),
from (N, S) to (Nold, Sold).
3b. Otherwise, add node (Nniew, Sni ew) to Q,
and edge, labelled (R, σ),
from (N, S) to (Nniew, Sni ew).
4. Q := Q − {(N, S)}.
which is thus a generalized successor of S1 via B1 (using
{W/2W}).
od
According to the optimization mentioned previously, suc-
cessors 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 optimiza-
tion consists in skipping step 3a in case an edge, labelled σ,
already exists from (N, S) to (Nold, Sold).
The latter scheme is minimally reducible via M4 (resp. M1),
but this yields only the subset #0+1W200+2# (resp.
#0+01W20+2#) of S2. Therefore S2 is its own general-
ized successor via M4 (using {W/W0}) and via M1 (using
{W/0W}).
Example. The graph for generalized chain generation of
Beauquier-Debas system Sꢀ, with T4 as an input, is depicted
in Fig.2.
4.3 Graph construction
It is convenient to represent a minimalreduction of the form
From the construction of the graph, we have:
S1σ1 ꢁR S2 under the form of an edge, labelled (R1, σ1),
1
Proposition 18. Suppose that during the scheme chain gen-
eration, there is a generated chain from U1 = {t1} to Un via
from S1 to S2. Likewise, a chain of the form S1σ1σ2 ꢁR
1
S2σ2 ꢁR S3 is represented as an edge (labelled (R1, σ1))
2
R1, . . . , Rn−1, using σ1, . . . , σn−1
:
from S1 to S2, followed by an edge (labelled (R2, σ2)) from
S2 to S3 (see the graph on the left in Fig.1). If additionally,
schemes are represented as labels of nodes and structure shar-
ing is used in order to merge the representation of nodes asso-
ciated with identicalschemes, then the generation of scheme
successors corresponds to the construction of a graph, where
pathsbetweennodesrepresentchainsoverschemes. Forexam-
ple, the graph on the right in Fig.1 corresponds to the minimal
reduction Sσ ꢁR S and represents under a compact form an
infinite number of chains Sσ ꢁR S, Sσ2 ꢁR Sσ ꢁR S,
etc.
t1σ1 . . . σn−1 ꢁR · · · ꢁR
Un.
1
n−1
Then, there is a path from (N1, {t1}) to a node of the form
(N, Un) via edges labeled (R1, σ1), . . . , (Rn−1, σn−1).
This gives a sufficient condition for self-stabilization:
Theorem 19. If, for each top rule t0 → t1 ∈ S as an in-
put, 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.

Rewrite systems for self-stabilization proofs
91
Middle M1 : #X10Y # → #X01Y # ( with Y = ε)
M2 : #X11Y # → #X02Y # ( with Y = ε)
M3 : #X12Y # → #X00Y # ( with Y = ε)
M4 : #X02Y # → #X20Y # ( with Y = ε)
M5 : #X22Y # → #X10Y # ( with Y = ε)
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 [5]). Therefore, S is
self-stabilizing iff there is no ground cyclic derivation via S
containing an element w ∈ L. As remarked in [5], one can
see that T1, T2, T3 are applied at most once. As a consequence
S is self-stabilizing iff there is no ground cyclic derivation
via S0 ≡ S − {T1, T2, T3} containing an element w ∈ L.
The measure ϕ over a word t ∈ (Σ ∪ V)∗, is defined as the
number of nonnull elements contained by t. Obviously, ϕ is
non-increasing with S0. Besides, among rules of S0 only rules
B1, M1, M4, T4 preserve the number of nonnull elements. The
ϕ-refinementofthebasicprocedurethusconsistsingenerating
top chains via Sꢀ ≡ {B1, M1, M4, T4} instead of S0.
The graph constructed in Fig.2 gives a complete picture of
the situation illustrated in the previous examples. Since there is
no infinite path using Top (T4 is used at most once), it follows
that there is no quasi-cyclic top chain t1 → · · · → tn via Sꢀ,
such that un ∈ L for some ground instance un of tn. Self-
stabilization is thus proved for Beauquier-Debas’s variant of
Dijkstra’s 3-state algorithm.
Fig. 2. The graph construction for T4
Proof. Suppose there is no path using Top infinitely often
S
(except paths passing by L). Then, by Proposition 18, there
is no chain over schemes using Top infinitely often (except
S
chains reaching L). Now, by Lemma 17, there is no chain over
words using Top infinitely often (except chains reaching L).
S
Finally, using the fact that S − Top terminates, there is no
5.2 Ghosh’s 4-state algorithm
S
infinite chain over words (except those reaching L), hence no
quasi-cyclic chain t0 → t1 → · · · → ti → · · · → tn = ti
(except if tn ∈ L). Therefore, S is self-stabilizing.
Self-stabilization of Ghosh’s algorithm [14], a variant of Dijk-
stra’s 4-state algorithm, can be proved formally along the same
lines. The system consists of a parametric number N of ma-
chines (0, 1, · · · , N − 1), which have four states: {0, 1, 2, 3},
except the top machine N −1 (resp. bottom machine 0) which
has only two states: {0, 2} (resp. {1, 3}). As explained in
Sect.2, the configuration of the system is the string of all ma-
chine states, delimited by special end symbols ‘#’. Writing
X, Y for nonempty string variables, the transitions correspond
to the following system S = Middle ∪ Top ∪ Bottom of
rewrite rules.
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 coun-
terpart over words, thus allowing to prove self-stabilization in
more cases.
5 Examples
Middle
M1 : #X(q + 1)qY # → #X(q + 1)(q + 1)Y #
In order to illustrate the method of Sect.4 we explain how
it applies on three examples. (The last two of them can be
skipped by the reader without loss of continuity.)
M2 : #Xq(q + 1)Y # → #X(q + 1)(q + 1)Y #
where q ∈ {0, 1, 2, 3} and ‘+’ is addition modulo 4.
Top
T1 : #X32# → #X30#
T2 : #X10# → #X12#
5.1 Beauquier-Debas algorithm
Bottom
This system originates from [5], and is an adaptation of Dijk-
stra’s third (3-state) algorithm [11]. In our formalism, it cor-
responds to the following system S:
B1 : #12X# → #32X#
B2 : #30X# → #10X#
L is defined as #{1+, 3+}{0+, 2+}#.
Bottom B1 : #2X1# → #1X2#
As mentioned in Sect.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ꢀ of the string which differ
Top
T1 : #X00# → #X21#
T2 : #X10# → #X01#
T3 : #X20# → #X11#
T4 : #X12# → #X21#
T5 : #X22# → #X01#

92
J. Beauquier et al.
Fig. 3. First-order generation of chain for T1
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.
all the paths 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.
5.3 Hoepman’s ring orientation algorithm
The Br-preserving version Sꢀ of S (cf. Sect.3.4) is ob-
tained by modifying the middle rules as follows:
We finally sketch out how our method adapts to uniform algo-
rithms (algorithms without distinguished top, bottom or mid-
dle rules). We take the self-stabilizing ring orientation algo-
rithm presented by Hoepman in [18], as an example. Our un-
derlying assumptions about the existence of distinguished top
rules Top and the termination of S − Top, do not hold any
longer in this context. The reasoning for proving convergence,
is modified by using an assumption of fairness (also used in
[18]) instead:Any infinite sequence of rules modifies infinitely
often the state of every machine of the ring.
M1: #X(q + 1)qqY # → #X(q + 1)(q + 1)qY #
M2: #Xqq(q + 1)Y # → #Xq(q + 1)(q + 1)Y #
The graph construction is illustrated in Fig.3 in the case of
initialruel T1 : #W32# → #W30#. Similarly, another
representative graph can be obtained, starting from the other
top rule righthand side #W12#. To make the figure more
readable, some details have been omitted:
• substitutions σ0 and σ0ꢀ are respectively {W/W0} and
{W/W03},
Hoepman’s algorithm is based on 16 rules applied to words
with the alphabet Σ = {1 , 1+, 0 , 0+} and uses the follow-
−
−
• theedgeslabelledbyM1 withoutasubstitutioncorrespond
to σ = id,
ing notations:
L0 = Σ∗ = {0, 1}∗ with 0 = {0+, 0 }, 1 = {1+, 1 },
L1 = (O1 I1)∗ with O1 = 0 ∪ {0+0−0+, 0 0+, 0+0 }
−
• most schemes appearing in the figure are closed by (gener-
alized) application of the rule M1 with σ = id and should
have a loop which is not represented.
and I1 = 1 ∪ {1+1 1+, 1 1+, 1+1−},
−
−
L2 = (O2 I2)∗ with O2 =−0∪{0+0 −} and I2 = 1∪{1+1 }.
−
−
−
A similar graph can be constructed, starting from top chain
T2 instead of T1. The important point is that, in both graphs,
The corresponding rewriting system S transforms a sub-
word pqr in pqꢀr, where qꢀ is given by the following tables:

Rewrite systems for self-stabilization proofs
93
rule p
q
0
1
1
0
r
q’
rule p
q
0
0
1
1
r
1
q’
1+
In order to prove self-stabilization via S, it is thus neces-
sary and sufficient to prove that there is no infinite sequence
of derivations via Sꢀ (apart from sequences ending at L2). We
thus focus on chains starting from a rule E (or Eꢀ, F, Fꢀ).
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 take E : 0 1W0+ → 1+1 W0 as
a
b
c
d
0
0
1
1
0
0
1
1
1
−
e
0+
−
−
−
−
−
1
−
0
−
0
−
e’
f
1
1+
0+ 1+
0 0+
−
1+ 0+
−
f’
0
−
−
−
rule p
q
r
1
0
1
q’
0+
0+
rule p
q
1
1
r
q’
1+
1+
a starting rule and we show that there is no infinite derivation
from E by first-order rewriting via Sꢀ (regardless of sequences
going to L2). 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 L2).
g
0
0
0
i
1
0
1
0
−
−
−
−
−
−
g’
h
1
i’
j
0
−
−
0+ 0+
0
−
0
−
1+ 1+
1
−
1
−
h’
1
0+ 0+
j’
0
1+ 1+
This graph can be found in Fig.4.
These rules can be applied at any position of the configu-
Only the edges corresponding to non trivial substitutions
(σ = 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
ration. (Formally, every transformation of pqr into pqꢀr corre-
sponds to 3 rules: #XpqrY # → #XpqꢀrY #, #rXpq# →
#rXpqꢀ#, #qrXp# → #qꢀrXp#.) Hoepman proves that
the system converges on L2 in two steps: first, he exhibits
a measure that strictly decreases, when applied to a ground
configuration of L0 unless this ground configuration belongs
to subset L1; second he exhibits another measure that strictly
decreases, when applied to a ground configuration of L1, un-
less it belongs to L2. (He proves that the system converges
from L2 to a third set L3, but this is beyond the scope of
this presentation.) In contrast, our method gives a direct proof
for the convergence to L2, viewed here as set L of legitimate
configurations, and does not appealto any strictly decreasing
mesure.
(I2O2)∗1+1 W1 1+(O2I2)∗O2,
−
−
with its three outgoing edges labeled respectively E, Eꢀ, Fꢀ:
• The substitution for rule E is {W/0+0 },
−
which gives (I2O2)∗1+1 01+1 1+(O2I2)∗O2,
−
−
generalized as Σ∗01+1 1+Σ∗.
−
• The substitution for rule Eꢀ is {W/0 0+},
−
which gives (I2O2)∗1+1 1+01 1+(O2I2)∗O2,
generalized as Σ∗1+1 1−+0Σ∗.
−
−
We preliminary transform Hoepman’s system into a sim-
pler set of rules. We first use a ϕ-refinement in order to dis-
regard rules (a) and (c). Here measure ϕ counts the num-
ber of maximalsubsequences of the same vaul e (either 0 or
1), inside a word (assuming the leftmost and rightmost el-
ements 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. There-
fore, (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 S −{a, c}. The remaining rules are themselves
merged into the simple new system Sꢀ = {E, Eꢀ, F, Fꢀ} given
by the table below.
• The substitution for rule Fꢀ is {W/W0},
which gives (I2O2)∗1+1 W0 0+1(O2I2)∗O2,
generalized as (I2O2)∗1+−1 W0 0+(I2O2)∗.
−
−
−
Also note that the two edges leading to L2 (our set of legitimate
configurations) are implicitly labeled by {W/ε}.
Considering this graph, we see that there are three kinds of
nodes.Thefirstonecorrespondstoafirstorderscheme LWM,
the second one to the legitimate scheme L2 and the third one to
ground schemes containing either 0+0 0+ or 1+1 1+. This
observation is summarized in Fig.5.
A simple analysis of this synthetic form, leads us to con-
clude that no infinite path exists in this graph (except those
passing in L2), for the following reasons:
−
−
rule p
q
0
0
1
1
r
p’ q’ r’
• Thereisnoinfiniteloopinthenodeswhichcontainpatterns
E
0+
1
0
1
1
0
1+
1+
0+
0+
1
0
0
1
−
−
−
−
−
like 0+0 0+ (resp. 1+1 1+) because no rule can rewrite
−
−
E’
F
1
0+
0
−
−
the centralletter which is in contradiction with the fairness
assumption.
• There is no infinite loop with a substitution σ = id because
X represents a finite word and then cannot be instanciated
infinitely often.
• There is no infinite loop with label σ = id because other-
wise, the string represented by X could never be modified
at its extremities which contradicts fairness.
1+
0
−
F’
1+
Note that each transformation is now a shorthand for 4
transformations. For example E transforms 0+0 1 or
−
−
0+0 1+ into 0 1+1 or 0+1+1 . As before, every trans-
−
−
−
−
formation of pqr into pꢀqꢀrꢀ corresponds to 3 rules:
Similar constructions and explanations hold for rules
#XpqrY # → #XpꢀqꢀrꢀY #,
#rXpq# → #rꢀXpꢀqꢀ#,
Eꢀ, F, Fꢀ. This achieves our proof of self-stabilization.
and #qrXp# → #qꢀrꢀXpꢀ#,
6 Conclusion and perspectives
depending on the position where it is applied.
It is easy to see that every sequence via S − {a, c} can be
In contrast with methods relying on the existence of a strictly
decreasing norm function [5,14,19,23], our technique re-
simulated by a sequence via Sꢀ = {E, Eꢀ, F, Fꢀ}.

94
J. Beauquier et al.
Fig. 4. First-order graph generation for E
1. focusing on derivations originating from top-configura-
tions instead of derivations starting from arbitrary config-
urations.
2. reasoning with 1st-order variables, and deriving new con-
figurations through a restricted strategy of reduction (top
chain generation) instead of considering all the possible
ground configurations, and all their possible ground suc-
cessors.
3. reasoning with regular languages (including 1st-order
variables), and integrating a process of generalization.
Fig. 5. A reduced form for the graph in Fig.4
From a mechanicalpoint of view, the operation of minimal
reduction over schemes can be implemented via the operation
of transducer (see [24]; cf [4]). It is also possible to analyse
further the constructed graph in order to extract a complex-
ity upperbound for the convergence. In [4], further results are
given, concerning a naturalcounterpart of Herman’s composi-
tionality result in our framework. We believe that our method
adapts easily to the case of uniform rings, as sketched out in
the case of Hoepman’s ring-orientation protocol. We are cur-
rently investigating an extension of the method to algorithms
running on arbitrary (non-ring) networks, that could use graph
rewriting techniques as proposed in [25–27].
quires only little specific knowledge and proposes a uniform
framework for the fullproof of severalnon trivialexamples, as
shown here on Ghosh’s 4-state algorithm [14] and Beauquier-
Debas’s3-statealgorithm[5].Theseexamplesaresimpleones,
which allow us to give a clear view of the procedure. Our
procedure is inspired by Dershowitz’s chain generation pro-
cedure [8], and proves convergence of self-stabilizing algo-
rithms much in the same way than Dershowitz proves the ter-
mination of rewrite systems. Following Hoepman [18], we
have enhanced the basic method by incorporating a process
of generalization of words as 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.
Acknowledgements. WewouldliketothankNachumDershowitzand
two anonymous referees for their helpful comments.
References
The main differences with traditionalproof methods of
self-stabilization, which use strictly decreasing measures over
ground configurations, come from:
1. G. Antonoiu, P.K. Srimani: A Self-Stabilizing Leader Election
Algorithm for Tree Graphs. J Parallel Distrib Comput 34(2),

Rewrite systems for self-stabilization proofs
95
227–232 (1996)
17. T. Herman:Adaptativity through distributed convergence. Ph.D.
Thesis, University of Texas at Austin, 1991
18. J.-H. Hoepman: Uniform Deterministic Self-Stabilizing Ring-
Orientation on Odd-Length Rings. Proc. 8th Workshop on Dis-
tributed Algorithms, LNCS 857, pp 265–279, Berlin Heidelberg
New York: Springer 1994
2. Y.Afek, S. Kutten, M.Yung M.: Memory efficient self stabilizing
protocols for general networks. Proc. 7th WDAG, LNCS 725,
pp 15–28, Berlin Heidelberg New York: Springer 1990
3. A.Arora, M.G. Gouda, T. Herman: Composite routing protocols.
Proc. 2nd IEEE Parall Distrib Process, 1990
4. J. Beauquier, B. Be´rard, L. Fribourg, F. Magniette: Proving Con-
vergence of Self-Stabilizing Systems Using First-Order Rewrit-
ing and Regular Languages. Research Report LSV-00-1, Lab.
Specification and Verification, ENS de Cachan, Cachan, France,
January 2000
19. S.C. Hsu, S.T. Huang: A self-stabilizing algorithm for maximal
matching. Inform Process Lett 43(2), 77–81 (1992)
20. J.-M. Hullot: Canonical Forms and Unification. Proc. 5th Conf.
onAutomatedDeduction, LNCS, pp318–334, BerlinHeidelberg
New York: Springer 1980
5. J. Beauquier, O. Debas: An optimal self-stabilizing algorithm
for mutualexcul sion on uniform bidirectionalrings. Proc. 2nd
Workshop on Self-Stabilizing Systems, Las Vegas, 1995, pp
226–239
6. R.V. Book, F. Otto: String-Rewriting Systems. Berlin Heidelberg
New York: Springer 1993
7. J.E. Burns, J. Pachl: Uniform Self-Stabilizing Rings. TOPLAS
11(2), 330–344 (1989)
8. N. Dershowitz: Termination of Linear Rewriting Systems. Proc.
ICALP, LNCS 115, pp 448–458, Berlin Heidelberg New York:
Springer 1981
9. N. Dershowitz, C. Hoot: Topics in termination. Proc. Rewriting
Techniques and Applications, LNCS 690, pp 198–212, Berlin
Heidelberg New York: Springer 1993
10. N. Dershowitz, J.-P. Jouannaud: Rewrite Systems. Handbook of
TheoreticalComputer Science.Vol. B, pp 243–320,Amsterdam:
Elsevier – MIT Press 1990
11. E.W. Dijkstra: Self-stabilizing systems in spite of distributed
control. Commun ACM 17(11), 643–644 (1974)
12. E.W. Dijkstra: A Belated Proof of Self-stabilization. Distrib
Comput 1(1), 5–6 (1986)
13. M. Fay: First-order unification in an equationaltheory. Proc.
4th Workshop on Automated Deduction, Austin, Texas, 1979,
pp 161–167
21. J. Jaffar: Minimaland Compelte Word Unification. J. ACM
37(1), 47–85 (1990)
22. S. Katz, K.J. Perry: Self-stabilizing extensions for message-
passing systems. Distrib Comput 7, 17–26 (1993)
23. J.L.W. Kessels: An Exercise in proving self-stabilization with a
variant function. Inform Process Lett 29, 39–42 (1988)
24. Y. Kesten, O. Maler, M. Marcuse, A. Pnueli, E. Shahar: Sym-
bolic Model-Checking with Rich Assertional Languages. Proc.
CAV’97, LNCS 1254, pp 424–435, Berlin Heidelberg NewYork:
Springer 1997
25. I. Litovski, Y. Me´tivier: Computing with Graph Rewriting Sys-
tems with Priorities. Theor Comput Sci 115(2), 191–224 (1993)
26. I. Litovski, Y. Me´tivier, E. Sopena: Different LocalControsl
for Graph Relabeling Systems. Math Syst Theory 28(1), 41–65
(1995)
27. I. Litovski, Y. Me´tivier, W. Zielonka: On the Recognition of
Families of Graphs with Local Computations. Inform Comput
118(1), 110–119 (1995)
28. G.S. Makanin: The problem of solvability of equations in a free
semigroup. Matematiceskij Sbornik 103, 147–236 (1977)
29. M. Schneider: Self-Stabilization. ACM Comput Surveys 25(1),
45–67 (1993)
30. J.R. Slagle:AutomatedTheorem-Proving forTheories with Sim-
plifiers, Commutativity, and Associativity. J. ACM 21(4), 622–
642 (1974)
31. G. Tel: Introduction to Distributed Algorithms. Cambridge Uni-
versity Press, 1994
32. O. Theel, F.C. Ga¨rtner: An Exercise in Proving Convergence
through Transfer Functions. Proc. 4th Workshop on Self-
stabilizing Systems, Austin, Texas, 1999, pp 41–47
14. S. Ghosh: An Alternative Solution to a Problem on Self-
Stabilization. ACM TOPLAS 15(4), 735–742 (1993)
15. M.G. Gouda:Thetriumphandtribulationofsystemstabilization.
Proc. 9th WDAG, LNCS 972, pp 1–18, Berlin Heidelberg New
York: Springer 1995
16. M.G. Gouda, T. Herman: Adaptative programming. IEEE Trans
Softw Eng 17, 911–921 (1991)