Swan Dubois
email: swan.dubois@lip6.fr

Toshimitsu Masuzawa
email: masuzawa@ist.osaka-u.ac.jp

Sébastien Tixeuil
email: sebastien.tixeuil@lip6.fr

Maximum Metric Spanning Tree made Byzantine Tolerant

Keywords: Byzantine fault, Distributed protocol, Fault tolerance, Stabilization, Spanning tree construction

Self-stabilization is a versatile approach to fault-tolerance since it permits a distributed system to recover from any transient fault that arbitrarily corrupts the contents of all memories in the system. Byzantine tolerance is an attractive feature of distributed systems that permits to cope with arbitrary malicious behaviors. This paper focus on systems that are both self-stabilizing and Byzantine tolerant.

We consider the well known problem of constructing a maximum metric tree in this context. Combining these two properties is known to induce many impossibility results. In this paper, we provide first two impossibility results about the construction of maximum metric tree in presence of transients and (permanent) Byzantine faults. Then, we provide a new self-stabilizing protocol that provides optimal containment of an arbitrary number of Byzantine faults.

Introduction

The advent of ubiquitous large-scale distributed systems advocates that tolerance to various kinds of faults and hazards must be included from the very early design of such systems. Selfstabilization [START_REF] Edsger | Self-stabilizing systems in spite of distributed control[END_REF][START_REF] Shlomi | Self-stabilization[END_REF][START_REF] Tixeuil | Algorithms and Theory of Computation Handbook, Second Edition, chapter Self-stabilizing Algorithms[END_REF] is a versatile technique that permits forward recovery from any kind of transient faults, while Byzantine Fault-tolerance [START_REF] Lamport | The byzantine generals problem[END_REF] is traditionally used to mask the effect of a limited number of malicious faults. Making distributed systems tolerant to both transient and malicious faults is appealing yet proved difficult [START_REF] Dolev | Self-stabilizing clock synchronization in the presence of byzantine faults[END_REF][START_REF] Daliot | Self-stabilization of byzantine protocols[END_REF][START_REF] Nesterenko | Tolerance to unbounded byzantine faults[END_REF] as impossibility results are expected in many cases.

Related Works A promizing path towards multitolerance to both transient and Byzantine faults is Byzantine containment. For local tasks (i.e. tasks whose correctness can be checked locally, such as vertex coloring, link coloring, or dining philosophers), the notion of strict stabilization was proposed [START_REF] Nesterenko | Tolerance to unbounded byzantine faults[END_REF][START_REF] Masuzawa | Stabilizing link-coloration of arbitrary networks with unbounded byzantine faults[END_REF]. Strict stabilization guarantees that there exists a containment radius outside which the effect of permanent faults is masked, provided that the problem specification makes it possible to break the causality chain that is caused by the faults. As many problems are not local, it turns out that it is impossible to provide strict stabilization for those. To circumvent impossibility results, the weaker notion of strong stabilization was proposed [START_REF] Masuzawa | Bounding the impact of unbounded attacks in stabilization[END_REF][START_REF] Dubois | Bounding the impact of unbounded attacks in stabilization[END_REF]: here, correct nodes outside the containment radius may be perturbated by the actions of Byzantine node, but only a finite number of times.

Our Contribution In this paper, we investigate the possibility of topology-aware strong stabilization for tasks that are global (i.e. for with there exists a causality chain of size r, where r depends on n the size of the network), and focus on the maximum metric tree problem. Our contribution in this paper is threefold. First, we provide two impossibility results for self-stabilizing maximum metric tree construction in presence of Byzantine faults. In more details, we characterize a specific class of maximizable metrics (which includes breath-firstsearch and shortest path metrics) that prevents the existence of strong stabilizing solutions and we generalize an impossibilty result of [START_REF] Dubois | On byzantine containment properties of the min+1 protocol[END_REF] that provides a lower bound on the containmemt area for topology-aware strong stabilization (Section 3). Second, we provide a topology-aware strongly stabilizing protocol that matches this lower bound on the containment area (Section 4). Finally, we provide a necessary and sufficient condition for the existence of a strongly stabilizing solution (Section 5).

Model, Definitions and Previous Results

State Model

A distributed system S = (V, L) consists of a set V = {v 1 , v 2 , . . . , v n } of processes and a set L of bidirectional communication links (simply called links). A link is an unordered pair of distinct processes. A distributed system S can be regarded as a graph whose vertex set is V and whose link set is L, so we use graph terminology to describe a distributed system S. We use the following notations: n = |V |, m = |L| and d(u, v) denotes the distance between two processes u and v (i.e the length of the shortest path between u and v).

Processes u and v are called neighbors if (u, v) ∈ L. The set of neighbors of a process v is denoted by N v . We do not assume existence of a unique identifier for each process. Instead we assume each process can distinguish its neighbors from each other by locally labeling them.

In this paper, we consider distributed systems of arbitrary topology. We assume that a single process is distinguished as a root, and all the other processes are identical. We adopt the shared state model as a communication model in this paper, where each process can directly read the states of its neighbors.

The variables that are maintained by processes denote process states. A process may take actions during the execution of the system. An action is simply a function that is executed in an atomic manner by the process. The action executed by each process is described by a finite set of guarded actions of the form guard -→ statement . Each guard of process u is a boolean expression involving the variables of u and its neighbors.

A global state of a distributed system is called a configuration and is specified by a product of states of all processes. We define C to be the set of all possible configurations of a distributed system S. For a process set R ⊆ V and two configurations ρ and ρ ′ , we denote ρ R → ρ ′ when ρ changes to ρ ′ by executing an action of each process in R simultaneously. Notice that ρ and ρ ′ can be different only in the states of processes in R. For completeness of execution semantics, we should clarify the configuration resulting from simultaneous actions of neighboring processes. The action of a process depends only on its state at ρ and the states of its neighbors at ρ, and the result of the action reflects on the state of the process at ρ ′ .

We say that a process is enabled in a configuration ρ if the guard of at least one of its actions is evaluated as true in ρ.

A schedule of a distributed system is an infinite sequence of process sets. Let Q = R 1 , R 2 , . . . be a schedule, where R i ⊆ V holds for each i (i ≥ 1). An infinite sequence of configurations e = ρ 0 , ρ 1 , . . . is called an execution from an initial configuration ρ 0 by a schedule Q, if e satisfies ρ i-1 R i → ρ i for each i (i ≥ 1). Process actions are executed atomically, and we distinguish some properties on the scheduler (or daemon). A distributed daemon schedules the actions of processes such that any subset of processes can simultaneously execute their actions. We say that the daemon is central if it schedules action of only one process at any step. The set of all possible executions from ρ 0 ∈ C is denoted by E ρ 0 . The set of all possible executions is denoted by E, that is, E = ρ∈C E ρ . We consider asynchronous distributed systems but we add the following assumption on schedules: any schedule is strongly fair (that is, it is impossible for any process to be infinitely often enabled without executing its action in an execution) and k-bounded (that is, it is impossible for any process to execute more than k actions between two consecutive action executions of any other process).

In this paper, we consider (permanent) Byzantine faults: a Byzantine process (i.e. a Byzantine-faulty process) can make arbitrary behavior independently from its actions. If v is a Byzantine process, v can repeatedly change its variables arbitrarily. For a given execution, the number of faulty processes is arbitrary but we assume that the root process is never faulty.

Self-Stabilizing Protocols Resilient to Byzantine Faults

Problems considered in this paper are so-called static problems, i.e. they require the system to find static solutions. For example, the spanning-tree construction problem is a static problem, while the mutual exclusion problem is not. Some static problems can be defined by a specification predicate (shortly, specification), spec(v), for each process v: a configuration is a desired one (with a solution) if every process satisfies spec(v). A specification spec(v) is a boolean expression on variables of P v (⊆ V ) where P v is the set of processes whose variables appear in spec(v).

The variables appearing in the specification are called output variables (shortly, O-variables).

In what follows, we consider a static problem defined by specification spec(v).

A self-stabilizing protocol ( [START_REF] Edsger | Self-stabilizing systems in spite of distributed control[END_REF]) is a protocol that eventually reaches a legitimate configuration, where spec(v) holds at every process v, regardless of the initial configuration. Once it reaches a legitimate configuration, every process never changes its O-variables and always satisfies spec(v). From this definition, a self-stabilizing protocol is expected to tolerate any number and any type of transient faults since it can eventually recover from any configuration affected by the transient faults. However, the recovery from any configuration is guaranteed only when every process correctly executes its action from the configuration, i.e., we do not consider existence of permanently faulty processes.

When (permanent) Byzantine processes exist, Byzantine processes may not satisfy spec(v). In addition, correct processes near the Byzantine processes can be influenced and may be unable to satisfy spec(v). Nesterenko and Arora [START_REF] Nesterenko | Tolerance to unbounded byzantine faults[END_REF] define a strictly stabilizing protocol as a self-stabilizing protocol resilient to unbounded number of Byzantine processes.

Given an integer c, a c-correct process is a process defined as follows.

Definition 1 (c-correct process) A process is c-correct if it is correct ( i.e. not Byzantine) and located at distance more than c from any Byzantine process.

Definition 2 ((c, f )-containment) A configuration ρ is (c, f )-contained for specification spec if, given at most f Byzantine processes, in any execution starting from ρ, every c-correct process v always satisfies spec(v) and never changes its O-variables.

The parameter c of Definition 2 refers to the containment radius defined in [START_REF] Nesterenko | Tolerance to unbounded byzantine faults[END_REF]. The parameter f refers explicitly to the number of Byzantine processes, while [START_REF] Nesterenko | Tolerance to unbounded byzantine faults[END_REF] dealt with unbounded number of Byzantine faults (that is f ∈ {0 . . . n}).

Definition 3 ((c, f )-strict stabilization) A protocol is (c, f )-strictly stabilizing for specification spec if, given at most f Byzantine processes, any execution e = ρ 0 , ρ 1 , . . . contains a configuration ρ i that is (c, f )-contained for spec.

An important limitation of the model of [START_REF] Nesterenko | Tolerance to unbounded byzantine faults[END_REF] is the notion of r-restrictive specifications. Intuitively, a specification is r-restrictive if it prevents combinations of states that belong to two processes u and v that are at least r hops away. An important consequence related to Byzantine tolerance is that the containment radius of protocols solving those specifications is at least r. For some (global) problems r can not be bounded by a constant. In consequence, we can show that there exists no (c, 1)-strictly stabilizing protocol for such a problem for any (finite) integer c.

