Lélia Blin

Gabriel Le Bouder

Franck Petit

Optimal Memory Requirement for Self-Stabilizing Token Circulation *

Keywords: Distributed algorithms, transient faults, self-stabilization, token circulation, memory optimization

In this paper, we consider networks where every transmitted message is received by all of the transmitter's neighbors. Typical such networks are wireless networks, in which to dedicate a message to a specific neighbor, the sender must specify who the recipient is by specifying the recipient's ID. Adding an identifier has a non-negligible cost, more precisely O(log n) bits in an n-node graph. Token Circulation (TC) is a fundamental problem that consists in guaranteeing that a single token circulates from one node to another, the token fairly visiting every node infinitely often. TC inherently requires that the token holder selects a unique neighboring node to which to pass the token. This paper proposes a solution that overcomes the communication of identifiers. It achieves optimal space complexity for the token circulation problem.

The contribution of this paper is fourfold. First, we present the first deterministic depthfirst token circulation algorithm for rooted wireless networks that uses only O(log log n) bits of memory per node. This is an exponential improvement compared to the classical addressing. Our algorithm assumes a Destination-Oriented Directed Acyclic Graph (DODAG) spanning the network. Less popular than spanning trees, DODAGs are nonetheless more general and adaptable spanning structures, since they do not need to distinguish one neighboring node as unique parent. Second, our algorithm has the very desirable property of being self-stabilizing. This means that starting from a configuration where zero or more than one token circulate in the network, the system is guaranteed to eventually work correctly, i.e., a single token eventually fairly visits every node infinitely often, following a depth-first order. Third, it works under the unfair scheduler, that is the most challenging scheduling assumption of the model. Finally, we show that our algorithm is optimal in terms of space complexity. Meaning that, for every n-node network, no TC algorithm can use less than Ω(log log n) bits of memory per node, even given a rooted spanning tree and even without considering self-stabilization.

Introduction

In recent decades, wireless network technology has gained tremendous importance. It not only more and more replaces so far "wired" network installations, but also gives rise to new applications and with them, new tech and soft stacks enabling specific communications. Many distributed algorithms written for wired networks assume that every node v of the system is equipped with a local set of labels, sometimes also referred to as port labels. This set maps the set of v's neighbors, that is the set of nodes directly linked to v by bidirectional communication links. By using their respective port sets, two neighboring nodes u and v can directly communicate by exchanging messages with each other without interfering with other nodes, and without any further specific information such as IDs. Furthermore, port labels allow to maintain global distributed spanning data structures such as various types of trees, rings, and so on, which makes solving many problems much easier.

By contrast, in wireless networks, nodes have a priori no knowledge of their neighborhood. In particular, without further information (particularly, IDs), nodes are unable to distinguish from which node a message is received, neither to pick out a particular node to whom send a message. Thus, in wireless networks, to differentiate the recipient or the sender of a particular message, classically, the message includes the identifier of the recipient. This identifier will be stored (temporarily or permanently) in the receiver's memory. In n-node networks, the inclusion of the identifier requires Ω(log n) bits. The dark side effect of the ID's inclusion is that, depending on the task considered, the message size is only determined by the size of the identifiers. Several problems can be specified by a constant number of bits, like the leader election or the token circulation, or by the number of bits depending of the degree of the network, like the coloration of the nodes. In this type of problem, the space complexity is entirely consumed by the inclusion of the identifier in the messages. Moreover, this is not appropriate to many settings, including sensor networks or swarms of robots, in which the memory of each process must be kept as small as possible, ideally constant.

Token Circulation, also referred to as token passing, is a fundamental problem to guarantee that a single token circulates from one node to another, and the token fairly visits every node infinitely often. The most popular way to implement such a mechanism in an arbitrary topology deterministically is the Depth-First Token Circulation (DFTC, for short). Briefly, this wellknown mechanism takes place by executing successive traversals, each of them initiated by a specific node, called the root. In each traversal, the token is passed among the nodes following a depth-first order. A traversal ends when the root holds the token again after every node has been visited by the token at least once. The overall DFTC mechanism is implemented by restarting traversals one after another by the root. By construction, the DFTC mechanism is fair, since the unvisited nodes become visited only once during each traversal cycle.

We are interested in self-stabilizing [START_REF] Edsger | Self-stabilizing systems in spite of distributed control[END_REF] token circulation in distributed systems. A selfstabilizing algorithm must return the system to a correct behavior in finite time, whatever its initial configuration. In the context of token circulation, typical examples of initial arbitrary system configurations are scenarios in which either no token or several tokens exist in the network. To satisfy the requirement of self-stabilization, a distributed token circulation algorithm must return in finite time the system in a configuration which contains exactly one token. Actually, it must do more than that: the algorithm must also guarantee that, eventually, this single token fairly circulates among the nodes. Following the seminal work of Dijkstra [START_REF] Edsger | Self-stabilizing systems in spite of distributed control[END_REF], token circulation has been widely investigated deterministically in the context of self-stabilization, on rings [START_REF] Burns | Uniform self-stabilizing rings[END_REF][START_REF] Gouda | The stabilizing token ring in three bits[END_REF], on (spanning) tree networks [START_REF] Brown | Token systems that self-stabilize[END_REF][START_REF] Ghosh | An alternative solution to a problem on self-stabilization[END_REF][START_REF] Petit | Optimal snap-stabilizing depth-first token circulation in tree networks[END_REF], and on arbitrary shaped networks [START_REF] St Huang | Self-stabilizing depth-first token circulation on networks[END_REF][START_REF] Dolev | Self-stabilization of dynamic systems assuming only read/write atomicity[END_REF][START_REF] Johnen | Space-efficient distributed self-stabilizing depth-first token circulation[END_REF][START_REF] Kumar Datta | Self-stabilizing depth-first token circulation in arbitrary rooted networks[END_REF][START_REF] Cournier | Snap-stabilizing depth-first search on arbitrary networks[END_REF][START_REF] Petit | Optimal snap-stabilizing depth-first token circulation in tree networks[END_REF][START_REF] Cournier | Light enabling snap-stabilization of fundamental protocols[END_REF], to quote only a few.

All the above algorithms were written in the well known (atomic-)state model [START_REF] Edsger | Self-stabilizing systems in spite of distributed control[END_REF], in the sequel denoted S, a high-level model where communication between nodes is abstracted by the ability for a node to atomically read the content of its neighbor registers, and update its own registers. More precisely, all of them were written assuming the ability for each node to locally select at least one of its neighbors: the one to which to pass the token. Such ability is commonly made with variables called pointers that maps N (v), the set of neighbors of v. Given two neighbors u and v, by reading p v , one of v's pointers, u is able to know whether p v maps the edge vu, i.e., the link leading to itself or not. Pointers are typically implemented in two ways: (i) the nodes use their identifiers, i.e., in the example, p v = u's ID, (ii) the model assumes port labels that maps N (v), the set of neighbors of v. So, if pointers are implemented with node IDs, then they require Ω(log n) bits of memory. If pointers are implemented with port labels, then they need Ω(log ∆) bits (∆ refers to the maximum degree of the network), but nodes must be able to recognize which of its neighbor port labels links it back to itself. Note that the use of pointers is particularly helpful for the problem of Token Circulation, where sending the token to exactly one neighbor is crucial to maintain the unicity of the token.

In this paper, we assume a model where no node is able to locally select one of its neighbors, except by its identifier. In S, this assumption makes the design of algorithms much more challenging, which often require the use of node identifiers or the construction of an underlying vertex coloring. Token circulation algorithms for S are proposed in [START_REF] Blin | Silent mst approximation for tiny memory[END_REF][START_REF] Blin | A self-stabilizing memory efficient algorithm for the minimum diameter spanning tree under an omnipotent daemon[END_REF][START_REF] Blin | A new self-stabilizing minimum spanning tree construction with loop-free property[END_REF]. All these algorithms work over tree topologies and use Θ(log n) bits of memory per node.

Aside from focusing on the algorithmic aspects of the self-stabilizing DFTC problem in S, we also aim to reduce the memory required to solve this problem. Note that memory optimization for the self-stabilizing token circulation has been widely addressed in the literature. As mentioned earlier, all of them assume pointers implemented over local ports and achieving O(log ∆) bits of memory per node, namely [START_REF] Edsger | Self-stabilizing systems in spite of distributed control[END_REF][START_REF] Burns | Uniform self-stabilizing rings[END_REF][START_REF] Gouda | The stabilizing token ring in three bits[END_REF][START_REF] Brown | Token systems that self-stabilize[END_REF][START_REF] Ghosh | An alternative solution to a problem on self-stabilization[END_REF] on rings or chains, [START_REF] Petit | Optimal snap-stabilizing depth-first token circulation in tree networks[END_REF] on trees, and [START_REF] Kumar Datta | Self-stabilizing depth-first token circulation in arbitrary rooted networks[END_REF] on arbitrary networks. Except [START_REF] Burns | Uniform self-stabilizing rings[END_REF] which assumes a uniform prime size ring, all the above algorithms require a root, i.e., a node with a particular local algorithm with respect to the other nodes.

In S, it has been shown that many standard "one-shot" tasks like leader election and spanning tree construction can be constructed in a self-stabilizing manner with memory O(log log n+ log ∆) bits in any n-node network with maximum degree ∆ [START_REF] Blin | Compact deterministic self-stabilizing leader election on a ring: the exponential advantage of being talkative[END_REF][START_REF] Blin | Compact self-stabilizing leader election for general networks[END_REF]. This indicates that some tasks can be achieved in S with only sublogarithmic memory. As suggested by the results established in [START_REF] Blin | Optimal space lower bound for deterministic self-stabilizing leader election algorithms[END_REF], it is much harder to reach o(log log n) memory. No previous work addresses the self-stabilizing DFTC in S without pointers.

Contributions

We present the first deterministic self-stabilizing depth-first token circulation algorithm in S that uses only O(log log n) bits of memory per node. This is an exponential improvement compared to the classical addressing. Our algorithm does not use any pointer variable. However, like many works in the fields of self-stabilization and networks, our algorithm assumes a specific underlying spanning distributed structure called Destination-Oriented Directed Acyclic Graph, DODAG for short [START_REF] Martin | Distribution of the time through a directed, acyclic network[END_REF]. DODAGs are bi-directional spanning data structure in which each edge is given an orientation, so that the resulting graph contains no loop, and has exactly one root: a node with only incoming edges from its neighbors. Less popular than other spanning data structures like virtual rings or spanning trees, DODAGs are nonetheless more general and adaptable than trees, since they do not need to distinguish one neighboring node as unique parent. Furthermore, they are particularly desirable in wireless networks because they allow multiple communication paths from every node to one single sink, thus limiting congestion and supporting link failures, as opposed to rooted spanning trees. As a matter of fact, DODAGs are the basic structures used in practice by RPL (Routing Protocol for Low power and lossy networks [START_REF] Winter | RPL: ipv6 routing protocol for low-power and lossy networks[END_REF]), which is the standard routing protocol for IPv6-based multi-hop wireless sensor networks [START_REF] Thubert | Routing for rpl (routing protocol for low-power and lossy networks) leaves[END_REF]. By contrast with rooted spanning trees, DODAGs allow the nodes to have more than one single parent, which drastically increases the difficulty to implement the DFTC.

Another quality of our algorithm is that is works under the unfair scheduler, the most powerful distributed scheduler. Roughly speaking, a scheduler is considered as an adversary which tries to prevent the protocol to behave as expected. The more powerful the scheduler is, the more it can prevent the algorithm to work correctly. The nuisance power of the scheduler is modeled by the notion of fairness. The scheduler is considered to be fair if it cannot prevent forever a node to execute an action (if it has one to execute). By contrast, the unfair scheduler can prevent forever a node to execute an action, unless if it is the only node able to execute an action.

Finally, we show that our algorithm is optimal in terms of space complexity. Meaning that, for every n-node network, no token passing algorithm can use less than Ω(log log n) bits of memory per node, even given a rooted spanning tree and even without considering selfstabilization.

Outline of the paper.

In Section 2, we describe the distributed systems and the model in which our self-stabilizing DFTC algorithm is written. Section 3 describes our algorithm. Due to the lack of space, the details of the correctness of our algorithm and the proof of space optimality are postponed in the appendix. However, both are sketched in Section 4. Finally, we make concluding remarks in Section 5.

Model and definitions 2.1 Algorithm syntax and semantics

A distributed system is formalized by a n-nodes graph. When two nodes u and v are able to communicate with each other, this bi-directional communication is represented by an edge between u and v. The nodes u and v are said to be neighbors. A distributed system is semiuniform if only one node is designated to have a particular role, in this paper we call this node root. In a distributed system, all the nodes have the same code, in semi-uniform system the root can have a different code. Let us formalise the semi-uniform distributed system, by an n-node graph G = (V, E, r), where V is the set of nodes, E is the set of edges, and r is the root. We consider an id-based system, where every node has a distinct identifier. Note that, like in a classical distributed system, the identifiers are not consecutive between 1 and n, but are taken in [1, n c ] where c > 1 is a constant. A system is said anonymous if nodes do not have identifiers.

Space-complexity in self-stabilization considers only mutable memory, the memory whose content changes during the execution of the algorithm. Mutable memory includes the space allocated for algorithm variables. On the other hand, the content of the non-mutable memory does not change during the execution. It typically stores the code, the constants (including the port label set, if any), and the node identifier. Therefore, IDs size is not a part of the space-complexity.

Each node contains variables and rules. Variable ranges over a domain of values. The variable var v denotes the variable var located at node v. A rule is of the form [START_REF] Edsger | Self-stabilizing systems in spite of distributed control[END_REF]:

⟨label⟩ : ⟨guard⟩ -→ ⟨command⟩
A guard is a boolean predicate over node variables. A command is a set of variable-assignments. A command of a node u can only update its own variables. On the other hand, u can read the variables of its neighbors. This classical communication model is called the state model.

An assignment of values to all variables in the system is called a configuration. Let Γ be the set of system configurations. A rule whose guard is true on one node u in some system configuration γ ∈ Γ is said to be enabled on u in γ. Similarly, u is said to be enabled in γ. The atomic execution of a subset of enabled rules (at most one rule per node) results in a transition of the system from one configuration to another. This transition is called a step. A run of a distributed system is a maximal alternating sequence of configurations and steps. Maximality means that the execution is either infinite or its final configuration has no rule enabled.

Schedulers

The asynchronism of the system is modeled by an adversary (a.k.a. scheduler ) which chooses, at each step, the subset of enabled nodes that are allowed to execute one of their rules during this step. Those schedulers can be classified according to their characteristics (like fairness, distribution, ...), and a taxonomy was presented in [START_REF] Dubois | A taxonomy of daemons in self-stabilization[END_REF]. In this paper, we assume an unfair asynchronous scheduler. Unfairness means that even if a node u is continuously enabled, then u may never be chosen by the scheduler, unless u is the only enabled node. Asynchronous implies that during a computation step, if one or more nodes are enabled, then the scheduler chooses at least one (possibly more) of these enabled nodes to execute an action. This scheduler is the most challenging since no assumption is made on the subset of enabled nodes chosen by the scheduler at each step.

Self-Stabilization

A predicate is a boolean function over the set of configuration Γ. A configuration γ ∈ Γ satisfies some predicate R, if R evaluates to true for γ. Otherwise, γ violates R. We define a special predicate true as follows: for any γ ∈ Γ, γ satisfies true. We use the terms closure and attractor in the definition of stabilization. Given a predicate R, provided that the system starts from a configuration in Γ satisfying R, R is said to be closed for a certain run r, if every configuration of that run satisfies R. Given two predicates R 1 and R 2 over Γ, R 2 is an attractor for R 1 if every run that starts from a configuration that satisfies R 1 contains a configuration that satisfies R 2 .

The specification SP P of a problem P is a predicate over runs of the system, which describes a specific behavior of the system. A distributed algorithm A solves a problem P under a certain scheduler if every execution of A under that scheduler satisfies the specification of P .

Definition 1 (Self-stabilization)

A distributed algorithm A is self-stabilizing for a specification SP P if there exists a predicate R for P such that:

• (Convergence) R is an attractor for true,

• (Closure) Any run of A starting from a configuration satisfying R satisfies R.

DODAGs

We assume that each edge {u, v} ∈ E is a bidirectional communication link provided with an orientation, from u to v, or from v to u, so that the resulting directed graph forms a Destination-Oriented Directed Acyclic Graph [START_REF] Martin | Distribution of the time through a directed, acyclic network[END_REF] (DODAG), i.e., a Directed Acyclic Graph (DAG) with a unique root (see Fig. 1). Such orientation assumption is similar the one that

R A B C D E F Figure 1: A DODAG.
assumes a consistent global orientation of a (virtual) ring-each node locally knows how to distinguish between its right and its left neighbor-, or of a spanning tree-each node knows locally how to distinguish between neighbors that do and do not belong to the spanning tree, and among those that do belong to the tree, between its descendants and a single parent.

Consider an oriented edge from node u to node v of the DODAG, we said v is the parent of u and u is the child of v. Thus each node v has two sets of neighbors, the set of parents and the set of children. Note that unlike in tree topologies a node can have several parents-refer to Appendix A, Subsection A.1 for the formal definitions.

Bit-by-Bit Communication of Identifier

In S, nodes cannot communicate information to one single neighbor without using the fact that identifiers are, at least locally, unique (this is formally proven in Section C.4). In other words, nodes must communicate their identifier stored in the immutable memory to their neighbors to address information to a unique neighbor. The size of an identifier is Θ(log n) bits, while we aim at designing a sub-logarithmic algorithm. To reach a Θ(log log n) memory, [START_REF] Blin | Compact deterministic self-stabilizing leader election on a ring: the exponential advantage of being talkative[END_REF] make the nodes communicate their identifier by smaller pieces, more precisely bit by bit. They define a function called Bit v (i), which returns the position of the i th most significant bit equal to 1 in id v . In this paper, to achieve Θ(log log n) bits of memory per node, we use a similar Bit v (i) function as [START_REF] Blin | Compact deterministic self-stabilizing leader election on a ring: the exponential advantage of being talkative[END_REF] (Appendix A.2).

Algorithm

Our token circulation algorithm is based on a perpetual Depth-First traversal from the root r to the other nodes of the network. The classical DFS algorithm can be summarized as follows: first r has the token, then, the token is given to one unvisited neighbor v of r, which becomes r's child and r becomes v's parent. Node v then sends the token to one of its unvisited neighbors, and the token keeps being given from node to node until it reaches a node w such that w has no unvisited neighbors. At this point, node w sends the token back to its parent, which resumes the process of selecting unvisited neighbors. This traversal continues until all nodes in the network have been visited and the token is returned to the root node r. We focus on DODAGs, so a node v with the token selects the next node in the DODAG traversal among its children, rather than among all of its neighbors. From a local point of view, the tasks for a node v are as follows: receive the token from a node p, check whether it has any unvisited children, and if so, pass the token to one of them; if not, send the token back to its parent p.

So the self-stabilizing implementation of the DFS token circulation relies on several key concepts, including the presence or absence of the token, the identification of unvisited and visited neighbors, the selection of an unvisited neighbors, and the recording of the neighbor from which the token was received (i.e., the parent).

In order to prevent token loss or duplication, the circulation of unique token cannot occur in a single step and requires acknowledgment messages. A node v must inform node u that it is sending the token, and once u has confirmed receipt, v must delete the token. If v sends the token but does not verify that u has received it, the token may be lost. If u receives the token but does not verify that v has deleted the token, the token may be duplicated.

In this work, we consider the problem of token circulation in networks with sub-logarithmic memory available in each node. Storing identifiers in variables is not feasible, as a result, selecting the next unvisited child to receive the token becomes a non-trivial task that cannot be achieved in a single step. To address this, we propose a negotiation step where the node with the token interacts with its unvisited children. During this step, each child announces its identifier piece by piece, and the child with the largest identifier wins the negotiation. We also account for unvisited children who did not win the negotiation by proposing a mechanism to ensure that they will be visited later. Self-stabilizing algorithms must be able to detect and correct inconsistencies locally caused by transient faults. One fundamental idea in the design of our algorithm is to minimize the frequency of node repairs. Firstly, the algorithm is already highly complex due to the numerous tasks that nodes must execute to achieve fair token circulation. Introducing additional rules to repair inconsistent situations would complicate both the algorithm and its proof. Secondly, in most cases, it is unnecessary to repair nodes as the token will eventually circulate in the network if the algorithm is resilient enough. The presence of the token and the rules for fair executions will allow the network to stabilize. However, there are some exceptions, i.e., repairing rules that are necessary for convergence.

To summarize our approach, let us introduce an informal algorithm (see Figure 2) that describes the steps of the algorithm for a node v.

Algorithm 1: Local DF S(v)

if The token is present and some inconsistency is detected then

Release the token and consider that the token is in one of your descendants else if Received token from the parent then -Switch as a visited node; -Wait for parent to release the token;

if Received token from a visited child then Wait for child to release the token;

if v has the token and nobody in its neighborhood has a token then if ∃ unvisited children then while ∃ more than one unvisited child which are candidates to receive the token do -Ask all the candidates unvisited children for a piece of their IDs; -Publish the strongest piece; -Wait for all the candidates which do not have the strongest piece to declare themselves losers; -Send the token to the winner; -Wait for the winner to receive the token; -Ask the losing unvisited children to be ready for the next negotiation; -Wait for the update of the unvisited children; -Release the token; else -Send the token to the parent; -Wait for the parent to receive the token; -Release the token;

Variables

Before presenting the rules of our algorithm, let us first introduce the four variables it uses.

Visited and Unvisited Children. Nodes have to remember which of their children have already been visited in order to either send the token to unvisited children or to send it back to a parent. Classically, we implement this with a boolean variable color :

c v ∈ {red, green}
Visited nodes are nodes that have the same color as the root. Nodes change from the state "unvisited" to "visited" (during a traversal initiated by the root) by changing their color upon receipt of the token, detailed bellow. The choice of the next child to be visited is based on the identifier of the unvisited children of the token holder: the chosen child is the one with highest identifier. As a consequence, the circulation of the token always follows the same traversal path, depending on the relative order of the identifiers in the DODAG. Let us consider a node v with the token, and choose one of its unvisited neighbors u and sends the token to it, and so on to a node w surrounded by visited nodes. The node w sends the token back to its parent w p which sends it to one of its unvisited children. The process is repeated until all nodes are visited, and the token returns to the node r. By construction the DFS token circulation is fair, since the unvisited nodes become visited exactly once. When the root r has no unvisited children, r switches its color to the other value (from red to green for example). Immediately, all the visited nodes become unvisited, for they now have the opposite color of r. This guarantees that this fair token circulation is perpetual. Only one operation, denoted by c v := ¬c v , is used in this variable, which is switching its value from red to green and vice versa.

State of the Token. To achieve atomicity of the operations required to maintain the network in a consistent state, we need to define a variable which takes eight different values.

tok v ∈ {⊥, ⋆, •, ⇊, ⟲, ↓, •, ↑}
Let us give some explanations on those different values. The state tok v = ⊥ corresponds to nodes that are away from the current token circulation. For example, when the root has the token, all the other nodes are such that tok v = ⊥. Reciprocally ⊥ is a value that cannot be taken by the root, which would mean that no token is circulating in the network.

When a node that is not involved in the current token circulation receives the token from its parent, it simultaneously switches it color, and switches its token value to tok v = ⋆. This value corresponds to the moment when a node receives the token from its parent, which is supposed to happen exactly once in each circulation round.

When the parent of v has finally left the token (recall that such operations are not atomic), v can start negotiating with its children to decide to which one it will send the token. To do that, it sets tok v = •, and keep that state until one winner is elected.

Once a winner u is elected i.e. when all nodes of a different color than v have declared themselves losers, u excepted, v updates tok v =⇊ to offer the token to one of its children. After that, the child u that won the negotiation can update its own variable tok u to ⋆.

After its child u took the token, v updates its variable to tok v =⟲, to let its children which lost the negotiation reset their variable in order to be ready for the next negotiation, when v will receive back the token from u.

When all the children of v have finished resetting their variable, v sets tok v =↓, which indicates that it is a node involved in a token circulation, but that the token it had is below it, to one of its descendants. After u has finished the token circulation below it, it sets tok u =↑, to send the token back to v. If nothing wrong happened, v has only one child with a value tok ̸ = ⊥ at that moment, and therefore can take the token. To do so, it updates tok v = •, and then waits for u to effectively drop the token, by setting tok u = ⊥. After that, v restarts a negotiation, setting tok v = •. After some time, v has no more children of a different color. When this happens, v offers the token to its parent w by setting tok v =↑. Before effectively dropping the token, v waits that w acknowledges the token by updating its variable to tok w = •, but it also waits for all of its children to update their variable linked to the negotiation.

Indeed, in the current situation, all the children of v have successively won the token. As explained above, those nodes are prevented from taking one token of another color, to avoid livelocks. But now, the circulation of the token of v is terminated, so this becomes irrelevant. Worse, if nodes do not reset their variable to a value that allows them to negotiate, then they will all be ignored when a token from another color will come the next round. When all the children of v have reset their variable, v finally drops the token, and sets tok v = ⊥.

Remark that for a node v with tok v / ∈ {⊥, ↓}, there is a strong pressure on the possible values of tok u , where u us a child of v, and most combinations are actually not supposed to occur in an execution. To summarize the Figure 3 represents the order between the different states taken by the variable tok.

Negotiation Variables: Bit-by-Bit Communication. To determine which of its children will receive the token, the parent progressively eliminates them, until only one remains. When it has exactly one child running for the token, it can finally declare that it gives the token. All the children that were eliminated ignore that message, and the one winner can take the token from its parent, and therefore no duplication of the token can occur.

The elimination process relies on the identifiers of the children, and on one additional variable which allows unvisited nodes to declare themselves as negotiating, or as losers of the negotiation.

Step by step, the parent asks for the value of the i-th bit of the identifier of its children, and when all have answered, it reveals the biggest value it sees. All the nodes that have not announced this value consider themselves as eliminated until their parent allows them to negotiate again. This moment, when the parent allows its children who lost the election to negotiate again happens immediately after the winner of the election takes the token.

To negotiate for the token, nodes send bit-by-bit the value of their identifier to their parent. Two variables are required for that. The first one, ph, is used to communicate the position of the bit that is currently asked. It takes values between 1 and N , where N is the largest length of an identifier in the network, and thus N ∈ O(log n). The second variable is b, and is used to communicate the value of the bit that each child has, and for the parent to communicate the highest value it has seen. The variable b v is used to communicate the values given by function Bit v . It takes values in {0, 1, ⊥}, where ⊥ is the value that corresponds, for children, to the absence of a bit at that position (the identifier is too short), and, for the parent, to the request of the value of the bit. For simplicity, we denote the tuple (ph v , b v ) by the notation id v . Figure 4: Process of the designation of one child to give the token to. The parent reveals the biggest bit announced, then the children with small identifiers quit the negotiation, and in the end the winner takes the token and the losers are ready to negotiate again.

The general scheme is the following: first the parent sets id v = (1, ⊥). Then all the children answer with the value of their first bit, by setting id u = (1, Bit u (1)). After all the children have answered, v sets id v = (1, b) where b is 1 if v saw a 1 in its children, and 0 otherwise. Then, all the children that do not have answered (1, b) lose the negotiation. After all losers have left the negotiation, v sets id v = (2, ⊥), and so on until only one node remains.

Negotiation Variables: State in the Negotiation Process. In addition to the identifier variables ph and b, we need a variable to remember where each node is in the negotiation process. This variable is denoted by play and takes four values:

play v ∈ {P, L, W, F}
Nodes v such that play v = P are the nodes that are available for a negotiation process with any of their parent that has a different color. They are the only nodes which can participate to a negotiation, the others have either already won, or lost. Note that P also stands for players.

When a node v loses the negotiation, it sets play v = L, and thus becomes a loser, and is not involved in the current negotiation process anymore.

When a node v wins the negotiation and receives the token, it updates its color, its variable tok v , and it also updates play v to W, to signify that it won a negotiation. After that, and until its parent sends the token back to its own parent, v won't negotiate with any of its parents. This guarantees that whatever the initial configuration of the system, v will not create oscillations between two tokens, and therefore no livelock.

However, the color is not sufficient to prevent livelocks or deadlocks caused by multiple circulating tokens. Indeed, even assuming only two tokens, one can design pathological configurations, and especially if the two tokens are of different colors. What we must absolutely prevent is situations in which one node alternatively takes a red token from one parent, sends it back later, then switches color and takes the green token from its other parent, sends it back, and then takes the red one again, and so on. With two such children, we can design scenarios where the tokens are in a livelock, and the circulation is blocked.

Note that nodes can neither simply ignore the token, for it would create a deadlock: both token would be blocked. To avoid such situations, we force a node that has received the token from one of its parents to not being available for a new token until this parent has sent the token back to its own parent. This requires being more subtle in how we define the election-related variables on the children.

As a consequence, we need the fourth value F to overcome a tricky situation. Recall that when a node u sends back the token to its parent w, it first waits for its children who won the negotiation (i.e. such that play v = W) to reset their variable play v to P, so that they will be able to negotiate during the next circulation round. But in triangle configurations, it might be that one such node v with play v = W has a common ancestor, with its parent u, as depicted in Figure 5. In such a situation, v should not update play v = P. Indeed if it does, then from w's perspective, it is exactly as if we never introduced the value W: it has one child who won the token and is at P. In particular, we can now create a livelock at the level of w.

But v can neither keep its value at W. That would create a deadlock with its parent u. Therefore, v fakes resetting its variable play v , by setting it to F, which is understood by its parent with tok u =↑ as a P value, but both v and its grandparent w do recall that v has already had the token. This requires that as soon as possible, node v update its variable play v = W, otherwise it could miss the opportunity to eventually reset its variable at P, notably if w sets tok w =↑. Although the alternating between two colors and the state play v = W share the common goal, which is to prevent a node to have several times the token, they are relevant in totally different situations. The alternation between two colors is built to prevent a node from receiving twice the same token, from parents that might be totally unrelated in the DODAG. On the other hand, the value W prevents a node from oscillating between two colors, from two different parents, which would block the circulation of the token.

↓, W ↑, W ⊥, W ⊥, W w u v •, W ↑, W ⊥, F ⊥, P w u v •, W ⊥, W ⊥, F ⊥, P w u v •, W ⊥, W ⊥, F ⊥, P w u v

Rules of our algorithm

Due to the lack of space, the formal descriptions and subtleties of the rules of our algorithm are reported in Appendix B. Figure 6 presents how the different rules follow each other during the execution of the algorithm, one rule, specific to the root is not presented ni this section. For the sake of readability, we have grouped the rules according to the task to which they relate: error handling, negotiation to choose the unvisited child, returning the token back to the parent, sending the token to a child.

Error. As hinted above, some combinations of the variable tok should not occur on a node and its children. To repair such errors, the principle is that the parent trusts its child, in the sense that if both v and u believe they have a token, then v forgets its token, and repairs itself by setting tok v =↓, acknowledging the fact that there is a token below it. The illegal pairs are detected by the predicate Er(v) and the correctness of the state of the token of node v is handled by Rule E TrustChild . All the other rules of the algorithm suppose that node v is not in such an error. For homogeneity and readability, we constrained the other rules with ¬Er(v).

Negotiation. In a negotiation, two types of nodes are involved, the parent v which owns the token, and the unvisited children involved in the negotiation (we call these children "players" formally defined by the set Players(v)).