Strong stabilization

To circumvent such impossibility results, [START_REF] Dubois | Bounding the impact of unbounded attacks in stabilization[END_REF] defines a weaker notion than the strict stabilization. Here, the requirement to the containment radius is relaxed, i.e. there may exist processes outside the containment radius that invalidate the specification predicate, due to Byzantine actions. However, the impact of Byzantine triggered action is limited in times: the set of Byzantine processes may only impact processes outside the containment radius a bounded number of times, even if Byzantine processes execute an infinite number of actions.

In the following of this section, we recall the formal definition of strong stabilization adopted in [START_REF] Dubois | Bounding the impact of unbounded attacks in stabilization[END_REF]. From the states of c-correct processes, c-legitimate configurations and c-stable configurations are defined as follows.

Definition 4 (c-legitimate configuration) A configuration ρ is c-legitimate for spec if every c-correct process v satisfies spec(v).

Definition 5 (c-stable configuration) A configuration ρ is c-stable if every c-correct process never changes the values of its O-variables as long as Byzantine processes make no action.

Roughly speaking, the aim of self-stabilization is to guarantee that a distributed system eventually reaches a c-legitimate and c-stable configuration. However, a self-stabilizing system can be disturbed by Byzantine processes after reaching a c-legitimate and c-stable configuration. The c-disruption represents the period where c-correct processes are disturbed by Byzantine processes and is defined as follows Definition 6 (c-disruption) A portion of execution e = ρ 0 , ρ 1 , . . . , ρ t (t > 1) is a c-disruption if and only if the following holds:

1. e is finite, 2. e contains at least one action of a c-correct process for changing the value of an O-variable, 3. ρ 0 is c-legitimate for spec and c-stable, and 4. ρ t is the first configuration after ρ 0 such that ρ t is c-legitimate for spec and c-stable. Now we can define a self-stabilizing protocol such that Byzantine processes may only impact processes outside the containment radius a bounded number of times, even if Byzantine processes execute an infinite number of actions.

Definition 7 ((t, k, c, f )-time contained configuration) A configuration ρ 0 is (t, k, c, f )-time contained for spec if given at most f Byzantine processes, the following properties are satisfied:

1. ρ 0 is c-legitimate for spec and c-stable, 2. every execution starting from ρ 0 contains a c-legitimate configuration for spec after which the values of all the O-variables of c-correct processes remain unchanged (even when Byzantine processes make actions repeatedly and forever), Note that a (t, k, c, f )-time contained configuration is a (c, f )-contained configuration when t = k = 0, and thus, (t, k, c, f )-time contained configuration is a generalization (relaxation) of a (c, f )-contained configuration. Thus, a strongly stabilizing protocol is weaker than a strictly stabilizing one (as processes outside the containment radius may take incorrect actions due to Byzantine influence). However, a strongly stabilizing protocol is stronger than a classical selfstabilizing one (that may never meet their specification in the presence of Byzantine processes).

The parameters t, k and c are introduced to quantify the strength of fault containment, we do not require each process to know the values of the parameters.

Topology-aware Byzantine resilience We saw previously that there exist a number of impossibility results on strict stabilization due to the notion of r-restrictive specifications. To circumvent this impossibility result, we describe here another weaker notion than the strict stabilization: the topology-aware strict stabilization (denoted by TA strict stabilization for short) introduced by [START_REF] Dubois | The impact of topology on byzantine containment in stabilization[END_REF]. Here, the requirement to the containment radius is relaxed, i.e. the set of processes which may be disturbed by Byzantine ones is not reduced to the union of cneighborhood of Byzantine processes (i.e. the set of processes at distance at most c from a Byzantine process) but can be defined depending on the graph topology and Byzantine processes location.

In the following, we give formal definition of this new kind of Byzantine containment. From now, B denotes the set of Byzantine processes and S B (which is function of B) denotes a subset of V (intuitively, this set gathers all processes which may be disturbed by Byzantine processes).

Definition 9 (S B -correct node) A node is S B -correct if it is a correct node ( i.e. not Byzantine) which not belongs to S B . Definition 10 (S B -legitimate configuration) A configuration ρ is S B -legitimate for spec if every S B -correct node v is legitimate for spec ( i.e. if spec(v) holds).

Definition 11 ((S B , f )-topology-aware containment) A configuration ρ 0 is (S B , f )-topologyaware contained for specification spec if, given at most f Byzantine processes, in any execution e = ρ 0 , ρ 1 , . . ., every configuration is S B -legitimate and every S B -correct process never changes its O-variables.

The parameter S B of Definition 11 refers to the containment area. Any process which belongs to this set may be infinitely disturbed by Byzantine processes. The parameter f refers explicitly to the number of Byzantine processes.

Definition 12 ((S B , f )-topology-aware strict stabilization) A protocol is (S B , f )-topologyaware strictly stabilizing for specification spec if, given at most f Byzantine processes, any execution e = ρ 0 , ρ 1 , . . . contains a configuration ρ i that is (S B , f )-topology-aware contained for spec.

Note that, if B denotes the set of Byzantine processes and

S B = v ∈ V |min b∈B (d(v, b)) ≤ c ,
then a (S B , f )-topology-aware strictly stabilizing protocol is a (c, f )-strictly stabilizing protocol. Then, the concept of topology-aware strict stabilization is a generalization of the strict stabilization. However, note that a TA strictly stabilizing protocol is stronger than a classical self-stabilizing protocol (that may never meet their specification in the presence of Byzantine processes). The parameter S B is introduced to quantify the strength of fault containment, we do not require each process to know the actual definition of the set.

Similarly to topology-aware strict stabilization, we can weaken the notion of strong stabilization using the notion of containment area. This idea was introduced by [START_REF] Dubois | On byzantine containment properties of the min+1 protocol[END_REF]. We recall in the following the formal definition of this concept.

Definition 13 (S B -stable configuration) A configuration ρ is S B -stable if every S B -correct process never changes the values of its O-variables as long as Byzantine processes make no action.

Definition 14 (S B -TA-disruption) A portion of execution e = ρ 0 , ρ

Maximum Metric Tree Construction

In this work, we deal with maximum (routing) metric trees as defined in [START_REF] Gouda | Maximizable routing metrics[END_REF]. Informally, the goal of a routing protocol is to construct a tree that simultaneously maximizes the metric values of all of the nodes with respect to some total ordering ≺. In the following, we recall all definitions and notations introduced in [START_REF] Gouda | Maximizable routing metrics[END_REF].

Definition 17 (Routing metric) A routing metric (or just metric) is a five-tuple (M, W, met, mr, ≺) where:

1. M is a set of metric values, 2.
W is a set of edge weights, 3. met is a metric function whose domain is M × W and whose range is M , 4. mr is the maximum metric value in M with respect to ≺ and is assigned to the root of the system, 5. ≺ is a less-than total order relation over M that satisfies the following three conditions for arbitrary metric values m, m ′ , and m ′′ in M :

(a) irreflexivity: m ≺ m, (b) transitivity : if m ≺ m ′ and m ′ ≺ m ′′ then m ≺ m ′′ , (c) totality: m ≺ m ′ or m ′ ≺ m or m = m ′ .
Any metric value m ∈ M \{mr} satisfies the utility condition (that is, there exist w 0 , . . . , w k-1 in W and

m 0 = mr, m 1 , . . . , m k-1 , m k = m in M such that ∀i ∈ {1, . . . , k}, m i = met(m i-1 , w i-1 )).
For instance, we provide the definition of four classical metrics with this model: the shortest path metric (SP), the flow metric (F), and the reliability metric (R). Note also that we can modelise the construction of a spanning tree with no particular constraints in this model using the metric N C described below and the construction of a BFS spanning tree using the shortest path metric (SP) with W 1 = {1} (we denoted this metric by BFS in the following).

SP = (M 1 , W 1 , met 1 , mr 1 , ≺ 1 ) F = (M 2 , W 2 , met 2 , mr 2 , ≺ 2 ) where M 1 = N where mr 2 ∈ N W 1 = N M 2 = {0, . . . , mr 2 } met 1 (m, w) = m + w W 2 = {0, . . . , mr 2 } mr 1 = 0 met 2 (m, w) = min{m, w} ≺ 1 is the classical > relation ≺ 2 is the classical < relation R = (M 3 , W 3 , met 3 , mr 3 , ≺ 3 ) N C = (M 4 , W 4 , met 4 , mr 4 , ≺ 4 ) where M 3 = [0, 1] where M 4 = {0} W 3 = [0, 1] W 4 = {0} met 3 (m, w) = m * w met 4 (m, w) = 0 mr 3 = 1 mr 4 = 0 ≺ 3 is the classical < relation ≺ 4 is the classical < relation
Definition 18 (Assigned metric) An assigned metric over a system S is a six-tuple (M, W, met, mr, ≺, wf ) where (M, W, met, mr, ≺) is a metric and wf is a function that assigns to each edge of S a weight in W .

Let a rooted path (from v) be a simple path from a process v to the root r. The next set of definitions are with respect to an assigned metric (M, W, met, mr, ≺, wf ) over a given system S.

Definition 19 (Metric of a rooted path) The metric of a rooted path in S is the prefix sum of met over the edge weights in the path and mr.

For example, if a rooted path p in S is v k , . . . , v 0 with v 0 = r, then the metric of p is