Before describing the negotiation itself, let's explain how the nodes involved in the negotiation can leave it. The parent can leave the negotiation phase in two ways. The first is captured by Rule R OfferUp , when the parent observes that the set of players(v) is empty, which means that it has finished circulating below itself. As a consequence, v returns the token to its own parent (tok v =↑). The second possibility happens when node v has exactly one child u in Players(v), after verifying some tricky problems (see Appendix B), v can send the token to u, to achieve that, v puts tok v :=⇊, thanks to Rule R Give . The first action that v takes, after u has actually received the token, is switching its variable tok to ⟲ to inform its other unvisited children who lost the negotiation (aka the losers) that the negotiation phase is terminated, this is made by Rule R NewPlay . So the losers can change theirs variables play w = P and become players again when v will receive the token back (see Rule R ReplayD ). Let us now consider the children u ∈ Players(v), u quits the negotiation if it quits Players(v). The node u can do this in three ways, u detects an inconsistent behavior in his neighborhood (see Rule R FakeWin ), u wins negotiation (see Rule R Win ), u loses in the negotiation (see Rule R Lose ). Now let us focus on the negotiation itself. When a node v has finished receiving the token (i.e., the parent of v has released the token tok p(v) =↓, Rule R Drop ), it can begin the negotiation (execution of Rule R Nego ). When all players have announced their binary value (see Rule R NewBit ), v announces the highest value (see Rule R maxPos ). After that, some players lose the negotiation and others remain players. If there is only one player left, the negotiation is over, otherwise v continues the negotiation (see Rule R NewPh ).

Reception of the Token from a Child. Now consider the actions when a child u offers the token to its parent v by setting tok u =↑. The node v needs to be sure that it does not have any other children involved in a token circulation. If it has, then taking the token would lead to an inconsistent configuration, where one token is above an other one. Actually, u may have several parents related to each other, and only the deepest should take the token. If v can take the token, it executes the Rule R Receive signifying to u that it has taken the token. Thus, when u is sure that v has taken the token, u can release the token and v can resume negotiating with its remaining players (Rule R ReNego ).

End of the Circulation. After it has offered the token to its parent, a node v which is not the root should eventually drop the token, and set tok v = ⊥ (Rule R Return ). Before that, it must check that all its children have correctly updated their variable from W to P to assure that when a token of the other color will come, all those nodes will be available for a negotiation phase.

In a similar situation, where all of its children have repaired themselves, the root does not drop the token, for it would simply destroy it. When the root is in such a situation, it means that the current circulation round is terminated, and one other can start. To achieve that the root changes its color, and thus if the circulation has already stabilized, the root has one color and all the node have the other color (i.e. all the other nodes are unvisited).

Let us consider a node v having parents that are sending the token higher and no other parent involved in a token circulation. If a node v is not ready to play again, then v cleans its variable play v to be ready for the next circulation round (Rule R ReplayUp ).

If v has some parents sending the token higher, and other parents which do not have terminated their token circulation, it must update its variable play v = F (Rule R Fake ).

Finally, we must design a rule to cancel the effect of updating one's variable at F, to reset it at W, without Rule R ReWin , the token could not be sent higher.

To summarize. Figure 6 presents the scheme of an execution of our algorithm. It presents the update of the variables of one node v by the different rules of our algorithm.

⊥, W ⊥, F ⊥, P ⊥, L ph, b , W •, W , W , W ↓, W •, W ↑, W RNewBit RWin RLose RReplayD RFake RReWin RNego RGive RmaxPos -RNewPh RFakeWin RReplayUp R F a k e W i n

RNewPlay

RDrop RReceive RReNego ROfferUp RReturn Figure 6: Chain of the states taken by a node during the execution of the algorithm. The update of c v is represented by color gray. Rules in blue corresponds to the negotiation. Rules in red correspond to the sending of a token from a child to a parent. Rules in black correspond to the sending of a token from a parent to a child.

Correctness

Due to the lack of space, the details of the correctness of our algorithm are postponed to Appendix C, but let us draw here a roadmap of it. We prove that our algorithm is a selfstabilizing algorithm for the token circulation problem, and we also prove that it is optimal in terms of memory, i.e. that any algorithm solving T C in S requires Ω(log log n) bits per nodes, even under less general hypothesis than ours.

This correctness is subdivided into four parts. First, we establish that maximal executions of our algorithm are infinite (Appendix C.1). Formally, we prove that in any configuration, there is at least one enabled node. This part of the proof is static, in the sense that we do not need to consider an execution of the algorithm but only isolated configurations. It boils down to a syntactical analysis of the guards of the rules of our algorithm (Algorithm 2), and to an induction for one specific case.

Although the previous does not need to consider executions, the two following parts of the proof are trickier. We aim at proving that eventually, one token fairly circulates in the network, in a self-stabilizing way. Therefore, we have to consider configurations in which several token exist in the network. To do so, we introduce a ad hoc structure which corresponds to the paths from the root to the tokens in the network, which is a DODAG. More precisely, it is a sub-DODAG of the DODAG representing the network. But there may exist some tokens that are not connected to the root by an admissible path. For these tokens, we also define this sub-DODAG structure, but we distinguish these tokens by saying that they are not pointed by the root. All the reasoning of the two following parts rely on these sub-DODAGs structures.

Secondly, we establish at once two crucial properties for the validity of our algorithm (Appendix C.2). The first property is that if a token is not pointed by the root of the network, then it can only circulate a finite number of times before being blocked, or deleted. This guarantees that no scheduler, even unfair, can create an execution in which the token pointed by the root is never activated. The second property is that even the token pointed by the root is restricted in its circulation, in the sense that it can only circulate a finite number of times before it reaches the root again, and the root "resets" it by the execution of a rule specific to the root, R r NewDFS . The combination of these two properties, and of the liveness established in Appendix C.1 leads to the guarantee that there is an infinity of finite circulations in any maximal execution of our algorithm. To prove both properties, we define a potential function, which associates a positive value (a weight) to each token in any configuration. Then, we establish that any computing step decreases the weight of the token, unless the token is reset by an execution of R r NewDFS . This establishes that a token cannot circulate indefinitely, since any step it takes makes a positive quantity decrease, unless this token is anchored at the root and there are an infinity of new circulations. Since we also prove that no token can be created, this guarantees that at some point, although several tokens may exist, only one is activated, the one which is pointed by the root.

Thirdly, we establish that our algorithm behaves correctly (Appendix C.3). By "behaves correctly" we mean that the token eventually fairly visit all the nodes of the network. To establish that, we largely use the previous results. In particular, we start the reasoning at a moment where the algorithm has already partly converged, in the sense that all the tokens except the one pointed by the root are not activated anymore. Then, we first establish some additional stability properties on the underlying structure of the DODAG which corresponds to the path from the root to the token. Then, after having properly defined what "to have the token" is, we establish that if one node receives the token from one of its parent, then all of its children that are able to receive the token will actually receive it at some point. On the other hand, we prove that if some children of one such node cannot receive the token, then after one or two additional circulations of the token, then these children will be able to receive it, and by the previous, will receive it. Therefore, circulation after circulation, the token visits nodes in deeper and deeper parts of the network. By induction, we finally prove that the token eventually fairly visits all the nodes of the network, indefinitely. In particular, this guarantees that all the other token were reached by the token pointed by the root, and merged with it.

Joined, these three first parts of the proof establish that our algorithm is a self-stabilizing algorithm for the fair token circulation in arbitrary DODAGs.

Finally, we extend the results of [START_REF] Blin | Optimal space lower bound for deterministic self-stabilizing leader election algorithms[END_REF] to prove that the space complexity of our algorithm is optimal (see Appendix C.4). More precisely, we prove that no algorithm can solve the fair token circulation problem using o(log log n) bits of memory per node, even under least challenging hypothesis than ours. We prove that even under a central strongly fair scheduler, or a synchronous scheduler, on a tree topology, and without the requirement of being selfstabilizing, no algorithm can solve the fair token circulation problem in anonymous network. The result established in [START_REF] Blin | Optimal space lower bound for deterministic self-stabilizing leader election algorithms[END_REF] concludes to the space optimality of our algorithm.

Conclusion

In this paper, we have presented a memory-optimal self-stabilizing algorithm for the fair token circulation in arbitrary DODAGs under the unfair scheduler. Our algorithm works in the state model where no information is given on the neighbors, and requires only Θ(log log n) bits per node. To our knowledge, this is the first self-stabilizing algorithm achieving this space complexity in this model for graphs of arbitrary degree.

Of course, the construction of a DODAGs with the same space complexity remains an open question. Beyond the issue of DODAGs, our algorithm is providing hope that it might be possible to design self-stabilizing token circulation algorithms for arbitrary networks with space-complexity O(log log n) bits per node. The design of such algorithms requires to overcome at least two problems: the presence of more than one root, and the symmetry caused by the presence of cycles. The presence of multiple roots is an issue which may not be too dramatic, as it may be possible to let several tokens circulate, one per root, and to remove the tokens one by one until a single token remains. The symmetries caused by the presence of cycles appear to cause severe difficulties, and our current knowledge is insufficient to guarantee that a space-complexity of O(log log n) bits per node can be achieved under such symmetries.

Such an algorithm with space-complexity Θ(log log n) bits per node, solving token circulation on arbitrary graphs would be a valuable toolbox which could be used to solve other problems, such as leader election, spanning tree construction, etc.

A Appendix on Model and formalisations A.1 DODAG formalisation

Let us be more formal: Definition 2 (Destination-Oriented Directed Acyclic Graph, DODAG)

A DODAG is a tuple D = (G, →) where G = (V, E) is a graph and → is a relation between the nodes of G which:

• covers the edges of G: (u → v ∨ v → u) ⇐⇒ {u, v} ∈ E,
• is acyclic: there does not exist any path from one node v to itself w.r.t. →, and

• is rooted: there exists one node r ∈ V such that ∀v ∈ V, v → * r.
The nodes of D are V , and the edges of D are →. By the acyclic property, such a node r is unique, and is called the root of D. Also by the acyclic property, for any edge {u, v} ∈ E, we have either u → v or v → u but not both.

In practice, the relation → is implemented at the layer of the local port numbers of the nodes. A DODAG is a graph in which the port numbers can be split into two disjoint sets port + and port -, and the relation → is defined by

u → v ⇐⇒ port u (v) ∈ port + .
In the latter, we often need to consider, on one node v, the set of its neighbors that precedes it, and the set of neighbors that it precedes. We call those sets the parents and the children of the node, by analogy with the lexical field relative to trees.

Note that contrary to what is possible in trees, nodes may have several parents in DODAGs.

Definition 3 (Parental Relationships in a DODAG)

Let D = (G, →) be a DODAG. We call parents of v in D the set P(v) = {u ∈ N v : v → u}. We call children of v in D the set C(v) = {u ∈ N v : u → v}.

Remark 1

The information of the set of the parents of each node is equivalent to the information of the relation →. In practice, we define a DODAG by the parental relationship it induces more than by expliciting the relation →.

It will be useful in the latter to reason on sub-structures of the DODAG in which our algorithm is executed. In most cases, the sub-structures considered also have the desirable property of being DODAGs. A sub-DODAG of D is any DODAG whose nodes and edges are a subset of those of D.

Definition 4 (Sub-DODAG of G, Anchor ) A tuple D ′ = (G ′ , → ′ ) is a sub-DODAG of D = (G, →) if • D ′ is a substructure of D: (V ′ ⊆ V ) ∧ (→ ′ ⊆→) ∧ (→ ′ ⊆ V ′ × V ′ ). • D ′ is a DODAG
Remark that the root of D ′ may not be the same than the root of D. To avoid being misleading, we call the root of a sub-DODAG an anchor.

Remark 2

Following what was stated in Remark 1, we will not use relation → ′ to define sub-DODAGs in practice, and rather use the underlying set of parents and children, P D ′ and C D ′ .

One typical example of sub-DODAG is the restriction of the DODAG to the nodes which can reach one particular node (other than the root) in (G, →).

Definition 5 (G a DODAG under a)

Let (G, →) be a DODAG, and let a ∈ V . We denote by V a the nodes that can reach a by →: V a = {v ∈ V : v → * a}. We denote by E a and → a the restrictions of E and → to nodes of V a :

E a = E ∩ P 2 (V a ) and → a =→ ∩(V a × V a ).
We denote by (G a , → a ), or simply G a , and call the DODAG under a, the sub-DODAG Although DODAGs are the structure in which our algorithm and our proofs are established, it is often simpler to reason on linear structures than on DODAGs. In the latter, we will consider branches of DODAGs, which are descending paths from one node to one of its descendants.

((V a , E a ), → a ).

Definition 6 (Branch of a DODAG)

We call branch of a DODAG D = (G, →) a path of nodes in D (which is a path of nodes in G w.r.t. →). For the sake of readability, we denote branches by starting at the highest node. For example, if w → v → u is a path in D, then we say that uvw is a branch of D.

We denote branches by the letter B.

A branch B = v 0 v 1 . . . v k of a DODAG D is maximal if v 0
is the root (or the anchor) of D, and if v k does not have any children in D.

Given a sub-DODAG of D, it will be interesting to consider the longest branches it shares with D. These longest branches are called projections of the sub-DODAG on branches.

Definition 7 (Projection of a sub-DODAG on a Branch)

Let us consider a DODAG D, and a sub-DODAG of D with anchor a, D a . Let B = v 1 v 2 . . . v k be a maximal branch of G a , the DODAG under a. In particular, v 1 = a.

We denote D a (B), and call the projection of D a on B the longest branch of D a that coincides with B:

D a (B) = v 1 v 2 • • • v j where ∀i < j, v i+1 ∈ C Da (v i ) and v j+1 / ∈ C Da (v j ) (recall that v ∈ C Da (u) ⇐⇒ v → Da ′ u). Remark 3 (DODAG ≡ D o )
In the latter, we consider different types of DODAGs, depending on their purpose. For the sake of readability, we will use D o as an alias for the classical notion of DODAG, and CD o , WD o , FD o as aliases for particular types of DODAG.

A.2 Bit-by-Bit Communication of Identifier

We use a similar technique as [START_REF] Blin | Compact deterministic self-stabilizing leader election on a ring: the exponential advantage of being talkative[END_REF], but for the sake of simplicity, we slightly modified this function for this work, and send the identifier bit-by-bit, which does not change the asymptotic complexity. Essentially, nodes do not communicate their entire identifier at once, but when asked for, they send to their neighbors the value of their i-th bit (which is 0 or 1). Although the value of the bit is 1-bit long, we must take into account the fact that the position of the bit which is asked, i, is now part of the message. This position variable i takes value between 1 and the maximal length of an identifier, which is in Θ(log n). Therefore, it is encoded on Θ(log log n) bits. To simplify, we suppose that all nodes are given a local function Bit that associates to each position, the value of the bit at this position in their identifier. If the position asked is bigger than the length of their identifier, then the function simply returns ⊥. Suppose for example that node v has identifier id v = 1011. Then we define the function Bit v by:

Bit v (i) :=            1 if i=1 0 if i=2 1 if i=3 1 if i=4 ⊥ if i > 4
Nodes keep storing their own identifier in their immutable memory, but what is communicated to the neighbors through the immutable memory is the tuple (i, bit), which requires Θ(log log n) bits. Remark that since the identifiers are globally unique, the different functions Bit are also globally unique, although they can coincide for some values of i.

A.3 Well-Founded Sets

Recall that an ordered set (M, ⪯) is well-founded if there does not exist infinite sequence of elements of M , v 0 v 1 . . . such that ∀i ∈ N, v i+1 ≺ v i . Such relations are very desirable to prove termination of algorithms, or their convergence. In the latter, we consider an arbitrary well-founded set (M, ⪯).

Given (M, ⪯), we can define an order on tuples of elements of M , which is itself well-founded when restricted to sequences of length at most k, for any k.

Definition 8 (Lexicographic Order )

For any k ≥ 1 we define the lexicographic order on M k induced by ⪯, and denote ⪯ k lex , by:

(u 1 , . . . , u k ) ≺ k lex (v 1 , . . . , v k ) ⇐⇒ ∃i ∈ [1, k] : (u 1 , . . . , u i-1 ) = (v 1 , . . . , v i-1 ) u i ≺ v i
In our proof, we are sometimes led to compare sequence of elements of M which have variable length. We extend the definition of lexicographic order to sequences of arbitrary length, which corresponds to the alphabetical order. The resulting order is itself well-founded.

Definition 9 (Alphabetical Order )

The lexicographic order on (possibly empty) sequences of elements of M induced by ⪯, is denoted ⪯ α and defined by:

(u 1 , . . . , u k ) ≺ α (v 1 , . . . , v l ) ⇐⇒    ∃i ≤ min k, l : (u 1 , . . . u i ) ≺ i lex (v 1 , . . . v i ) ∨ k < l ∧ (u 1 , . . . , u k ) = (v 1 , . . . , v k )

A.4 Token Circulation

In this article, we consider the problem of fair token circulation, which requires that one unique token perpetually circulates through the network.

The part of the specification of the token circulation problem which corresponds to the existence and unicity of the token is not complicated to state, and is basically what is made in [START_REF] Blin | Optimal space lower bound for deterministic self-stabilizing leader election algorithms[END_REF] when the authors give a specification for the leader election problem. It boils down to defining a local predicate on nodes, which represents the fact that the token is held by that node, and guaranteeing that the predicate is evaluated to true on exactly one node in each configuration. This first predicate will be denoted by T , for token.

It is a bit harder to formally specify the fairness circulation property. For a token circulation to be fair, one could expect that all nodes have the token at the same rate. But the more a node has children, the more it will receive it back from its children before sending it to its other children. We must be more specific on what fairness is. We define a more restrictive local predicate, which represents the fact that the node has the token and is allowed to use it to access the resource, the service. . . This second predicate will be denoted by R, for resource access.

Now that we have this second predicate, we only have to guarantee that, between two configurations in which one particular node has access to the resource, then all the other nodes also have it, and exactly once. In practice, the node that we consider to delimit fairness is the root. A sub-execution in which the root receives the token for access, then drops it, and then receives it back for access, is called a round, or a circulation round.

Definition 10 (Round according to R)

Let R be a local predicate, and let

ϵ = γ 0 → γ 1 → • • • be an execution. A sub-execution ϵ ′ = γ i → • • • → γ j of ϵ is a round according to R if: • ¬R γ i-1 (r) • R γ j+1 (r) • ∃i ≤ k < j such that -∀t ∈ [i, k], R γt (r) -∀t ∈ [k + 1, j], ¬R γt (r)
Note that by construction, circulation rounds perfectly follow each other in any execution.

We say that a circulation round is fair if for any node v, there exists exactly one continuous sequence of configurations in which v has access to the resource. Definition 11 (Fair Round according to R)

Let ϵ = γ 0 → γ 1 → • • • be an execution, and let ϵ ′ = γ i → • • • → γ j be a round according to R. ϵ ′ is fair if for any v ∈ V , there exist i ≤ t 1 < t 2 ≤ j such that • ∀t ∈ [t 1 , t 2 ], R γt (v) • ∀t ∈ [i, j] \ [t 1 , t 2 ], ¬R γt (v)
We can now formally define the specification of Fair Token Circulation:

Specification 1 (Token Circulation)

T C (Token Circulation) is defined by the existence of two local predicates T and R such that ¬T ⇒ ¬R.

A configuration γ is correct if it contains one unique token

U T C (γ) ≡ ∃!v ∈ V : T γ (v) An execution ϵ = γ 0 → • • • is correct if 1. All its configurations are correct: ∀i ≥ 0, U T C (γ i ).
2. ϵ is infinite and can be divided into an infinite number of rounds according to R.

All of these rounds are fair

Definition 12 (Circulation Rounds)

In the context of Token Circulation, we call Circulation Round a round according to the predicate R.

B Appendix on our Algorithm B.1 Common Sets

To define the rules of our algorithm, some sets are especially useful. An important distinction that nodes almost systematically do is the difference between their parents with the same color, and their parents with the other color.

P eq (v) = {u ∈ P(v) | c u = c v } (1)
P neq (v) = {u ∈ P(v) | c u ̸ = c v } (2)
Similarly, nodes distinguish their children with the same color from their children with the other color.

C eq (v) = {u ∈ C(v) | c u = c v } (3)
C neq (v) = {u ∈ C(v) | c u ̸ = c v } (4)
One other central set for the negotiation is the set of the nodes with whom the parent negotiates. The parent negotiates with its children that do not have the same color, and such that play u = P. A node that negotiates is not supposed to have any children u such that tok u ̸ = ⊥, and a specific rule is designed for such erroneous situations. Yet, to simplify some reasoning, we also add as a constraint the fact that v only negotiates with its children such that tok u = ⊥. In the latter, we call these nodes the players of v.

Players(v) = {u ∈ C neq (v) |tok v = ⊥ ∧ play u = P} (5)

B.1.1 Rules of the Algorithm

In this section, we present the predicates, actions, and rules of our algorithm. For the sake of readability, we have grouped the rules according to the task they relate to. In Section B.1.1, we present the rule dedicated to deal with inconsistencies of the variable tok. In Section B.1.3, we present the negotiation process, based on the identifiers of the children of the node holding the token. In Section B.1.2 we present the rules that make nodes quit that negotiation process. In Section B.1.4 we present the rules which reset variables of nodes to a proper value after the end of the negotiation process. In Section B.1.5 we present the rules that allow one node to receive the token back from one of its children. In Section B.1.6 we present the rules that are executed when one circulation below a node is terminated, whether the node is the root or another node. Finally, in Section B.1.7, all the rules are gathered to allow an easy access during the reading of the proofs.

Error As hinted above, some combinations of the variable tok should not occur on a node and its children. In general, a node v that has the token, or which is very near a token, i.e. with tok v ∈ {⋆, •, ⇊, ⟲, •, ↑}, should only have children u with tok u = ⊥, with a few exceptions. Indeed, if tok v ∈ {⇊, ⟲}, then v is allowed to have a child such that tok u = ⋆, the child to which it just gave the token.

If tok v = •, then v is allowed to have a child such that tok u =↑, the child from which it is receiving the token.

One other exception is when tok v =↑. In this case, v is sending the token back to its parent, which means that it is on its way to set tok v = ⊥. We do not consider any error for such nodes, since it would not be very effective, and could create an error at the level of its own parent.

To repair such errors, the principle is that the parent trusts its child, in the sense that if both v and u believe they have a token, then v forgets its token, and repairs itself by setting tok v =↓, acknowledging the fact that there is a token below it.

The illegal pairs are detected by the predicate Er(v) and the correctness of the state of the token of node v is handled by the rule E TrustChild .

Er(v) ≡ tok v ∈ {•, ⋆} ∧ ∃u ∈ C(v) : tok u ̸ = ⊥ ∨ tok v ∈ {⇊, ⟲} ∧ ∃u ∈ C(v) : tok u / ∈ {⊥, ⋆} ∨ tok v = • ∧ ∃u ∈ C(v) : tok u / ∈ {⊥, ↑} -→ tok v :=↓ (6) E TrustChild : for all v ∈ V Er(v) -→ tok v :=↓
All the other rules of the algorithm suppose that node v is not in such an error. For homogeneity and readability, we constrained all rules with ¬Er(v), even rules which suppose that tok v ∈ {⊥, ↓, ↑}.

B.1.2 End of the Negotiation Phase

Before showing how the negotiation phase is implemented, let us first explain how nodes may quit this phase. In a negotiation, two types of nodes are involved, the parent v which has the token, such that tok v = •, and the children u elements of Players(v).

The parent can quit the negotiation phase by two means.

Rule R OfferUp The first one is when the parent observes that all of its children in Players(v) have been visited, which means that it ended the circulation below itself. When this happens the parent sends the token back to its own parent. Before doing so, the parent must first be assured that it is not in a situation as depicted in the last configuration of Figure 5. If v has a child u such that play u = F, then it is a node which actually won the token, but faked being reset to P to another parent p such that tok p =↑. If v is the last parent of u, and switches tok v =↑, then u will never be reset to P, which breaks the fairness of the token circulation. Therefore, before executing this action, v waits that all of its children have quit the value F.

The predicate WaitSib corresponds to this requirement.

WaitSib(v) ≡ ∃c ∈ C eq (v) : play c = F (7) R OfferUp : for all v ∈ V ¬Er(v)∧tok v = •∧¬WaitSib(v)∧(∀u ∈ C neq (v) : play u ∈ {W, F}) -→ tok v :=↑
Note that even if the root has no parent, it may execute rule R OfferUp when it does not have any more children to visit. Since some operations subsequent to having finished circulation below oneself are identical for the root and the other nodes, we factorize the rules as far as possible.

Rule R Give The second possibility for a parent to quit the negotiation is to decide to offer the token to one of its children. This happens when node v has exactly one child in Players(v).

But there is one other situation to which we must give attention. Suppose that due to a wrong initialization of the network, no node belongs to Players(v), but the circulation is not over yet, for one or several children of v are losers, i.e. play u = L. In this situation, node v needs to reset the variable play of these children to P, and then will perform a negotiation between them. One simple way to do that is to follow the transition diagram of tok depicted in Figure 3. No child of v will take the token offered by tok v =⇊, but immediately after, when tok v is set to ⟲, the losers will update play u = P, which will allow a further negotiation process.

Actually, v basically executes a full round of its variable tok just to refresh its wrongly initialized children. Note that this may only be caused by a corrupted initial configuration, and that after convergence, this part of the rule becomes useless.

The predicate Give describes the situations in which node v ends the negotiation by sending the token to one of its children.

Give(v) ≡ |Players(v)| = 1 ∨ (|Players(v)| = 0 ∧ ∃u ∈ C neq (v) : play u = L) (8) R Give : for all v ∈ V ¬Er(v) ∧ tok v = • ∧ Give(v) -→ tok v :=⇊
Let us now consider the children u ∈ Players(v). A child quits the negotiation if it quits Players(v). It may do that by three means.

Rule R FakeWin The first situation in which a child quits the negotiation is when it has an inconsistent parenthood. More precisely, if v has several parents that are dealing with a token. Such parents are those whose value tok p / ∈ {⊥, ↓, ↑}. We do not consider the nodes who are not involved in a token circulation (tok p = ⊥) neither do we consider the nodes who announce a token in their descendants (tok p =↓). We also do not consider ↑ for the same reason that it was ignored in predicate Er: such parent is about to drop the token to its own parent, it is therefore unnecessary to consider it.

The parents which may force v to quit the negotiation are ParNeg:

ParNeg(v) = {p ∈ P(v) | tok p ̸ ∈ {⊥, ↑, ↓}} (9)
Let us describe the situations where v does not have to quit the negotiation due to an inconsistent parenthood. First, if v has exactly one parent in ParNeg(v), then there is no inconsistency. If v has no parent in ParNeg(v), there is no inconsistency either.

There is one other situation that may occur in legal execution. In a triangle configuration, v has two parents and one of them is the children of the other. Then the middle one receives the token and set its variable tok to ⋆, there is a moment where v has its variable play v = P and also has two parents in ParNeg(v), since the other parent is at ⟲. This is described in Figure 8 ⊥, P Formally, the situations that do not force v to interrupt the negotiation are:

⊥, L ⊥, L ⊥, L ⊥, P
OkNeg(v) ≡    |ParNeg(v)| ≤ 1 ∨ (|ParNeg(v)| = 2 ∧ {tok p | p ∈ ParNeg(v)} = {⟲, ⋆}) (10)
When a node decides to stop negotiating with its parent for inconsistency reasons, it fakes winning the token, in the sense that it becomes visited by switching its color, and updates its variable play, but does not actually take the token. In most cases, switching to W is sufficient. Hence, if before switching its color, v has a parent of the other color, such that tok p =↑, then at the next computing step, v will update play v to F, as shown in Figure 5. In order to spare one computing step, and to simplify some proofs, we set play v at the right value at once.

The action corresponding to the rule R FakeWin is given by FakeWin:

FakeWin(v) ≡    c v := ¬c v ; play v := W if ∀p ∈ P neq (v), tok p ̸ =↑; F if ∃p ∈ P neq (v), tok p =↑; (11)
R FakeWin : for all v ∈ V \ {r} ¬Er(v) ∧ tok v = ⊥ ∧ play v = P ∧ ¬OkNeg(v) :-→ FakeWin(v)
Rule R Win The second situation in which a child quits the negotiation is when it wins the negotiation. A node v wins the negotiation if its parents are not in an inconsistent configuration (which is OkNeg(v)), and if it is still at play v = P when its parent offers it the token (i.e. when tok p =⇊).

The predicate WinNeg is dedicated to detect such situations.

WinNeg(v) ≡ OkNeg(v) ∧ ∃p ∈ P neq (v) : tok p =⇊ (12)
When a node v wins the negotiation, it takes the token, and switches its color. Furthermore, it updates its variable play v to W. Contrary to how we did for FakeWin, we do not have to worry about the precise value of play v right now. Indeed, since v has a value different that ⊥ for tok v , v does not have to worry about the moment where it will be reactivated by its parent, which happens at the end of the circulation of its parent.

Win(v) ≡    tok v := ⋆; c v := ¬c v ; play v := W; (13) R Win : for all v ∈ V \ {r} ¬Er(v) ∧ tok v = ⊥ ∧ play v = P ∧ WinNeg(v) -→ Win(v)
Rule R Lose The third and last situation in which a child quits the negotiation is when it loses it. The exact condition of how a child loses the negotiation will be properly defined in the following section. For now, let us just consider that there exists a predicate LosePar(v, p), which depends on the values of id v and id p , where p ∈ P neq (v), which describes that v should lose the negotiation according to p.