m k = met(m k-1 , wf ({v k , v k-1 })) with ∀i ∈ {1, . . . , k -1}, m i = met(m i-1 , wf ({v i , v i-1 }) and m 0 = mr.
Definition 20 (Maximum metric path) A rooted path p from v in S is called a maximum metric path with respect to an assigned metric if and only if for every other rooted path q from v in S, the metric of p is greater than or equal to the metric of q with respect to the total order ≺.

Definition 21 (Maximum metric of a node) The maximum metric of a node v = r (or simply metric value of v) in S is defined by the metric of a maximum metric path from v. The maximum metric of r is mr.

Definition 22 (Maximum metric tree) A spanning tree T of S is a maximum metric tree with respect to an assigned metric over S if and only if every rooted path in T is a maximum metric path in S with respect to the assigned metric.

The goal of the work of [START_REF] Gouda | Maximizable routing metrics[END_REF] is the study of metrics that always allow the construction of a maximum metric tree. More formally, the definition follows.

Definition 23 (Maximizable metric) A metric is maximizable if and only if for any assignment of this metric over any system S, there is a maximum metric tree for S with respect to the assigned metric.

Given a maximizable metric M = (M, W, mr, met, ≺), the aim of this work is to study the construction of a maximum metric tree with respect to M which spans the system in a selfstabilizing way in a system subject to permanent Byzantine faults (but we must assume that the root process is never a Byzantine one). It is obvious that these Byzantine processes may disturb some correct processes. It is why we relax the problem in the following way: we want to construct a maximum metric forest with respect to M. The root of any tree of this forest must be either the real root or a Byzantine process.

Each process v has three O-variables: a pointer to its parent in its tree (prnt v ∈ N v ∪ {⊥}), a level which stores its current metric value (level v ∈ M ) and an integer which stores a distance (dist v ∈ N). Obviously, Byzantine process may disturb (at least) their neighbors. We use the following specification of the problem.

We introduce new notations as follows. Given an assigned metric (M, W, met, mr, ≺, wf ) over the system S and two processes u and v, we denote by µ(u, v) the maximum metric of node u when v plays the role of the root of the system. If u and v are neighbors, we denote by w u,v the weight of the edge {u, v} (that is, the value of wf ({u, v})).

Definition 24 (M-path) Given an assigned metric M = (M, W, mr, met, ≺, wf ) over a system S, a path (v 0 , . . . , v k ) (k ≥ 1) of S is a M-path if and only if:

1. prnt v 0 = ⊥, level v 0 = mr, dist v 0 = 0, and v 0 ∈ B ∪ {r}, 2. ∀i ∈ {1, . . . , k}, prnt v i = v i-1 and level v i = met(level v i-1 , w v i ,v i-1 ), 3. ∀i ∈ {1, . . . , k}, met(level v i-1 , w v i ,v i-1 ) = max ≺ u∈Nv {met(level u , w v i ,u )}, 4. ∀i ∈ {1, . . . , k}, dist v i = legal dist v i-1 with ∀u ∈ N v , legal dist u = dist u + 1 if level v = level u 0 otherwise , and 5. level v k = µ(v k , v 0 ).
We define the specification predicate spec(v) of the maximum metric tree construction with respect to a maximizable metric M as follows.

spec(v) :

prnt v = ⊥ and level v = mr, and

dist v = 0 if v is the root r there exists a M-path (v 0 , . . . , v k ) such that v k = v otherwise

Previous results

In this section, we summarize known results about maximum metric tree construction. The first interesting result about maximizable metrics is due to [START_REF] Gouda | Maximizable routing metrics[END_REF] that provides a fully characterization of maximizable metrics as follow.

Definition 25 (Boundedness) A metric (M, W, met, mr, ≺) is bounded if and only if: ∀m ∈ M, ∀w ∈ W, met(m, w) ≺ m or met(m, w) = m Definition 26 (Monotonicity) A metric (M, W, met, mr, ≺) is monotonic if and only if: ∀(m, m ′ ) ∈ M 2 , ∀w ∈ W, m ≺ m ′ ⇒ (met(m, w) ≺ met(m ′ , w) or met(m, w) = met(m ′ , w))
Theorem 1 (Characterization of maximizable metrics [START_REF] Gouda | Maximizable routing metrics[END_REF]) A metric is maximizable if and only if this metric is bounded and monotonic.

Secondly, [START_REF] Gouda | Stabilization of maximal metric trees[END_REF] provides a self-stabilizing protocol to construct a maximum metric tree with respect to any maximizable metric. Now, we focus on self-stabilizating solutions resilient to Byzantine faults. Following discussion of Section 2, it is obvious that there exists no strictly stabilizing protocol for this problem. If we consider the weaker notion of topology-aware strict stabilization, [START_REF] Dubois | The impact of topology on byzantine containment in stabilization[END_REF] defines the best containment area as:

S B = {v ∈ V \ B |µ(v, r) max ≺ {µ(v, b), b ∈ B} } \ {r}
Intuitively, S B gathers correct processes that are closer (or at equal distance) from a Byzantine process than the root according to the metric. Moreover, [START_REF] Dubois | The impact of topology on byzantine containment in stabilization[END_REF] proves that the algorithm introduced for the maximum metric spanning tree construction in [START_REF] Gouda | Stabilization of maximal metric trees[END_REF] performed this optimal containment area. More formally, [START_REF] Dubois | The impact of topology on byzantine containment in stabilization[END_REF] proves the following results.

Theorem 2 ( [START_REF] Dubois | The impact of topology on byzantine containment in stabilization[END_REF]) Given a maximizable metric M = (M, W, mr, met, ≺), even under the central daemon, there exists no (A B , 1)-TA-strictly stabilizing protocol for maximum metric spanning tree construction with respect to M where A B S B . Theorem 3 ( [START_REF] Dubois | The impact of topology on byzantine containment in stabilization[END_REF]) Given a maximizable metric M = (M, W, mr, met, ≺), the protocol of [START_REF] Gouda | Stabilization of maximal metric trees[END_REF] is a (S B , n -1)-TA strictly stabilizing protocol for maximum metric spanning tree construction with respect to M. Some other works try to circumvent the impossibility result of strict stabilization using the concept ot strong stabilization but do not provide results for any maximizable metric. Indeed, [START_REF] Dubois | Bounding the impact of unbounded attacks in stabilization[END_REF] proves the following result about spanning tree.

Theorem 4 ([7]

) There exists a (t, 0, n -1)-strongly stabilizing protocol for maximum metric spanning tree construction with respect to N C (that is, for a spanning tree with no particular constraints) with a finite t.

On the other hand, regarding BFS spanning tree construction, [START_REF] Dubois | On byzantine containment properties of the min+1 protocol[END_REF] proved the following impossibility result.

Theorem 5 ([6]) Even under the central daemon, there exists no (t, c, 1)-strongly stabilizing protocol for maximum metric spanning tree construction with respect to BFS where t and c are two finite integers. Now, if we focus on topology-aware strong stabilization, [START_REF] Dubois | On byzantine containment properties of the min+1 protocol[END_REF] introduced the following containment area:

S * B = {v ∈ V |min b∈B (d(v, b)) < d(r, v
)}, and proved the following results.

Theorem 6 ([6]

) Even under the central daemon, there exists no (t, A * B , 1)-TA strongly stabilizing protocol for maximum metric spanning tree construction with respect to BFS where

A * B S *
B and t is a finite integer.

Theorem 7 ([6])

The protocol of [START_REF] Huang | A self-stabilizing algorithm for constructing breadth-first trees[END_REF] is a (t, S * B , n -1)-TA strongly stabilizing protocol for maximum metric spanning tree construction with respect to BFS where t is a finite integer.

The main motivation of this work is to fill the gap between results about TA strong and strong stabilization in the general case (that is, for any maximizable metric). Mainly, we define the best possible containment area for TA strong stabilization, we propose a protocol that provides this containment area and we characterize the set of metrics that allow strong stabilization.

Impossibility Results

In this section, we provide our impossibility results about containment radius (respectively area) of any strongly stabilizing (respectively TA strongly stabilizing) protocol for the maximum metric tree construction.

Strong Stabilization

We introduce here some new definitions to characterize some important properties of maximizable metrics that are used in the following. Then, we define a specific class of maximizable metrics and we prove that it is impossible to construct a maximum metric tree in a strongly-stabilizing way if we do not consider such a metric.

Definition 29 (Strongly maximizable metric) A maximizable metric M = (M, W, mr, met, ≺ ) is strongly maximizable if and only if |M | = 1 or if the following properties holds:

• |M | ≥ 2,
• M is strictly decreasing, and

• M has one and only one fixed point.

Note that N C is a strongly maximizable metric (since |M 4 | = 1) whereas BFS or SP are not (since the first one has no fixed point, the second is not strictly decreasing). If we consider the metric MET defined below, we can show that MET is a strongly maximizable metric such that |M | ≥ 2.

MET = (M 5 , W 5 , met 5 , mr 5 , ≺ 5 ) where Proof We prove this result by contradiction. We assume that M = (M, W, mr, met, ≺) is a maximizable metric such that there exist a finite integer t and a protocol P that is a (t, c, 1)strongly stabilizing protocol for maximum metric spanning tree construction with respect to M. We distinguish the following cases (note that they are exhaustive):

M 5 = {0, 1, 2, 3} W 5 = {1} met 5 (m, w) = max{0, m -w} mr 5 = 3 ≺ 5 is the classical < relation Now,
µ(p c , r) µ(p c+1 , r) µ(p c+2 , b) µ(p c+3 , b) µ(p 2c+2 , b) mr µ(p 1 , r) µ(p c , r) µ(p c+1 , r) µ(p c+2 , r) µ(p c+3 , r) µ(p 2c+2 , r) µ(p b , r) mr µ(p 1 , r) µ(p c , r) µ(p c+1 , r) µ(p c+2 , r) µ(p c+3 , r) µ(p 2c+2 , r) mr
Case 1: M is a strongly maximizing metric and c < |M | -2.

As c ≥ 0, we know that |M | ≥ 2 and by definition of a strongly stabilizing metric, M is strictly decreasing and has one and only one fixed point.

By assumption on M, we know that there exist c + 3 distinct metric values m 0 = mr, m 1 , . . . , m c+2 in M and w 0 , w 1 , . . . , w c+1 in W such that: ∀i ∈ {1, . . . , c + 2},

m i = met(m i-1 , w i-1 ) ≺ m i-1 .
Let S = (V, E, W) be the following weighted system V = {p 0 = r, p 1 , . . . , p 2c+2 , p 2c+3 = b}, E = {{p i , p i+1 }, i ∈ {0, . . . , 2c + 2}} and ∀i ∈ {0, c + 1}, w p i ,p i+1 = w p 2c+3-i ,p 2c+2-i = w i . Note that the choice w p c+1 ,p c+2 = w c+1 ensures us the following property when level Assume that the initial configuration ρ 0 of S satisfies: prnt r = prnt b = ⊥, level r = level b = mr, and other variables of b (in particular dist) are identical to those of r (see Figure 1, variables of other processes may be arbitrary). Assume now that b takes exactly the same actions as r (if any) immediately after r. Then, by symmetry of the execution and by convergence of P to spec, we can deduce that the system reaches in a finite time a configuration ρ 1 (see Figure 1) in which: ∀i ∈ {1, . . . , c + 1}, prnt

p i = p i-1 , level p i = µ(p i , r) = m i , dist p i = legal dist prntp i and ∀i ∈ {c+ 2, . . . , 2c+ 2}, prnt p i = p i+1 , level p i = µ(p i , b) = m 2c+3-i ,
and dist p i = legal dist prntp i (because this configuration is the only one in which all correct process v satisfies spec(v) when prnt r = prnt b = ⊥ and level r = level b = mr by construction of W). Note that ρ 1 is c-legitimate and c-stable.

Assume now that the Byzantine process acts as a correct process and executes correctly its algorithm. Then, by convergence of P in fault-free systems (remember that a strongly-stabilizing algorithm is a special case of self-stabilizing algorithm), we can deduce that the system reach in a finite time a configuration ρ 2 (see Figure 1) in which: ∀i ∈ {1, . . . , 2c+3}, prnt p i = p i-1 , level p i = µ(p i , r), and dist p i = legal dist prntp i (because this configuration is the only one in which all process v satisfies spec(v)). Note that the portion of execution between ρ 1 and ρ 2 contains at least one c-perturbation (p c+2 is a c-correct process and modifies at least once its O-variables) and that ρ 2 is c-legitimate and c-stable.

Assume now that the Byzantine process b takes the following state: prnt b = ⊥ and level b = mr. This step brings the system into configuration ρ 3 (see Figure 1). From this configuration, we can repeat the execution we constructed from ρ 0 . By the same token, we obtain an execution of P which contains c-legitimate and c-stable configurations (see ρ 1 ) and an infinite number of c-perturbation which contradicts the (t, c, 1)-strong stabilization of P.

Case 2: M is not strictly decreasing.

By definition, we know that M is not a strongly maximizable metric. Hence, we have |M | ≥ 2. Then, the definition of a strictly decreasing metric implies that there exists a metric value m ∈ M such that: ∃w ∈ W, met(m, w) = m and ∃w ′ ∈ W, m ′ = met(m, w ′ ) ≺ m (and thus m is not a fixed point of M). By the utility condition on M , we know that there exists a sequence of metric values m 0 = mr, m 1 , . . . , m l = m in M and w 0 , w 1 , . . . , w l-1 in W such that ∀i ∈ {1, . . . , l}, m i = met(m i-1 , w i-1 ). Denote by k the length of the shortest such sequence. Note that this implies that ∀i ∈ {1, . . . , k}, m i ≺ m i-1 (otherwise we can remove m i from the sequence and this is contradictory with the construction of k). We distinguish the following cases:

Case 2.1: k ≥ c + 2.
We can use the same token as case 1 above by using w ′ instead of w c+1 in the case where k = c + 2 (since we know that met(m, w ′ ) ≺ m).

Case 2.2: k < c + 2.

Let S 1 = (V, E, W) be the following weighted system V = {p 0 = r, p 1 , . . . , p 2c+2 , p 2c+3 = b}, E = {{p i , p i+1 }, i ∈ {0, . . . , 2c+2}}, ∀i ∈ {0, . . . , k-1}, w p i ,p i+1 = w p 2c+3-i ,p 2c+2-i = w i , ∀i ∈ {k, . . . , c}, w p i ,p i+1 = w p 2c+3-i ,p 2c+2-i = w and w p c+1 ,p c+2 = w ′ (see Figure 2). This construction allows us to follow the same proof as in case 1 above.

w k-1 p 2c+3-k p 2c+2-k p 2c+4-k p 2c+1-k p 0 = r p 1 p c p c+1 p c+2 p c+3 p 2c+2 . . . . . . . . . . . . p 2c+3 = b w 0 . . . . . . p k p k-1 p k+1 p k+2 w w w w w w k-1 S 2 w w ′ 0 w ′ k ′ -1 p 2c+3-k ′ p 2c+2-k ′ p 2c+4-k ′ p 2c+1-k ′ . . . . . . . . . . . .
Case 3: M has no or more than two fixed point, and is strictly decreasing.

If M has no fixed point and is strictly decreasing, then |M | is not finite and then, we can apply the result of case 1 above since c is a finite integer.

If M has two or more fixed points and is strictly decreasing, denote by Υ and Υ ′ two fixed points of M. Without loss of generality, assume that Υ ≺ Υ ′ . By the utility condition on M , we know that there exists sequences of metric values m 0 = mr, m 1 , . . . , m l = Υ and

m ′ 0 = mr, m ′ 1 , . . . , m ′ l ′ = Υ ′ in M and w 0 , w 1 , . . . , w l-1 and w ′ 0 , w ′ 1 , . . . , w ′ l ′ -1 in W such that ∀i ∈ {1, . . . , l}, m i = met(m i-1 , w i-1 ) and ∀i ∈ {1, . . . , l ′ }, m ′ i = met(m ′ i-1 , w ′ i-1
). Denote by k and k ′ the length of shortest such sequences. Note that this implies that ∀i ∈ {1, . . . , k}, m i ≺ m i-1 and ∀i ∈ {1, . . . , k ′ }, m ′ i ≺ m ′ i-1 (otherwise we can remove m i or m ′ i from the corresponding sequence). We distinguish the following cases:

Case 3.1: k > c + 2 or k ′ > c + 2.
Without loss of generality, assume that k > c + 2 (the second case is similar). We can use the same token as case 1 above.

Case 3.2: k ≤ c + 2 and k ′ ≤ c + 2.
Let w be an arbitrary value of W . Let S 2 = (V, E, W) be the following weighted system This construction allows us to follow a similar proof as in case 1 above (note that any process u which satisfies µ(u, r) ≺ Υ ′ will be disturb infinitely often, in particular at least p c+1 and p c+2 which contradicts the (t, c, 1)-strong stabilization of P).

V = {p 0 = r, p 1 , . . . , p 2c+2 , p 2c+3 = b}, E = {{p i , p i+1 }, i ∈ {0, . . . , 2c + 2}}, ∀i ∈ {0, k -1}, w p i ,p i+1 = w i , ∀i ∈ {0, k ′ -1}, w p 2c+3-i ,p 2c+2-i = w ′ i and ∀i ∈ {k, 2c + 2 -k ′ }, w p i ,p i+1 = w (see
In any case, we show that there exists a system which contradicts the (t, c, 1)-strong stabilization of P that ends the proof.

Topology Aware Strong Stabilization

First, we generalize the set S * B previously defined for the BFS metric in [START_REF] Dubois | On byzantine containment properties of the min+1 protocol[END_REF] to any maximizable metric M = (M, W, mr, met, ≺).

S * B = v ∈ V \ B µ(v, r) ≺ max ≺ b∈B {µ(v, b)}
Intuitively, S * B gathers the set of corrects processes that are strictly closer (according to M) to a Byzantine process than the root. Figures from 3 to 5 provide some examples of containment areas with respect to several maximizable metrics and compare it to S B , the optimal containment area for TA strict stabilization.

Note that we assume for the sake of clarity that V \ S * B induces a connected subsystem. If it is not the case, then S * B is extended to include all processes belonging to connected subsystems of V \ S * B that not include r. Now, we can state our generalization of Theorem 6.

Theorem 9 Given a maximizable metric M = (M, W, mr, met, ≺), even under the central daemon, there exists no (t, A * B , 1)-TA-strongly stabilizing protocol for maximum metric spanning tree construction with respect to M where A * B S * B and t is a given finite integer.

Proof Let M = (M, W, mr, met, ≺) be a maximizable metric and P be a (t, A * B , 1)-TA-strongly stabilizing protocol for maximum metric spanning tree construction protocol with respect to M where A * B S * B and t is a finite integer. We must distinguish the following cases: This implies that there exists w ′ ∈ W such that: met(m, w ′ ) ≺ m (remember that M is bounded). Consider the following system: that the system reaches in a finite time a configuration ρ 1 (see Figure 6) in which:

V = {r, u, u ′ , v, v ′ , b}, E = {{r, u}, {r, u ′ }, {u, v}, {u ′ , v ′ }, {v, b}, {v ′ , b}}, w r,u = w r,u ′ = w v,b = w v ′ ,b = w, and w u,v = w u ′ ,v ′ = w ′ (b is a Byzantine process). We can see that S * B = {v, v ′ }. Since A * B S B , we have: v / ∈ A * B or v ′ / ∈ A * B .
prnt r = prnt b = ⊥, prnt u = prnt u ′ = r, prnt v = prnt v ′ = b, level r = level b = mr, level u = level u ′ = level v = level v ′ = m,
and ∀v ∈ V, dist v = legal dist prntv (because this configuration is the only one in which all correct process v satisfies spec(v) when prnt r = prnt b = ⊥ and level r = level b = mr since met(m, w ′ ) ≺ m). Note that ρ 1 is A * B -legitimate for spec and A * B -stable (whatever A * B is). Assume now that b behaves as a correct processor with respect to P. Then, by convergence of P in a fault-free system starting from ρ 1 which is not legitimate (remember that a TA-strongly stabilizing algorithm is a special case of self-stabilizing algorithm), we can deduce that the system reach in a finite time a configuration ρ 2 (see Figure 6) in which:

prnt r = ⊥, prnt u = prnt u ′ = r, prnt v = u, prnt v ′ = u ′ , prnt b = v (or prnt b = v ′ ), level r = mr, level u = level u ′ = m level v = level v ′ = met(m, w ′ ) = m ′ , level b = met(m ′ , w) = m ′′ , and ∀v ∈ V, dist v = legal dist prntv .
Note that processes v and v ′ modify their O-variables in the portion of execution between ρ 1 and ρ 2 and that ρ 2 is A * B -legitimate for spec and A * B -stable (whatever A * B is). Consequently, this portion of execution contains at least one A * B -TA-disruption (whatever A * B is). Assume now that the Byzantine process b takes the following state: prnt b = ⊥ and level b = mr. This step brings the system into configuration ρ 3 (see Figure 6). From this configuration, we can repeat the execution we constructed from ρ 0 . By the same token, we obtain an execution of P which contains c-legitimate and c-stable configurations (see ρ 1 ) and an infinite number of A * B -TA-disruption (whatever A * B is) which contradicts the (t, A * B , 1)-TA-strong stabilization of P.

r r r r u u u u v v v v b b b b u' u' u' u' v' v' v' v' ρ 0 ρ 1 ρ 2 ρ 3 © s © s ' ' s ©

Topology-Aware Strongly Stabilizing Protocol

The goal of this section is to provide a (t, S * B , n -1)-TA strongly stabilizing protocol in order to match the lower bound on containment area provided by the Theorem 9. If we focus on the protocol provided by [START_REF] Dubois | The impact of topology on byzantine containment in stabilization[END_REF] (which is (S B , n -1)-TA strictly stabilizing), we can prove that this protocol does not satisfy our constraints since we have the following result.

Theorem 10 Given a maximizable metric M = (M, W, mr, met, ≺), the protocol of [START_REF] Dubois | The impact of topology on byzantine containment in stabilization[END_REF] is not a (t, S * B , 2)-TA strongly stabilizing protocol for maximum metric spanning tree construction with respect to M where t is a given finite integer.

Proof To prove this result, it is sufficient to construct an execution of the protocol of [START_REF] Dubois | The impact of topology on byzantine containment in stabilization[END_REF] for a given metric M which contains an infinite number of S * B -TA disruptions with two Byzantine processes.

Consider the shortest path metric SP defined above and the weighted system defined by Figure 7 (r denotes the root and b 1 and b 2 are two Byzantine processes). We recall that the protocol of [START_REF] Dubois | The impact of topology on byzantine containment in stabilization[END_REF] uses an upper bound D on the length of any path of the tree and that the protocol is built in such a way that a process cannot choose as parent a neighbor with a dist variable greater or equals to D -1. Here, we assume that D = 10.

If we consider the initial configuration ρ 1 defined by Figure 8, we can state that processes p 2 and p 3 cannot modify their state as long as b 1 remains in its state. Moreover, r and p 1 are never enabled by the protocol. In this way, it is possible to construct the following portion of execution e 1 : b 2 modifies its level variable to 1. Then, p 5 and p 4 update their level variable to obtain configuration ρ 2 of Figure 8. Note that e 1 contains a S * B -TA disruption since p 4 modified one of its O-variables (namely, level) and p 4 / ∈ S * B . From ρ 2 , it is possible to construct the following portion of execution e 2 : b 2 modifies its level variable to 0. Then, p 5 and p 4 update their level variable to obtain configuration ρ 1 .

v / dist v ).
Consequently, it is possible to construct an infinite execution e 1 e 2 e 1 e 2 . . . starting from ρ 1 that contains an infinite number of S * B -TA disruptions with two Byzantine processes. This finishes the proof.

Presentation of the Protocol

In contrast of Theorem 10, we provide in this paper a new protocol which is (t, S * B , n -1)-TA strongly stabilizing for maximum metric spanning tree construction. Our protocol needs a supplementary assumption on the system. We introduce the following definition.

Definition 30 (Set of used metric values) Given an assigned metric AM = (M, W, met, mr, ≺ , wf ) over a system S, the set of used metric values of AM is defined as

M (S) = {m ∈ M |∃v ∈ V, (µ(v, r) = m) ∨ (∃b ∈ B, µ(v, b) = m)}.
We assume that we always have |M (S)| ≥ 2 (the necessity of this assumption is explained below). Nevertheless, note that the contrary case (|M (S)| = 1) is possible if and only if the assigned metric is equivalent to N C. As the protocol of [START_REF] Dubois | Bounding the impact of unbounded attacks in stabilization[END_REF] performs (t, 0, n -1)-strong stabilization with a finite t for this metric, we can achieves the (t, S * B , n -1)-TA strong stabilization when |M (S)| = 1 (since this implies that S * B = ∅). In this way, this assumption does not weaken the possibility result.

Although the protocol of [START_REF] Dubois | The impact of topology on byzantine containment in stabilization[END_REF] is not TA strongly stabilizing (see Theorem 10), our protocol borrows fundamental strategy from it. In this protocol, any process try to maximize its level in the tree by choosing as its parent the neighbor that provide the best metric value. The key idea of this protocol is to use the distance variable (upper bounded by a given constant D) to detect and break cycles of process which has the same maximum metric. To achieve the TA strict stabilization, the protocol ensures a fair selection along the set of its neighbor with a round-robin order.

The possibility of infinite number of disruptions of the protocol of [START_REF] Dubois | The impact of topology on byzantine containment in stabilization[END_REF] mainly comes from the following fact: a Byzantine process can independently lie about its level and its dist variable. For example, a Byzantine process can provide a level equals to mr and a dist arbitrarily large. In this way, it may lead a correct process of S B \ S * B to have a dist variable equals to D -1 such that no other correct process can choose it as its parent (this rule is necessary to break cycle) but it cannot modify its state (this rule is only enabled when dist is equals to D). Then, this process may always prevent some of its neighbors to join a M-path connected to the root and hence allow another Byzantine process to perform an infinite number of disruptions.

It is why we modified the management of the dist variable (note that others variables are managed exactly in the same way as in the protocol of [START_REF] Dubois | The impact of topology on byzantine containment in stabilization[END_REF]). In order to contain the effect of Byzantine process on dist variables, each process that has a level different from the one of its parent in the tree sets its dist variable to 0. In this way, a Byzantine process modifying its dist variable can only affect correct process that have the same level. Consequently, in the case where |M (S)| ≥ 2, we are ensured that correct processes of S B \ S * B cannot keep a dist variable equals or greater than D -1 infinitely. Hence, a correct process of S B \ S * B cannot be disturbed infinitely often without joining a M-path connected to the root.

We can see that the assumption |M (S)| ≥ 2 is essential to perform the topology-aware strong stabilization. Indeed, in the case where |M (S)| = 1, Byzantine processes can play exactly the scenario described above (in this case, our protocol is equivalent to the one of [START_REF] Dubois | The impact of topology on byzantine containment in stabilization[END_REF]).

The second modification we bring to the protocol of [START_REF] Dubois | The impact of topology on byzantine containment in stabilization[END_REF] follows. When a process has an inconsistent dist variable with its parent, we allow it only to increase its dist variable. If the process needs to decrease its dist variable (when it has a strictly greater distance than its parent), then the process must change its parent. This rule allows us to bound the maximal number of steps of any process between two modifications of its parent (a Byzantine process cannot lead a correct one to infinitely often increase and decrease its distance without modifying its pointer).

Our protocol is formally described in Algorithm 4.1.

algorithm 4.1 SSMAX , TA strongly stabilizing protocol for maximum metric tree construction.

Data: Nv: totally ordered set of neighbors of v. D: upper bound of the number of processes in a simple path.

Variables:

prntv ∈ {⊥} if v = r Nv if v = r
: pointer on the parent of v in the tree.

levelv ∈ {m ∈ M |m mr}: metric of the node. distv ∈ {0, . . . , D}: hop counter.

Functions:

For any subset A ⊆ Nv, choosev(A) returns the first element of A which is bigger than prntv (in a round-robin fashion). This proof is similar to the one of [START_REF] Dubois | The impact of topology on byzantine containment in stabilization[END_REF] but we must modify it to take in account modifications of the protocol. In [START_REF] Dubois | The impact of topology on byzantine containment in stabilization[END_REF], we proved the following useful property about maximizable metrics.

current distv() = 0 if levelprnt v = levelv min(distprnt v + 1, D) if levelprnt v = levelv Rules: (Rr) :: (v = r) ∧ ((levelv = mr) ∨ (distv = 0)) -→ levelv := mr; distv := 0 (R1) :: (v = r) ∧ (prntv ∈ Nv) ∧ ((distv < current distv ()) ∨ (levelv = met(levelprnt v , wv,prnt v ))) -→ levelv := met(levelprnt v , wv,prnt v ); distv := current distv () (R2) :: (v = r) ∧ ((distv = D) ∨ (distv > current distv())) ∧ (∃u ∈ Nv, distu < D -1) -→ prntv := choosev({u ∈ Nv|distv < D -1}); levelv := met(levelprnt v , wv,prnt v ); distv := current distv() (
Lemma 1 For any process v ∈ V , we have:

∀u ∈ N v , met max ≺ p∈B∪{r} {µ(u, p)}, w u,v max ≺ p∈B∪{r} {µ(v, p)}
Given a configuration ρ ∈ C and a metric value m ∈ M , let us define the following predicate: If a correct process v ∈ R with v = r, then there exists a neighbor p of v such that

IM m (ρ) ≡ ∀v ∈ V, level v max ≺ m, max ≺ u∈B∪{r} {µ(v, u)}
level p max ≺ m, max ≺ u∈B∪{r} {µ(p, u)} in ρ (since IM m (ρ) = true) and prnt v = p and level v = met(level p , w v,p ) in ρ ′ (since v is activated during this step).
If we apply the Lemma 1 to met and to neighbor p, we obtain the following property:

met max ≺ u∈B∪{r} {µ(p, u)}, w v,p max ≺ u∈B∪{r} {µ(v, u)}
Consequently, we obtain that, in ρ ′ :

level v = met(level p , w v,p ) met max ≺ m, max ≺ u∈B∪{r} {µ(p, u)} , w v,p by monotonicity of M max ≺ met(m, w v,p ), met max ≺ u∈B∪{r} {µ(p, u)}, w v,p max ≺ m, max ≺ u∈B∪{r} {µ(v, u)} since met(m, w v,p ) m
We can deduce that IM m (ρ ′ ) = true, that concludes the proof. Given an assigned metric to a system G, we can observe that the set of metrics value M is finite and that we can label elements of M by m 0 = mr, m 1 , . . . , m k in a way such that ∀i ∈ {0, . . . , k -1}, m i+1 ≺ m i .

We introduce the following notations:

∀m i ∈ M, P m i = v ∈ V \ S B µ(v, r) = m i ∀m i ∈ M, V m i = i j=0 P m j ∀m i ∈ M, I m i = v ∈ V max ≺ u∈B∪{r} {µ(v, u)} ≺ m i ∀m i ∈ M, LC m i = ρ ∈ C (∀v ∈ V m i , spec(v)) ∧ (IM m i (ρ)) LC = LC m k Lemma 3 For any m i ∈ M , the set LC m i is closed by actions of SSMAX .
Proof Let m i be a metric value from M and ρ be a configuration of LC m i . By construction, any process v ∈ V m i satisfies spec(v) in ρ.

In particular, the root process satisfies: prnt r = ⊥, level r = mr, and dist r = 0. By construction of SSMAX , r is not enabled and then never modifies its O-variables (since the guard of the rule of r does not involve the state of its neighbors).

In the same way, any process v ∈ V m i satisfies:

prnt v ∈ N v , level v = met(level prntv , w prntv,v ), dist v = legal dist prntv , and level v = max ≺ u∈Nv {met(level u , w u,v )}. Note that, as v ∈ V m i
and spec(v) holds in ρ, we have:

level v = µ(v, r) = max ≺ p∈B∪{r} {µ(v, p)} and dist v ≤ D -1 by construction of D. Hence, process v is not enabled in ρ.
Assume that there exists a process v ∈ V m i that takes a step ρ ′ R → ρ ′′ in an execution starting from ρ (without loss of generality, assume that v is the first process of v ∈ V m i that takes a step in this execution). Then, we know that v = r. This activation implies that a neighbor u / ∈ V m i (since v is the first process of V m i to take a step) of v modified its level u variable to a metric value m ∈ M such that level v ≺ met(m, w u,v ) in ρ ′ (note that O-variables of v and prnt v remain consistent since v is the first process to take a step in this execution).

Hence, we have

level v = max ≺ p∈B∪{r} {µ(v, p)} = µ(v, r) (since spec(v) holds), level v ≺ met(m, w u,v )
(since u causes an action of v), and m i level v (since v ∈ V m i and level v = µ(v, r)). Moreover, the closure of IM m i (established in Lemma 2) ensures us that m = level u max ≺ m i , max ≺ p∈B∪{r} {µ(u, p)} . Let us study the two following cases:

Case 1: max ≺ m i , max ≺ p∈B∪{r} {µ(u, p)} = m i .
We have then m m i . As the boundedness of M ensures that met(m, w u,v ) m, we can conclude that level v ≺ met(m, w u,v ) m m i level v , that is absurd. In conclusion, any process v ∈ V m i takes no step in any execution starting from ρ and then always satisfies spec(v). Then, the closure of IM B (established in Lemma 2) concludes the proof.

Lemma 4 Any configuration of LC is (S B , n -1)-TA contained for spec.

Proof This is a direct application of the Lemma 3 to LC = LC m k .

Lemma 5 Starting from any configuration of C, any execution of SSMAX reaches in a finite time a configuration of LC mr .

Proof Let ρ be an arbitrary configuration. Then, it is obvious that IM mr (ρ) is satisfied. By closure of IM mr (proved in Lemma 2), we know that IM mr remains satisfied in any execution starting from ρ.

If r does not satisfy spec(r) in ρ, then r is continuously enabled. Since the scheduling is strongly fair, r is activated in a finite time and then r satisfies spec(r) in a finite time. Denote by ρ ′ the first configuration in which spec(r) holds. Note that r takes no step in any execution starting from ρ ′ .

The boundedness of M implies that P mr induces a connected subsystem. If P mr = {r}, then we proved that ρ ′ ∈ LC mr and we have the result.

Otherwise, observe that, for any configuration of an execution starting from ρ ′ , if all processes of P mr are not enabled, then all processes v of P mr satisfy spec(v). Assume now that there exists an execution e starting from ρ ′ in which some processes of P mr take infinitely many steps. By construction, at least one of these processes (note it v) has a neighbor u which takes only a finite number of steps in e (recall that P mr induces a connected subsystem and that r takes no step in e). After u takes its last step of e, we can observe that level u = mr and dist u < D -1 (otherwise, u is activated in a finite time that contradicts its construction).

As v can execute consequently (R 1 ) only a finite number of times (since the incrementation of dist v is bounded by D), we can deduce that v executes (R 2 ) or (R 3 ) infinitely often. In both cases, u belongs to the set which is the parameter of function choose. By the fairness of this function, we can deduce that prnt v = u in a finite time in e. Then, the construction of u implies that v is never enabled in the sequel of e. This is contradictory with the construction of e.

Consequently, any execution starting from ρ ′ reaches in a finite time a configuration such that all processes of P mr are not enabled. We can deduce that this configuration belongs to LC mr , that ends the proof. Lemma 6 For any m i ∈ M and for any configuration ρ ∈ LC m i , any execution of SSMAX starting from ρ reaches in a finite time a configuration such that:

∀v ∈ I m i , level v = m i ⇒ dist v = D
Proof Let m i be an arbitrary metric value of M and ρ 0 be an arbitrary configuration of LC m i . Let e = ρ 0 , ρ 1 , . . . be an execution starting from ρ 0 .

Note that ρ 0 satisfies IM m i by construction. Hence, we have ∀v ∈ I m i , level v m i . The closure of IM m i (proved in Lemma 2) ensures us that this property is satisfied in any configuration of e.

If any process v ∈ I m i satisfies level v ≺ m i in ρ 0 , then the result is obvious. Otherwise, we define the following variant function. For any configuration ρ j of e, we denote by A j the set of processes v of I m i such that level v = m i in ρ j . Then, we define f (ρ j ) = min v∈A j {dist v }. We will prove the result by showing that there exists an integer k such that f (ρ k ) = D.

First, if a process v joins A j (that is, v / ∈ A j-1 but v ∈ A j ), then it takes a distance value greater or equals to f (ρ j-1 ) + 1 by construction of the protocol. We can deduce that any process that joins A j does not decrease f . Moreover, the construction of the protocol implies that a process v such that v ∈ A j and v ∈ A j+1 can not decrease its distance value in the step ρ j → ρ j+1 .

Then, consider for a given configuration ρ j a process v ∈ A j such that dist v = f (ρ j ) < D. We claim that v is enabled in ρ j and that the execution of the enabled rule either increases strictly dist v or removes v from A j+1 . We distinguish the following cases:

Case 1: level v = met(level prntv , w v,prntv )
The fact that v ∈ I m i , the boundedness of M and the closure of IM m i imply that prnt v ∈ A j (and, hence that level prntv = m i ). Then, by construction of f (ρ j ), we know that dist prntv ≥ f (ρ j ) = dist v . Hence, we have dist v < dist prntv + 1 in ρ j . Then, v is enabled by (R 1 ) in ρ j and dist v increases of at least 1 during the step ρ j → ρ j+1 if this rule is executed.

Case 2: level v = met(level prntv , w v,prntv ) Assume that v is activated by (R 2 ) or (R 3 ) during the step ρ j → ρ j+1 . If v does not belong to A j+1 (if level v = m i in ρ j+1 ), the claim is satisfied. In the contrary case (v belongs to A j+1 ), we know that level v = m i in ρ j+1 . The boundedness of M and the closure of IM m i imply that level prntv = m i in ρ j+1 . We can conclude that dist v increases of at least 1 during the step ρ j → ρ j+1 since the new parent of v has a distance greater than f (ρ j ) by construction of A j+1 .

Otherwise, we know that the rule (R 1 ) is enabled for v in ρ j . If this rule is executed during the step ρ j → ρ j+1 , one of the two following sub cases appears.

Case 2.1: met(level prntv , w v,prntv ) ≺ m i in ρ j . Then, v does not belong to A j+1 by definition.

Case 2.2: met(level prntv , w v,prntv ) = m i in ρ j .

Remind that the closure of IM m i implies then that level prntv = m i . By construction of f (ρ j ), we have dist prntv ≥ f (ρ j ) in ρ j . Then, we can see that dist v increases of at least 1 during the step ρ j → ρ j+1 .

In all cases, v is enabled (at least by (R 1 )) in ρ j and the execution of the enabled rule either increases strictly dist v or removes v from A j+1 .

As I m i is finite and the scheduling is strongly fair, we can deduce that f increases in a finite time in any execution starting from ρ j . By repeating the argument at most D times, we can deduce that e contains a configuration ρ k such that f (ρ k ) = D, that shows the result.

Lemma 7 For any m i ∈ M and for any configuration

ρ ∈ LC m i such that ∀v ∈ I m i , level v = m i ⇒ dist v = D,
any execution of SSMAX starting from ρ reaches in a finite time a configuration such that:

∀v ∈ I m i , level v ≺ m i
Proof Let m i ∈ M be an arbitrary metric value and ρ 0 be a configuration of

LC m i such that ∀v ∈ I m i , level v = m i ⇒ dist v = D.
Let e = ρ 0 , ρ 1 , . . . be an arbitrary execution starting from ρ 0 . For any configuration ρ j of e, let us denote

E ρ j = {v ∈ I m i |level v = m i }.
By the closure of IM m i (which holds by definition in ρ 0 ) established in Lemma 2, we obtain the result if there exists a configuration ρ j of e such that E ρ j = ∅.

If there exist some processes v ∈ I m i \E ρ 0 (and hence level v ≺ m i ) such that prnt v ∈ E ρ 0 and met(level prntv , w v,prntv ) = m i in ρ 0 , then we can observe that these processes are continuously enabled by (R 1 ). As the scheduling is strongly fair, v activates this rule in a finite time and then, level v = m i and dist v = D. In other words, v joins E ρ l for a given integer l. We can conclude that there exists an integer k such that the following property (P ) holds: for any

v ∈ I m i \ E ρ 0 , either prnt v / ∈ E ρ k or met(level prntv , w v,prntv ) ≺ m i .
Then, we prove that, for any integer j ≥ k, we have E ρ j+1 ⊆ E ρ j . For the sake of contradiction, assume that there exists an integer j ≥ k and a process v ∈ I m i such that v ∈ E ρ j+1 and v / ∈ E ρ j . Without loss of generality, assume that j is the smallest integer which performs these properties. Let us study the following cases:

Case 1: v activates (R 1 ) during the step ρ j → ρ j+1 .

Note that the property (P ) still holds in ρ j by the construction of j. Hence, we know that prnt v / ∈ E ρ j in ρ j . But in this case, we have: level prntv ≺ m i . The boundedness of M implies that level v = met(level prntv , w v,prntv ) ≺ m i in ρ j+1 that contradicts the fact that v ∈ E ρ j+1 .

Case 2: v activates either (R 2 ) or (R 3 ) during the step ρ j → ρ j+1 .

That implies v chooses a new parent which has a distance smaller than D -1 in ρ j . This implies that this new parent does not belongs to E ρ j . Then, we have level prntv ≺ m i .

The boundedness of M implies that level v = met(level prntv , w v,prntv ) ≺ m i in ρ j+1 that contradicts the fact that v ∈ E ρ j+1 .

In the two cases, our claim is satisfied. In other words, there exists a point of the execution (namely ρ k ) afterwards the set E cannot grow (this implies that, if a process leaves the set E, it is a definitive leaving). Assume now that there exists a step ρ j → ρ j+1 (with j ≥ k) such that a process v ∈ E ρ j is activated. Observe that the closure of IM m i implies that v can not be activated by the rule (R 3 ). If v activates (R 1 ) during this step, then v modifies its level during this step (otherwise, we have a contradiction with the fact that level prntv = m i ⇒ dist v = D). The closure of IM m i implies that v leaves the set E during this step. If v activates (R 2 ) during this step, then v chooses a new parent which has a distance smaller than D -1 in ρ j . This implies that this new parent does not belongs to E ρ j . Then, we have level prntv ≺ m i . The boundedness of M implies that level v ≺ m i in ρ j+1 . In other words, if a process of E ρ j is activated during the step ρ j → ρ j+1 , then it satisfies v / ∈ E ρ j+1 . Finally, observe that the construction of the protocol and the construction of the bound D ensures us that any process v ∈ I m i such that dist v = D is activated in a finite time. In conclusion, we obtain that there exists an integer j such that E ρ j = ∅, that implies the result. Proof Let m i be a metric value of M and ρ be an arbitrary configuration of LC m i . We know by Lemma 8 that any execution starting from ρ reaches in a finite time a configuration ρ ′ such that IM m i+1 holds. By closure of IM m i+1 and of LC m i (established respectively in Lemma 2 and 3), we know that any configuration of any execution starting from ρ ′ belongs to LC m i and satisfies IM m i+1 .

We know that V m i = ∅ since r ∈ V m i for any i ≥ 0. Remind that V m i+1 is connected by the boundedness of M. Then, we know that there exists at least one process p of P m i+1 which has a neighbor q in V m i such that µ(p, r) = met(µ(q, r), w p,q ). Moreover, Lemma 3 ensures us that any process of V m i takes no step in any executions starting from ρ ′ .

Observe that, for any configuration of an execution starting from ρ ′ , if any process of P m i+1 is not enabled, then all processes v of P m i+1 satisfy spec(v). Assume now that there exists an execution e starting from ρ ′ in which some processes of P m i+1 take infinitely many steps. By construction, at least one of these processes (note it v) has a neighbor u such that µ(v, r) = met(µ(u, r), w v,u ) which takes only a finite number of steps in e (recall the construction of p). After u takes its last step of e, we can observe that level u = µ(u, r) and dist u < D-1 (otherwise, u is activated in a finite time that contradicts its construction).

As v can execute consequently (R 1 ) only a finite number of times (since the incrementation of dist v is bounded by D), we can deduce that v executes (R 2 ) or (R 3 ) infinitely often. In both cases, u belongs to the set which is the parameter of function choose (remind that IM m i+1 By Lemma 4, we know that q takes no action in e. Once p chooses q as its parent, its state is consistent with the one of q (by construction of rules (R 2 ) and (R 3 )). Hence, p is never enabled after choosing q as its parent. Consequently, we obtain that p takes at most ∆D actions in e, that proves (P 0 ). Induction: d > 0 and (P d-1 ) is true.

Let v be a process of E i B such that d As δ denotes the maximal diameter of connected components of the subsystem induced by E B , then we know that d E i B (p, v) ≤ δ for any process v in E i B . For any process v of E B , there exists i ∈ {0, . . . , ℓ} such that v ∈ E i B . We can deduce that any process of E B takes at most Π(k, δ)∆D actions in e, that implies the result.

Lemma 12 If ρ is a configuration of LC and v is a process such that v ∈ E B , then for any execution e starting from ρ either 1. there exists a configuration ρ ′ of e such that spec(v) is always satisfied after ρ ′ , or 2. v is activated in e.

Proof Let ρ be a configuration of LC and v be a process such that v ∈ E B . By contradiction, assume that there exists an execution starting from ρ such that (i) spec(v) is infinitely often false in e and (ii) v is never activated in e.

For any configuration ρ, let us denote by P v (ρ) = (v 0 = v, v 1 = prnt v , v 2 = prnt v 1 , . . . , v k = prnt v k-1 , p v = prnt v k ) the maximal sequence of processes following pointers prnt (maximal means here that either prnt pv = ⊥ or p v is the first process such that there p v = v i for some i ∈ {0, . . . , k}).

Let us study the following cases:

Case 1: prnt v ∈ V \ S B in ρ.
Since ρ ∈ LC, prnt v satisfies spec(prnt v ) in ρ and in any execution starting from ρ (by Lemma 4). Hence, prnt v is never activated in e. If v does not satisfy spec(v) in ρ, then we have level v = met(level prntv , w v,prntv ) or dist v = 0 in ρ. Then, v is continuously enabled in e and we have a contradiction between assumption (ii) and the strong fairness of the scheduling. This implies that v satisfies spec(v) in ρ. The fact that prnt v is never activated in e and that the state of v is consistent with the one of prnt v ensures us that v is never enabled in any execution starting from ρ. Hence, spec(v) remains true in any execution starting from ρ. This contradicts the assumption (i) on e.

Case 2: prnt v / ∈ V \ S B in ρ. By the assumption (i) on e, we can deduce that there exists infinitely many configurations ρ ′ such that a process of P v (ρ ′ ) is enabled (since spec(v) is false only when the state of a process of P v (ρ ′ ) is not consistent with the one of its parent that made it enabled). By construction, the length of P v (ρ ′ ) is finite for any configuration ρ ′ and there exists only a finite number of processes in the system. Consequently, there exists at least one process which is infinitely often enabled in e. Since the scheduler is strongly fair, we can conclude that there exists at least one process which is infinitely often activated in e.

Let A e be the set of processes which are infinitely often activated in e. Note that v / ∈ A e by assumption (ii) on e. Let e ′ = ρ ′ . . . be the suffix of e which contains only activations of processes of A e . Let p be the first process of P v (ρ ′ ) which belongs to A e (p exists since at least one process of P v is enabled when spec(v) is false). By construction, the prefix of P v (ρ ′′ ) from v to p in any configuration ρ ′′ of e remains the same as the one of P v (ρ ′ ). Let p ′ be the process such that prnt p ′ = p in e ′ (p ′ exists since v = p implies that the prefix of P v (ρ ′ ) from v to p counts at least two processes). As p is infinitely often activated and as any activation of p modifies the value of level p or of dist p (at least one of these two variables takes at least two different values in e ′ ), we can deduce that p ′ is infinitely often enabled in e ′ (since the value of level p ′ is constant by construction of e ′ and p). Since the scheduler is strongly fair, p ′ is activated in a finite time in e ′ , that contradicts the construction of p.

In the two cases, we obtain a contradiction with the construction of e, that proves the result.

Let LC * be the following set of configurations: Proof Let ρ be a configuration of LC * . As S * B ⊆ S B , we know by Lemma 4 that any process v of V \ S B satisfies spec(v) and takes no action in any execution starting from ρ.

LC * = {ρ ∈ C |(ρ is S * B -
Let v be a process of E B . By Lemmas 11 and 12, we know that v takes at most Π(k, δ)∆D actions in any execution starting from ρ. Moreover, we know that v satisfies spec(v) after its last action (otherwise, we obtain a contradiction between the two lemmas). Hence, any process of E B takes at most Π(k, δ)∆D actions and then, there are at most nΠ(k, δ)∆D S * B -TA-disruptions in any execution starting from ρ (since

|E B | ≤ n).
By definition of a TA time contained configuration, we obtain the result.

Lemma 14 Starting from any configuration, any execution of SSMAX reaches a configuration of LC * in a finite time.

Proof Let ρ be an arbitrary configuration. We know by Lemma 10 that any execution starting from ρ reaches in a finite time a configuration ρ ′ of LC.

Let v be a process of E B . By Lemmas 11 and 12, we know that v takes at most Π(k, δ)∆D actions in any execution starting from ρ ′ . Moreover, we know that v satisfies spec(v) after its last action (otherwise, we obtain a contradiction between the two lemmas). This implies that any execution starting from ρ ′ reaches a configuration ρ ′′ such that any process v of E B satisfies spec(v). It is easy to see that ρ ′′ ∈ LC * , that ends the proof.

Theorem 12 SSMAX is a (nΠ(k, δ)∆D, S * B , n -1)-TA strongly stabilizing protocol for spec.

Proof This result is a direct consequence of Lemmas 13 and 14.

Definition 27 (

 27 Strictly decreasing metric) A metric M = (M, W, mr, met, ≺) is strictly decreasing if, for any metric value m ∈ M , the following property holds: either ∀w ∈ W, met(m, w) ≺ m or ∀w ∈ W, met(m, w) = m. Definition 28 (Fixed point) A metric value m is a fixed point of a metric M = (M, W, mr, met, ≺ ) if m ∈ M and if for any value w ∈ W , we have: met(m, w) = m.

Figure 1 :

 1 Figure 1: Configurations used in proof of Theorem 8, case 1.

  r = level b = mr: µ(p c+1 , b) ≺ µ(p c+1 , r) (and by symmetry, µ(p c+2 , r) ≺ µ(p c+2 , b)). Process p 0 is the real root and process b is a Byzantine one. Note that the construction of W ensures the following properties when level r = level b = mr: ∀i ∈ {1, . . . , c + 1}, µ(p i , r) = µ(p 2c+3-i , b), µ(p i , b) ≺ µ(p i , r) and µ(p 2c+3-i , r) ≺ µ(p 2c+3-i , b).

  Note that this choice ensures us the following property when level r = level b = mr: µ(p c+1 , b) ≺ µ(p c+1 , r) (and by symmetry, µ(p c+2 , r) ≺ µ(p c+2 , b)). Process p 0 is the real root and process b is a Byzantine one. Note that the construction of W ensures the following properties when level r = level b = mr: ∀i ∈ {1, . . . , c + 1}, µ(p i , r) = µ(p 2c+3-i , b), µ(p i , b) ≺ µ(p i , r) and µ(p 2c+3-i , r) ≺ µ(p 2c+3-i , b).

Figure 2 :

 2 Figure 2: Configurations used in proof of Theorem 8, cases 2 and 3.

Figure 2 )Figure 3 :

 23 Figure 3: Examples of containment areas for SP.

Figure 4 :Case 2 :

 42 Figure 4: Examples of containment areas for F.

Figure 5 :

 5 Figure 5: Examples of containment areas for R.

Figure 6 :

 6 Figure 6: Configurations used in proof of Theorem 9.

Figure 7 :Figure 8 :

 78 Figure 7: System used in proof of Theorem 10.

  R3) :: (v = r) ∧ (∃u ∈ Nv, (distu < D -1) ∧ (levelv ≺ met(levelu, wu,v))) -→ prntv := choosev u ∈ Nv (levelu < D -1) ∧ (met(levelu, wu,v) = max≺ q∈Nv /levelq <D-1 {met(levelq , wq,v)}) ; levelv := met(levelprnt v , wprnt v ,v ); distv := current distv () 4.2 Proof of the (S B , n -1)-TA Strict Stabilization for spec

Lemma 2

 2 For any metric value m ∈ M , the predicate IM m is closed by actions of SSMAX . Proof Let m be a metric value (m ∈ M ). Let ρ ∈ C be a configuration such that IM m (ρ) = true and ρ ′ ∈ C be a configuration such that ρ R → ρ ′ is a step of SSMAX . If the root process r ∈ R (respectively a Byzantine process b ∈ R), then we have level r = mr (respectively level b mr) in ρ ′ by construction of (R r ) (respectively by definition of level b ). Hence, level r max ≺ m, max ≺ u∈B∪{r} {µ(r, u)} = mr (respectively level b max ≺ m, max ≺ u∈B∪{r} {µ(b, u)} = mr).

Case 2 :

 2 max ≺ m i , max ≺ p∈B∪{r} {µ(u, p)} = max ≺ p∈B∪{r} {µ(u, p)}.We have then m max ≺ p∈B∪{r} {µ(u, p)}. By monotonicity of M, we can deduce that met(m, w u,v ) met( max ≺ p∈B∪{r} {µ(u, p)}, w u,v ). Consequently, we obtain that max ≺ p∈B∪{r} {µ(v, p)} ≺ met( max ≺ p∈B∪{r} {µ(u, p)}, w u,v ). This is contradictory with the result of Lemma 1.

Lemma 8 Lemma 9

 89 For any m i ∈ M and for any configuration ρ ∈ LC m i , any execution of SSMAX starting from ρ reaches in a finite time a configuration ρ ′ such that IM m i+1 holds.Proof This result is a direct consequence of Lemmas 6 and 7. For any m i ∈ M and for any configuration ρ ∈ LC m i , any execution of SSMAX starting from ρ reaches in a finite time a configuration of LC m i+1 .

  v) = d. By construction, there exists a neighbor u of v which belongs toE i B such that d E i B (p, u) = d -1. By (P d-1), we know that u takes at most Π(k, d -1)∆D actions in e. The k-boundedness of the daemon allows us to conclude that v takes at most k × Π(k, d -1)∆D actions before the last action of u. Then, a similar reasoning to the one of the initialization part allows us to say that v takes at most ∆D actions after the last action of u (note that the fact that |M (S)| ≥ 2, the construction of D and the management of dist variables imply that dist u < D -1 after the last step of u). In conclusion, v takes at most k × Π(k, d -1)∆D + ∆D = Π(k, d)∆D actions in e, that proves (P d ).

  legitimate for spec) ∧ (IM m k (ρ) = true) } Note that, as S * B ⊆ S B , we can deduce that LC * ⊆ LC. Hence, properties of Lemmas 11 and 12 also apply to configurations of LC * . Lemma 13 Any configuration of LC * is (nΠ(k, δ)∆D, Π(k, δ)∆D, S * B , n-1)-TA time contained for spec.

  is S B -legitimate for spec and S B -stable, and 4. ρ t is the first configuration after ρ 0 such that ρ t is S B -legitimate for spec and S B -stable.

	2. every execution starting from ρ 0 contains a S B -legitimate configuration for spec after
	which the values of all the O-variables of S B -correct processes remain unchanged (even
	when Byzantine processes make actions repeatedly and forever),
	3. every execution starting from ρ 0 contains at most t S B -TA-disruptions, and
	4. every execution starting from ρ 0 contains at most k actions of changing the values of
	O-variables for each S B -correct process.
	Definition 16 ((t, S B , f )-TA strongly stabilizing protocol) A protocol A is (t, S B , f )-TA
	strongly stabilizing if and only if starting from any arbitrary configuration, every execution in-
	volving at most f Byzantine processes contains a (t, k, S B , f )-TA-time contained configuration
	that is reached after at most l rounds of each S B -correct node. Parameters l and k are respec-
	tively the (t, S B , f )-stabilization time and the (t, S B , f )-process-disruption time of A.
	1 , . . . , ρ t (t > 1) is a
	S B -TA-disruption if and only if the followings hold:
	1. e is finite,
	2. e contains at least one action of a S B -correct process for changing the value of an O-
	variable,
	3. ρ 0 Definition 15 ((t, k, S B , f )-TA time contained configuration) A configuration ρ 0 is (t, k, S B ,
	f )-TA time contained for spec if given at most f Byzantine processes, the following properties
	are satisfied:
	1. ρ 0 is S B -legitimate for spec and S B -stable,

  we can state our first impossibility result.

	ρ 0	p 0 = r	w 0	p 1	. . . . . .	p c	w c	p c+1	w c+1	p c+2	w c	p c+3	. . . . . .	p 2c+2	p 2c+3 = b w 0
		mr		?		?		?		?		?		?		mr
				µ(p 1 , r)												mr
	ρ 1	'	'	. . .	'	'				E	E	. . .	E		E
		mr
	ρ 2	'	'	. . .	'	'		'		'	'	. . .	'	'
	ρ 3	'	'	. . .	'	'		'		'	'	. . .	'	'
	Theorem 8 Given a maximizable metric M = (M, W, mr, met, ≺), even under the central
	daemon, there exists no (t, c, 1)-strongly stabilizing protocol for maximum metric spanning tree
	construction with respect to M for any finite integer t if:
				M is not a strongly maximizable metric, or
				c < |M | -2