A node loses the negotiation if its parents are not in an inconsistent configuration (which is OkNeg(v), and if it does not win the negotiation (which is ¬WinNeg(v)).

All these conditions are grouped in the predicate LoseNeg(v):

LoseNeg(v) ≡ OkNeg(v) ∧ ¬WinNeg(v) ∧ ∃p ∈ P neq (v) : (tok p = • ∧ LosePar(v, p)) (14)
When v loses the negotiation, it simply sets play v = L.

R Lose : for all v ∈ V \ {r} ¬Er(v) ∧ tok v = ⊥ ∧ play v = P ∧ LoseNeg(v) -→ play v := L B.1.

Negotiation Identifier-Based

In the negotiation phase, the only children which are relevant to consider, from the parent's perspective, are the children in Players(v). In the description of the rules, we write players instead of children in Players(v), to facilitate the reading.

Let us first describe the general mechanism of the election, then explain some subtleties, before presenting the rules of the bit-by-bit negotiation.

One first important idea is that the parent does not execute any action unless all of its players have executed their rule. In particular, the parent waits for all of its players to be at the same value of ph as it is.

Synch(v) ≡ ∀u ∈ Players(v), ph u = ph v (15)
One other general principle, which is crucial due to the asynchrony of the system, and due to the self-stabilizing requirement, is that nodes do not correct their answer. More precisely, if one node v (parent or child in the negotiation) is in a state that may have an influence on the execution of a rule by one other node u, then v does not update its state. Even if this state is inconsistent with its identifier, for a child, or with the values of id u on its players, for a parent, v waits that its neighbors have finished interpreting this state, and accept the consequences of this error. Such inconsistencies are typically due to an incorrect initialization of the system. This general principle only applies to the negotiation rules, and does not prevent nodes to execute rules such as E TrustChild , R FakeWin , or R Give for example.

Let us recall the general scheme of how the negotiation process happens 0. Parent v asks for the value of the first bit of its players u ∈ Players(v), by setting

id v = (1, ⊥).
1. Players u of v answers with their own value (1, Bit u (1)) (rule R NewBit ).

2. When all its players have answered, i.e. when all have the right value ph u = 1, v announces the biggest value it sees, by setting

id v = (1, b) (rule R maxPos ).
3. Players u of v which have a lower value than b v lose the negotiation (rule R Lose ).

4. When all of its players have ph u = 1 and b u = b v , v asks for the value of the second bit of its remaining players, by setting id v = (2, ⊥) (rule R NewPh ), and so on.

A particular situation is when all the players u of v answer (ph, ⊥), i.e. when all the players declare that they do not have a long-enough identifier to provide a ph-th bit. This situation is not possible in correct executions, since all identifiers are distinct, we cannot reach a point where several identifiers are similar and terminated. Hence, this may happen in the early steps of an execution which starts in an inconsistent configuration. Either at least one child has an identifier actually greater than ph, and could go further, but due to an incorrect initialization, it has a wrong value for b, either due to an incorrect initialization of the parent, the negotiation process did not start at ph = 1 but further, and we could have missed the opportunity to distinct the identifiers of the nodes in Players(v).

When this happens, the parent cannot simply increase ph, since its players formulate that they can't even reach the current value of ph. Therefore, if all of its players answer (ph, ⊥), then the correct move for the parent is to restart at ph v = 1. Only one exception to that rule, is when it happens when ph v = 1 already. In this situation, v would not change a single bit of information by setting id v = (1, ⊥). We suppose that all identifiers have at least one bit, even if it is a single bit 0. Therefore, (1, ⊥) can never be a valid answer for a child. In consequences, without any contradiction with the previous principle stating that no possibly valid answer can be revised, players such that id v = (1, ⊥) can actually update their state to send their actual value for Bit u (1). This is not true for other values of ph: if id v = (ph, ⊥) with ph > 1 and Bit v (ph) ̸ = ⊥, then to avoid confusing its parent, it does not update its state.

Let us now treat the different rules corresponding to the scheme presented above.

Rule R NewBit Some first conditions for a node v to answer the negotiation is that its parenthood is not inconsistent, and it is not winning the negotiation, nor losing it. This corresponds to the partial predicate OkNeg(v) ∧ ¬WinNeg(v) ∧ ¬LoseNeg(v).

The other condition is that v is in a situation where it is its turn to answer. One first situation in which it should answer is when it does not have the same value of ph as its negotiating parent p. The second situation is the particular case where ph v = ph p = 1, and v has answered ⊥, which is never a valid answer, and the parent p is still waiting for its players to answer. Indeed, in an poorly initialized configuration, the parent p could have already decided which value was the highest, and thus v must not answer. This is synthesized in predicate AnswerPar:

AnswerPar(v, p) ≡ ph v ̸ = ph p ∨    ph p = 1 b p = ⊥ b v = ⊥ (16)
We also define the predicate which excludes concurrency with R FakeWin , R Win , and R Lose :

AnswerNeg(v) ≡ OkNeg(v) ∧ ¬WinNeg(v) ∧ ¬LoseNeg(v)∧ ∃p ∈ P neq (v) : (tok p = • ∧ AnswerPar(v, p)) (17)
The action which corresponds to answering the negotiation is updating variable ph v to the value of our parent, and b v according to function Bit v .

Remark that such a parent p is necessarily unique, due to OkNeg(v). To simplify the notations, we consider that such parent p is given as an external information to the action which corresponds to AnswerNeg, Announce:

Announce(v) ≡ id v := (ph p , Bit v (ph p ) (18)
R NewBit : for all v ∈ V \ {r} ¬Er(v) ∧ tok v = ⊥ ∧ play v = P ∧ AnswerNeg(v) -→ Announce(v)
Rule R maxPos One first condition for the parent to announce the maximal value it sees on its players is that the negotiation is not over yet, i.e. there are at least two players. One second condition is that all of those players have answered, i.e. that they have the same value as itself for ph, which is captured by Synch(v).

One third condition is that it does not have already announced a value, i.e. b v = ⊥.

There are two more subtleties. The first one is that if we have ph v = 1 then v actually waits for all of its players to produce a non-empty answer, a value for b u which is not ⊥, an invalid answer for ph = 1.

The second subtlety is that if, for a value of ph greater than 1, all the players of v announce ⊥, then it is irrelevant to keep increasing phases, and actually irrelevant to answer ⊥ as well. In this situation, the correct move is to restart the negotiation from ph v = 1, which will be dealt by rule R NewPh .

The last condition and the subtleties are described by predicate NextPlay.

NextPlay(v) ≡ b v = ⊥ ∧    ph v = 1 ∧ ∀u ∈ Players(v), b u ̸ = ⊥ ∨ ph v ̸ = 1 ∧ ∃u ∈ Players(v) : b u ̸ = ⊥ (19)
Once all these conditions are fulfilled, v can announce the biggest value of b it sees in its playing childhood (classically we have ⊥ < 0 < 1). This action is denoted MaxPos.

MaxPos(v) ≡ b v := max u∈Players(v) b u (20) R maxPos : for all v ∈ V ¬Er(v)∧tok v = •∧|Players(v)| ≥ 2∧Synch(v)∧NextPlay(v) -→ MaxPos(v)
Predicate for Rule R Lose In the previous section we did not explicitly give the predicate LosePar. One node v loses the negotiation when they have the same value of ph as their parent, and that the answer provided by their parent is different from the one they have.

LosePar(v, p) ≡ ph p = ph v ∧ b p ̸ = ⊥ ∧ b p ̸ = b v (21)
Rule R NewPh The parent increases its phase only when the negotiation round is terminated, which means that nonetheless all its players have the same value as it has, for ph, but also that they all have the same value as is has for b. Either this value is ⊥, and therefore all players are out of bits, and the new phase should be 1, either it is not ⊥, and therefore all the nodes asked to lose have actually lost and are now out of Players(v), and the new phase should be one more than the current one.

There is one particular case where this increase should not happen: when we have ph = 1 and b = ⊥ (on both the parent and its players), since it does not correspond to a valid answer. Predicate PhComplete summarizes that.

PhComplete(v) ≡ (ph v ̸ = 1 ∨ b v ̸ = ⊥) ∧ ∀u ∈ Players(v), b u = b v (22)
PhasePlus(v) ≡    b v := ⊥ ph v := 1 if ∀u ∈ Players(v), b u = ⊥ ph v + 1 if ∃u ∈ Players(v), b u ̸ = ⊥ (23) R NewPh : for all v ∈ V ¬Er(v)∧tok v = •∧|Players(v)| ≥ 2∧Synch(v)∧PhComplete(v) -→ PhasePlus(v)

B.1.4 Operations Post-Negotiation

In this section we consider actions subsequent to the executions of R Give by the parent, and R Win by one child, which were presented in Section B.1.2. The parent has its variable tok =⇊, the winning player has its variable tok = ⋆, and the other children that have not received the token yet have their variable play = L.

Rule R NewPlay The first action that the parent takes, after its child has actually received the token, is switching its variable tok to ⟲ to inform its other children that the negotiation phase is terminated, and that they are free to negotiate again. This is necessary to ensure a proper depth-first traversal, since some of them may also be children of the winning player.

This can be done as soon as v does not have any players. Since we classically suppose that v is not in error, it means that its children u of the opposite color are either at tok u = ⋆, or at play u ̸ = P.

R NewPlay : for all v ∈ V ¬Er(v) ∧ tok u =⇊ ∧(∀u ∈ C neq (v) : play u ̸ = P ∨ tok u = ⋆) -→ tok v :=⟲
Rule R ReplayD When v has one parent which notifies that it can reset its value of play v to P, v first gets sure that it is not near one other negotiation phase. Indeed, v should not join a running negotiation phase by updating play v from L to P. In correct executions, v cannot be close to several negotiation phases, by unicity of the token. Yet, due to an inconsistent initialization of the network, this must be considered.

Parents that correspond to ongoing negotiation phases are those with tok p = • and tok p =⇊.

ReplayL(v) ≡ ∀u ∈ P neq (v), tok u / ∈ {•, ⇊} ∧ ∃u ∈ P neq (v), tok u ∈ {⟲, •} (24)
Note that we also consider situations where v has a parent p with tok p = •. This corresponds to a similar situation, which we will develop in Section B. 1.5 When this predicate is satisfied, v updates play v to P, and simultaneously resets its variable id v to a neutral value.

Replay(v) ≡ play v := P; id v := (1, ⊥) (25)
R ReplayD : for all v ∈ V \ {r} ¬Er(v) ∧ tok v = ⊥ ∧ play v = L ∧ ReplayL(v) -→ Replay(v)
Rule R Drop When all of its children have reset their variable play from L to P, node v can finally update its variable tok to ↓, which terminates the passing of the token to the child who won the negotiation.

To avoid deadlocks due to an inconsistent initial configuration, we must consider situations in which some child of v has the token (tok u = ⋆) but also has its variable play u at L. Rather than creating a new rule to make u updates its variable play, we chose to let v drop the token in such situations.

R Drop : for all v ∈ V ¬Er(v) ∧ tok v =⟲ ∧(∀u ∈ C neq (v) : play u ̸ = L ∨ tok u = ⋆) -→ tok v :=↓ Rule R Nego
Once the parent of the node v who won the negotiation has terminated the previous actions, and has set its variable tok to ↓, v can finally start negotiating with its own children, by setting tok v = • and its variables ph and b to the initial value of the negotiating process.

StartNego(v) ≡ tok v := •; id v := (1, ⊥); (26)
R Nego : for all v ∈ V ¬Er(v) ∧ tok v = ⋆ ∧ (∀p ∈ P(v) : tok u ̸ ∈ {⇊, ⟲}) -→ StartNego(v)
Figure 10 presents the process of how a token is given to a child. In this section we consider actions subsequent to the execution of R OfferUp (presented in Section B.1.2). We consider one node v such that tok v =↓, which has one child u that offered the token to its parent by setting tok u =↑.

•, W ⊥, P ⊥, P •, W ⊥, P ⊥, L RLose , W ⊥, P ⊥, L RGive , W , W ⊥, L RWin , W , W ⊥, L RNewPlay , W , W ⊥, P RReplayD ↓, W , W ⊥, P RDrop ↓, W •, W ⊥, P RNego
Rule R Receive When node v has its child u announcing that it returns the token back, v needs to be sure that it does not have any other children which is involved in a token circulation, in which case it cannot take the token before its other children have terminated their circulation.

If v takes the token while having another child involved in a token circulation, it becomes in error, and thus executes E TrustChild , and sets tok v =↓, which may create a livelock.

R Receive : for all v ∈ V ¬Er(v) ∧ tok v =↓ ∧(∀u ∈ C(v), tok u ∈ {⊥, ↑}) -→ tok v := • Rule R ReNego If node v did not
have any children and took the token by setting tok v = • with rule R Receive , then before starting negotiating, it waits that its child, from which it received the token, actually drops it.

More precisely, v start negotiating only if it all of its children are such that tok u = ⊥, otherwise it would create an error by setting tok v = •. The following predicate guarantees that one node has no children involved in a token circulation:

Leaf(v) ≡ ∀u ∈ C(v), tok u = ⊥ (27)
Furthermore, before starting a negotiation round, v also waits that all its children which have not won the token yet have properly reset their variable play to L. This is guaranteed since Rule B.1.4 applies to situations where the parent has its variable tok = •.

R ReNego : for all v ∈ V ¬Er(v) ∧ tok v = • ∧ Leaf(v) ∧ ∀u ∈ C neq (v) : play u ̸ = L -→ StartNego(v)

B.1.6 End of the Circulation

In this section we also present actions subsequent to the execution of R OfferUp (presented in Section B.1.2), but from the child perspective. We consider the node which executed R OfferUp , and its potential children.

Rule R Return After it has offered the token to its parent, a node v which is not the root should eventually drop the token, and set tok v = ⊥. Before that, it must check that all its children have correctly updated their variable W to P to assure that when a token of the other color will come, all those nodes will be available for a negotiation phase. This only applies to children of v which have the same color as v, since other children may be involved in a concurrent token circulation, and we do not want to create any livelock. Also, it only applies to nodes which are not involved in any circulation of the token, i.e. such that tok u = ⊥ (recall that since tok v =↑, v cannot be in error).

If such children u of v, with play u = W still have parents involved in a negotiation, they will shift that value to F, faking a reset to v. Thus, v should tolerate children u with play u = F.

On the other hand, if v has children u which have their variable play u = L, those children might be involved in another negotiation phase, which they have lost. Those children should not reset their variable play to P, for it would harm the negotiation process.

Thus, v checks that all of its children with the same color have a value of play different from W before it sends the token back.

We add one more consistency check, which is that v does not have any parent in error, i.e. parents p such that tok p ∈ {⋆, •, ⇊, ⟲}. If it has, it waits for those parents to execute E TrustChild before returning the token to its parents. This predicate is not necessary for our algorithm to work, but it may make convergence faster.

These predicates are combined in predicate MayDropUp.

MayDropUp(v) ≡ ∀p ∈ P(v), tok p ∈ {⊥, ↓, ↑, •} ∧ ∀u ∈ C eq (v), (tok u = ⊥ ⇒ play u ∈ {P, L, F}) (28)
When this condition is fulfilled, v can drop the token. This includes setting tok v = ⊥ and updating play v to a correct value depending on the parents of v. As depicted in Figure 5, there are situations where nodes without a token must set their variable at F instead of W, to avoid blocking one parent which is close to execute R Return itself.

Drop(v) ≡    tok v := ⊥; play v := W if ∀p ∈ P eq (v), tok p ̸ =↑ F if ∃p ∈ P eq (v), tok p =↑ (29) R Return : for all v ∈ V \ {r} ¬Er(v) ∧ tok v =↑ ∧MayDropUp(v) -→ Drop(v)
Rule R r NewDFS In a similar situation, where all of its children have repaired themselves, the root does not drop the token, for it would simply destroy it. When the root is in such a situation, it means that the current circulation round is terminated, and one other can start.

To do that, the root reset its token value to ⋆, which corresponds to the first time the token is held by any node in the new circulation round, and switches its color. After that, the root will be able to execute rule R Nego and to start a negotiation process with its children.

NewToken(r) ≡ c r := ¬c r tok r := ⋆ (30)
This action can be seen as one atomic execution of the two actions Drop and Win, which corresponds to what r would have done, non-atomically, if it were not the root.

R r

NewDFS :

for v = r ¬Er(v) ∧ tok v =↑ ∧MayDropUp(v) -→ NewToken(v)
Let us now consider the actions taken by children of such a node, i.e. a node v which has one parent of the same color and its variable tok =↑.

Rule R ReplayUp If node v only has parents that are sending the token higher, i.e. no other parent which is still involved in a token circulation, then v can reset its variable play v = P to be ready for the next circulation round.

ReplayW(v) ≡ ∃p ∈ P eq (v) : tok p =↑ ∧∀p ∈ P eq (v), tok p ∈ {⊥, ↑} (31)
Note that v only consider its parent with the same color, since the situation which we want to prevent is livelock caused by the oscillation between two tokens. Therefore, v can join a negotiation of the other color by this action.

R ReplayUp : for all v ∈ V \ {r} ¬Er(v) ∧ tok v = ⊥ ∧ play v = W ∧ ReplayW(v) -→ Replay(v)
Rule R Fake If v has, in addition to some parents that are sending the token higher, other parents which do not have terminated their token circulation, it must update its variable play v = F. FakeReplay(v) ≡ ∃p ∈ P eq (v), tok p =↑ ∧¬ReplayW(v) (32)

R Fake : for all v ∈ V \ {r} ¬Er(v) ∧ tok v = ⊥ ∧ play v = W ∧ FakeReplay(v) -→ play v := F
Rule R ReWin Finally, we must design a rule to cancel the effect of updating one's variable at F, to reset it at W. Without this rule, the predicate WaitSib could be infinitely false one one parent of v, and thus the token could not be sent higher. This rule can be activated only when the node does not have any parent with the same color such that tok =↑. Up to this rule, all the guards of the rules require that the node is near a token. For consistency, we also require proximity of a token for this rule, but it is not actually necessary.

StopFaking(v) ≡ ∃p ∈ P eq (v) : tok v ̸ = ⊥ ∧ ∀p ∈ P eq (v), tok p ̸ =↑ (33) R ReWin : for all v ∈ V \ {r} ¬Er(v) ∧ tok v = ⊥ ∧ play v = F ∧ StopFaking(v) -→ play v := W Figure 9
present the process of how a token is returned to a parent.

↓, W •, W ⊥, W ⊥, W ↓, W ↑, W ⊥, W ⊥, W ROfferUp ↓, W ↑, W ⊥, P ⊥, P RReplayUp •, W ↑, W ⊥, P ⊥, P RReceive •, W ⊥, W ⊥, P ⊥, P RReturn •, W ⊥, W ⊥, P ⊥, P

RReNego

Figure 10: Execution of rules for returning the token back to one parent. The activated node is the one with its line doubled

B.1.7 Complete Algorithm

Algorithm 2 presents all the rules of our algorithm.

Algorithm 2: Token Circulation algorithm

∀v ETrustChild : Er(v) -→ tokv :=↓ ∀v ROfferUp : ¬Er(v) ∧ tokv = • ∧ ¬WaitSib(v) ∧ (∀u ∈ Cneq(v) : play u ∈ {W, F}) -→ tokv :=↑ ∀v RGive : ¬Er(v) ∧ tokv = • ∧ Give(v) -→ tokv :=⇊ v ̸ = r RFakeWin : ¬Er(v) ∧ tokv = ⊥ ∧ play v = P ∧ ¬OkNeg(v) -→ FakeWin(v) v ̸ = r RWin : ¬Er(v) ∧ tokv = ⊥ ∧ play v = P ∧ WinNeg(v) -→ Win(v) v ̸ = r RLose : ¬Er(v) ∧ tokv = ⊥ ∧ play v = P ∧ LoseNeg(v) -→ play v := L v ̸ = r RNewBit : ¬Er(v) ∧ tokv = ⊥ ∧ play v = P ∧ AnswerNeg(v) -→ Announce(v) ∀v RmaxPos : ¬Er(v) ∧ tokv = • ∧ |Players(v)| ≥ 2 ∧ Synch(v) ∧ NextPlay(v) -→ MaxPos(v) ∀v RNewPh : ¬Er(v) ∧ tokv = • ∧ |Players(v)| ≥ 2 ∧ Synch(v) ∧ PhComplete(v) -→ PhasePlus(v) ∀v RNewPlay : ¬Er(v) ∧ toku =⇊ ∧(∀u ∈ Cneq(v) : play u ̸ = P ∨ toku = ⋆) -→ tokv :=⟲ v ̸ = r RReplayD : ¬Er(v) ∧ tokv = ⊥ ∧ play v = L ∧ ReplayL(v) -→ Replay(v) ∀v RDrop : ¬Er(v) ∧ tokv =⟲ ∧(∀u ∈ Cneq(v) : play u ̸ = L ∨ toku = ⋆) -→ tokv :=↓ ∀v RNego : ¬Er(v) ∧ tokv = ⋆ ∧ (∀p ∈ P(v) : toku ̸ ∈ {⇊, ⟲}) -→ StartNego(v) ∀v RReceive : ¬Er(v) ∧ tokv =↓ ∧(∀u ∈ C(v), toku ∈ {⊥, ↑}) -→ tokv := • ∀v RReNego : ¬Er(v) ∧ tokv = • ∧ Leaf(v) ∧ ∀u ∈ Cneq(v) : play u ̸ = L -→ StartNego(v) v ̸ = r RReturn : ¬Er(v) ∧ tokv =↑ ∧MayDropUp(v) -→ Drop(v) r R r NewDFS : ¬Er(v) ∧ tokv =↑ ∧MayDropUp(v) -→ NewToken(v) v ̸ = r RReplayUp : ¬Er(v) ∧ tokv = ⊥ ∧ play v = W ∧ ReplayW(v) -→ Replay(v) v ̸ = r RFake : ¬Er(v) ∧ tokv = ⊥ ∧ play v = W ∧ FakeReplay(v) -→ play v := F v ̸ = r RReWin : ¬Er(v) ∧ tokv = ⊥ ∧ play v = F ∧ StopFaking(v) -→ play v := W
Figures 11 and 12 present the scheme of an execution of our algorithm. These are two dual visions of the same phenomenon. The first one focuses on the values of the different variables of one node v, and the second on the executions of the rules on one node v.

⊥, W ⊥, F ⊥, P ⊥, L ph, b , W •, W , W , W ↓, W •, W ↑,

C Appendix on the Correctness of our Algorithm

In this section, we prove that Algorithm 2 is a self-stabilizing algorithm for the token circulation problem, as it is defined in Specification 1. We also prove that this algorithm is optimal in terms of memory, i.e. that any algorithm which solves T C in S requires Ω(log log n) bits per nodes, even under less general hypothesis than ours.

This section is subdivided in four subsections. In Section C.1 we establish that maximal executions of our algorithm are infinite. Formally, we prove that in any configuration, there is at least one enabled node. This work is static in the sense that we do not need to consider an execution of the algorithm. It boils down to a syntactical analysis of the guards of the rules of our algorithm (Algorithm 2).

In Section C.2 we establish that no token can circulate indefinitely in the D o , unless it regularly reaches the root and is reset by the execution of R r NewDFS . This guarantees that a token which is not anchored at the root of the D o either vanishes, or is eventually not activated. Using the previous, we also establish that there are an infinite number of circulation rounds in maximal executions of our algorithm. This guarantees that our algorithm satisfies Condition 2 of Specification 1.

In Section C.3 we use the previous results to establish that the token anchored at the root circulates fairly in deeper and deeper parts of the D o . Thus, even if there are other tokens in the network, they will eventually be reached and destroyed by the legitimate token anchored at the root. Therefore we prove in this section that, at some point, the execution of our algorithm satisfies Conditions 1 and 3 of Specification 1, which means that it is a self-stabilizing algorithm for T D.

Finally, in Section C.4 we use the results of [START_REF] Blin | Optimal space lower bound for deterministic self-stabilizing leader election algorithms[END_REF] to prove that the space complexity of our algorithm is optimal.

In order to prove that our algorithm satisfies conditions of Specification 1, we must first define the predicates T and R involved in this specification. One node v is considered to hold the token if it has a non-empty value for its variable tok v , and if none of its children holds the token. One node v is considered to have access to the resource if it is in the state where it just received the token from its parent, which corresponds to tok v = ⋆.

Definition 13 (Predicates for our Token Circulation Algorithm)

The resolution of T D by our algorithm will be proven under the following specification predicates:

T (v, γ) ≡ tok γ v ̸ = ⊥ ∧ ∀u ∈ C(v), tok γ u = ⊥ R(v, γ) ≡ T (v, γ) ∧ tok γ v = ⋆ Definition 14 (Reset Points) Let ϵ = γ 0 → • • • be an execution. We say that γ i is a reset point of ϵ if r executes R r NewDFS during γ i-1 → γ i+1 .
We say that two reset points γ i and γ j are consecutive if i < j and ∀k ∈ [i + 1, j + 1], γ k is not a reset point.

Theorem 1 (Circulation Rounds) Let ϵ = γ 0 → • • • be an execution. Let us denote by t 0 ≤ t 1 ≤ • • • all the reset points of ϵ, such that ∀i ≥ 0, γ t i and γ t i+1 are consecutive. ∀i ≥ 0,

γ t 1 → • • • → γ t i+1 -1 is a circulation round.
Proof : For any computing step cs = γ → γ ′ , we have ¬R γ (r) ∧ R γ ′ (r) if and only if r executes R r NewDFS , which is equivalent to γ ′ being a reset point.

C.1 Liveness

Recall that we denote by A e (γ) the set of the enabled nodes for A in configuration γ. In this section, we prove that ∀γ ∈ Γ, A e (γ) ̸ = ∅.

The proof is subdivided in several lemmas. In each lemma we work under the hypothesis that some value for tok v , on one node v, is present in γ, and in each case we prove that there exists at least one enabled node, in γ. Not all the lemmas are independent: it happens that to prove a lemma, we simply prove that there exists one node u with another value of tok u , value which has already been dealt in a previous lemma.

One lemma is even proven by induction, the lemma which considers as a hypothesis the presence of a node v such that tok v =↓. Such nodes can actually pretty far from the actual token, and thus to find an enabled node, we may have to descend a branch of the D o , until we fall on a leaf, or on a node with a different value for tok v .

More precisely, we prove that either we can find an enabled node, either there exists one other node u such that tok u =↓, but u is deeper than v in the DODAG. Since DODAGs are finite, and acyclic, there can only be a finite number of times where the second hypothesis is the right one, and therefore this proves that there exists at least one enabled node.

The proofs are basically reasoning by case disjunction, which forms decision trees of variable depth. We must guarantee that at the end of each branch i.e. at each leaf, we find one enabled node.

Since it is basically syntactical analysis, we only present the different decision trees, which contain all the elements of the proofs, and are easier to parse than the written version of the proofs.

In each proof, we also provide a reasoning toolbox, to remind the reader the detail of the predicates considered in the reasoning.

Lemma 1

Let γ ∈ Γ. If there exists v ∈ V such that tok v =↑ in γ then A e (γ) ̸ = ∅.

Proof : The proof is given in Figure 13

∀v ETrustChild : Er(v) -→ tokv :=↓ v ̸ = r RReturn : ¬Er(v) ∧ tokv =↑ ∧MayDropUp(v) -→ Drop(v) r R r NewDFS : ¬Er(v) ∧ tokv =↑ ∧MayDropUp(v) -→ NewToken(v) v ̸ = r RReplayUp : ¬Er(v) ∧ tokv = ⊥ ∧ play v = W ∧ ReplayW(v) -→ Replay(v) v ̸ = r RFake : ¬Er(v) ∧ tokv = ⊥ ∧ play v = W ∧ FakeReplay(v) -→ play v := F Er(v) ≡ tokv ∈ {•, ⋆} ∧ ∃u ∈ C(v) : toku ̸ = ⊥ ∨ tokv ∈ {⇊, ⟲} ∧ ∃u ∈ C(v) : toku / ∈ {⊥, ⋆} ∨ tokv = • ∧ ∃u ∈ C(v) : toku / ∈ {⊥, ↑} -→ tokv :=↓ MayDropUp(v) ≡ ∀p ∈ P(v), tokp ∈ {⊥, ↓, ↑, •} ∧ ∀u ∈ Ceq(v), (toku = ⊥ ⇒ play u ∈ {P, L, F}) ReplayW(v) ≡ ∃p ∈ Peq(v) : tokp =↑ ∧∀p ∈ Peq(v), tokp ∈ {⊥, ↑} FakeReplay(v) ≡ ∃p ∈ Peq(v), tokp =↑ ∧¬ReplayW(v) Lemma 2 Let γ ∈ Γ. If there exists v ∈ V such that tok v =⇊ in γ then A e (γ) ̸ = ∅.
Proof : The proof is given in Figure 14

play u ̸ = P ∨ toku = ⋆) -→ tokv :=⟲ ∀v ̸ = r RWin : ¬Er(v) ∧ tokv = ⊥ ∧ play v = P ∧ WinNeg(v) -→ Win(v) ∀v ̸ = r RFakeWin : ¬Er(v) ∧ tokv = ⊥ ∧ play v = P ∧ ¬OkNeg(v) -→ FakeWin(v) Er(v) ≡ tokv ∈ {•, ⋆} ∧ ∃u ∈ C(v) : toku ̸ = ⊥ ∨ tokv ∈ {⇊, ⟲} ∧ ∃u ∈ C(v) : toku / ∈ {⊥, ⋆} ∨ tokv = • ∧ ∃u ∈ C(v) : toku / ∈ {⊥, ↑} -→ tokv :=↓ WinNeg(v) ≡ OkNeg(v) ∧ ∃p ∈ Pneq(v) : tokp =⇊ OkNeg(v) ≡ |ParNeg(v)| ≤ 1 ∨ (|ParNeg(v)| = 2 ∧ {tokp | p ∈ ParNeg(v)} ∈ {{⇊, ⋆}, {⟲, ⋆}}) ParNeg(v) = {p ∈ P(v) | tokp ̸ ∈ {⊥, ↑, ↓}} Lemma 3 Let γ ∈ Γ. If there exists v ∈ V such that tok v = • in γ then A e (γ) ̸ = ∅.
Proof : The proof is given in Figures 15 and16 Tools Lemma 3 Let γ ∈ Γ. If there exists v ∈ V such that tok v =⟲ in γ then A e (γ) ̸ = ∅.

∀v ETrustChild : Er(v) -→ tokv :=↓ ∀v RmaxPos : ¬Er(v) ∧ tokv = • ∧ |Players(v)| ≥ 2 ∧ Synch(v) ∧ NextPlay(v) -→ MaxPos(v) ∀v RNewPh : ¬Er(v) ∧ tokv = • ∧ |Players(v)| ≥ 2 ∧ Synch(v) ∧ PhComplete(v) -→ PhasePlus(v) ∀v RGive : ¬Er(v) ∧ tokv = • ∧ Give(v) -→ tokv :=⇊ ∀v ROfferUp : ¬Er(v) ∧ tokv = • ∧ ¬WaitSib(v) ∧ (∀u ∈ Cneq(v) : play u ∈ {W, F}) -→ tokv :=↑ v ̸ = r RNewBit : ¬Er(v) ∧ tokv = ⊥ ∧ play v = P ∧ AnswerNeg(v) -→ Announce(v) v ̸ = r RLose : ¬Er(v) ∧ tokv = ⊥ ∧ play v = P ∧ LoseNeg(v) -→ play v := L v ̸ = r RWin : ¬Er(v) ∧ tokv = ⊥ ∧ play v = P ∧ WinNeg(v) -→ Win(v) v ̸ = r RFakeWin : ¬Er(v) ∧ tokv = ⊥ ∧ play v = P ∧ ¬OkNeg(v) -→ FakeWin(v) v ̸ = r RReWin : ¬Er(v) ∧ tokv = ⊥ ∧ play v = F ∧ StopFaking(v) -→ play v := W Er(v) ≡ tokv ∈ {•, ⋆} ∧ ∃u ∈ C(v) : toku ̸ = ⊥ ∨ tokv ∈ {⇊, ⟲} ∧ ∃u ∈ C(v) : toku / ∈ {⊥, ⋆} ∨ tokv = • ∧ ∃u ∈ C(v) : toku / ∈ {⊥, ↑} -→ tokv :=↓ AnswerPar(v, p) ≡ (ph v ̸ = ph p ) ∨ (ph p = 1 ∧ bp = ⊥ ∧ bv = ⊥) LosePar(v, p) ≡ ph p = ph v ∧ bp ̸ = ⊥ ∧ bp ̸ = bv ParNeg(v) = {p ∈ P(v) | tokp ̸ ∈ {⊥, ↑, ↓}} OkNeg(v) ≡ |ParNeg(v)| ≤ 1 ∨ (|ParNeg(v)| = 2 ∧ {tokp | p ∈ ParNeg(v)} ∈ {{⇊, ⋆}, {⟲, ⋆}}) WinNeg(v) ≡ OkNeg(v) ∧ ∃p ∈ Pneq(v) : tokp =⇊ LoseNeg(v) ≡ OkNeg(v) ∧ ¬WinNeg(v) ∧ ∃p ∈ Pneq(v) : tokp = • ∧ LosePar(v, p) AnswerNeg(v) ≡ OkNeg(v) ∧ ¬WinNeg(v) ∧ ¬LoseNeg(v) ∧ ∃p ∈ Pneq(v) : tokp = • ∧ AnswerPar(v, p) Players(v) = {u ∈ Cneq(v) |tokv = ⊥ ∧ play u = P} Synch(v) ≡ ∀u ∈ Players(v), ph u = ph v NextPlay(v) ≡ bv = ⊥ ∧    ph v = 1 ∧ ∀u ∈ Players(v), bu ̸ = ⊥ ∨ ph v ̸ = 1 ∧ ∃u ∈ Players(v) : bu ̸ = ⊥ PhComplete(v) ≡ (ph v ̸ = 1 ∨ bv ̸ = ⊥) ∧ ∀u ∈ Players(v), bu = bv Give(v) ≡ |Players(v)| = 1 ∨ (|Players(v)| = 0 ∧ ∃u ∈ Cneq(v) : play u = L) WaitSib(v) ≡ ∃c ∈ Ceq(v) : play c = F StopFaking(v) ≡ ∃p ∈ Peq(v) : tokv ̸ = ⊥ ∧ ∀p ∈ Peq(v), tokp ̸ =↑ tokv = • ∀u ∈ C(v) : toku = ⊥ |Players(v)| = 0 ∃c ∈ Cneq(v) : play c = L v : RGive ∀c ∈ Cneq(v), play c ∈ {W, F} ∀c ∈ Ceq(v), play c ̸ = F v : ROfferUp ∃c ∈ Ceq(v) : play c = F ∀p ∈ Peq(c), tokp ̸ =↑ c : RReWin ∃p ∈ Peq(c) : tokp =↑ p : Lemma 1 |Players(v)| = 1 v : RGive |Players(v)| ≥ 2 ∃c ∈ Players(v) : ¬OkNeg(c) c : RFakeWin ∀u ∈ Players(v), OkNeg(u) ∧ ∃c ∈ Players(v) : WinNeg(c) c : RWin ∀u ∈ Players(v), (OkNeg(u) ∧ ¬WinNeg(u)) ∧ ∃c ∈ Players(v) : LoseNeg(c) c : RLose ∀u ∈ Players(v), (OkNeg(u) ∧ ¬WinNeg(u) ∧ ¬LoseNeg(u)) ∧ ∃c ∈ Players(v) : ph c ̸ = ph v c : RNewBit ∀u ∈ Players(v), (OkNeg(u) ∧ ¬WinNeg(u) ∧ ¬LoseNeg(u)) ∧ Synch(v) ∃u ∈ C(v) : toku ̸ = ⊥ v : ETrustChild
Synch(v) ph v = 1 b v = ⊥ ∃c ∈ Players(v) : b c = ⊥ c : R NewBit ∀c ∈ Players(v), b c ̸ = ⊥ v : R maxPos b v ̸ = ⊥ ∃c ∈ Players(v) : b c ̸ = b v c : R Lose ∀c ∈ Players(v), b c = b v v : R NewPh ph v ̸ = 1 b v = ⊥ ∃c ∈ Players(v), b c ̸ = ⊥ v : R maxPos ∀c ∈ Players(v), b c = ⊥ v : R NewPh b v ̸ = ⊥ ∃c ∈ Players(v) : b c ̸ = b v c : R Lose ∀c ∈ Players(v), b c = b v v : R NewPh
Proof : The proof is given in Figure 17 tokv =⟲

Er(v) -→ tokv :=↓ ∀v RDrop : ¬Er(v) ∧ tokv =⟲ ∧(∀u ∈ Cneq(v) : play u ̸ = L ∨ toku = ⋆) -→ tokv :=↓ ∀v ̸ = r RReplayD : ¬Er(v) ∧ tokv = ⊥ ∧ play v = L ∧ ReplayL(v) -→ Replay(v) Er(v) ≡ tokv ∈ {•, ⋆} ∧ ∃u ∈ C(v) : toku ̸ = ⊥ ∨ tokv ∈ {⇊, ⟲} ∧ ∃u ∈ C(v) : toku / ∈ {⊥, ⋆} ∨ tokv = • ∧ ∃u ∈ C(v) : toku / ∈ {⊥, ↑} -→ tokv :=↓ ReplayL(v) ≡ ∀u ∈ Pneq(v), toku / ∈ {•, ⇊} ∧ ∃u ∈ Pneq(v), toku ∈ {⟲, •} Lemma 5 Let γ ∈ Γ. If there exists v ∈ V such that tok v = • in γ then A e (γ) ̸ = ∅.
Proof : The proof is given in Figure 18 tokv

play u ̸ = L -→ StartNego(v) v ̸ = r RReplayD : ¬Er(v) ∧ tokv = ⊥ ∧ play v = L ∧ ReplayL(v) -→ play v := P Er(v) ≡ tokv ∈ {•, ⋆} ∧ ∃u ∈ C(v) : toku ̸ = ⊥ ∨ tokv ∈ {⇊, ⟲} ∧ ∃u ∈ C(v) : toku / ∈ {⊥, ⋆} ∨ tokv = • ∧ ∃u ∈ C(v) : toku / ∈ {⊥, ↑} -→ tokv :=↓ ReplayL(v) ≡ ∀u ∈ Pneq(v), toku / ∈ {•, ⇊} ∧ ∃u ∈ Pneq(v), toku ∈ {⟲, •} Lemma 6 Let γ ∈ Γ. If there exists v ∈ V such that tok v = ⋆ in γ then A e (γ) ̸ = ∅.
Proof : The proof is given in Figure 19 tok

(v) -→ tokv :=↓ v ̸ = r RNego : ¬Er(v) ∧ tokv = ⋆ ∧ (∀p ∈ P(v) : toku ̸ ∈ {⇊, ⟲}) -→ StartNego(v) Er(v) ≡ tokv ∈ {•, ⋆} ∧ ∃u ∈ C(v) : toku ̸ = ⊥ ∨ tokv ∈ {⇊, ⟲} ∧ ∃u ∈ C(v) : toku / ∈ {⊥, ⋆} ∨ tokv = • ∧ ∃u ∈ C(v) : toku / ∈ {⊥, ↑} -→ tokv :=↓ Lemma 7 Let γ ∈ Γ. If there exists v ∈ V such that tok v =↓ in γ then A e (γ) ̸ = ∅.
Proof : The proof is given in Figure 20 ∀v ETrustChild :

Er(v) -→ tokv :=↓ ∀v RReceive : ¬Er(v) ∧ tokv =↓ ∧(∀u ∈ C(v), toku ∈ {⊥, ↑}) -→ tokv := • Er(v) ≡ tokv ∈ {•, ⋆} ∧ ∃u ∈ C(v) : toku ̸ = ⊥ ∨ tokv ∈ {⇊, ⟲} ∧ ∃u ∈ C(v) : toku / ∈ {⊥, ⋆} ∨ tokv = • ∧ ∃u ∈ C(v) : toku / ∈ {⊥, ↑} -→ tokv :=↓

C.2 Progress

In this section we formally establish, at once, two crucial properties for the validity of our algorithm. The first property is that if a token is not anchored at the root of the D o (we will give later a proper definition of the anchor of a token), then it can only circulate a finite number of times before being blocked, or deleted. This means that no scheduler, even unfair, can create an execution in which the token held by the root is never activated. The second property is that circulation rounds (see Section A.4), are always finite. We actually prove that the token held by the root can only circulate a finite number of times before it reaches the root, and the root executes R r NewDFS . The combination of these two properties, and of the liveness established in Theorem 2 leads to the guarantee that there is an infinity of finite circulation round in any maximal execution of our algorithm. We will prove in the next section that, eventually, the circulation of the token is fair.

To prove both properties, we define a potential function, which associates a positive value (a weight) to each token in any configuration. Then, we establish that any computing step decreases the weight of the token, unless the token is reset by an execution of R r NewDFS . This establishes that a token cannot circulate indefinitely, since any step it takes makes a positive quantity decrease, unless this token is anchored at the root and there are an infinity of new circulation rounds.

In this section we provide a formal proof of these properties. Let us have first an overview of this proof. In a corrupted initial configuration, the network may contain several tokens, which may have common ancestors, and also have several ancestors. To deal with the diversity of possible configurations, we define a new object to reason on, circulation DODAGs, denoted by CD o , for each token. Then, we define a weight function, which associates a weighted DODAG, denoted by WD o , to each CD o . We finally prove that each time a node of a CD o is activated, the corresponding WD o decreases. According to Theorem 2, there are at least one enabled node in each configuration, which guarantees that WD o 's actually decrease in maximal executions.

In Section C.

C.2.1 Difficulties to Overcome, Circulation DODAG

To associate a decreasing weight to a token, the main difficulty to overcome is that during one circulation, the token shifts a lot, upward and downward alternately. Thus, the information of whether the token is very close to the end of the circulation round, or still far, is not local. This information strongly depends, for example, on which branches have already been visited by the token, on the number of unvisited children the different nodes have, on whether one error will be raised, etc. As a result, we cannot focus only on the token if we want to succeed in estimating how many steps it still has to execute before it ends its circulation.

One first condition for our potential function to be consistent is that it takes into account the variables of the node holding the token, but also information relative to some ancestors of that node. In practice, only the ancestors which are somehow pointing to this token will be considered.

Yet, it might happen that one node in the ancestry of the token holder has several children involved in a token circulation. If this is due to a triangle topology, i.e. if one node has two parents, one being the parent of the other one, then considering the ascendants of the token is sufficient. But this could also be a situation in which one node has two independent token circulations below it. Our algorithm does not create such situations, but they might exist due to an incorrect initial configuration. In such a situation, our previous definition is not fully satisfactory since it does not highlight the fact that those two token circulation are, though independent, intertwined.

To embrace that complexity, we define an ad hoc object, called a Circulation DODAG, denoted CD o , which has a D o structure. That new object follows the same idea as the upwards branch starting at the token, but we reverse that idea. We first look for nodes with no ancestry (called anchor ), that is to say nodes v such that tok v ̸ = ⊥ ∧ ∀p ∈ P(v), tok p ∈ {⊥, ↑}. Then, we go down from each anchor to all its descendants, following nodes u such that tok u ̸ = ⊥. Since nodes with tok u =↑ can only be updated by R Return , with effect tok u := ⊥, we include them in our structures, but not their potential descendants: such nodes are necessarily leaves of the CD o . Note that if the initial configuration is inconsistent, it may contain several CD o 's. In Section C.2.2 we formally define CD o 's and we establish some basic properties on CD o 's.

Our goal is now to associate a finite positive quantity, a weight, to any CD o in any configuration. Such an association will be called a weight function. A weight function is said admissible if any activation of the CD o results in a decrease of the weight of the CD o . Since there does not exist infinite decreasing sequence of positive integers, it comes that any CD o has a finite lifetime. Actually, since our algorithm of token circulation does not terminate, there necessarily exists one rule that does not respect that specification. The rule R r NewDFS is the only rule that increases the weight of a CD o , as it refreshes the token by switching its color. Since only the root of the D o can execute R r NewDFS , we guarantee that any other CD o , anchored at another node than the root, has a finite lifetime.

Unfortunately, associating a simple integer to a CD o does not allow to take into account the diversity of situations that we must consider. The appropriate quantity to reason on has itself a D o structure, which has the same topology as the CD o to which it is associate by the weight function. Such D o 's are called weighted DODAGs and are denoted WD o .

More precisely, a WD o is a 5-tuple of D o 's. Each component of the tuple deals with one aspect of the algorithm. The order in which are set the different components is crucial. Indeed, it happens that some computing step makes one of the component increase. We prove that this can be only if one component with higher priority decreases at the same time.

• The first component of the 5-tuple evaluates the number of unvisited children of each node of the CD o .

• The second component the numbers of errors in the network.

• The third component is dedicated to the updates of variable tok on each node, as depicted in Figure 3.

• The fourth component to the variable play on the children of each node of the CD o .

• And the last component is dedicated to the negotiation process near nodes with tok = •.

C.2.2 Circulation DODAGs

In this subsection, we define tools to capture the behavior of the token circulation, and especially Circulation DODAGs, CD o 's. We prove in particular that the number of CD o 's can never increase, which is a very desirable property to have to establish that the token is eventually unique. Remember that we denote by var γ v the state of variable var for the node v in configuration γ, and by P γ (v) the values of predicate P on node v in configuration γ.

We first define the anchors of our CD o 's. The anchors are nodes v that are involved in a token circulation, i.e. tok v ̸ = ⊥, and which do not have any parent in this token circulation. Recall that nodes u such that tok u =↑ cannot be considered as parents, since they can only execute rule R Return , which makes them quit the circulation.

Definition 15 (Anchor )

Let γ ∈ Γ be a configuration. Node a ∈ V is an anchor in γ if

• tok γ a ̸ = ⊥, and

• ∀u ∈ P(a), tok γ u ∈ {⊥, ↑}.
We denote by A(γ) the set of all anchors at γ, and by A * (γ) the set of all anchors except the root.

Remark 4

The root of G is an anchor in any configuration γ.

Now that we have defined anchors, we can define the nodes of the CD o anchored at one particular anchor. The nodes of the CD o anchored at a are all the nodes which can reach a by paths corresponding to a actual token circulation. In other words, we only consider paths in which all nodes have a value tok ̸ = ⊥, and such that all the nodes apart from the source have a value tok ̸ =↑. Indeed, nodes u such that tok u =↑ are necessarily leaves of CD o 's.

Definition 16 (Nodes of a Circulation DODAG)

Let us consider a configuration γ ∈ Γ and an anchor a ∈ A(γ). We define by induction the nodes of the Circulation DODAG (CD o ) anchored at a in γ, and denote by V γ a as the smallest set which contains the node a and such that:

v ∈ V γ a ⇐⇒ tok γ v ̸ = ⊥ ∃u ∈ P(v) : u ∈ V γ a ∧ tok γ u ̸ =↑ .
We now give a definition of CD o and we present an example with several CD o 's in one D o in Figure 21.

Definition 17 (Circulation DODAG)

Let us consider a configuration γ ∈ Γ and an anchor a ∈ A(γ). We define the Circulation DODAG (CD o ) anchored at a in γ, and denote D γ a , as the D o with nodes V γ a , and whose parental relationship is defined by:

∀u, v ∈ V γ a , (u ∈ C D γ a (v) ⇐⇒ u ∈ C G (v) ∧ tok γ v ̸ =↑) Remark 5
We use the notation v ∈ D γ a as an alias for v ∈ V γ a .

Remark 6

A CD o with anchor a is a sub-D o of G a , the D o under a (see Definition 5).

Lemma 8 establishes that any node v such that tok v ̸ = ⊥ belongs to at least one CD o . It will be useful in the latter to prove that any action taken by some node has an effect on at least one CD o , and therefore decreases the weight of at least one CD o .

Lemma 8 ∀v ∈ V , if tok γ v ̸ = ⊥, then there exists an anchor a ∈ A(γ) such that v ∈ D γ a Proof : Let us consider a maximal sequence v 0 v 1 • • • v k such that v = v 0 and ∀i ∈ [1, k], tok γ vi / ∈ {⊥ ↑} ∧ v i ∈ P(v i-1
). Since the sequence is maximal, v k ∈ A(γ), and by definition we also have ∀i,

v i ∈ D γ v k . Consequently, v ∈ D γ v k .
Lemma 9 states that the set of anchors A of G is non-increasing: if one node v is not an anchor in a configuration γ, then it will never be an anchor in a further configuration. This lemma justifies that focusing on the decrease of the weight of CD o is sufficient, since no CD o appears. Let cs = γ → γ ′ be a computing step. We have A(γ ′ ) ⊆ A(γ)

Proof : Let us prove the equivalent statement: V \ A(γ) ⊆ V \ A(γ ′ ). Let the node v be v / ∈ A(γ), and prove that v / ∈ A(γ ′ ).

• Suppose first that

tok γ v = ⊥. If tok γ ′ v = ⊥, then v / ∈ A(γ ′ ). Otherwise, we have tok γ v = ⊥ and tok γ ′ v ̸ = ⊥,

Remark 7

In the latter, when considering the effect of a computing step γ → γ ′ on a CD o , we always work under the hypothesis that a ∈ A(γ ′ ), which also implies that a ∈ A(γ) according to Lemma 9.

Corollary 1

The number of CD o does not increase.

A CD o evolves through an execution of the algorithm, and in particular it can federate new nodes during some computing steps, if some node close to the CD o executes R Win . To be able to consider such situations, we introduce the notion of border of a CD o , which are close nodes that might join the CD o .

Definition 18 (Border of a CD o )

Let D γ a be a CD o . We define the border of D γ a and denote B(D γ a ) the set of nodes v ∈ V such that tok γ v = ⊥, and ∃p ∈ P(v)

: p ∈ D γ a ∧ tok γ p ̸ =↑.
The border of a CD o describes the nodes that can join a CD o . On the other hand, some nodes can leave a CD o . Lemma 10 establishes that the only nodes susceptible to leave a CD o during one computing step are the leaves of the CD o : the nodes v such that tok v =↑.

Lemma 10

Let cs = γ → γ ′ be a computing step, and let a ∈ A(γ ′ ).

Let v 1 v 2 • • • v k be a branch of D γ a such that v 1 = a. Then v 1 v 2 • • • v k-1 is a branch of D γ ′ a , and if v k does not execute R Return during cs, then v 1 v 2 • • • v k is a branch of D γ ′ a .
Proof :

If B = v 1 v 2 • • • v k is a branch of D γ ′
a the result is immediate. Let us rather suppose that B is not a branch of D γ ′ a , and let us consider the highest value i such that

B i = v 1 v 2 • • • v i is a branch of D γ ′ a . Remark that v 1 = a is necessarily a branch of D γ ′ a , so i ∈ [1, k -1]. By definition, v i+1 ∈ C D γ a (v i ),
= v k , which means that v i = v k-1 and thus v 1 v 2 • • • v k-1 is a branch of D γ ′ a , and if v k does not execute R Return then v 1 v 2 • • • v k is a branch of D γ ′ a .
Lemma 11 establishes constraints on which actions might be taken by a node.

Lemma 11

Let cs = γ → γ ′ be a computing step, and let v be a node.

If v = r then v can update c v only if tok γ v =↑, and if v ̸ = r then v can update c v only if tok γ v = ⊥. Proof : If v = r then only R r NewDFS can update c v ,

C.2.3 Introduction to the potential function W

To prove that one CD o can only be activated a finite number of time, we associate a weight to each CD o in each configuration γ. We design this weight function (or potential function) such that if one node is activated in the CD o or near it during the computing step γ → γ ′ , then the weight of the CD o is less in γ ′ than in γ. The goal is to provide the domain of weights with a well-founded order, so that such decreasing sequences are necessarily finite. Recall that decreasing occurs only during periods during which no execution of R r NewDFS resets the weight of a CD o to a high value.

Unfortunately, the structure of CD o is too complex for it can be valuated by a object as simple as an integer. The most natural way to associate a weight to a CD o is to build a D o , similar to the CD o considered, but whose nodes are labeled with weights. We call such structures Weighted DODAGs, denoted WD o 's for short.

In this section, we consider (M, ≤) an arbitrary well-founded set. Although our weight function is defined on CD o 's, it is simpler to work through this section by considering arbitrary D o 's. Since CD o 's have a D o structure, all this work naturally applies to CD o 's.

Definition 19 formally introduces WD o 's: the object on which we will define a well-founded order and that will later be considered as the weight of D o 's.

Definition 19 (Weighted DODAG)

A weighted D o (WD o ) is a D o with labels in M : (D a , W), where D a is a D o and W ∈ M Va is a map that associates an element of M to each node of D a .

The next step is to define an order of WD o 's. This is feasible only if the two WD o 's we compare are based on D o 's having the same anchor a. This won't be restrictive since in practice, we compare the weights of the same CD o at different, consecutive, configuration of an execution.

To compare WD o 's, the first step is to compare branches of WD o 's. Since two WD o 's that share the same anchor do not necessarily share the same branches in their topology, the appropriate notion to this comparison is the projection of WD o 's on the branches of the D o under their common anchor. This is similar to what we introduced in Definition 7.

Definition 20 (Projection of a WD o on a Branch)

Let (D a , W) be a WD o , and let B = v 1 v 2 • • • v k be a maximal branch of G a . We call projection of (D a , W) on B, and denote (D a , W)(B) the sequence W(v 1 )W(v 2 ) • • • W(v j ), where D a (B) = v 1 v 2 • • • v j is the projection of D a on B.
Since the branches of two WD o 's may have variable length, we compare them using the alphabetical order (see Definition 9). This order is well-founded since the branches of the WD o 's are all bounded by n, the number of nodes in the graph.

To compare WD o 's, we compare the weights of all the branches which start at a. We define a partial order on WD o 's which share the same anchor by:

(D ′ a , W ′ ) ⪯ (D a , W) ⇐⇒ for all maximal branch B of G a , (D ′ a , W ′ )(B) ⪯ α (D a , W)(B)
By construction, the resulting order is not a total order. Indeed, there exists D o 's and branches such that

(D ′ a , W ′ )(B 1 ) ≺ α (D a , W)(B 1
), on the one hand, and

(D a , W)(B 2 ) ≺ α (D ′ a , W ′ )(B 2
) on the other hand. Yet, we guarantee in the following sections that any computing step makes the weight of the D o decrease (which implies that the corresponding WD o 's are comparable).

Lemma 12

Definition 21 defines a well-founded order.

Proof : By construction, ⪯ is reflexive, anti-symmetric, and transitive. Let us prove that it is also well-founded. Consider an infinite sequence of

WD o 's (D n a , W n ) n∈N such that ∀n, (D n+1 a , W n+1 ) ⪯ (D n a , W n ),
, W n+1 )(B) ⪯ α (D n a , W n )(B)
. But ⪯ α is a well-founded order on sequences of length at most k, and ∀n,

(D n a , W n )(B)
is a sequence of length at most k. Consequently, there exists

N B ∈ N such that ∀n ≥ N B , (D n+1 a , W n+1 )(B) = (D n a , W n )(B).
Since there exists a finite number of maximal branches B of G a , let us consider N = max B (N B ). By definition, ∀n ≥ N , for all maximal branch

B of G a , (D n a , W n )(B) = (D N a , W N )(B), and thus, ∀n ≥ N, (D N a , W N ) ⪯ (D n a , W n ). Since ⪯ is an order, we have ∀n ≥ N, (D n a , W n ) = (D N a , W N ).
We now show how to associate a WD o to any CD o as soon as we are given a weight function W on nodes of G. This association is itself a weight function on CD o , induced by the weight function on nodes. For simplicity, we also call W the induced weight function.

Contrary to what was presented in Definition 19, the weight function on nodes may depend on the global configuration γ of the system, and not only of the state of nodes v. More formally, we now consider a weight function W(v, γ) which associates an element of M to each node in a given configuration. This does not pose any fundamental problem since, given γ, we can still associate a WD o to any CD o D γ a . We can as well associate, given γ, a weight to any projection of D γ a on any branch of G a . This is formally stated in Definition 22.

Definition 22 (Weight of a circulation DAG)

Let W : V × Γ → M be a function that associates a weight to any node of a configuration. For any fixed configuration γ ∈ Γ, we define W( • , γ) ∈ M V Da the function that associates to any node v ∈ V Da the weight of v in γ:

W( • , γ)(v) = W(v, γ).
Then, for all γ ∈ Γ, for all CD o D γ a at γ, we can consider W(D γ a , γ) the weight of D γ a in γ, which is the WD o (D γ a , W( • , γ)). We also define the weight of a branch

B = v 1 v 2 • • • v k of D γ a in γ, and denote W(D γ a (B), γ) = W(D γ a , γ)(B) = (D γ a , W( • , γ))(B) = W(v 1 , γ)W(v 2 , γ) • • • W(v k , γ).
To deal with all the different aspects of the algorithm, we actually define several weight functions in Sections C.2.4 to C.2.8, dealing with the different aspects of our algorithm. Each of these functions defines one different WD o to the same CD o . In order to deduce global properties on the evolution of the entire algorithm, we must combine all those function and to compare the different induces WD o 's all at once. To do so, we simply use the lexicographic order on WD o 's that is induced by the order ⪯ introduced in Definition 21.

Definition 23 (Lexicographic order on WD o 's)

We denote by ⪯ k the lexicographic order on k-tuples of WD o 's which share the same anchor, induced by the order ⪯. ∀k ∈ N, ⪯ k is a well-founded order, as a lexicographic order induced by a well-founded order.

Our goal is now to prove two properties. The first one is that the WD o 's associated to one CD o never increases unless the anchor of the CD o is the root, and the root executes R r NewDFS . The second property is that each time one node of the CD o , or near it, is activated (by a rule which is not R r NewDFS ), the weight of the CD o decreases. A weight function which respects the first property is said pre-admissible, and it is said admissible if it respects both.

Since the weight of a CD o is expressed as a tuple of WD o 's, the formal definitions of admissibility and pre-admissibility lie on the lexicographic order introduced in Definition 23. Each potential function has an even stronger weight as it appears on the first component of the tuple.

The exact definition of admissibility actually depends on how we define what a node near a CD o is. This definition depends on constraints which will emerge from the definitions of the weight functions, and therefore will be provided later, in Definition 26 of Section C.2.9.

We give here the definition of pre-admissibility.

Definition 24 (Pre-admissible weight-functions)

Let W 1 , . . . , W k : V × Γ → M be k weight functions on nodes. We say that (W 1 , . . . , W k ) is pre-admissible if for any computing step cs = γ → γ ′ such that r does not execute R r NewDFS during cs, for all CD o D γ ′ a , we have

W 1 (D γ ′ a , γ ′ ), • • • , W k (D γ ′ a , γ ′ ) ⪯ k W 1 (D γ a , γ), • • • , W k (D γ a , γ) .

Remark 8

In order to have relatively short and readable equations in the following, the previous inequality will often be written:

W 1 , . . . , W k (D γ ′ a , γ ′ ) ⪯ k W 1 , . . . , W k (D γ a , γ)
In Sections C.2.4 to C.2.8 we define five weight functions on nodes, that belong to V ×Γ → N: which are W Ch , W Er , W Circ , W Play and W Nego . Each one of those 5 functions deals with one specific part of the algorithm, by decreasing order of importance, and is treated separately in one of the next five sections. Thus, we define, for each configuration, 5 WD o 's that, associated with the lexicographic order ⪯ 5 , will allow us to formally prove that the token circulation terminates. Figure 22 summarizes the effects of the rules, and for each of them indicates which component of W it decreases.

We prove that W = (W Ch , W Er , W Circ , W Play , W Nego ) is pre-admissible, by proving step by step that all the prefixes of that 5-tuple are pre-admissible. We also establish some properties that will allow us to prove, in Section C.2.9, that (W Ch , W Er , W Circ , W Play , W Nego ) is admissible.

C.2.4 First component of W: W Ch future children of v

Explanations One property which guarantees that circulation rounds are finite is that one node can receive the token from its parent only once, as long as the parent does not return the token to its own parent.

Indeed, once a node u receives the token from one of its parent p, it takes the same color as that parent, and its variable play becomes W. Variable play u then cannot be set to P before tok p is set to ↑, which implies that u cannot take the token once again from p before p itself returns the token to its own parent.

For that reason, the first component of the weight function W should, at least, count on each node u ∈ V the number of children of u that are susceptible to execute R Win before u execute R OfferUp . The variables that we must consider to establish if one node is susceptible to execute R Win are play and c. In the following we detail how we formally define this count.

Let us consider one node v and one of its children u. Remark first that if tok v ∈ {⊥, ↑}, then the weight of v can be defined as 0. Indeed, such a node cannot be involved in a pass of the token to its children before it itself receives the token from one of its parents. Thus, when v receives the token from its parent, its own weight increases from 0 to the actual count of how many children susceptible to execute R Win it has. But at the same moment, the weight of v's parent decreases by one due to v cannot execute R Win anymore. Consequently, due to how we defined ⪯ α on weighted chains, the weight of each branch of a CD o that contains v and its parent decrease when v execute R Win .

We now consider one node v such that tok v / ∈ {⊥, ↑} and one child u of v. In this section, we only focus on the transmission of the token between nodes, and not on the transitions of the variable tok on one node. Thus, we treat indifferently the different cases when tok v ∈ {•, ⋆, ⇊ , ⟲, •, ↓}. Let us establish under which circumstances u might receive the token from v.

node Rule id tok c play W v = r R Win ⊥ → switch P → W W Ch v = r R FakeWin switch P → {W, F} W Ch ∀v ∈ V E TrustChild {•, , , •, } →↓ W Er ∀v ∈ V R Give • → W Circ ∀v ∈ V R NewPlay → W Circ ∀v ∈ V R Drop →↓ W Circ ∀v ∈ V R Nego (1, ⊥) → • W Circ v = r R OfferUp • →↑ W Circ ∀v ∈ V R Receive ↓→ • W Circ ∀v ∈ V R ReNego (1, ⊥) • → • W Circ v = r R Return ↑→ ⊥ → {W, F} W Circ v = r R Lose P → L W Play v = r R ReplayD L → P W Play v = r R ReplayUp W → P W Play v = r R Fake W → F W Play ∀v ∈ V R maxPos max u∈C(v) id u W Nego ∀v ∈ V R NewPh (ph + 1, ⊥) W Nego v = r R NewBit (ph, Bit(ph)) W Nego v = r R ReWin F → W r R r NewDFS ↑→ switch
• Node u can receive the token, at first, if c u ̸ = c v and play u ∈ {P, L}, by simply executing R Win (or after one execution of R ReplayD ).

• Secondly, if c u ̸ = c v and play u ∈ {W, F}, then u can execute R ReplayUp , and R ReWin if necessary, and then arrives in the previous situation. Therefore, we must count u as a node that might receive the token.

• Finally, if c u = c v and play u ∈ {P, L}, then u can execute R Win or R FakeWin , and then arrives in the previous situation.

Note that if c u = c v and play u ∈ {W, F} then u cannot execute R Win nor R FakeWin due to play u , and cannot execute R ReplayUp since tok v ∈ {⊥, ↑}. This is described in Figure 23.

All the transitions presented in the diagram of Figure 23 bring the node that executes the corresponding rule closer to the stable state where c u = c v ∧ play u ∈ {W, F}. We need to fully describe the process that leads to the passing of the token to one child. Therefore, we define W Ch such that any execution of a rule that corresponds to a transition presented in Figure 23 makes W Ch decrease on the parent of the node that executes it.

Yet, remark that we cannot treat R ReplayUp the same way as we treat R Win and R FakeWin . Indeed, any execution of R Win or R FakeWin by one node u requires that at least one parent v of u has its variable tok v different from {⊥, ↑}, which means that any such execution corresponds to a transition on that diagram for that node v. On the contrary, one node u might execute R ReplayUp without any parent v such that tok v / ∈ {⊥, ↑}. Thus, although we treat some, we do not treat all possible executions of R ReplayUp with W Ch . This means that, by the end of this section, we prove that any activation of R Win or R FakeWin makes W decrease, and that some specific activation of R ReplayUp make W decrease. This piece of knowledge will nevertheless be useful in the following sections until we prove that any activation of R ReplayUp makes W decrease. This is formally stated in Theorems 3 and 4.

c u = c v play u ∈ {P, L} c u = c v play u ∈ {W, F} c u = c v play u ∈ {P, L} c u = c v play u ∈ {W, F} R Win (only if tok v =↓ ) R FakeWin R ReplayUp R Win R FakeWin
Definitions Since children u of v move along the different boxes of Figure 23, we must design W Ch such that any transition taken by u makes W Ch (v, γ ′ ) < W Ch (v, γ). Our solution is to attribute different coefficients to the different boxes: the further node u is from the stable configuration c u = c v ∧ play u ∈ {P, L}, the higher the coefficient. Somehow, the coefficient represents the number of transitions needed by one node to reach the stable configuration. The coefficients are the integer above and below the boxes in Figure 24.

AllCand(v) ReplayCand(v) EqColCand(v) c u = c v play u ∈ {P, L} c u = c v play u ∈ {W, F} c u = c v play u ∈ {P, L} c u = c v play u ∈ {W, F} R Win R FakeWin R ReplayUp R Win R FakeWin ×1 ×2 ×0 ×3
Figure 24: Weight associated to a child of node v with tok v / ∈ {⊥, ↑}.

In practice, to make the proof easier to approach, we define 3 sets on each node v, such that any transition taken by one child u of v brings u out of one of the set. Those sets have a non-empty intersection, and are such that the coefficient attributed to one node is the number of sets it belongs to.

• One set includes all the nodes that are potential candidates to receiving the token from Lemma 17 establishes that the function W Ch is adapted to Definitions 9 and 21. Indeed, it might happen that one node sees its weight increase, but only if all of its parents see their weight decrease.

Lemma 17

Let cs = γ → γ ′ be a computing step and let v ∈ V such that v does not execute R r NewDFS during cs. If W Ch (v, γ ′ ) > W Ch (v, γ) then ∀p ∈ P(v) such that tok γ p / ∈ {⊥, ↑}, we have W Ch (p, γ ′ ) < W Ch (p, γ), and there exists at least one such p.

Proof : According to Lemmas 13, 14, and 15, if Theorem 3 establishes that W Ch is pre-admissible.

tok γ v ∈ {•, ⋆, ⇊, ⟲, ↓, •}, then W Ch (v, γ ′ ) ≤ W Ch (v, γ). Furthermore, if tok γ v =↑, then tok γ ′ v ∈ {↑, ⊥} and thus W Ch (v, γ ′ ) = W Ch (v, γ). Finally, if tok γ v = ⊥, then W Ch (v, γ ′ ) > W Ch (v, γ) is possible only if v executes

Theorem 3

Let cs = γ → γ ′ be a computing step, and let a be an anchor at γ ′ , and suppose that a does not execute R r NewDFS during cs. We have

W Ch (D γ ′ a , γ ′ ) ⪯ W Ch (D γ a , γ). Proof : Let B = v 1 v 2 • • • v k be a maximal branch of G a , and let v 1 v 2 • • • v j = D γ ′ a (B) be the projection of D γ ′ a on B.
Let us consider the following cases:

• If v 1 v 2 • • • v j is a branch of D γ a (B) and ∀i ∈ [1, j], W Ch (v i , γ ′ ) = W Ch (v i , γ). Then we have W Ch (v 1 , γ ′ )W Ch (v 2 , γ ′ ) • • • W Ch (v j , γ ′ ) = W Ch (v 1 , γ)W Ch (v 2 , γ) • • • W Ch (v j , γ) and thus W Ch (D γ ′ a (B), γ ′ ) ⪯ α W Ch (D γ a (B), γ). • If v 1 v 2 • • • v j is a branch of D γ a (B) and ∃i ∈ [1, j] : W Ch (v i , γ ′ ) ̸ = W Ch (v i , γ). Let us consider the smallest i such that W Ch (v i , γ ′ ) ̸ = W Ch (v i , γ). According to Lemma 17, W Ch (v i , γ ′ ) < W Ch (v i , γ), and as a consequence, W Ch (v 1 , γ ′ )W Ch (v 2 , γ ′ ) • • • W Ch (v j , γ ′ ) ≺ W Ch (v 1 , γ)W Ch (v 2 , γ) • • • W Ch (v j , γ Thus, we have W Ch (D γ ′ a (B), γ ′ ) ≺ α W Ch (D γ a (B), γ). • If v 1 v 2 • • • v j is not a branch of D γ a . Let us consider v 1 v 2 • • • v l = D γ a (B) the projection of D γ a on B. Since v 1 v 2 • • • v j is not a branch of D γ
a we have 1 ≤ l < j, and thus l + 1 ≤ j. Remark first that since (v l , v l+1 ) is an edge in D γ ′ a , we have tok γ ′ v l / ∈ {↑, ⊥}, and thus tok γ v l ̸ =↑. But v l+1 / ∈ D γ a , so tok γ v l+1 = ⊥, and since v l+1 ∈ D γ ′ a , tok γ ′ v l+1 ̸ = ⊥ so v l+1 executes R Win during cs. Thus, Lemma 16 applies, and as a consequence

W Ch (v l , γ ′ ) < W Ch (v l , γ). Let us consider the smallest i ≤ l such that W Ch (v i , γ ′ ) ̸ = W Ch (v i , γ). According to Lemma 17, W Ch (v i , γ ′ ) < W Ch (v i , γ)
, and as a consequence,

W Ch (v 1 , γ ′ )W Ch (v 2 , γ ′ ) • • • W Ch (v j , γ ′ ) ≺ W Ch (v 1 , γ)W Ch (v 2 , γ) • • • W Ch (v l , γ). Thus, we have W Ch (D γ ′ a (B), γ ′ ) ≺ α W Ch (D γ a (B), γ). We prove that for any maximal branch v 1 v 2 • • • v k of G t , W Ch (D γ ′ a (B), γ ′ ) ⪯ α W Ch (D γ a (B), γ). By definition, we have W Ch (D γ ′ a , γ ′ ) ⪯ W Ch (D γ a , γ).
Theorem 4 and Lemma 18 prove that under certain circumstances, we are certain that the weight of one CD o decreases. The first theorem focuses on the application of rules R Win and R FakeWin , and will be useful to prove that W is an admissible weight function, but also to prove that the other, longer, prefixes of W are pre-admissible. Indeed, if in any computing step, one node executes R Win or R FakeWin , we do not need to look beyond the first component to be assured that the weight does not increase, since ⪯ k is a lexicographic order. The second lemma focuses on the length of the branches of a CD o , and is useful for us to write proofs in the following. Just as we explained before, we can now suppose in the following proofs of pre-admissibility that branches of CD o 's never increase, since it would make the first component of W decrease.

Theorem 4

Let cs = γ → γ ′ be a computing step, and let a be an anchor at γ ′ , and suppose that a does not execute R r NewDFS during cs.

If ∃v ∈ B(D γ a ) such that v executes R Win , R FakeWin , or R ReplayUp during cs, we have W Ch (D γ ′ a , γ ′ ) ≺ W Ch (D γ a , γ). Proof : Let us consider one node v ∈ B(D γ a ) that executes R Win , R FakeWin , or R ReplayUp during cs. By definition, ∃p ∈ P(v) : p ∈ D γ a ∧ tok γ v ̸ =↑. Let us consider B = v 1 v 2 • • • v k a branch of D γ a such that v k = p. According to Lemma 10, B is a branch of D γ ′ a . According to Lemma 16, W Ch (p, γ ′ ) < W Ch (p, γ), and according to Theorem 3, W Ch (D γ ′ a (B), γ ′ ) ⪯ α W Ch (D γ a (B), γ). Consequently, W Ch (D γ ′ a (B), γ ′ ) ≺ α W Ch (D γ a (B), γ)
, and thus according to Theorem 3,

W Ch (D γ ′ a , γ ′ ) ≺ W Ch (D γ a , γ).

Lemma 18

Let cs = γ → γ ′ be a computing step, and let a be an anchor at γ ′ , and suppose that a does not execute R r NewDFS during cs. If there exists

B = v 1 v 2 • • • v k a branch of G a such that D γ ′ a (B) is longer than D γ a (B), then W Ch (D γ ′ a , γ ′ ) ≺ W Ch (D γ a , γ). Proof : Let us consider v 1 v 2 • • • v j = D γ a (B). Let us prove that v = v j+1 satisfies the conditions of Theorem 4. Remark first that tok γ vi ̸ =↑. Indeed, if tok γ vi =↑ then tok γ ′ vi ∈ {↑, ⊥}, which is contradictory since v ∈ C D γ ′ a (v i ). Then, we have tok γ v = ⊥ which implies v ∈ B(D γ a ), otherwise we would have v ∈ C D γ a (v i ). But since v ∈ D γ ′ a , we have tok γ ′ v ̸ = ⊥, which is possible only if v executes R Win during cs.
We can apply Theorem 4 to our situation, and consequently

W Ch (D γ ′ a , γ ′ ) ≺ W Ch (D γ a , γ).

C.2.5 Second component of W: W Er errors descending from v

Explanations One major quantity in our algorithm that should decrease during an execution is the number of nodes v such that Er(v). Indeed, we expect that after some convergence time, no node will execute E TrustChild , and that our CD o will have the expected shape. Although that last sentence will be proven true in the following, the number of nodes v such that Er(v) might occasionally increases. Indeed when a node executes E TrustChild , it might happen that it creates an error in some of its parents. For example, if node v has p as a parent, and tok γ v = ⋆, tok γ p =⇊. We have ¬Er γ (p), but if in γ → γ ′ , v executes E TrustChild , then tok γ ′ v =↓ and thus Er γ ′ (p). In the described case, the number of nodes in error does not increase, but if node v has several parents p with tok γ p ∈ {⇊, ⟲} then that number will actually increase. One first idea to prevent this from happening is that each node counts the number of descendants it has that are in error. This almost works, but not totally. Indeed, suppose v has two parents p, that both have the same parent a, and we have tok γ v = ⋆, tok γ p =⇊, tok γ a =↓. In γ, a only has one descendant in error, but has two once v executes E TrustChild . The fact that errors can split through several branches forces us to design W Er such that it counts a descendant in error as many times as there exists paths to that node.

Fortunately, we can stop the count in our descendants as soon as we reach a node v such that tok v ∈ {⊥, ↑, ↓}. Indeed, such nodes cannot execute E TrustChild , which implies that errors cannot ride up through such nodes.

There exists another situation that increases the number of nodes in error. Suppose one node v executes R Win during γ → γ ′ . We have W Er (v, γ) = 0 by definition. Yet, it might happen that one child u of v is such that tok γ ′ u ̸ = ⊥. It might even happen that W Er (u, γ ′ ) > 0, with an arbitrary value. In such a situation, the weight of v, and thus W Er (D γ a ) can increase arbitrarily. Hopefully, we proved in the previous section that at the same moment, W Ch (D γ a ) decreases, and thus no problem is raised.

Definition According to what precedes, we define W Er the second component of our weight function by 0 on nodes v such that tok v ∈ {↓, ↑, ⊥}, and by the number of nodes in error they can see within range, themselves included, otherwise.

W Er (v, γ) =    0 if tok γ v ∈ {↓, ↑, ⊥} u∈C(v) W Er (u, γ) + 1 if Er γ (v) u∈C(v) W Er (u, γ) otherwise (38) ↑ ⊥ • ↓ 0 1 2 3 3 2 0 6 0 node v such that Er(v) W Er (v, γ)
γ v ̸ = ⊥, or if W Ch (v, γ ′ ) < W Ch (v, γ) which implies that W Ch (D γ ′ a , γ ′ ) ≺ W Ch (D γ a , γ), or if ∃u ∈ C(v)
such that u executes E TrustChild during cs. In that last case, we have Er γ (u) so W Er (u, γ) ≥ 1, and tok γ ′ u =↓ and so W Er (u, γ ′ ) = 0. Since we took v one deepest node such that W Er (v, γ ′ ) > W Er (v, γ), we have ∀u ∈ C(v), W Er (u, γ ′ ) ≤ W Er (u, γ), so, by considering the child that executes E TrustChild , we have u∈C(v) W Er (u, γ ′ ) < u∈C(v) W Er (u, γ), and thus

W Er (v, γ ′ ) ≤ W Er (v, γ).
Theorem 6 proves that under certain circumstances, we are certain that the weight of one CD o decreases. It will be useful to prove that W is an admissible function, but also to prove that the other, longer, prefixes of W are pre-admissible. Indeed, if in any computing step one node executes E TrustChild then we do not need to look beyond the second component to be assured that the weight does not increase, since ⪯ k is a lexicographic order.

Theorem 6

Let cs = γ → γ ′ be a computing step, and let a be an anchor at γ ′ , and suppose that a does not execute R r NewDFS during cs. If ∃v ∈ D γ a such that v executes E TrustChild during cs,

then (W Ch , W Er )(D γ ′ a , γ ′ ) ≺ 2 (W Ch , W Er )(D γ a , γ).
Proof : Let us consider one such node v ∈ D γ a , and one branch B of G a such that v ∈ D γ a (B). If v / ∈ D γ ′ a (B), then according to Lemma 18, we have (W Ch , W Er )(D γ ′ a , γ ′ ) ≺ 2 (W Ch , W Er )(D γ a , γ). Else, remark that W Er (v, γ) > 1 since Er γ (v), and W Er (v, γ ′ ) = 0 since tok γ v =↓. Thus, W Er (v, γ ′ ) < W Er (v, γ), and so

W Er (D γ ′ a (B), γ ′ ) ≺ α W Er (D γ a (B), γ) since v ∈ D γ ′ a (B). Since (W Ch , W Er )(D γ ′ a , γ ′ ) ⪯ 2 (W Ch , W Er )(D γ a , γ), we conclude (W Ch , W Er )(D γ ′ a , γ ′ ) ≺ 2 (W Ch , W Er )(D γ a , γ).

C.2.6 Third component of W: W Circ , circulation of variable tok

Explanations Now that we have considered the cases where nodes execute E TrustChild , we can consider that variable tok is updated in accordance with Figure 3. The third component of the weight function should treat all the transitions of variable tok depicted in this diagram.

We could think at first sight that since the diagram is circular, we will have difficulty defining a weight function that decreases along the diagram. Yet, if the algorithm behaves correctly, when a node v is updated from • to ⇊, one child of v is supposed to execute R Win in the next computing steps, and then W Ch will decrease on the observed CD o . Since W Ch has higher priority in the lexicographic order than W Circ , we are going to design W Circ so that it increases exactly when W Ch decreases. Therefore, we can cycle as many times as necessary through the transition diagram of Figure 3 and having the 3-tuple (W Ch , W Er , W Circ ) decrease at each step.

To do this, we must associate a different weight to a node v with tok v =⇊ depending on whether it still has one child that is going to execute R Win (or R FakeWin ) in the next computing steps. More precisely, if there still exists one child u of v that belongs to Players(v), we associate a lower weight to v that if such child u does not exist. When v executes R Win or R FakeWin , W Circ increases on v, but W Ch decreases at the same time.

But since we work in the framework of self-stabilization, it might happen that registers are incorrectly initialized, and that when node v executes R Give , and updates tok v from • to ⇊, v immediately has no children susceptible to execute R Win . Indeed, if in the initial configuration, id v is inconsistent with the id of its children, it might happen that after some computations, all the children u of v such that play u = P eventually lose the negotiation. In such a situation, after v executes R Give , we arrive in a configuration in which W Circ (v, γ ′ ) is already at its high value. But this high value is precisely designed to be the highest assigned value of the diagram. To overcome that issue, we add one possible value for W Circ (v, γ) when tok γ v = •, higher than the high value for nodes with tok γ v =⇊. This value is taken by W Circ (v, γ) only if we detect that after few computations, we fall into a situation where no children of v can execute R Win . It is crucial that this situation cannot happen consecutively to an execution of R ReNego , otherwise we should also design two possible outcomes for the weight of some node v with tok v = •. The predicate FullRound achieves that detection for node v such that tok v = •.

For the other values that tok v might take, we only associate integers that decrease along the classical scheme depicted in Figure 3. The definition of W Circ is summarized in Figure 26 Definitions The weight of one node v such that tok v =⇊ depends on if it has children susceptible to take the token. If it has, then we set its weight to one low value, so that when the child takes the token, W Ch decreases on v at the same time that we make W Circ increases on v. If it has not, then it must be a high value so that the weight of v can decrease through the transitions of Figure 26.

⊥ ⋆ • ⇊ ⟲ ↓ • ↑ 0 8 2 (7
W ⇊ Circ (v, γ) = 6 if Players γ (v) = ∅ 1 if Players γ (v) ̸ = ∅ (39)
Let us now define the weight of one node v such that tok v = •. The weight of such a node can also be taken between two values that are 2 and 7, so that it can easily be bigger than W ⇊ Circ . We must design W • Circ such that, if after v executes R Give we have W ⇊ Circ (v, γ ′ ) = 6 then we have W • Circ (v, γ) = 7 just before, otherwise the weight would increase. But we also require that we never have W

• Circ (v, γ) = 2 ∧ W • Circ (v, γ ′ ) = 7.
In other words, if W ⇊ Circ is set to 6 immediately after the execution of R Give , it must be detected at the very beginning of the execution (or as soon as tok v is set to •).

The situation described just above happens if before v executes R Give , all the nodes u ∈ Players γ (v) execute R Lose . In such a situation, no children u of v wins the negotiation, and

γ ′ (v). In both cases, W γ ′ Circ (v) = 2 < W γ Circ (v). • If tok γ v =↑ then either v ̸ = r and thus tok γ v ∈ {↑, ⊥} so W Circ (v, γ ′ ) ≤ W Circ (v, γ), either v = r and thus, if activated, v executes R r
NewDFS and the property holds.

Theorem 7 establishes that (W Ch , W Er , W Circ ) is pre-admissible.

Theorem 7

Let cs = γ → γ ′ be a computing step, and let a be an anchor at γ ′ , and suppose that a does not execute R r NewDFS during cs. We have

(W Ch , W Er , W Circ )(D γ ′ a , γ ′ ) ⪯ 3 (W Ch , W Er , W Circ )(D γ a , γ).
Proof : According to Theorem 5, we already have (W Ch , W Er )(D γ ′ a , γ ′ ) ⪯ (W Ch , W Er )(D γ t , γ). Consequently, we only have to prove that if

W Circ (D γ ′ a , γ ′ ) > W Circ (D γ a , γ), then we have (W Ch , W Er )(D γ ′ a , γ ′ ) ≺ 2 (W Ch , W Er )(D γ
a , γ). In the same way as we did in the proof of Theorem 5, we can suppose that for any branch B of G a , D γ ′ a (B) is not longer than D γ a (B). In such circumstances, we have

W Circ (D γ ′ a , γ ′ ) > W Circ (D γ a , γ) only if there exists a branch B of G a such that ∃v ∈ D γ a (B) : W Circ (v, γ ′ ) > W Circ (v,
)(D γ ′ a , γ ′ ) ≺ 2 (W Ch , W Er )(D γ a , γ).
Theorem 8 proves that under certain circumstances, we are certain that the weight of one CD o decreases. It will be useful to prove that W is an admissible function, but also to prove that the other, longer, prefixes of W are pre-admissible. Indeed, if in any computing step one node updates its variable tok then we do not need to look beyond the third component to be assured that the weight does not increase, since ⪯ k is a lexicographic order.

Theorem 8

Let cs = γ → γ ′ be a computing step, and let a be an anchor at γ ′ , and suppose that a does not execute R r NewDFS during cs.

If ∃v ∈ D γ a such that v executes one rule among R Give , R NewPlay , R Drop , R Nego , R OfferUp , R Receive , R Return , R ReNego during cs, then (W Ch , W Er , W Circ )(D γ ′ a , γ ′ ) ≺ 3 (W Ch , W Er , W Circ )(D γ a , γ).
, W Circ )(D γ ′ a , γ ′ ) ⪯ 3 (W Ch , W Er , W Circ )(D γ a , γ), we have (W Ch , W Er , W Circ )(D γ ′ a , γ ′ ) ≺ 3 (W Ch , W Er , W Circ )(D γ a , γ).
C.2.7 Fourth component of W: W Play , circulation of variable play on children Explanations The three weight functions that we previously defined, W Ch , W Er , and W Circ totally embrace the rules that affect tok v and c v . Thus, we can now consider that both these variable are constant on nodes, and focus on the two other variables that are play and id. In this section, we only treat variable play. Remark that the rules R Win , R FakeWin , and R Return have an impact on variable play, but were already treated in Sections C.2.4 and C.2.6. Thus, although we discussed rule R ReplayUp in Section C.2.4, we did not treat all the cases where this rule might be executed, and thus we must consider it in this section. Consequently, the rules that interest us in this section are R Lose , R ReplayD , R ReplayUp , R Fake , and R ReWin . Depending on its variable tok v , it happens that one node v is waiting for some of its children to update their variable play, before it executes a rule that updates tok v to the next state. For example, if tok v =⇊, then v does not execute R NewPlay until all of its children u such that tok u = P updates play u to L, W, or F. In order to prove that our algorithm progresses, and that circulation might terminate, we need to prove that the number of children u of v such that play u = P never increases, at least as long as tok v =⇊. Indeed, as soon as tok v is updated, then we already know that (W Ch , W Er , W Circ ) decreases. Actually, when tok v =⇊, children u of v such that play u = P will update play u with rule R Win or R FakeWin , both cases have already been treated in Section C.2.4, so we do not need to elaborate any further on this case.

There exists other situations where one node v waits until its children u have some specific values for their variable play u before v itself updates tok v . For each of those situations, we want to define W Play such that any time one child u of v updates its variable play u in a sense that allows v to update tok v , W Play decreases on v. Thus, we define W Play such that each node v counts the number of children it has that prevent it from updating its variable tok v . In order to have a function that is pre-admissible, we also require that W Play never increases, and thus that no action taken by one node u might add u to the set of children that prevent one of its parents v to update tok v .

The situations where one node v waits for its children u to update play u occurs when tok v ∈ {•, ⟲, •, ↑}. Let us give some details:

• If tok v = • and b v ̸ = ⊥,
then v waits for some of its children u to execute R Lose and update play u from P to L.

Although rule R Lose could be treated in the following section that focuses on negotiation, we treat it here for two reasons. First, it concerns variable play as well, and thus it remains consistent here. Second, having already treated executions of rule R Lose will help us greatly in the section on negotiation.

• If tok v = • or tok v =⟲, then v does not execute R Drop until all of its children u such that tok u = L execute R ReplayD and update play u to P.

• If tok v =↑, then before executing R Return , v waits for all of its children u such that play u = W execute R ReplayUp or R Fake , and update play u from W to P or F, depending on whether u still has parents in any CD o .

From what precedes, if one node u executes R Lose , R ReplayD , R ReplayUp , or R Fake , it will make decrease the weight of the CD o 's that contain the parents v of u that have the corresponding value of tok v . Indeed, all of these four rules are conditioned by the existence of at least one parent v with the adapted value of tok v .

Remark that we did not mentioned rule R ReWin . It is not difficult to define a weight function that decreases on v each time one child u of v execute R ReWin . The difficulty comes from proving that the weight function we defined that way is pre-admissible. Indeed, R ReWin might be executed in very various situations: as soon as u has one no parent v such that tok v =↑. Unfortunately, there exists situations in which we can give no guarantee that there won't be executions of R Fake that cancels executions of R ReWin , and thus we cannot treat both R Fake and R ReWin at the same layer of W.

However, the design of the algorithm allows us design W Play that is pre-admissible and such that it decreases any time one node u executes R Lose , R ReplayD , R ReplayUp , or R Fake . This is stated in Theorems 9 and 10.

Figure 27 summarizes the different transitions that might be taken by variable play u on one node u. We represented in blue the rules that have already been treated in the previous sections, and in red the rule R ReWin that is not treated in that section.

L P W F {P, L, W, F} R Lose R ReplayD R Win , R FakeWin R F a k e W i n R ReplayUp R ReWin R Fake R R e t u r n R R e t u r n
Furthermore since v ∈ D γ a , it is obvious that tok γ v ̸ = ⊥ and thus that v cannot execute R Win or R FakeWin .

As a direct consequence, we have tok

γ ′ v = tok γ v and c γ ′ v = c γ v . Since tok γ ′ v = tok γ v we can have W Play (v, γ ′ ) > W Play (v, γ) only if tok γ v ∈ {•, ⟲, ↑, •}. Since tok γ v = tok γ ′
v and for the cases where tok γ v ∈ {•, ⟲, •}, we have no children u ∈ C(v) executes R Win or R FakeWin during cs, then we fall in the preconditions of Lemmas 25, 26, and 27. Whatever the value of tok γ v , the corresponding lemma guarantees that W Play (v, γ ′ ) ≤ W Play (v, γ).

Theorem 9 establishes that (W Ch , W Er , W Circ , W Play ) is pre-admissible.

Theorem 9

Let cs = γ → γ ′ be a computing step, and let a be an anchor at γ ′ , and suppose that a does not execute R r NewDFS during cs. We have

(W Ch , W Er , W Circ , W Play )(D γ ′ a , γ ′ ) ⪯ 4 (W Ch , W Er , W Circ , W Play )(D γ a , γ). Proof : Theorem 7 establishes (W Ch , W Er , W Circ )(D γ ′ a , γ ′ ) ⪯ 3 (W Ch , W Er , W Circ )(D γ a , γ). Suppose now W Play (D γ ′ a , γ ′ ) > W Play (D γ a , γ), and prove (W Ch , W Er , W Circ )(D γ ′ a , γ ′ ) ≺ 3 (W Ch , W Er , W Circ )(D γ a , γ).
In the same way as we did in the proof of Theorem 5, we can suppose that for any branch B of G a , D γ ′ a (B) is not longer than D γ a (B). In such circumstances, we have

W Play (D γ ′ a , γ ′ ) > W Play (D γ a , γ) only if there exists a branch B of G a such that ∃v ∈ D γ a (B) : W Play (v, γ ′ ) > W Play (v, γ). But then, according to Lemma 28, we have (W Ch , W Er , W Circ )(D γ ′ a , γ ′ ) ≺ 3 (W Ch , W Er , W Circ )(D γ a , γ).
Theorem 10 proves that under certain circumstances, we are certain that the weight of one CD o decreases. It will be useful to prove that W is admissible, but also to prove that it is pre-admissible.

Theorem 10

Let cs = γ → γ ′ be a computing step, let a be an anchor at γ ′ that does not execute R r NewDFS during cs.

If ∃v ∈ D γ a and u ∈ C Ga (v) such that:

• tok γ v = • and c γ u ̸ = c γ v and u executes R Lose during cs, or • tok γ v ∈ {⟲, •} and c γ u ̸ = c γ v and u executes R ReplayD during cs, or • tok γ v =↑ and c γ u = c γ v and u executes R Fake or R ReplayUp during cs, we have (W Ch , W Er , W Circ , W Play )(D γ ′ a , γ ′ ) ≺ 4 (W Ch , W Er , W Circ , W Play )(D γ a , γ).
Proof : Let us consider such nodes v and u, and one branch

B of G a such that v ∈ D γ a (B). If v / ∈ D γ ′ a (B), or if tok γ ′ v ̸ = tok γ v , or if tok γ v ∈ {•, ⟲, •}
and one child u of v executes R Win or R FakeWin , then we according to Lemma 18, or Theorems 6 and 8, or Theorem 4, we have

(W Ch , W Er , W Circ , W Play )(D γ ′ a , γ ′ ) ≺ 4 (W Ch , W Er , W Circ , W Play )(D γ a , γ)
We can now suppose that v ∈ D γ ′ a (B) and

tok γ ′ v = tok γ v and if tok γ v ∈ {•, ⟲, •} then no child of v executes R Win or R FakeWin .
Depending on which of the three situations has to be considered, Lemma 25, Lemma 26, or Lemma 27 applies and guarantees that W Play (v, γ ′ ) < W Play (v, γ). From Theorem 9 we conclude

(W Ch , W Er , W Circ , W Play )(D γ ′ a , γ ′ ) ≺ 4 (W Ch , W Er , W Circ , W Play )(D γ a , γ).

C.2.8 Fifth component of W: W Nego negotiation between one parent and its children

Explanations Only one aspect of the algorithm has not been treated yet: the negotiation between one node v that has the token tok v = • and its children u ∈ Players(v). This negotiation occurs only if there are several nodes in Players(v), otherwise v decides that the negotiation is terminated, and executes R Give or R OfferUp depending on whether there exist some candidates for the token or not. Furthermore, let us remark that if Players(v) evolves during an execution, whether by an addition (with R ReplayUp ) or a deletion (with R Lose for example), then according to Theorems 4 and 10 the weight of the CD o which contains v decreases. Thus, we can suppose in the following that we work under the following hypothesis: Players(v) is constant, and there are at least two nodes in it.

Due to the impact of PhasePlus(v) on variable ph v , we cannot guarantee at first sight that the negotiation does not cycle. Indeed, if all the children u of v declare that they cannot give an answer for ph v , then v decides to restart from ph v = 1 so it does not eliminate all of its children. But as soon as v can restart, we must prove that it does not restart indefinitely, what would create a livelock in the negotiation phase.

To overcome this problem, we statically determine the first value ph v which, when taken by v, will push one child u ∈ Players(v) to execute R Lose . Such values exist since we supposed that there are at least two nodes in Players(v) and that the identifiers are globally unique. If we prove that ultimately, some node u can only execute R Lose and thus makes W Play decrease, we prove that the negotiation is livelock-free. Unfortunately, it is not trivial to determine the value of the first incoming value of ph v which will induce an execution of R Lose . Basically, we are looking for the lowest value greater or equal to ph v which induces different answers on two children u ∈ Players(v).

One first subtlety comes with the fact that, since we work in the framework of self-stabilization, there might not be such greater value. Indeed, if the initial value of ph v is different from 1, and if all the values of ph v which might differentiate two children u ∈ Players(v) are less than this initial value, then the differentiation will not happen before a reset of ph v . Under such circumstances, v executes a full round of all the possible value for ph, increasing as long as its children u produce answers different from b u = ⊥, and when they all, at the same moment by hypothesis, cannot, v restart from ph v = 1. Then, v will increase ph v until it reaches one value which differentiates two of its children u ∈ Players(v).

One other, trickier, subtlety coming from the self-stabilizing framework, is that the registers of the children might be incorrectly initialized. If, due to an incorrect initialization, we miss an occasion to differentiate two children in Players(v), a similar scheme will happen. In such situation, v increases ph v until it reaches the next value which differentiates two of its children of Players(v). It might even happen that the initial value of ph v is the only value which can differentiate any two children of Players(v). In this situation, node v will execute a full round of all the possible value for ph v , increasing as long as all of its children produce answers different from b u = ⊥, then restarting from ph v = 1 until it reaches again the initial value which differentiates its children. On the contrary, an incorrect initialization of the values of b u on some node u ∈ Players(v) might implies that u executes R Lose while it is not supposed to, according to its actual id. That last case will be said to be a false positive.

Incorrect initializations of variable b u might only happen at the very beginning of the execution, and might be taken into account only if u does not update it before any action if its parent, i.e. if ¬AnswerPar(u, v). Then, as soon as u takes a step, either it executes R Lose , either it updates b u according to its identifier, and then we will not face any incorrect initialization anymore. Thus, we have to consider the possibilities of wrong initializations only in few cases, basically only for the current value of ph v and only if ¬AnswerPar(u, v). For any other situation, Bit u (ph) is the adapted value, which describes the value of b u taken into account during the negotiation.

To summarize, we can distinguish three situations.

• The first, simplest, situation, is when the current value of ph v actually differentiates at least two children of Players(v). This situation includes false positive, when ph v is not meant to play this role regarding to identifiers, and excludes situations where an incorrect initialization of the b u prevents the expected differentiation to actually happen.

• The second situation is when the current value of ph v does not differentiate two children of Players(v), but there exists a value greater than ph v which does. In such a situation, we only have to wait for ph v to increase until it reaches the first such value, and we fall in the previous situation.

• The third and last situation is when neither the current value of ph v , neither any value greater than it, can differentiate two children of Players(v). This situation includes, as an extreme case, the situation where the current value of ph v is the only one which might differentiate two children of Players(v), but an incorrect initialization of some b u prevents the differentiation from being effective. In this third situation, we wait for ph v to increase until the value for which all children of Players(v), at the same moment, answer ⊥. At this moment, ph v is set to 1 and then we fall in one of the previous situations.

We want to design a function dealing with as many aspects, or as many rules, of the algorithm as possible. Thus, we intend to define W Nego such that any action involving R maxPos , R NewPh , or R NewBit , makes W Nego decrease. It is pretty natural to treat R NewPh since it increases (or reduces down to 1) the value of ph v , and thus bring closer to the expected value. Since any two execution of R NewPh are separated by an execution of R maxPos , which updates b v from ⊥ to a value different from ⊥, we will not have much trouble to use those properties in the design of W Nego . Finally, we want W Nego to decrease any time one child u ∈ Players(v) executes R NewBit . In other words, we must, in a certain way, count the number of children of v which can execute R NewBit . But any execution of R NewPh recreates the conditions under which all the nodes u ∈ Players(v) can execute R NewBit , and thus if we simply decrease W Nego by one for the execution of R NewPh , but it increases by |Players(v)| at the same time, we fail. Two options are left to us. First, we can define W Nego as a 2-tuple, the first component focuses on the progress of ph v , and the second one focuses on the decreasing of the number of nodes which can execute R NewBit . The other option is to deal this in one single function, and to give some coefficients to the different components involved. In a certain sense, it boils down to the same as the previous option, but instead of using the lexicographic order, we define manually high coefficients on the first component so that it all works the same with one integer value. To avoid making this proof even more tedious, we chose the second option.

Definitions Before properly defining W Nego , let us first formally determine the three different situations which were described above, whether we reached the expected value for ph v , or whether not but there we will reach this value with only increasing ph v , or whether we will have to reset ph v to 1 before we reach it.

Recall that to decide if the current value of ph v will differentiate two children u ∈ Players(v), we cannot simply rely on the values of Bit u (ph v ). Indeed, we must take into account that the register of b v and/or b u might be incorrectly initialized. If this happens, and if the current state of one node u can be interpreted as an answer by its parent, then it does not update it, and thus b u is the value used to decide what the future of the negotiation is. Otherwise, u has to first execute R NewBit before anything else, and then erase its previous state and only Bit u (ph v ) is to say if we must execute R NewPh at least once before reaching the value that differentiates children of v. By definition, after v executes R NewPh , we necessarily have AnswerPar(u, v) for all children u ∈ Players γ (v). Thus, in such situations, Bit u is the relevant tool to decide whether some value for ph v will differentiate children of v. Remark also that Separators γ (v) only depends on Players γ (v), which will be supposed constant in the following. Consequently, we will suppose Separators γ (v) constant too. Finally, since we are interested in considering the negotiation phase, v has at least two children, and then Separators γ (v) contains at least one value. Let us now define the two other predicates, which correspond to situations where node v will not reset ph v to 1 before it reaches a value which differentiates two of its children, and to the situation where it will.

WontReset γ (v) ≡ ¬Finished γ (v) ∧    ∃i > ph γ v : i ∈ Separators γ (v) ∧ ¬ForcedReset γ (v) (56) WillReset γ (v) ≡ ¬Finished γ (v) ∧    ∀i > ph γ v , i / ∈ Separators γ (v) ∨ ForcedReset γ (v) (57)
Remark that the three predicates Finished, WontReset, and WillReset are mutually exclusive, and that ∀γ ∈ Γ, ∀v ∈ V, Finished γ (v) ∨ WontReset γ (v) ∨ WillReset γ (v). This justifies the use of these three predicates to distinguish cases in any situation.

Let us now define, for each of these three cases, the value of ph which, when reach by ph v , will provoke one execution of R Lose on one child u ∈ Players γ (v).

SepVal γ (v) =    ph γ v if Finished γ (v) min{i | i ∈ Separators γ (v) ∧ i > ph γ v } if WontReset γ (v) min{i | i ∈ Separators γ (v)} if WillReset γ (v) (58)
Finally, we are able to define one first aspect of W Nego , which is the distance between ph γ v and SepVal γ (v), which corresponds to the number of executions of R NewPh required for v. This definition is very simple in both situations Finished γ (v) and WontReset γ (v). It is slightly more difficult when WillReset γ (v) since we must determine how high ph v will reach before it is reset to 1. Two situations might occur. If, due to an incorrect initialization of variables, all the children u of Players γ (v) produce ⊥ as an answer for ph γ v , then the next execution of R NewPh by v will set ph v to 1 and then ph γ v is the maximal value which will be reached before ph v is reset to 1.

Otherwise, there will be at least one execution of R NewPh by v before we reach the maximal value, and thus only the functions Bit u are relevant. In this last case, the maximal value reached before ph v is reset to 1 is the lowest value such that, when reached, all the children u of Players γ (v) produce ⊥ as an answer.

MaxPh γ (v) = ph γ v if ForcedReset γ (v) min{i > ph γ v | ∀u ∈ Players γ (v) : Bit u (i) = ⊥} if ¬ForcedReset γ (v) (59)
Finally, the definition of SepDist(v) which is the number of executions of R NewPh v has to make before we have ph v = SepVal γ (v).

SepDist γ (v) =    0 if Finished γ (v) SepVal γ (v) -ph γ v if WontReset γ (v) SepVal γ (v) + (MaxPh γ (v) -ph γ v ) if WillReset γ (v) (60)
Finally, since b γ v = ⊥ we have ¬OneDiffers γ (v), so Finished γ (v) ⇐⇒ TwoDiffer γ (v) ⇐⇒ TwoDiffer γ ′ (v) ⇐⇒ OneDiffers γ ′ (v) ∨ TwoDiffer γ ′ (v) ⇐⇒ Finished γ ′ (v).

The four following lemmas give information on how an execution of R NewPh might alter some of the predicates we consider here, or establish relations between them. Lemma 35 proves that one node v which executes R NewPh resets ph v = 1 if and only if it was actually detected by ForcedReset before its action.

Theorem 11 establishes that (W Ch , W Er , W Circ , W Play , W Nego ) is pre-admissible.

Theorem 11

Let cs = γ → γ ′ be a computing step and let a be an anchor at γ ′ such that a does not execute R r NewDFS during cs. (W Ch , W Er , W Circ , W Play , W Nego )(D γ ′ a , γ ′ ) ⪯ 5 (W Ch , W Er , W Circ , W Play , W Nego )(D γ a , γ). Theorem 12 establishes that under certain circumstances, we are certain that the weight of one CD o decreases. It will we useful to prove the admissibility of W.

Theorem 12

Let cs = γ → γ ′ be a computing step and let a be an anchor at γ ′ such that a does not execute R r NewDFS during cs.

C.2.9 Conclusions

In this section we combine the results of Sections C.2.4 to C.2.8 to provide a suitable definition of admissible potential function. More precisely, we provide a definition of admissibility which is wide enough to include our weight function W, and tight enough to be convenient in the following proofs.

The final theorem of this section states that our algorithm satisfies Condition 2 of Specification 1, but other intermediate theorems will be used in the following section.

From now on, to ease the reading, when we use comparison operations on 5-tuple induced by W, we simply use the symbol ≺ rather than ≺ 5 to denote the lexicographic order on 5-tuples of WD o 's.

Theorem 13 states that W is pre-admissible. Let cs = γ → γ ′ be a computing step, let a be an anchor at γ ′ , and let u ∈ V be a node. We say that u activates D γ a during cs if:

• u = a and u executes R r NewDFS during cs, or • ∃v ∈ D γ a , v ∈ P eq (u), tok γ v =↑ and u executes R Fake or R ReplayUp during cs.

We say that D γ a is activated during cs if there exists one node u ∈ V which activates D γ a during cs.

We now prove that the definition of activation matches the evolution of CD o 's. Namely, if one CD o is not activated during one computing step, either it is unchanged, either it disappears, its anchor becoming an intern node of one other CD o .

Lemma 48

Let cs = γ → γ ′ be a computing step, and let a ∈ A(γ) be an anchor at γ. If D γ a is not activated during cs then either D γ ′ a = D γ a , either a / ∈ A(γ ′ ).

Proof : Let us suppose that D γ a is not activated during cs and that a ∈ A(γ ′ ), and let us prove D γ ′ a = D γ a . To achieve this, let us prove that for all branch

B = v 1 • • • v k of G a , D γ ′ a (B) = D γ a (B).
Remark first that ∀i ∈ [1, k], tok γ ′ vi = tok γ vi , which implies D γ a (B) ⊂ D γ ′ a (B). We have already seen in the proof of Lemma 18 that if D γ ′ a (B) is longer than D γ a (B) then there exists v ∈ B(D γ a ) which executes R Win during cs, which would activate D γ a . Consequently, D γ ′ a (B) = D γ a (B). This, being true for all branch B of G a , proves D γ ′ a = D γ a .

We now prove that the definition of activation captures almost all computing steps of our algorithm. The only situation in which no CD o is activated is when all activated nodes execute R ReWin , rule which is not considered by W, but which cannot be responsible of livelock only by itself.

Lemma 49

Let cs = γ → γ ′ be a computing step. There exists an anchor a ∈ A(γ) such that D γ a is activated during cs, or all nodes activated during cs execute R ReWin .

Proof : Let us suppose that there exists at least one node u ∈ V such that u executes one rule different from R ReWin during cs.

• If u executes R r NewDFS during cs then u is the root, and u activates D We can finally provide a definition of admissibility, which corresponds to our weight function W according to Theorem 14.

Definition 26 (Admissible weight function)

Let W 1 , . . . , W k : V × Γ → M be k weight functions on nodes such that (W 1 , . . . , W k ) is preadmissible. We say that (W 1 , . . . , W k ) is admissible if for all computing step cs = γ → γ ′ , for all CD o D γ ′ a , if D γ a is activated during cs and if a does not execute R r NewDFS during cs, then

(W 1 , . . . , W k )(D γ ′ a , γ ′ ) ≺ k (W 1 , . . . , W k )(D γ a , γ) Theorem 14
W is admissible. We now prove that if the anchor of a CD o does not execute R r NewDFS , then the CD o can only be activated a finite number of time.

Theorem 15

Let ϵ = γ 0 → γ 1 → • • • be an infinite execution, and let a ∈ V such that ∀t ≥ 0, a ∈ A(γ t ), and such that a does not execute R r NewDFS during ϵ. There only exists a finite number of computing steps cs t = γ t → γ t+1 such that D γt a is activated during cs t .

Proof : According to Theorem 14, W is admissible, so if D γt a is activated during cs t , we have W(D γt+1 a , γ t+1 ) ≺ W(D γt a , γ t ). Let us now reason by contradiction and suppose that there exists an infinity of such computing steps, cs t0 , cs t1 , . . . . We have ∀i ≥ 0, W(D γt i +1 a , γ ti+1 ) ≺ W(D γt i a , γ ti ). Furthermore, according to Theorem 13, we also have ∀i ≥ 0, W(D γt i+1 a , γ ti+1 ) ⪯ W(D γt i +1 a , γ ti+1 ). Thus, we deduce ∀i ≥ 0, W(D γt i+1 a , γ ti+1 ) ≺ W(D γt i a , γ ti ). Since ≺ is a well-founded order on WD o 's, such infinite decreasing sequence does not exist, and thus we raised a contradiction. Consequently, there only exists a finite number of computing steps cs t = γ t → γ t+1 such that D γt a is activated during cs t .

The following theorem is crucial, since it states that at some point, the CD o which are not anchored at the root cease being activated, and cease disappearing too. It is a key theorem to prove the last result of this section, but will also be determining in the following section to prove the fairness of our algorithm.

Theorem 16

Let ϵ = γ 0 → γ 1 → • • • be an infinite execution. There exists t 0 ≥ 0 such that for all t ≥ t 0 , A * (γ t ) = A * (γ t 0 ) and ∀a ∈ A * (γ t ), D γt a is not activated during γ t → γ t+1 .

Proof : Let us first define t 0 , and let us consider a ∈ A * (γ 0 ). If ∃t ≥ 0 : a / ∈ A * (γ t ) then let us set t a = t. According to Lemma 9, ∀t ≥ t a , a / ∈ A(γ t ). Otherwise, we have ∀t ≥ 0, a ∈ A * (γ t ). According to Theorem 15, there exists only a finite number of computing steps cs t = γ t → γ t+1 such that D γt a is activated during cs t (since a ̸ = r, it cannot execute R r NewDFS ). Let us consider t ′ the highest value of t such that D γt a is activated during cs t , and let us set t a = t ′ + 1.

Let us now set t 0 = max a∈A * (γ0) t a . Let us consider one anchor a ∈ A * (γ t0 ). We have ∀t ≥ t 0 , a ∈ A * (γ t ), since if not, we would have t a > t 0 which is contradictory with the definition of t 0 . Therefore we have ∀t ≥ t 0 , A * (γ t0 ) ⊆ A * (γ t ), and according to Lemma 9 we conclude ∀t ≥ t 0 , A * (γ t0 ) = A * (γ t ).

Furthermore, since ∀t ≥ t 0 , a ∈ A * (γ t ), t a has been defined as one more than the highest value such that D γt a is activated during cs t . Therefore, ∀t ≥ t 0 , D γt a is not activated during cs t .

Figure 2 :

 2 Figure 2: Local algorithm for a node v of DFS Token circulation

Figure 3 :

 3 Figure 3: Transition diagram for variable tok v .

Figure 5 :

 5 Figure 5: Cleaning children before sending up the token in a triangle: play v = F.

  a

Figure 7 :

 7 Figure 7: Example of a DODAG under the anchor a in blue, and of a sub-DODAG of G in red

Figure 8 :

 8 Figure 8: Node with several parents indicating a token

Figure 9 :

 9 Figure 9: Execution of rules for returning the token back to one child. The activated node is the one with its line doubled

Figure 11 :RFigure 12 :

 1112 Figure11: Chain of the states taken by a node during the execution of the algorithm. The update of c v is represents by color gray. Rules in blue corresponds to the negotiation. Rules in red correspond to the sending of a token from a child to a parent. Rules in black correspond to the sending of a token from a parent to a child.

Figure 13 :

 13 Figure 13: Proof of Lemma 1

Figure 14 : 2 ∀v

 142 Figure 14: Proof of Lemma 2

Figure 15 :

 15 Figure 15: Proof of Lemma 3, part. 1

Figure 16 :

 16 Figure 16: Proof of Lemma 3, part. 2

  ∀c ∈ C(v) : tokc ∈ {⊥, ⋆} ∀c ∈ Cneq(v) : play c ̸ = L ∨ tokc = ⋆ v : RDrop ∃c ∈ C(v) : play c = L ∧ tokc = ⊥ ∃p ∈ Pneq(c) : tokp ∈ {•, ⇊} p : Lemma 3 or Lemma 2 ∀p ∈ Pneq(c) : tokp / ∈ {•, ⇊} c : RReplayD ∃c ∈ C(v) : tokc ̸ ∈ {⊥, ⋆} v : ETrustChild

Figure 17 :

 17 Figure 17: Proof of Lemma 4

  = • ∀c ∈ C(v) : tokc = ⊥ ∃c ∈ Cneq(v) : play c = L ∃p ∈ Pneq(c) : tokp ∈ {•, ⇊} p : Lemma 3 or Lemma 2 ∀p ∈ Pneq(c) : tokp / ∈ {•, ⇊} c : RReplayD ∀c ∈ Cneq(v) : play c ̸ = L v : RReNego ∃c ∈ C(v) : tokc ̸ = ⊥ ∃c ∈ C(v) : tokc =↑ c : Lemma 1 ∃c ∈ C(v) : tokc / ∈ {⊥, ↑} v : ETrustChild

Figure 18 : 5 Tools Lemma 5 ∀v

 1855 Figure 18: Proof of Lemma 5

Figure 19 : 6 ∀v

 196 Figure 19: Proof of Lemma 6

  tok v =↓ ∃u ∈ C(v) : tok u =↓ u : Lemma:7, prof u < prof v ∃u ∈ C(v) : tok u ∈ {⇊, •, ⟲, •,⋆} u : Lemma 2 or Lemma 3 or Lemma 4 or Lemma 5 or Lemma 6 ∀u ∈ C(v) : tok u ∈ {⊥, ↑} v : R Receive

Figure 20 :

 20 Figure 20: Proof of Lemma 7

Theorem 2 ∀γ

 2 ∈ Γ, A e (γ) ̸ = ∅ Proof : Let γ ∈ Γ be a configuration. Since tok r ∈ {↑, ⇊, •, ⟲, •, ⋆, ↓}, one of the following lemmas applies: 1, 2, 3, 4, 5, 6, 7.

Figure 21 :

 21 Figure 21: Example of three CD o 's in the same graph G

  and let us prove that there exists N ∈ N such that ∀n ≥ N, (D n a , W n ) = (D N a , W N ). Let B be a maximal branch of G a , and let k be the length of B. By definition, ∀n, (D n+1 a

Figure 22 :

 22 Figure 22: Dedicated weight function for each rule. For readability, one color is associated to each weight function.

Figure 23 :

 23 Figure 23: Evolution of the state of a child of node v with tok v / ∈ {⊥, ↑}.

Figure 26 :

 26 Figure 26: Value of W Circ depending on the variable tok v .

  We have ∀u ∈ C neq γ (v), play γ u ̸ = L. Let us first prove that ∀u ∈ C neq γ ′ (v), play γ ′ u ̸ = L, and let us consider u ∈ C γ (v). Since v executes R ReNego during cs, we have tok γ u = ⊥. If c γ u = c γ v then u switches its color only if it executes R Win or R FakeWin , and thus the property holds. Otherwise if c γ u = c γ v then play γ u ̸ = L and since tok γ v = • u cannot execute R Lose during cs, and thus play γ ′ u ̸ = L. Since b γ ′ v = ⊥, we have Losers γ ′ (v) = ∅. Thus, either ∃u ∈ Players γ ′ (v) and thus Losers γ ′ ̸ = Players γ ′ (v) so ¬FullRound γ ′ (v), either Players γ ′ (v) = ∅ but then according to what we established just above, we have Candidates γ ′ (v) = ∅ and once again ¬FullRound

Proof:

  Let us consider one such node v ∈ D γ a , and one branchB of G a such that v ∈ D γ a (B). If v / ∈ D γ ′ a (B) then according to Lemma 18 we have (W Ch , W Er , W Circ )(D γ ′ a , γ ′ ) ≺ 3 (W Ch , W Er , W Circ )(D γ a , γ).Else, since any of these rules guarantee that W Circ (v, γ ′ ) ̸ = W Circ (v, γ) and since we established in Theorem 7 that (W Ch , W Er

Figure 27 :

 27 Figure 27: Diagram of variable play u .

  Separators γ (v) = {ph ∈ [0, ⌈log n⌉] | ∃u 1 , u 2 ∈ Players γ (v) : Bit u 1 (ph) ̸ = Bit u 2 (ph)} (55)

Proof:

  According to Theorem 9, (W Ch , W Er , W Circ , W Play )(D γ ′ a , γ ′ ) ⪯ 4 (W Ch , W Er , W Circ , W Play )(D γ a , γ).If (W Ch , W Er , W Circ , W Play )(D γ ′ a , γ ′ ) ≺ 4 (W Ch , W Er , W Circ , W Play )(D γ a , γ), then the result is trivial. Let us now suppose that (W Ch , W Er , W Circ , W Play )(D γ ′ a , γ ′ ) = (W Ch , W Er , W Circ , W Play )(D γ a , γ), and prove that W Nego (D γ ′ a , γ ′ ) ⪯ W Nego (D γ a , γ).In the same way we did in the proof of Theorem 5, we can suppose that for any branch B of G a , D γ ′ a (B) is not longer than D γ a (B). In such circumstances, we haveW Nego (D γ ′ a , γ ′ ) ≻ W Nego (D γ a , γ) only if there exists a branch B of G a such that ∃v ∈ D γ ′ a (B) such that W Nego (v, γ ′ ) > W Nego (v, γ). Let us consider one such node v ∈ D γ ′a (B). According to Theorems 6 and 8, we havetok γ ′ v = tok γ v . If tok γ v ̸ = •, then W Nego (v, γ ′ ) = 0 = W Nego (v, γ). If tok γ v = • and tok γ ′ v =•, then we fall under the hypothesis of Lemma 47 and thus W Nego (v, γ ′ ) ≤ W Nego (v, γ).Thus, for any branch B of G a , for any node v ∈ D γ ′ a (B), W Nego (v, γ ′ ) ≤ W Nego (v, γ), and thus W Nego (D γ ′ a , γ ′ ) ⪯ W Nego (D γ a , γ).

  If ∃v ∈ D γ a such that tok γ v = • and either v executes R NewPh or R maxPos during cs, either ∃u ∈ Players γ (v) such that u executes R NewBit during cs, then(W Ch , W Er , W Circ , W Play , W Nego )(D γ ′ a , γ ′ ) ≺ 5 (W Ch , W Er , W Circ , W Play , W Nego )(D γ a , γ) Proof : According to Theorem 11, (W Ch , W Er , W Circ , W Play , W Nego )(D γ ′ a , γ ′ ) ⪯ 5 (W Ch , W Er , W Circ , W Play , W Nego )(D γ a , γ). If (W Ch , W Er , W Circ , W Play )(D γ ′ a , γ ′ ) ≺ 4 (W Ch , W Er , W Circ , W Play )(D γ a , γ), then the result is trivial. Let us now suppose that (W Ch , W Er , W Circ , W Play )(D γ ′ a , γ ′ ) = (W Ch , W Er , W Circ , W Play )(D γ a , γ), and prove that W Nego (D γ ′ a , γ ′ ) ≺ W Nego (D γ a , γ). Let us consider v ∈ D γ a such that tok γ v =• and either v executes R NewPh or R maxPos during cs, either ∃u ∈ Players γ (v) such that u executes R NewBit during cs. According to Theorems 6 and 8, we have tok γ ′ v = •. Thus, we fall under the hypothesis of Lemma 47 and we haveW Nego (v, γ ′ ) ≺ W Nego (v, γ). Thus, W Nego (D γ ′ a , γ ′ ) ̸ = W Nego (D γ a , γ) so according to Theorem 11, we conclude that (W Ch , W Er , W Circ , W Play , W Nego )(D γ ′ a , γ ′ ) ≺ 5 (W Ch , W Er , W Circ , W Play , W Nego )(D γ a , γ).

Theorem 13

 13 Let ϵ = γ 0 → γ 1 → • • • → γ m be an execution. If a is an anchor at γ m , and if a does not execute R r NewDFS during ϵ, then W(D γm a ) ⪯ W(D γ 0 a ). Proof : By definition, ∀t ∈ [0, m -1], a does not execute R r NewDFS during γ t → γ t+1 , so according to Theorem 11, ∀t ∈ [0, m -1], W(D γt+1 a ) ⪯ W(D γt a ). By transitivity, we conclude W(D γm a ) ⪯ W(D γ0 a ). As hinted above, to define admissibility we must first interest to what an activation of a CD o is. Definition 25 (Activation of a CD o )

•

  u ∈ B(D γ a ) and u executes R Win or R FakeWin during cs, or • u ∈ D γ a and u executes E TrustChild or R Give or R NewPlay or R Drop or R Nego or R OfferUp or R Receive or R Return or R ReNego or R NewPh or R maxPos during cs, or • ∃v ∈ D γ a , v ∈ P(u), tok γ v = • and u executes R Lose or R NewBit during cs, or • ∃v ∈ D γ a , v ∈ P neq (u), tok γ v ∈ {⟲, •} and u executes R ReplayD during cs, or

  γ r . • If u executes R Win or R FakeWin during cs then ∃u ∈ P(v) : tok γ p / ∈ {⊥, ↑, ↓}, so according to Lemma 8, ∃a ∈ A(γ) such that v ∈ D γ a and thus u ∈ B(D γ a ), and u activates D γ a . • If u executes E TrustChild or R Give or R NewPlay or R Drop or R Nego or R OfferUp or R Receive or R Return or R ReNego or R NewPh or R maxPos during cs then tok γ u ̸ = ⊥ so according to Lemma 8, there exists a ∈ A(γ) such that u ∈ D γ a and thus u activates D γ a . • If u executes R Lose or R NewBit during cs then LoseNeg γ (u) ∨ AnswerNeg γ (u). In both cases, ∃p ∈ P(u) : tok γ p = •, so according to Lemma 8, there exists a ∈ A(γ) such that v ∈ D γ a and thus u activates D γ a . • If u executes R ReplayD during cs then ReplayL γ (u) and thus ∃p ∈ P neq (u) : tok γ p ∈ {⟲, •}. According to Lemma 8, there exists a ∈ A(γ) such that v ∈ D γ a and thus u activates D γ a . • If u executes R Fake or R ReplayUp during cs then ∃v ∈ P neq γ (u) : tok γ v =↑. According to Lemma 8, there exists a ∈ A(γ) such that v ∈ D γ a and thus u activates D γ a .

Proof:

  We established in Theorem 13 that W is pre-admissible. Let us now consider one computing step γ → γ ′ , one CD o D γ ′ a which is activated during cs, and suppose that a does not execute R r NewDFS during cs. Let us consider one node u which activates D γ a during cs. • If u ∈ B(D γ a ) and u executes R Win or R FakeWin during cs, then according to Theorem 4, W(D γ ′ a , γ ′ ) ≺ W(D γ a , γ). • If u ∈ D γ a and u executes E TrustChild or R Give or R NewPlay or R Drop or R Nego or R OfferUp or R Receive or R Return or R ReNego or R NewPh or R maxPos during cs, then according to Theorems 6, 8, and 12, W(D γ ′ a , γ ′ ) ≺ W(D γ a , γ). • ∃v ∈ D γ a , v ∈ P(u), tok γ v =• and u executes R Lose or R NewBit during cs, then since OkNeg γ (u), we deduce v ∈ P neq γ (v), and thus according to Theorems 10 and 12W(D γ ′ a , γ ′ ) ≺ W(D γ a , γ). • ∃v ∈ D γ a , v ∈ P neq (u), tok γ v ∈ {⟲, •} and u executes R ReplayD during cs, then according to Theorem 12 W(D γ ′ a , γ ′ ) ≺ W(D γ a , γ). • ∃v ∈ D γa , v ∈ P eq (u), tok γ v =↑ and u executes R Fake or R ReplayUp during cs, then according to Theorem 12 W(D γ ′ a , γ ′ ) ≺ W(D γ a , γ).

  W

		RReplayUp	RNewBit	RmaxPos -RNewPh
				RWin	RNego	RGive	RNewPlay	RDrop	RReceive
		RFakeWin
	RFake	RReWin	R F a k e W i n	RLose RReplayD	RReturn	ROfferUp	RReNego

  2.1 we present the inherent difficulties to overcome for proving our results, and show how CD o 's and WD o 's are suitable solutions. In Section C.2.2 we formally define CD o 's and establish basic properties on them. In Section C.2.3 we show how to define the weight function we use, and introduce the concept of WD o 's. Then, in Sections C.2.4, C.2.5, C.2.6, C.2.7, and C.2.8 we define the actual weight function, step by step, and prove properties on it at each step. Finally, we establish our main theorems in Section C.2.9.

  which is possible only if v executes R Win during cs. But this is possible only if v has one parent p such that tok γ p =⇊. But in such a case, we necessarily have tok γ ′ Let us prove that tok γ ′ p / ∈ {⊥, ↑}. Rule R OfferUp is the only rule whose effect might update tok from a state that is neither ⊥ nor ↑, to a state that is ⊥ or ↑. But p can execute R OfferUp during cs only if tok γ p = •. Under such circumstances, since tok γ v ̸ = ⊥, Er γ (p) = true, so p cannot execute R OfferUp during cs. Thus, tok γ ′

p ∈ {⇊, ⟲, ↓}, and thus v / ∈ A(γ ′ ).

• Suppose now that tok γ v ̸ = ⊥. Since v / ∈ A(γ), v has one parent p such that tok γ p / ∈ {⊥, ↑}. p / ∈ {⊥, ↑} and by definition, v / ∈ A(γ ′ ).

  so tok γ vi / ∈ {⊥, ↑} and tok γ vi+1 ̸ = ⊥. Let us first prove that tok γ ′ vi / ∈ {⊥, ↑}. The only possibility for the opposite would be that v i executes R OfferUp during cs. But this implies that tok γ vi = • and thus Er γ (v i ) due to v i+1 . Thus, if activated, v i does not execute R OfferUp during cs but E TrustChild . Return during cs. But then, tok γ vi+1 =↑ and thus v i+1 has no children in D γ a . We deduce that v i+1

	Consequently, since we have v i+1 / ∈ C D γ ′

a (v i ), we deduce that tok γ ′ vi+1 = ⊥, and thus v i+1 executes R

  and it is enabled only if tok γ v =↑. If v ̸ = r then only R Win and R FakeWin can update c v , and both are enabled only if tok γ

v = ⊥.

  One WD o D 1 a is less than or equal to one other WD o D 2 a if, for any branch B of G a the D o under a, the projection of D 1 a on B is less than or equal to the projection of D 2 a on B. Definition 21 presents a well-founded order on WD o 's.

	Definition 21 (Order on WD o 's)

  R Win during cs, and thus Lemma 16 states that ∀p ∈ P(v) such that tok γ p / ∈ {⊥, ↑}, we have W Ch (p, γ ′ ) < W Ch (p, γ).

  Figure 25: Example of the definition of W Er on a D o .Proofs Lemma 19 describes under which conditions one node that is not in error before a computing step can become in error after that computing step. It states that either it makes W Ch decrease, either it comes from the fact that one child of that node executed E TrustChild ,We suppose now that for any branchB of G a , D γ ′ a (B) is not longer than D γ a (B). Let us establish that ∀v ∈ D γ ′ a , W Er (v, γ ′ ) ≤ W Er (v, γ), or W Ch (D γ ′ a , γ ′ ) ≺ W Ch (D γ a , γ). Since the branches of D γ ′ a are included in the branches of D γ a , this becomes W Er (D γ ′ a , γ ′ ) ⪯ W Er (D γ a , γ) or W Ch (D γ ′ a , γ ′ ) ≺ W Ch (D γa , γ), and thus this actually proves the theorem. Let us prove that if ∃v ∈ D γ ′ a :W Er (v, γ ′ ) > W Er (v, γ) then W Ch (D γ ′ a , γ ′ ) ≺ W Ch (D γ a , γ),and let us consider one such v with highest depth. Let us first prove that tok γ v / ∈ {⊥, ↑, ↓}. Since v ∈ D γ a , tok γ v ̸ = ⊥. If tok γ v =↑ then tok γ ′ v ∈ {↑, ⊥}, and thus W Er (v, γ ′ ) = 0 which is contradictory with our hypothesis, so tok γ v ̸ =↑. Finally, if tok γ v =↓ then W Er (v, γ ′ ) > 0 is possible only if v executes R Receive during cs, which implies that ∀u ∈ C(v), tok γ u ∈ {⊥, ↑}. None of these children executes R Win during cs, because if one u does then the edge (v, u) belongs to D γ ′ a (because tok γ ′ v = •) while it does not belong to D γ a , which is contradictory with our hypothesis on branches. Consequently, ∀u ∈ C(v), tok γ ′ u ∈ {⊥, ↑}, and thus ¬Er γ ′ (v), and W Er (v, γ ′ ) = 0. Thus, we can indeed assume that tok γ v / ∈ {⊥, ↑, ↓}. Since all branches of D γ ′ a are also branches of D γ a , and since v is one deepest node of D γ ′ a such that W Er (v, γ ′ ) > W Er (v, γ), we have ∀u ∈ C(v), W Er (u, γ ′ ) ≤ W Er (u, γ). As a consequence, W Er (v, γ ′ ) > W Er (v, γ) becomes possible only if ¬Er γ (v) and Er γ ′ (v). According to Lemma 19, this is possible only if during cs, v executes R Win , which cannot happen since tok

  γ). Let us now apply Lemma 24. If v executes R Win or E TrustChild (it cannot execute R r NewDFS by hypothesis), then Theorem 3 or Theorem 5 guarantees that (W Ch , W Er )(D γ ′ a , γ ′ ) ≺ 2 (W Ch , W Er )(D γ a , γ). Win or R FakeWin or R ReplayUp or E TrustChild , and once again Theorem 3 or Theorem 5 guarantees that (W Ch , W Er

	Otherwise, tok γ v / ∈ {⊥, ↑, ↓} and ∃u ∈ C(v) that executes R

This work has been partially supported by the ANR projects SKYDATA (ANR-22-CE25-0008) and DREAMY (ANR-21-CE48-0003).

v, that is to say all the children u of v that are not in a stable state.

• One other set, included in the first one, includes all of those candidates that must execute R ReplayUp before they might receive the token from v.

• Finally, the last set, included in the second one, includes all of those candidates that must execute R Win or R FakeWin before they can execute R ReplayUp and receive the token from v, that are also the candidates that are the same color as v.

Let us define those three sets, starting from the last, and smallest, one.

Finally, we can define W Ch (v, γ) such that the coefficients on Figure 24 are respected:

Proofs Lemmas 13, 14, and 15 state that ∀v ∈ V , the three sets defined previously can only decrease during an execution, as long as tok v / ∈ {⊥, ↑}. Basically, we prove that there is no other transition that the ones we represented in Figure 24. These three lemmas are one of the main arguments to establish that W Ch is a pre-admissible weight function.

Lemma 13

Let cs = γ → γ ′ be a computing step and let v ∈ V be a node. If tok γ v / ∈ {⊥, ↑} then AllCand γ ′ (v) ⊆ AllCand γ (v).

Proof : We prove the equivalent statement:

Since tok γ v / ∈ {⊥, ↑}, then according to Lemma 11, v does not update c v during cs. Let us consider one child u of v such that u / ∈ AllCand γ (v). By definition, c γ u = c γ v ∧ play γ u ∈ {W, F}. During cs, u does not execute R Win nor R FakeWin since play γ u ̸ = P, and does not execute R r

NewDFS

since it has at least one parent. Furthermore, u does not execute R ReplayUp during cs since v ∈ P eq γ (u) ∧ tok γ v =↑. Thus,

Lemma 14

Let cs = γ → γ ′ be a computing step and let v ∈ V be a node. If tok γ v / ∈ {⊥, ↑} then ReplayCand γ ′ (v) ⊆ ReplayCand γ (v).

Proof : We prove the equivalent statement:

Since tok γ v / ∈ {⊥, ↑}, then according to Lemma 11, v does not update c v during cs. Let us consider one child u of v such that u / ∈ ReplayCand γ (v). If u / ∈ AllCand γ (v) then according to Lemma 13, u / ∈ AllCand γ ′ (v) and thus u / ∈ ReplayCand γ ′ (v). Let us suppose now that u ∈ AllCand γ (v) \ ReplayCand γ (v), i.e. c γ u ̸ = c γ v ∧ play γ u ∈ {P, L}. If u executes R Win or R FakeWin during cs, then c γ ′ u = c γ ′ v ∧ play γ ′ u = W and thus u / ∈ ReplayCand γ ′ (v). Otherwise, since u has at least one parent it does not execute R r NewDFS and thus does not update c v , and it can neither update c u to W or L, and thus u / ∈ ReplayCand γ ′ (v). As a result, C(v) \ ReplayCand γ (v) ⊆ C(v) \ ReplayCand γ ′ (v).

Lemma 15

Let cs = γ → γ ′ be a computing step and let v ∈ V be a node. If tok γ v / ∈ {⊥, ↑} then EqColCand γ ′ (v) ⊆ EqColCand γ (v).

Proof : We prove the equivalent statement:

Since tok γ v / ∈ {⊥, ↑}, then according to Lemma 11, v does not update c v during cs. Let us consider one child u of v such that u / ∈ EqColCand γ (v). If u / ∈ ReplayCand γ (v) then according to Lemma 14, u / ∈ ReplayCand γ ′ (v) and thus u / ∈ EqColCand γ ′ (v).

Let us suppose now that u ∈ ReplayCand γ (v) \ EqColCand γ (v), i.e. c γ u ̸ = c γ v ∧ play γ u ∈ {W, F}. Since u has at least one parent, it does not execute R r NewDFS during cs, and since play γ u ̸ = P, u does not execute R Win nor R FakeWin during cs. Thus, we have c γ ′ u ̸ = c γ ′ v and thus u / ∈ EqColCand(v, γ ′ ). As a result, C(v) \ EqColCand γ (v) ⊆ C(v) \ EqColCand γ ′ (v). Lemma 16 establishes that if one node executes R Win , R FakeWin , or R ReplayUp , then the weight of all its parents in any CD o decrease. Basically, we formally prove that any such activation corresponds to one of the transition represented in Figure 24, and thus that it makes one of the three sets decrease.

Lemma 16

Let cs = γ → γ ′ be a computing step, and let v ∈ V be a node. If v executes R Win , R FakeWin , or R ReplayUp during cs, then ∀p ∈ P(v) such that tok γ p / ∈ {⊥, ↑}, we have W Ch (p, γ ′ ) < W Ch (p, γ).

Proof : Let us consider p ∈ P(v) such that tok γ p / ∈ {⊥, ↑}. Lemma 11 guarantees that c γ ′ p = c γ p . Suppose first that v executes R Win or R FakeWin during cs, which induces play γ v = P and play γ ′ v ∈ {W, F}. If c γ v = c γ p then v ∈ EqColCand γ (p). But since play γ ′ v ∈ {W, F}, v / ∈ EqColCand γ ′ (p), which according to Lemma 15 means that EqColCand γ ′ (p) ⊊ EqColCand γ (p). According to Lemmas 13 and 14, we obtain W Ch (p, γ ′ ) < W Ch (p, γ).

Otherwise, c γ v ̸ = c γ p . Since play γ v = P, we have v ∈ AllCand γ (p), and since play γ v ∈ {W, F} and v switches its color during cs, we also have v / ∈ AllCand γ ′ (p). According to Lemma 13, AllCand γ ′ (p) ⊊ AllCand γ (p), and according to Lemmas 14 and 15, we obtain W Ch (p, γ ′ ) < W Ch (p, γ).

Let us now suppose that v executes R ReplayUp during cs. Since tok γ p / ∈ {⊥, ↑}, predicate ReplayW γ (v) implies that c γ p ̸ = c γ v . Since v execute R ReplayUp during cs, we have play γ v = W, and thus v ∈ ReplayCand γ (p), and we also know that v updates play v to P and that it does not update its variable c v which implies that c γ ′ v ̸ = c γ ′ p ∧play γ ′ v = P. Thus, v / ∈ ReplayCand γ ′ (p) so according to Lemma 14 means that ReplayCand γ ′ (p) ⊊ ReplayCand γ (p). According to Lemmas 13 and 15, we obtain W Ch (p, γ ′ ) < W Ch (p, γ).

which does not lead to any increase of W Er . This lemma is the main argument to establish that (W Ch , W Er ) is a pre-admissible weight function.

Lemma 19

Let v ∈ V be a node and let cs = γ → γ ′ be a computing step. If ¬Er γ (v) and Er γ ′ (v), then W Ch (v, γ ′ ) < W Ch (v, γ) or v executes R Win during cs or ∃u ∈ C(v) such that u executes E TrustChild during cs.

Proof : We prove the equivalent statement: if ¬Er γ (v) then ¬Er γ ′ (v) or W Ch (v, γ ′ ) < W Ch (v, γ) or, during cs, v executes R Win or ∃u ∈ C(v) such that u executes E TrustChild .

Since ¬Er γ (v), only few cases must be considered.

1. If tok γ v = ⊥ then either v executes R Win during cs, either it does not, but then tok γ ′ v = ⊥ and thus ¬Er γ ′ (v).

If tok γ

v =↑ then tok γ ′ v ∈ {↑, ⊥} and thus ¬Er γ ′ (v).

If tok γ

v =↓ then if v does not execute R Receive during cs, tok γ ′ v =↓ and thus ¬Er γ ′ (v). Otherwise, v executes R Receive during cs and then ∀u ∈ C(v), tok γ u ∈ {⊥, ↑}. Either one child u of v executes R Win , and then W Ch (v, γ ′ ) < W Ch (v, γ) according to Lemma 16, either no one does, but then ∀u ∈ C(v), tok γ ′ u ∈ {⊥, ↑}, and since tok γ ′ v = •, we have ¬Er γ ′ (v). 4. If tok γ v = ⋆ ∧ ∀u ∈ C(v), tok γ u = ⊥ then either one child u of v executes R Win , and then W Ch (v, γ ′ ) < W Ch (v, γ) according to Lemma 16, either no one does, but then ∀u ∈ C(v), tok γ ′ u = ⊥ which means that ¬Er γ ′ (v). 5. If tok γ v = • ∧ ∀u ∈ C(v), tok γ u = ⊥ then children u of v cannot execute R Win during cs: either u has one other parent p such that tok γ p =⇊, and then ¬OkNeg γ (u), either it has not, and thus it cannot execute R Win either. Thus, ∀u ∈ C(v), tok γ ′ u = ⊥, so ¬Er γ ′ (v). 6. If tok γ v =⇊ ∧∀u ∈ C(v), tok γ u ∈ {⊥, ⋆} then children u of v cannot execute R Nego since they have one parent v with tok γ v =⇊. If no children u of v executes E TrustChild during cs, then ∀u ∈ C(v), tok γ ′ u ∈ {⊥, ⋆}. Furthermore, tok γ ′ v ∈ {⇊, ⟲} since ¬Er γ (v). Thus, if no children u of v executes E TrustChild during cs, ¬Er γ ′ (v).

If tok

Win during cs: either u has one other parent p such that tok γ p =⇊, and then ¬OkNeg γ (u), either it has not, and thus it cannot execute R Win either. This implies that ∀u ∈ C(v), tok γ ′ u ∈ {⊥, ↑} and thus ¬Er γ ′ (v).

Theorem 5 establishes that (W Ch , W Er ) is pre-admissible.

Theorem 5

Let cs = γ → γ ′ be a computing step, and let a be an anchor at γ ′ , and suppose that a does not execute R r NewDFS during cs. We have

Proof : According to Theorem 3, we already have

Consequently, by definition of the lexicographic order, we only have to establish that if

v executes a full cycle of the cycle of Figure 26, which indeed forces us to attribute 7 to the weight of v. Hopefully, the design of our algorithm guarantees that this can only happen if the values of id v and/or id u are inconsistent. In other words, as soon as v executes one action, we guarantee that this situation cannot occur anymore, this will be proven in Lemma 23. Thus, we only have to deduce if u ∈ Players(v) will execute R Lose before any action of v, from the values of id v and id u . This strongly depends on the value of b γ v . If b γ v ̸ = ⊥ then v announces one value that defines the partial winners of that turn of the negotiation. It the configuration is inconsistent, it is very possible that no children u ∈ Players γ (v) has produced, neither will produce that answer. All of the nodes that have announced a different value than b γ v , or that will announce a different value than b γ v will execute R Lose , immediately for the first ones, and after one execution of R NewBit for the second ones

. Therefore, no children u ∈ Players γ (v) can execute R Lose before an action of v. We define the set Losers(v) that depends on the value of b v .

We are now tempted to say that W γ Circ (v) = 7 if and only if Losers γ (v) = Players γ (v). Yet, one subtlety must be treated before. Indeed, when all the children u of v have received the token, then u will not execute R Give but R OfferUp , and thus we do not have to reason based on the constraint of W ⇊ Circ . Moreover, in that situation, we must not attribute a weight of 7 to v since it would be an increase when v executes R ReNego , and updates tok v from • to •. This situation cannot happen as long as there remains players, because after the execution of StartNego(v), we have Losers(v) = ∅. The only case to consider is therefore when no node children of v is susceptible to receive the token, and in that situation we force W • Circ (v, γ) to be 2.

In order to make the proof easier to approach, we first define the set Candidates(v) that contains all the nodes that still have to negotiate and win the token before the circulation from v is over. This set reminds one of the different cases depicted in Figure 23.

We can now define the main predicate if that section, FullRound, which decides whether v has to execute one full cycle before any of its children receives the token.

We deduce function W • Circ that allows us to define W Circ .

Proofs Lemma 20 establishes that actions that make the negotiation progress are non simultaneous on the parent and on its children.

Lemma 20

Let γ be a configuration and let v ∈ V be a node such that Synch γ (v)

Proof : Since we are only interested in properties at γ, no confusion can be made, and thus we do not precise the configuration in which the predicates and sets are evaluated in that proof.

By definition of Synch(v), we have ph u = ph v . Consequently, we have:

Let us first suppose that PhComplete(v). Then by definition, b u = b v , and thus ¬LosePar(u, v). Furthermore, we also have

Let us now suppose that NextPlay(v). We deduce that b v = ⊥, and thus ¬LosePar(u, v). Furthermore, we have AnswerPar(u, v)

requires that b u ̸ = ⊥, which is contradictory. Thus, ¬AnswerPar(u, v).

Lemmas 21 and 22 prove that the definition of predicate Losers is adapted to the algorithm. We prove that all the nodes that execute R Lose were actually counted in the set Losers, and that execution of R NewBit does not bring any new node in the set Losers.

Lemma 21

Let cs = γ → γ ′ be a computing step, and let v ∈ V be a node such that

Thus, we have

Lemma 22

Let cs = γ → γ ′ be a computing step, and let v ∈ V be a node such that tok γ v = • and such that v is not activated during cs.

Let u ∈ Players γ (v) be a node that executes R NewBit during cs.

Proof : Since u executes R NewBit during cs, OkNeg γ (v) = true so v is the only parent of u such that tok p v γ = •. Thus, the execution of Announce produces

, and then we conclude that Bit

Lemma 23 proves that the definition of FullRound is adapted to our algorithm. Indeed, we establish that one node v such that tok v = • both before and after a computing step does not see its weight by W Circ increase, unless it makes decrease one higher component of W at the same time.

Lemma 23

Let cs = γ → γ ′ be a computing step, and let v ∈ V be a node such that

Let us now suppose that Losers γ (v) = Players γ (v), which implies Candidates γ (v) = ∅. Since Players γ (v) ⊆ Candidates γ (v), we have Players γ (v) = ∅, so v cannot execute R maxPos or R NewPh . Thus, v is not activated during cs (recall that by hypothesis,

, then either u executes R Win or R FakeWin , and then the theorem is established, either not, and then Lemma 24 establishes under which conditions we can have an increase of W Circ on one node v. It proves that if this happens, then we fall into the conditions of Theorem 4 or of Theorem 6. This lemma, which largely uses Lemma 23, is the main argument to establish that (W Ch , W Er , W Circ ) is pre-admissible.

Lemma 24

Let cs = γ → γ ′ be a computing step, let a be an anchor at γ ′ , and let v ∈ D γ a be a node.

NewDFS during cs, or tok γ v / ∈ {⊥, ↑, ↓} and one child u of v executes R Win , R FakeWin , R ReplayUp or E TrustChild during cs.

Proof : Let us consider different cases depending on the value of tok γ v :

Let us consider that last case. Remark first that if Candidates γ (v) = ∅ then ¬Give γ (v), and thus v cannot execute R Give during cs. As a consequence, we have Candidates γ (v) ̸ = ∅. Then, since ¬FullRound γ (v) we must have Losers γ (v) ̸ = Players γ (v), which is possible only if Players γ (v) ̸ = ∅ (recall that Losers γ (v) ⊆ Players γ (v)). Thus, we necessarily have Players γ (v) ̸ = ∅, and actually since v executes R Give during cs, there Players γ (v) = 1. Let u be that node in Players γ (v). If u executes R Win or R FakeWin , we have our result, let us now consider that it does not. Since Losers γ (v) ̸ = Players γ (v), u / ∈ Losers γ (v) and thus, according to Lemma 21, u does not execute R Lose during cs. As a consequence, u either executes R NewBit , either is not activated during cs. In both cases, variables tok, c, and play are not updated on u during cs, and thus u ∈ Players γ ′ (v), so

As a consequence, v does not execute R NewPlay during cs. If v executes E TrustChild during cs, then the desired property holds. Let us now suppose that v does not execute any rule during cs. Since tok γ v =⇊, u cannot execute R Lose or R NewBit during cs, since it requires that one other parent p of u is such that tok γ p = •, and then ¬OkNeg γ (u). Thus, either u executes R Win or R FakeWin during cs and then our property holds, either it does not, but then it is not activated and thus Definitions Let us first define the different sets that contain the children u of v that we are going to count in the different cases described above.

If tok γ v = •, then we want to count children u ∈ C neq γ (v) that might execute R Lose . One node u can execute R Lose only if play γ u = P, so nodes u ∈ C neq γ (v) : play γ u = P must obviously be counted. Yet, we cannot count only those children of v. Indeed, it might happen that one node u ∈ C neq γ (v) : play γ u = W execute R ReplayUp , which produces play γ ′ u = P, and would make W Play increase on v. Although it would at the same time make W Play decrease on one other node w such that play w =↑, since we require that W decrease on each branch of each CD o , we must prevent this from happening. Thus, we must include nodes u ∈ C neq γ (v) : play γ u = W in our count for tok v = •. For the same reason, due to rule R ReWin , we must also include nodes u ∈ C neq γ (v) : play γ u = F in that set. This leads to the following predicate:

•, then we want to count children u ∈ C neq γ (v) that might execute R ReplayD . One node u can execute R ReplayD only if play γ u = L. Furthermore, due to predicate OkNeg, no node u that has a parent v with tok γ v ∈ {⟲, •} can execute R Lose . This leads to the following predicate:

If tok γ v =↑ then we want to count children u ∈ C eq γ (v) that might execute R ReplayUp or R Fake . One node might execute R ReplayUp or R Fake only if play γ u = W. One node u might updates its variable play u from P to W only if it executes R Win or R FakeWin , cases that have been treated previously. Furthermore, due to predicate StopFaking, no node u that has a parent v ∈ P eq (u) such that tok v =↑ can execute R ReWin , and thus update its variable play u from F to W. This leads to the following predicate:

We can now define W Play (v, γ) depending on the value of tok γ v .

Proofs Lemmas 25, 26 and 27 prove that the definitions of ChLose, ChReplay, and ChEnd are consistent with our algorithm. For ChLose(v) and ChReplay(v) we prove in Lemmas 25 and 26 that both these sets do not increase unless it is by one node u ∈ C(v) that executes R Win or R FakeWin , which makes decrease one more important quantity. We cannot use the same reasoning for ChEnd(v). Indeed, since we consider one node v such that tok v =↑, W Ch (v) is not affected by any action taken by one child u ∈ C(v). Thus, we prove in Lemmas 27 that ChEnd(v) never increases, as long as tok v =↑. We also establish in these lemmas some particular cases which necessarily decrease W Play .

Lemma 25

Let cs = γ → γ ′ be a computing step and let v be a node such that

Proof : For the first part, we prove the equivalent statement, under the same conditions:

, and thus play γ u = L. Since v ∈ P neq γ (v) and tok v = •, ¬ReplayL γ (u) so u does not execute R ReplayD so play γ ′ u = L and thus u / ∈ ChLose γ ′ (v). Let us now prove the second part. By definition of R Lose we have

Lemma 26

Let cs = γ → γ ′ be a computing step and let v be a node such that tok γ v ∈ {⟲, •} and

Proof : For the first part, we prove the equivalent statement, under the same conditions:

Lemma 27

Let cs = γ → γ ′ be a computing step and let v be a node such that tok γ v =↑ and

Proof : For the first part, we prove the equivalent statement:

Lemma 28 combines the results of Lemmas 25, 26 and 27 and proves that W Play can decrease on one node only if the previous components of W decrease on the CD o 's that include that node.

Lemma 28

Let cs = γ → γ ′ be a computing step, let a be an anchor at γ ′ that does not execute R r NewDFS during cs, and let v ∈ D γ a be a node.

Proof : Let us first eliminate the cases in which the decrease of (W Ch , W Er , W Circ ) is immediate. According to Theorem 4 we can assume that, if tok γ v ̸ =↑, then ∀u ∈ C(v), u does not execute R Win or R FakeWin . Furthermore, according to Theorems 6 and 8, we can assume that v does not execute any rule among

is relevant. Thus, we first formally define what actual value will be taken as the answer by the parent v of u for the current step of the negotiation, which depends for each node u on whether it will produce a new answer to its parent, or not.

Let us now detail the situations in which the current value of ph v differentiates two children u ∈ Players γ (v). The first, most natural, situation is when two different nodes will produce different values for b in response to ph γ v . If this happens, then after v executes R maxPos (or before, if we already have b γ v ̸ = ⊥, at least one of them will be in a situation where it must execute R Lose .

The previous captures almost all the situations where one node is close to execute R Lose . There exists one other, unusual, situation, which is not described here, which is when all the nodes u ∈ Players γ (v) will produce the same value for ph v , but due to an incorrect initialization of variables, v has already picked a value, which is different from the common value proposed by its children. In this situation, all the children will actually execute R Lose at very short term.

We can now define the first of our three cases, which corresponds to the situation where one node u ∈ Players γ will execute R Lose before any update of ph v .

Let us now discuss the two other situations, in which the current value ph γ v does not differentiate any two children of Players γ (v). We need to determine whether v will reset ph v to 1 before we reach a value which differentiates two of its children of Players γ (v), or whether not. We could think, at first, that it is sufficient to determine whether there exists one value greater than ph γ v which differentiates two nodes of Players γ (v) or not. If there is not such greater value, ph v will indeed be reset to 1 before we terminate the negotiation phase. Yet, it might happen that, although there exists such a greater value, we are nevertheless forced to reset ph v to 1 before we reach this greater value. Indeed, it could happen that, due to an incorrect initialization of variables b u , all the children u ∈ Players γ (v) produce ⊥ as an answer for ph γ v while there exists a greater value which would differentiate two of them. If this happens, then the execution of PhasePlus(v) will reset ph v = 1. Hopefully, this is can happen only due to incorrect initialization of variables, and thus can only happen for the initial value of ph v . Remark that if only few of the nodes produce ⊥ as an answer for ph γ v then we have Finished γ (v). Let us define the predicate ForcedReset(v) which corresponds to configurations where an execution of R NewPh by v will set ph v to 1.

If ForcedReset γ (v), then we are sure that v will first reset ph v = 1. But if not, we must determine whether there exists one value greater than ph γ v which differentiates two nodes of Players γ (v) or not. Let us first define Separators γ (v) the set of all the values for ph v which can differentiate two children u ∈ Players γ (v). Remark that this set is defined statically: it does not depend at all on the values of ph v , b v , ph u , b u , and only relies on the values of the different identifiers of children of v in Players γ (v). Yet, we consider this set only if ¬Finished γ (v), that We now formally define the weight of one node v. The goal is to count the number of actions each node, among v and its children in Players γ (v), can take before the execution of R Lose is necessary.

Node v will execute two actions for each increase of ph v , since it must execute both R NewPh , and R maxPos for each step. A node u ∈ Players γ (v) executes R Lose when b v ̸ = ⊥, which means immediately after one execution of R maxPos , and not of R NewPh . Thus, v executes a sequence of R NewPh ; R maxPos in this order, which might be preceded by one execution of R maxPos if necessary.

One children u ∈ Players γ (v) only executes R NewBit , by hypothesis. Every time it executes R NewBit , u sets ph u at the current value of ph v , which will be updated exactly SepDist γ (v) times. Thus, u executes R NewBit once for each updated value of ph v , and execute one more action if, in the initial configuration, u has to produce an answer for ph v .

We finally define W Nego .

Preliminaries Our overall goal is to prove that W Nego behaves as expected, which is proving that associated with the four previous components, it is pre-admissible, and that in some specific cases, it is a decreasing function. Before we formally establish this, we need to establish some basic, yet numerous, properties which describe how the different predicates and sets we defined above behave during an execution. Indeed, since the definition of W Nego strongly depends on Finished, WontReset, and WillReset, among other things. In this preliminary, we focus on establishing properties of stability for those three predicates, depending on the activation of node v. To achieve this, we first prove some stability properties on other, more basic, predicates, namely AnswerPar, Answer, ForcedReset. Some of those preliminary lemmas will be reused as well in the demonstrations of the next section.

Our goal is to prove that (W Ch , W Er , W Circ , W Play , W Nego ) is pre-admissible. Thus, according to Theorem 9, most of the proof will be done under the hypothesis that (W Ch , W Er , W Circ , W Play ) is constant. Actually, this is hypothesis is explicitly used only in the proof of Lemma 29, which states that Players(v) and Separators(v) are constant. In all the other lemmas, this hypothesis on (W Ch , W Er , W Circ , W Play ) is actually used through Lemma 29: we suppose Players(v) and Separators(v) are constant.

Lemma 29

Let cs = γ → γ ′ be a computing step and let v be a node such that

If u executes R Lose then according to Lemma 25, we have W Play (v, γ ′ ) < W Play (v, γ) which cannot happen by hypothesis. If u executes R Win or R FakeWin then according to Lemma 16, we have W Ch (v, γ ′ ) < W Ch (v, γ) which cannot happen by hypothesis. Thus, u can only execute R NewBit , and whatever happens, u ∈ Players γ ′ (v).

Let us now consider one node

Due to its parent v, u cannot execute R ReplayD , and if it executes R ReplayD , then according to Lemma 16, we have W Ch (v, γ ′ ) < W Ch (v, γ) which cannot happen by hypothesis. As a consequence, in any case, u / ∈ Players γ ′ (v).

We just established that u ∈ Players γ ′ (v) ⇐⇒ u ∈ Players γ (v), which means that Players γ ′ (v) = Players γ (v). Since Separators γ (v) only depends on Players γ (v), we can conclude that Separators γ ′ (v) = Separators γ (v) as well.

From now on, since all the following lemmas of this section are under, at least, the hypothesis of Lemma 29, we allow ourselves to simply write Players(v) and Separators(v) without referring to the configuration in which the set is evaluated.

Lemma 30 proves that, unless node v asks for one new information, which concerns one new value for ph, then the value which will be taken as an answer for the negotiation does not evolve. It partly justifies the definition of Answer.

Lemma 30

Let cs = γ → γ ′ be a computing step and let v be a node such that

Proof : Let us consider u ∈ Players(v). If u is activated, then according to Theorems 4 and 10, u executes R NewBit . Therefore, OkNeg γ (u) so v is the only parent of u with tok v / ∈ {⊥, ↑, ↓}, and, on the other hand, AnswerPar γ (u, v). Therefore, by definition of the action Announce(u),

Suppose now that u is not activated during cs. If v is not activated either, then we obviously have Answer γ ′ (u, v) = Answer γ (u, v). Let us rather suppose that v executes R maxPos during cs.

According to Lemma 20, we have ¬AnswerPar γ (u, v), so Answer γ (u, v) = b γ u , and since u is not activated during cs we even have b γ ′ u = b γ u . By definition, we have Synch γ (v) so ph γ u = ph γ v , which implies, according to NextPlay(v), that

Lemma 32 proves that once the predicate Finished evaluates to true, then it does in all the following configurations too. In order to prove it, we first establish Lemma 31 which proves that when we have Finished γ (v), node v cannot execute R NewPh , which justifies the name of this predicate. Lemma 32 is the first fundamental lemma which will be helpful in the next section.

Lemma 31

Let cs = γ → γ ′ be a computing step and let v be a node such that tok

Proof : Suppose that Finished γ (v) ∧ Synch γ (v) and prove that ¬PhComplete γ (v). Whether we have TwoDiffer γ (v) or OneDiffers γ (v), there exists u ∈ Players(v) : Answer γ (u, v) ̸ = b γ v . If AnswerPar γ (u, v) then according to Lemma 20, ¬PhComplete γ (v). Otherwise, ¬AnswerPar γ (u, v) and then b γ u ̸ = b γ v and once again, ¬PhComplete γ (v).

Lemma 32

Let cs = γ → γ ′ be a computing step and let v be a node such that tok

, and thus Finished γ (v) ⇒ Finished γ ′ (v).

Proof : If TwoDiffer γ (v) then Finished γ (v) so according to Lemma 31, v does not execute R NewPh during cs, and thus according to Lemma 30, ∀u ∈ Players(v), Answer γ ′ (u, v) = Answer γ (u, v). Thus, let us consider u 1 , u 2 ∈ Players(v) such that Answer γ (u 1 , v) ̸ = Answer γ (u 2 , v). Immediately, we have Answer γ (u 1 , v) ̸ = Answer γ (u 2 , v) and thus TwoDiffer γ ′ (v).

Similarly, if OneDiffers γ (v), then Finished γ (v) so according to Lemma 31, u does not execute R NewPh during cs, and thus ∀u ∈ Players(v), Answer γ ′ (u, v) = Answer γ (u, v). By definition of OneDiffers γ (v), we have b γ v ̸ = ⊥, so v does not execute R maxPos during cs, which implies that v is not activated during cs.

The two following lemmas prove that, when v does not execute R NewPh , then the predicates ForcedReset and Finished remain constant.

Lemma 33 proves that, as long as v does not update ph v , then whether the next execution of R NewPh will reset ph v = 1 or not, ForcedReset(v) keeps the same boolean value. It, partly, justifies the definition of ForcedReset.

Lemma 33

Let cs = γ → γ ′ be a computing step and let v be a node such that

If v does not execute R NewPh during cs then ForcedReset γ ′ (v) ⇐⇒ ForcedReset γ (v).

Proof : Since ForcedReset only depends on Answer, this is a direct consequence of Lemma 30

Lemma 34 establishes that, as long as v does not update ph v , then whether we have reached the final value for ph v or not, Finished(v) keeps the same boolean value. In a certain sense, it specifies Lemma 32.

Lemma 34

Let cs = γ → γ ′ be a computing step and let v be a node such that tok

Lemma 35

Let cs = γ → γ ′ be a computing step and let v be a node such that

Proof : According to Lemma 20, ∀u ∈ Players(v), ¬AnswerPar γ (u, v). Consequently, ∀u ∈ Players(v), Answer γ (u, v) = b γ u . Thus, ForcedReset γ (v) ≡ ∀u ∈ Players(v), b γ u = ⊥, which is exactly the condition which decides whether ph v is set to 1 by PhasePlus(v).

Lemma 36 states that if node v verifies WontReset, then it will not reset ph v = 1, as we expect.

Lemma 36

Let cs = γ → γ ′ be a computing step and let v be a node such that

If WontReset γ (v) then v does not reset ph v = 1 during cs.

Proof : If v does not execute R NewPh during cs, then this result is immediate. If v executes R NewPh during cs, then since WontReset γ (v), we have ¬ForcedReset γ (v), and thus according to Lemma 35, v does not reset ph v = 1 during cs.

Lemma 37 states that if v executes R NewPh , i.e. if it asks for one new information to its children, then all of them will have to produce a new answer, so after this we can trust the values of Bit u in the negotiation process. Associated to Lemma 30 it fully justifies the definition of Answer.

Lemma 37

Let cs = γ → γ ′ be a computing step and let v be a node such that

If v executes R NewPh during cs then ∀u ∈ Players(v), AnswerPar γ ′ (u, v).

Proof : Let us consider one node u ∈ Players(v). According to Lemma 20, u is not activated during cs. Furthermore, since v executes R NewPh , we deduce

Lemma 38 states that if one node v executes R NewPh , then we have reached the value on which the negotiation is finished if and only if this value belongs to the set Separators(v). Associated with Lemmas 31 and 34 it fully specifies the situations where a computing step leads to a configuration which satisfies Finished.

Lemma 38

Let cs = γ → γ ′ be a computing step and let v be a node such that tok γ v = • and tok γ ′ v = •, and suppose that

, we obtain:

The two following lemmas, the last of this section, and establish how situations where ¬Finished(v) can evolve.

Lemma 39 states that if we are in a configuration such that we will reach the terminal value for ph v without resetting ph v = 1, then it remains true. Associated with Lemmas 34 and 38, it fully describes what configuration is reached after a computing step which starts with WontReset(v).

Lemma 39

Let cs = γ → γ ′ be a computing step and let v be a node such that tok γ v = • and tok γ ′ v = •, and suppose that

Proof : Recall that WontReset γ (v) implies ∃i > ph γ v : i ∈ Separators(v) and ¬ForcedReset γ (v). Suppose first that v does not execute R NewPh during cs. According to Lemma 33, we have

Now suppose that v executes R NewPh during cs. According to Lemma 36,

then according to Lemma 38 Finished γ ′ (v) and thus we obtain the desired result.

Let us now suppose that

We now finish the proof by establishing ¬ForcedReset γ ′ (v).

Since ∃i > ph γ ′ v : i ∈ Separators(v), we deduce ∃u 1 , u 2 ∈ Players(v) : Bit u1 (i) ̸ = Bit u2 (i). At least one of them, let us say u, is such that Bit u (i) ̸ = ⊥. By definition of Bit u , since ph γ ′ v < i, Bit u (ph γ ′ v ) ̸ = ⊥, and by Lemma 37, we deduce Answer γ ′ (u, v) ̸ = ⊥. Thus, ¬ForcedReset γ ′ (v), and finally

Lemma 40 states that if we are in a configuration such that we need to reset ph v = 1 before reaching the terminal value for ph v , then this remains true after a computing step, unless we do reset ph v = 1 during this computing step. Associated with Lemmas 35 and 38, it fully describes what configuration is reached after a computing step which starts with WillReset(v).

Lemma 40

Let cs = γ → γ ′ be a computing step and let v be a node such that tok γ v = • and tok γ ′ v = •, and suppose that

If WillReset γ (v), we have:

If v does not execute R NewPh during cs then according to Lemma 34, ¬Finished γ ′ (v), and according to Lemma 33,

Suppose now that v executes R NewPh during cs. According to Lemma 37 ∀u ∈ Players(v), AnswerPar

Remark that ¬ForcedReset γ (v). Indeed, according to Lemma 20 we have ∀u ∈ Players(v), ¬AnswerPar γ (u, v), and thus if ForcedReset γ (v) then ∀u ∈ Players(v), b γ u = ⊥ and thus the execution of

, so according to Lemma 38, ¬Finished γ ′ (v). Furthermore, we have ∀i > ph γ ′ v , i / ∈ Separators(v), and thus WillReset γ ′ (v).

Let us now prove that if

Let us now prove that ¬ForcedReset γ ′ (v) to finish the proof. Since v executes R NewPh during cs, ForcedReset γ ′ (v) ⇐⇒ ∀u ∈ Players(v), Bit u (1) = ⊥, which cannot be by hypothesis on the identifiers. Thus, ∃i

Proofs In this section, we finally address the function W Nego , the lemmas established in the previous section are going to be extremely useful.

One first step is to establish that what we defined as the last value for ph v during the negotiation phase, SepVal(v), is consistent through an execution. We prove in Lemma 42 that this value remains constant. Let us first prove Lemma 41 which states that unless we reset ph v = 1, then the maximum value for ph v which we will reach before the reset remains constant as well.

Lemma 41

Let cs = γ → γ ′ be a computing step and let v be a node such that tok

Proof : If v does not execute R NewPh during cs then ph γ ′ v = ph γ v , and according to Lemma 33 ForcedReset γ ′ (v) ⇐⇒ ForcedReset γ (v), and thus MaxPh γ ′ (v) = MaxPh γ (v).

Suppose now that v executes R NewPh during cs. By hypothesis, ph v is not reset to 1 during cs, so ph γ ′ v = ph γ v + 1, and according to Lemma 35 we also have ¬ForcedReset γ (v). Thus, we deduce MaxPh γ (v) = min{i ≥ ph γ v | ∀u ∈ Players(v), Bit u (i) = ⊥}. On the other hand, since v executes R NewPh during cs, we know by Lemma 37 that ∀u ∈ Players(v), AnswerPar γ ′ (u, v),

Lemma 42

Let cs = γ → γ ′ be a computing step and let v be a node such that tok γ v = • and tok γ ′ v = •, and suppose that

Then SepVal γ ′ (v) = SepVal γ (v).

Proof : Let us distinguish three cases:

• If Finished γ (v), then according to Lemma 31, v does not execute R NewPh during cs, and thus ph γ ′ v = ph γ v . Furthermore, according to Corollary 32, Finished γ ′ (v). Thus, we have

, two cases must be considered.

If v does not execute R NewPh during cs, then ph γ ′ v = ph γ v , and according to Lemma 34, ¬Finished γ ′ (v), and according to Lemma 30, ∀u ∈ Players(v), Answer γ ′ (u, v) = Answer γ (u, v). Thus, we have WontReset γ ′ (v), and thus

∈ Separators(v) then according to Lemmas 39 and 38 WontReset γ ′ (v). Furthermore, since

If v executes R NewPh and sets ph γ ′ v = 1, then according to Lemma 40, Finished γ ′ (v) ∨ WontReset γ ′ (v), and according to Lemma 38,

Let us now suppose that v does not execute R NewPh , or that, if it does, then it does not set ph v = 1. According to Lemma 40, WillReset γ ′ (v), and we deduce SepVal

From now on, for all the lemmas of this section which are stated under, at least, the hypotheses of Lemma 42, which by the way are the same as the hypothesis of Lemma 29, we allow ourselves to simply write SepVal(v) without referring to the configuration in which this function is evaluated. This being established, we are going to follow the different components of W Nego introduced for its definition: SepDist, ParSteps, ChSteps, and finished W Nego itself. For each of those four functions, we prove that it corresponds to a non-increasing function, and for each of them we present the cases where we can guarantee its decrease.

Lemma 43

Let cs = γ → γ ′ be a computing step and let v be a node such that tok γ v = • and tok γ ′ v = •, and suppose that

Then SepDist γ ′ (v) ≤ SepDist γ (v).

Proof : Let us consider three cases.

• If Finished γ (v) then according to Corollary 32, Finished γ ′ (v) and thus

Otherwise, if v executes R NewPh during cs, and sets ph γ ′ v = ph γ v + 1, then according to Lemma 40 ¬WillReset γ ′ (v), and thus we deduce

Lemma 44

Let cs = γ → γ ′ be a computing step and let v be a node such that tok γ v = • and tok γ ′ v = •, and suppose that

If v executes R NewPh during cs we have SepDist γ ′ (v) < SepDist γ (v).

Proof : Let us consider three cases.

• If Finished γ (v) then according to Lemma 31, v does not execute R NewPh during cs.

, and so SepDist γ (v) > 0. Let us now suppose that ¬Finished γ ′ (v). According to Lemma 39 WontReset γ ′ (v). Furthermore, according to Lemma 36,

, and according to Lemma 41

. By definition of MaxPh γ (v), we have MaxPh γ (v) ≥ ph v , so SepDist γ (v) ≥ SepVal(v). On the other hand, whether Finished γ ′ (v) or WontReset γ ′ (v), we have SepDist γ (v) < SepVal(v). As a consequence, we obtain SepDist γ ′ (v) < SepDist γ (v).

Lemma 45

Let cs = γ → γ ′ be a computing step and let v be a node such that tok

Then ParSteps γ ′ (v) ≤ ParSteps γ (v), and if v executes R maxPos or R NewPh during cs, then ParSteps γ ′ (v) < ParSteps γ (v).

Proof : Remark first that if v is not activated during cs, then according to Lemma 43

Finally, if v executes R maxPos during cs, then according to Lemma 43

Lemma 46

Let cs = γ → γ ′ be a computing step and let v be a node such that

Let us consider u ∈ Players(v). Then ChSteps γ ′ (v) ≤ ChSteps γ (v), and if u executes R NewBit during cs, then ChSteps γ ′ (v) < ChSteps γ (v).

Proof : Suppose first that u does not execute R NewBit .

If v is not activated, then ChSteps γ ′ (v) = ChSteps γ (v). If v executes R NewPh during cs then according to Lemma 44, SepDist γ ′ (v) < SepDist γ (v), and thus ChSteps γ ′ (u, v) ≤ ChSteps γ (u, v).

If v executes R maxPos during cs then no children of v is activated during cs according to Lemma 20, and thus, Synch γ (v). Consequently,

Now suppose that u executes R NewBit during cs. According to Lemma 20, v is not activated during cs. Furthermore, we have, by definition, AnswerPar γ (u, v). The execution of Announce(u) sets

Lemma 47

Let cs = γ → γ ′ be a computing step and let v be a node such that tok

Proof : This is a direct consequence of Lemmas 45 and 46.

We now formally prove that our algorithm satisfies Condition 2 of Specification 1.

Theorem 17

Let ϵ = γ 0 → γ 1 → • • • be a maximal execution, and let r be the root of G. ϵ is infinite, and can be divided into an infinite number of circulation rounds.

Proof : According to Theorem 1, we only have to prove that there exists an infinite number of computing steps cs i = γ i → γ i+1 such that r executes R r NewDFS during cs i . According to Theorem 16, there exists t 0 ≥ 0 such that ∀a ∈ A(γ t ) \ {r}, ∀t ′ ≥ t 0 , a ∈ A(γ t ′ ) and D

Let us reason by contradiction and suppose that there only exists a finite number of computing steps cs i = γ i → γ i+1 such that r executes R r NewDFS during cs i . Then, there exists t 1 ≥ 0 such that ∀t ≥ t 1 , r does not execute R r NewDFS during cs t . Thus, according to Theorem 15, there exists t 2 ≥ t 1 such that ∀t ≥ t 2 , D γt r is not activated during cs t . Let us consider t 3 = max(t 0 , t 2 ), and the infinite execution ϵ 3 = γ t3 → γ t3+1 → • • • . By definition, no CD o is activated during ϵ 3 . Thus, during ϵ 3 , nodes only execute R ReWin . But once a node v executes R ReWin , it cannot execute it again before the execution of one other rule sets play v = F. Thus, there does not exist such execution, so we reached a contradiction.

Consequently, there exists an infinite number of computing steps cs i = γ i → γ i+1 such that r executes R r NewDFS during cs i .

C.3 Convergence

In this section, we establish that our algorithm behaves correctly, by largely using results established in Section C.2, and especially in Section C.2.9. We use in particular Theorems 16 and 17, that allow us to start the reasoning at a moment where the algorithm has already partly converged. Namely, we consider executions in which the set of all the anchors remain constant, and such that all the CD o 's which are not anchored at the root of the D o are not activated. Once this is considered, the proof is organized according to the following scheme. We first establish some additional stability properties on the CD o anchored at the root of the D o . Then, we give a formal definition of the notion of having the token, for one node. The formal notion we use to describe the part of an execution where one node is involved in the token circulation is circulation round, introduced in Theorem 1 and Definition 28. After that, we prove that if one node executes a circulation round, then all of its children which might take the token (depending on their variables play and c) actually do it too, and execute a circulation round as well. We can thus reason by induction an prove that, starting at the root, the token browses a part of the D o . Finally we prove that the alternation of the color of the root, which occurs each time it executes R r NewDFS , associated to properties of the algorithm, especially its effect on the variables play of the children of a node, guarantee that the part of the D o which is being browsed by the token grows each time the root executes R r NewDFS , and eventually become the entire D o .

As we said before, we consider executions which start after the value of t 0 guaranteed by Theorem 16. In particular, the set of anchors does not evolve during the executions we consider, and according to Lemma 48, no CD o other than the one anchored at r will be updated. Consequently, to enhance readability, we allow ourselves to simply write A (resp. A * ) without referring to the configuration in which this set is evaluated, and to simply write D a when a ∈ A * without referring to the configuration in which we consider the CD o anchored at a.

Lemma 50

Let ϵ be a maximal execution. We have ∀t ≥ 0, ∀a ∈ A * , D γt r ∩ D a = ∅.

Proof : Let us reason by contradiction and suppose that ∃v ∈ D γt r ∩ D a . Remark first that since v ∈ D a and a ̸ = r, we have v ̸ = r.

According to Theorem 17, there exists t ′ ≥ t such that r executes R r NewDFS during γ t ′ → γ t ′ +1 . By definition, at γ t ′ , only r is a branch of D γ t ′ r , and in particular, B is not. Let us consider t 0 the smallest value greater than t such that B is a branch of D γt 0 r and B is not a branch of D γt 0 +1 r . According to Lemma 10, we deduce that v executes R Return during γ t0 → γ t0+1 .

By definition, we deduce that v activates D a during γ t0 → γ t0+1 , which is contradictory.

Lemma 51

Let D γ a be a clean branch-CD o , and let us label its vertices

Proof : This is a direct consequence of the definition of predicate Er, since nodes are not in error and form a branch in G.

Lemma 52

Let ϵ = γ 0 → γ 1 → • • • be an execution such that r execute R r NewDFS during γ 0 → γ 1 . Then ∀t, D γt r is a clean branch-CD o .

Proof : We reason by induction. The base case is true since r executes R r NewDFS in γ 0 → γ 1 , thus tok γ0 r =↑ and thus D γ0 r = {r}, which is a clean branch-CD o . Let us also prove that D γ1 r is a clean branch-CD o . We have tok γ1 r = ⋆. Let us prove by contradiction that D γ1 r = {r}, and suppose r has one child u with tok γ1 u ̸ = ⊥. Since u / ∈ D γ0 r , u is not activated during γ 0 → γ 1 , and thus tok γ0 u ̸ = ⊥. According to Lemma 8, ∃a ∈ A * : u ∈ D a . As a consequence, u ∈ D a ∩ D γ1 r which cannot be according to Lemma 50, and therefore D γ1 r is a clean branch-CD o . Let us now suppose that the property holds at γ t , and prove it at γ t+1 . Remark first that if no node u joins D r by executing R Win , then the guards of the rules that update tok guarantee that no error can be generated.

, tok vi =↓, and are not enabled, neither is v k . Furthermore, Players γ (v k-1 ) = ∅ and no node reaches Players γ (v k-1 ) for the same reason as previously. Therefore, From now on, we suppose that the executions start after at least one R r NewDFS and thus we suppose that no node executes R FakeWin during the executions.

We presented in Definition 14 and in Theorem 1 the notion of circulation rounds for the root. Hence, for the sake of the proof, we also introduce the notion of circulation round on nodes that are not the root. This will allow us to consider circulation round on any node v ∈ V , root or not. Namely, this corresponds to the part of a circulation round in which one particular node holds the token, or in which the token is in one of its descendants.

Definition 28 (Circulation Round for v ̸ = r)

Let ϵ = γ 0 → • • • → γ k be a finite execution. We say that v ̸ = r executes a circulation round during ϵ if v executes R Win and R Return , exactly once during ϵ, in that order.

We call circulation round of v during ϵ, and denote ϵ rt (v, ϵ) the subexecution of ϵ : γ i+1 → • • • → γ j where γ i → γ i+1 (resp. γ j → γ j+1 ) is the computing step of ϵ where r executes R Win (resp. R Return ).

Lemma 53

Let

Proof : Let us prove the three items separately. If v ̸ = r then v updates c v only with the action of R FakeWin , which is not executed according to Corollary 2, or with the action of R Win , which is not executed by v during ϵ by definition.

2. Since v executes a circulation round, it is activated and thus belongs to D r . According to Lemma 52, ¬Er γ0 (v). Furthermore, by definition of circulation round, we have tok γ0 v ∈ {•, ⋆}. Thus, ∀u ∈ C(v), tok γ0 u = ⊥. 3. By definition of a circulation round, v executes R r NewDFS or R Return during γ k → γ k+1 and thus tok γ k v =↑ and MayDropUp γ k (v).

In the following lemma, we establish that if one node v executes a circulation round, then its playing children also execute a circulation round. This will allow us in the latter to reason by induction.

Lemma 54

Let us consider one node v ∈ V , and let

Then ∀u ∈ Candidates γ 0 (v), u executes a circulation round during ϵ.

Lemma 53 also assures that tok γ0 u = ⊥ which implies that, during ϵ, u cannot execute R Return before it executes R Win . Let us first prove that u executes R Win during ϵ.

Whether v = r or v ̸ = r has no incidence on the fact that, necessarily, v executes R OfferUp during ϵ. Otherwise, we would have tok Consequently, u executes one circulation round during ϵ.

We now introduce the notion of Free DODAG. This notion is defined only on reset points, i.e. configuration immediately subsequent to an execution of R r NewDFS (see Definition 14). A Free DODAG corresponds to all the nodes which can reach the root by a path in G, such that no node of this path has any parent in one other CD o . It corresponds to nodes which have the possibility to receive the token sent from the root by executing R Win (we do not take into account the color of the nodes on this path in this definition).

Definition 29 (Free DODAG)

Let γ be a reset point of an execution ϵ. We call free DODAG in γ, and denote FD o (γ), the smallest set that contains r and such that ∀w ̸ = r:

Let γ 1 and γ 2 be two reset points of an execution. We have FD o (γ 1 ) = FD o (γ 2 ).

Proof : The set of nodes v such that tok γ 1 v ̸ = ⊥ is the union of D γ 1 r = {r} and of all CD o 's D γ 1 a , a ∈ A(γ 1 ). By hypothesis, the CD o 's anchored to a node of A are not activated during the execution, and thus the set of nodes v such that tok v ̸ = ⊥ is the same in γ 1 as in γ 2 . As a consequence, FD o (γ 1 ) = FD o (γ 2 ).

FD o corresponds to all the nodes that may receive the token from the root, without considering variables c and play. In order to gain in precision, we define the set of all nodes which will actually receive the token during the starting circulation round.

Definition 30 (Reachable area from r)

Let γ be a reset point. We define the reachable area from r at γ, and denote Reach r (γ):

}

We prove in the following Lemma that nodes in the Reachable area actually receive the token, and execute exactly one circulation round during the circulation round of the root.

Lemma 56

Let ϵ = γ 0 → γ 1 → • • • → γ k be a circulation round of r. Then ∀u ∈ Reach r (γ), u executes exactly one circulation round during ϵ.

Proof : Let us prove that lemma by induction on the depth of node u in Reach r (γ). The base case comes immediately, since r is the only node with depth 0 and by definition, r executes a circulation round during ϵ.

Let us now establish the induction step and suppose that for any node u with depth less that d of Reach r (γ), u executes a circulation round during ϵ. Let us consider one node v ∈ Reach r (γ) with depth d + 1, and one of its ancestors u ∈ Reach r (γ) with depth d. By hypothesis, u executes a circulation round during ϵ. Let us consider ϵ rt (u, ϵ) = γ i → • • • → γ j the circulation round of u during the circulation round of r. If v ∈ Candidates γi (u) then we can apply Lemma 54 and thus v executes a circulation round during ϵ rt (u, ϵ).

Thus v executes at least one circulation round during ϵ. Furthermore, v cannot execute several circulation round during ϵ, since v cannot activate any other CD o than D γ r , and after its first circulation round it has the same color as the root, and thus the same color as any node of the branch-CD o .

The token does not only circulate through the reachable area of r indefinitely, it also makes its reachable area increase at each circulation round. Indeed, suppose one node v has the token, and has one child u with the same color as v. Then u is already seen as visited, which means that it won't receive the token, as being out of the reachable area. Yet, when sending the token upwards to its parent, v forces u to reset play u to P, which means that in the next circulation round, when the color of the token has switched, u will be able to receive the token. Note that this only works if u ∈ FD o (γ), otherwise u has other parents, and therefore updates play u to F.

Also note that if one child u does not receive the token for its variable play is already set to W or F, but had the appropriate color to receive it, then u will have to wait two circulation rounds before it actually receives the token. To embrace this behavior, we define the expansion areas of r, which constitutes all nodes in FD o (γ) which have a parent in Reach r (γ) without being in Reach r (γ) themselves.

Definition 31 (Expansion areas of r)

Let γ be a reset point. We define the expansion area of order 1 and of order 2 of r at γ, and denote Exp 1 r (γ) and Exp 2 r (γ):

The following Lemma proves that the three sets defined above are jointly increasing, as intended. This will allow us to prove that at some point, the reachable area contains the entire FD o .

Lemma 57

Let γ 1 and γ 2 be two consecutive reset points of an execution, and let ϵ = γ 0 → • • • → γ k be the circulation round of r between γ 1 and γ 2 .

Proof :

1. Remark that r ∈ Reach r (γ 2 ) by definition. Let us consider one node u ∈ Reach r (γ 1 ), u ̸ = r, and prove that play γ 2 u ∈ {P, L} ∧ c γ 2 u ̸ = c γ 2 r . According to Lemma 56, u executes one circulation round during ϵ. After ϵ, u cannot execute R Win after, at least, tok r =⇊ which occurs after γ 2 . Thus, in γ 2 , u still has the color it took when reaching D r during ϵ Thus, c γ

By definition of Reach r , ∃v ∈ P(u) such that v ∈ Reach r (γ 1 ). According to Lemma 56, v executes a circulation round during ϵ, and thus v executes R OfferUp during ϵ. Let us consider cs i = γ i → γ i+1 the last computing step of ϵ such that one parent v of u executes R OfferUp . At γ i , u terminated its circulation round. Indeed, if at γ i , u has not begun its circulation round, then c γi u ̸ = c γi v and play γi u ∈ {P, L} which would prevent v to execute R OfferUp . Furthermore, since ¬Er γ (v), we have tok γi u = ⊥ so u terminated its circulation round at γ i . Consequently, we have c γi u = c γi r and since ¬WaitSib γi (v), we also have play γi u ̸ = F. Furthermore, according to Lemma 50, we know that u has no parent such that tok γi p / ∈ {⊥, ↑} apart from D γi r , which implies that u has only one parent such that tok γi p / ∈ {⊥, ↑}, which is v. Consequently, since v is the last parent of u that executes a circulation round, then from γ i+1 to the end of ϵ, all the parents of u are such that tok γ p ∈ {⊥, ↑}. Thus, during that part of the execution, we have constantly ¬FakeReplay(u), and thus for that entire part of the execution, play u ̸ = F. Let us now consider γ j the last configuration that is part of the circulation round of v. According to Lemma 53 we have MayDropUp γj (v), so play γj u ̸ = W and thus play γj u ∈ {P, L}. Since v does not execute R Win nor R FakeWin after its first circulation round of ϵ, we deduce play γ 2 u ∈ {P, L} Since this is true for all the nodes of Reach r (γ 1 ), we can conclude Reach r (γ 1 ) ⊆ Reach r (γ 2 )

2. Let us consider one node u ∈ Exp 1 r (γ 1 ). By definition of Exp 1 r , there exists p ∈ P(v) : p ∈ Reach r (γ 1 ). According to what we established above, p ∈ Reach r (γ 2 ), so we only have to prove that c γ 2 u ̸ = c γ 2 r ∧ play γ 2 u ∈ {P, L} to establish that u ∈ Reach r (γ 2 ). By definition, we have c γ0 u = c γ0 r . Since r does not update c r during ϵ, and since D r is a branch-CD o along ϵ, then until u executes R Win , it has the same color as all the nodes of D γ r during ϵ. Since, on the other hand, u cannot activate any other CD o , we deduce that u actually does not execute R Win during ϵ, neither during γ k → γ 2 for the same reason. Consequently, we have c γ 2 u ̸ = c γ 2 r . Now, the proof we made for the previous case totally applies: we can select the last computing step such that one parent p of u executes R OfferUp , at that moment we have c u = c p , thus we can infer from WaitSib(v) that play u ̸ = F and from the non-activation of other CD o 's that this remains true until at least γ 2 . FInally, we can reason about MayDropUp as well to establish that play γ 2 u ∈ {P, L} which terminates the proof. 3. Let us consider one node u ∈ Exp 2 r (γ 1 ). By definition of Exp 2 r , there exists p ∈ P(v) : p ∈ Reach r (γ 1 ). According to what we established above, p ∈ Reach r (γ 2 ), so we only have to prove that c γ 2 u = c γ 2 r to establish that u ∈ Reach r (γ 2 ). By definition, we have c γ0 u ̸ = c γ0 r ∧ play γ0 u ∈ {W, F}. Thus, u cannot execute R Win before it executes R ReplayUp . Since u does not activate any other CD o than D r , u executes R ReplayUp only if it has one parent p ∈ D r such that tok p =↑ and c p = c v . But this cannot happen in ϵ before u executes R Win , since according to Lemma 52, all the nodes of D r have the same color c γ0 r , which is the opposite that c u until it executes R Win . We just found a loop of dependencies. We prove that u cannot update c u before at least γ 2 , and thus u ∈ Exp 1 (γ 2 ).

The two following lemmas prove that the sets of reachable and expansion areas of r allow a permanent growth of Reach, which stops only when Reach includes all the nodes of FD o .

Lemma 58

Let γ be a reset point of an execution. This node has a parent in FD o (γ) ∩ Reach r (γ) (otherwise it would not be minimal in depth). Thus, u belongs to Exp 1 r (γ) ∪ Exp 2 r (γ).

Lemma 59

There exists a reset point γ f such that Reach r (γ f ) = FD o (γ f ).

). If we now suppose that ∀i, Reach r (γ i ) ̸ = FD o (γ i ), then we build an infinite sequence of growing sets of nodes, which cannot happen. By contradiction, we conclude.

Since we can now apply the properties of Reach, and especially Lemma 56 to FD o , we can conclude that at some point, FD o = G.

Theorem 18

FD o (γ f ) = G Proof : Let us reason by contradiction and suppose there exists one node u / ∈ FD o (γ f ). Let us consider one such node u with maximal height, i.e. such that ∀p ∈ P(u), p ∈ FD o (γ f ). By definition this implies that ∀p ∈ P(u), tok γ p = ⊥ ∨ p = r. Thus, u / ∈ FD o (γ f ) is possible only by tok γ f v ̸ = ⊥. Since γ f is a reset point, it means that ∃a ∈ A * : v ∈ D a , and thus v is not activated at all.

Let us now consider one parent p of v. According to Lemma 59, we have p ∈ Reach γ f r , and according to Lemma 56, p executes a circulation round after γ f . But thus, according to Lemma 53 when p starts its circulation round we have tok v = ⊥ which is contradictory.

Corollary 3

Reach r (γ f ) = G.

Theorem 19

Our algorithm is a fair self-stabilizing token circulation algorithm.

Proof : We already proved in Theorem 17 that our algorithm satisfies Condition 2 of Specification 1.

Let us consider one execution ϵ = γ 0 → • • • , and more precisely the subexecution

Remark that having FD o (γ f ) = G implies that all nodes v but the root are such that tok γ f v = ⊥. Therefore, A * (γ f ) = ∅, and by Lemma 9, this is true in all configurations of ϵ f . In particular, in any configuration of ϵ f , the set of nodes with tok v ̸ = ⊥ corresponds to the clean branch-CD o D γ r , and by construction, we have U T C (γ). This proves that our algorithm satisfies Condition 1 of Specification 1.

Furthermore, let us consider one circulation round of ϵ f which starts at γ 1 , and let us denote γ 2 the reset point consecutive to γ 1 . According to Lemma 56, all nodes of Reach r (γ 1 ) = G execute exactly one circulation round during that circulation round. Since ∀v ∈ G \ {r}, tok γ 1 v = tok γ 2 v = ⊥, this means that there is exactly one computing step in which v executes R Win , and thus there exists a finite, continuous, subexecution of this round in which R(v). Therefore, this circulation round is fair.

C.4 Space Optimality of our Algorithm

In this section, we prove that our algorithm is asymptotically optimal in terms of memory for the token circulation problem. Our algorithm has a space complexity S(A) ∼ log log n bits per node.

Thus, we are going to prove that there does not exist any deterministic algorithm solving T C in S using o(log log n) bits per node. We prove this lower bound under less challenging hypotheses than those under which our algorithm works. Namely, our algorithm is self-stabilizing, it works under the unfair distributed scheduler and in any DODAG. Our lower bound is established for general distributed algorithms (without any stabilization requirements), under simpler schedulers (the synchronous scheduler and the central strongly fair scheduler), and in a very simple class of D o : the bi-branch D o .

We basically use Theorem 3 established in [START_REF] Blin | Optimal space lower bound for deterministic self-stabilizing leader election algorithms[END_REF] which introduces the equivalence between executions of small-memory algorithms in identified networks, and in anonymous networks. Specification 1 of T C relies on two local predicates, T and R. We can consider the function (A, T, R), which has asymptotically the same space complexity as A, and to apply Theorem 3 to this new function.

Let us first define the topology used to prove our lower bound. A bi-branch D o is a D o in which the root has two children, and all the other nodes have one child, and one parent.

Although we call it D o , it actually a tree, with bounded degree. For simplicity, we provide the set of edges of the bi-branch as a set of oriented edges, which matches the relation →.

Definition 32 (bi-branch D o B k )

For any k ≥ 1, we define B k the k-th bi-branch D o by B k = (V k , E k ) where:

• E k = {(u 1 , r), (u 2 , u 1 ), • • • , (u k , u k-1 ), (v 1 , r), (v 2 , v 1 ), • • • , (v k , v k-1 )}. The class G = (B i ) i≥1 contains graphs of arbitrary large size, and is ∆-limited by log n since all the graphs it contains have degree 2. Therefore, we can apply Theorem 3. Rather than simply applying it to A, we consider the tuple (A, T, R). Theorem 3 guarantees that, for any n large-enough, there exist n distinct identifiers ID 1 , . . . , ID n in [1, n c ] which the tuple (A, T, R) does not distinguish.

Let us now consider one such large-enough network B n , such that the identifiers of the nodes are ID 1 , . . . , ID n . We consider the framework of distributed algorithms, where the initial configuration is not corrupted. Therefore, we suppose a configuration γ 0 such that the root holds the token (i.e. T γ0 (r) = true), and that all the other nodes are in one unique state. By definition, γ 0 is symmetric. Let us build step by step an infinite execution such that ∀i ∈ N, T γi (r). This is clearly contradictory with the fairness of the token circulation.

We reason by induction, building step by step an execution in such that each one or two configuration is symmetric, and such that the root permanently holds the token. The base case is immediate: γ 0 respects both properties.

Let us suppose that γ k is symmetric, and T γ k (r) = true. By symmetry, we have ∀i ∈ [1, k], for all rules R of R A , R is enabled on u i if and only if it is enabled on v i . In particular, u i is enabled if and only of v i is enabled. Since by hypothesis A solves T C, there is at least one enabled node.

If the central strongly fair scheduler activates r in γ k , then the resulting configuration γ k+1 is symmetric. Predicate T only relies on the states of the nodes, since it cannot distinguish the identifiers by construction, and therefore T γ k+1 (u i ) ⇐⇒ T γ k+1 (v i ) by symmetry. By unicity of the token, we have T γ k+1 (r), and the induction step is established.

Suppose now that the central strongly fair scheduler activates u i in γ k . In this case, the scheduler can activate v i in γ k+1 . Since there is no edge between u i and v i , the action of u i does not have any incidence on v i , which means that v i takes the exact same step as u i . As a result, γ k+2 is symmetric, and consequently r holds the token in γ k+2 . Finally, we prove that r also holds the token in γ k+1 . Since predicate T is local, and since only u i is activated in γ k , only neighbors of u i or u i itself may have their value on T updated between γ k and γ k+1 . Let w the node such that T γ k+1 (w) = true, and suppose that w ̸ = r, i.e. w = u j with j ∈ {i -1, i, i + 1}. Therefore, by symmetry and since v i takes the exact same step as u i , and is the only activated node in γ k+1 , T γ k+2 (v j ) = T γ k+2 (u j ) = true, which breaks the unicity of the token. As a consequence, r holds the token in γ k+1 , and the induction step is established.

Let us now consider the synchronous scheduler. All the enabled nodes are activated at each step, which preserves symmetry at each step, and thus the root permanently holds the token too.