is satisfied and that u has the better possible metric among v's neighbors). By the construction of this function, we can deduce that prnt v = u in a finite time in e. Then, the construction of u implies that v is never enabled in the sequel of e. This is contradictory with the construction of e.

Consequently, any execution starting from ρ ′ reaches in a finite time a configuration such that all processes of P m i+1 are not enabled. We can deduce that this configuration belongs to LC m i+1 , that ends the proof.

Lemma 10 Starting from any configuration, any execution of SSMAX reaches a configuration of LC in a finite time.

Proof Let ρ be an arbitrary configuration. We know by Lemma 5 that any execution starting from ρ reaches in a finite time a configuration of LC mr = LC m 0 . Then, we can apply at most k times the result of Lemma 9 to obtain that any execution starting from ρ reaches in a finite time a configuration of LC m k = LC, that proves the result.

Theorem 11 SSMAX is a (S B , n -1)-TA-strictly stabilizing protocol for spec.

Proof This result is a direct consequence of Lemmas 4 and 10.

Proof of the

that the subsytem induced by E B may have several connected components. In the following, we use the following notations: Lemma 11 If ρ is a configuration of LC, then any process v ∈ E B is activated at most Π(k, δ)∆D times in any execution starting from ρ.

Proof Let ρ be a configuration of LC and e be an execution starting from ρ. Let p be a process of E i B (i ∈ {0, . . . , ℓ}) such that there exists a neighbor q which satisfies q ∈ V \ S B and µ(p, r) = met(µ(q, r), w p,q ) (such a process exists by construction of E i B ). We are going to prove by induction on d the following property:

denotes the distance in the subsystem induced by E i B ), then v executes at most Π(k, d)∆D actions in e.

Initialization: d = 0. This implies that v = p. Then, by construction, there exists a neighbor q which satisfies q ∈ V \ S B and µ(p, r) = met(µ(q, r), w p,q ). As ρ ∈ LC, Lemma 4 ensures us that level q = µ(q, r) and dist q < D -1 in any configuration of e. Then, the boundedness of M implies that q belongs to the set which is parameter to the macro choose at any execution of rules (R 2 ) or (R 3 ) by p. Consequently, p executes at most ∆ times rules (R 2 ) and (R 3 ) in e before choosing q as its parent. Moreover, note that p can execute rule (R 1 ) at most D times between two consecutive executions of rules (R 2 ) and (R 3 ) (because (R 1 ) only increases dist p which is bounded by D). Consequently, p executes at most ∆D actions before choosing q as its parent.

Concluding Remarks

We discuss now about the relationship between TA strong and strong stabilization on maximum metric tree construction. We characterize by a necessary and sufficient condition the set of assigned metric that allow strong stabilization. Indeed, properties on the metric itself are not sufficient to conclude on the possibility of strong stabilization: we must know information about the considered system (assignation of the metric).

Informally, it is possible to construct a maximum metric tree in a strongly stabilizing way if and only if the considered metric is strongly maximizable and if the desired containment radius is sufficiently large. More formally, Theorem 13 Given an assigned metric AM = (M, W, mr, met, ≺, wf ) over a system S, there exists a (t, c, n -1)-strongly stabilizing protocol for maximum metric spanning tree construction with a finite t if and only if:

(M, W, met, mr, ≺) is a strongly maximizable metric, and c ≥ max{0, |M (S)| -2} Proof We split this proof into two parts: 1) Proof of the "if " part: Denote (M, W, met, mr, ≺) by M and assume that M is a strongly maximizable metric and that c ≥ max{0, |M (S)| -2}. We distinguish the following cases: We can deduce that it is equivalent to construct a maximum metric spanning tree for M and for N C over this system. By Theorem 4, we know that there exists a (t, 0, n -1)-strongly stabilizing protocol for this problem with a finite t, that proves the result. In other words,

strongly stabilizing protocol, that proves the result with t = nΠ(k, δ)∆D.

2) Proof of the "only if " part: This result is a direct consequence of Theorem 8 when we observe that |M (S)| ≤ |M | by definition.

We can now summarize all results about self-stabilizing maximum metric tree construction in presence of Byzantine faults with the above table. Note that results provided in this paper fill all gaps pointed out in related works. To conclude about results presented in this paper, we must bring some precisions about specifications. We chose to work with a specification of the problem that consider the dist variable as a O-variable. This choice may appear strong but it seems us necessary to keep the consistency of results. Indeed, impossibility results of Section 3 can be proved with a weaker specification that does not consider the dist variable as a O-variable (see [START_REF] Dubois | Self-Stabilization, Byzantine Containment, and Maximizable Metrics: Necessary Conditions[END_REF]). On the other hand, we need the stronger specification to bound the number of disruptions of the proposed protocol. We postulate that our protocol is also TA strongly stabilizing with the weaker specification but we do no succeed to bound exactly the number of disruptions.

The following questions are still open. Is it possible to bound the number of disruptions with the weaker specification? Is it possible to perform TA strong stabilization with a weaker daemon? Is it possible to decrease the number of disruptions without loose the optimality of the containment area?