Marjorie Bournat

Ajoy K Datta

Swan Dubois

Self-Stabilizing Robots in Highly Dynamic Environments *

This paper deals with the classical problem of exploring a ring by a cohort of synchronous robots. We focus on the perpetual version of this problem in which it is required that each node of the ring is visited by a robot infinitely often.

The challenge in this paper is twofold. First, we assume that the robots evolve in a highly dynamic ring, i.e., edges may appear and disappear unpredictably without any recurrence, periodicity, nor stability assumption. The only assumption we made (known as temporal connectivity assumption) is that each node is infinitely often reachable from any other node. Second, we aim at providing a self-stabilizing algorithm to the robots, i.e., the algorithm must guarantee an eventual correct behavior regardless of the initial state and positions of the robots.

In this harsh environment, our contribution is to fully characterize, for each size of the ring, the necessary and sufficient number of robots to solve deterministically the problem.

Introduction

We consider a cohort of autonomous and synchronous robots that are equipped with motion actuators and sensors, but that are otherwise unable to communicate [START_REF] Suzuki | Distributed anonymous mobile robots: Formation of geometric patterns[END_REF]. They evolve in a discrete environment, represented by a graph, where the nodes represent the possible locations of robots and the edges the possibility for a robot to move from one location to another. Refer to [START_REF] Potop-Butucaru | Distributed computing with mobile robots: An introductory survey[END_REF] for a survey of results in this model. One fundamental problem is the exploration of graphs by robots. Basically, each node of the graph has to be visited by at least one robot. There exist several variants of this problem depending on whether the robots are required to stop once they completed the exploration of the graph or not.

Typically, the environment of the robots is modeled by a static undirected connected graph meaning that both vertex and edge sets do not evolve with time. In this paper, we consider dynamic environments that may change over time, for instance, a transportation network, a building in which doors are closed and open over time, or streets that are closed over time due to work in process or traffic jam in a town. More precisely, we consider dynamic graphs [START_REF] Xuan | Computing shortest, fastest, and foremost journeys in dynamic networks[END_REF][START_REF] Casteigts | Time-varying graphs and dynamic networks[END_REF] in which edges may appear and disappear unpredictably without any stability, recurrence, nor periodicity assumption. However, to ensure that the problem is not trivially unsolvable, we made the assumption that each node is infinitely often reachable from any other one through a temporal path (a.k.a. journey [START_REF] Casteigts | Time-varying graphs and dynamic networks[END_REF]). In the following, such dynamic graphs are indifferently called highly dynamic or connected-over-time.

As in other distributed systems, fault-tolerance is a central issue in robot networks. Indeed, it is desirable that the misbehavior of some robots does not prevent the whole system to reach its objective. Self-stabilization [START_REF] Dijkstra | Self-stabilizing systems in spite of distributed control[END_REF][START_REF] Dolev | Self-stabilization[END_REF][START_REF] Tixeuil | Algorithms and Theory of Computation Handbook, chapter Self-stabilizing Algorithms[END_REF] is a versatile technique to tolerate transient (i.e., of finite duration) faults. After the occurrence of a catastrophic failure that may take the system to some arbitrary global state, self-stabilization guarantees recovery to a correct behavior in finite time without external (i.e., human) intervention. In the context of robot networks, that implies that the algorithm must guarantee an eventual correct behavior regardless of the initial state and positions of the robots.

Our objective in this paper is twofold. First, we want to investigate for the first time the problem of exploration of a highly dynamic graph by a cohort of self-stabilizing deterministic robots. Second, we aim at characterizing, for the specific case of the ring, the necessary and sufficient number of robots to perform this task (in function of the size of the ring).

Related Work. Since the seminal work of Shannon [START_REF] Shannon | Presentation of a maze-solving machine[END_REF], exploration of graphs by a cohort of robots has been extensively studied. There exist mainly three variants of the problem: (i) exploration with stop, where robots are required to detect the end of the exploration, then stop moving (e.g., [START_REF] Flocchini | Computing without communicating: Ring exploration by asynchronous oblivious robots[END_REF]); (ii) exploration with return, where robots must come back to their initial location once the exploration completed (e.g., [START_REF] Diks | Tree exploration with little memory[END_REF]); and (iii) perpetual exploration, where each node has to be infinitely often visited by some robots (e.g., [START_REF] Baldoni | On the solvability of anonymous partial grids exploration by mobile robots[END_REF]). Even if we restrict ourselves to deterministic approaches, there exist numerous solutions to these problems depending on the topology of the graphs to explore (e.g., ring-shaped [START_REF] Flocchini | Computing without communicating: Ring exploration by asynchronous oblivious robots[END_REF], line-shaped [START_REF] Flocchini | How many oblivious robots can explore a line[END_REF], tree-shaped [START_REF] Flocchini | Remembering without memory: Tree exploration by asynchronous oblivious robots[END_REF], or arbitrary network [START_REF] Chalopin | Network exploration by silent and oblivious robots[END_REF]), and the assumptions made on robots (e.g., limited range of visibility [START_REF] Datta | Ring exploration by oblivious agents with local vision[END_REF], common sense of orientation [START_REF] Blin | Exclusive perpetual ring exploration without chirality[END_REF], etc.).

Note that all the above work consider only static graphs. Recently, some work dealt with the exploration of dynamic graphs. We review them in the following.

The first two papers [START_REF] Flocchini | Exploration of periodically varying graphs[END_REF][START_REF] Ilcinkas | On the power of waiting when exploring public transportation systems[END_REF] focused on the exploration (with stop) by a single agent of so-called PV-graphs. A PV-graph is a very specific kind of dynamic graph in which a set of entities (called carriers) infinitely often move in a predetermined way, each of them periodically visiting a subset of nodes of the graph. An agent (controlled by the algorithm) is initially located at a node and can move from node to node only using a carrier. This is a relevant model for transportation networks. In this context, these two papers study the necessity and the sufficiency of various assumptions (like the anonymity of nodes, the knowledge of the size of the network, or of a bound on the periodicity of the carriers, etc.) as well as their impact on the complexity of the exploration. The main difference between these two works lies on the assumption whether the agent is able to wait a carrier on nodes [START_REF] Ilcinkas | On the power of waiting when exploring public transportation systems[END_REF] or not [START_REF] Flocchini | Exploration of periodically varying graphs[END_REF].

A second line of research [START_REF] Ilcinkas | Exploration of the t-interval-connected dynamic graphs: The case of the ring[END_REF][START_REF] Ilcinkas | Exploration of constantly connected dynamic graphs based on cactuses[END_REF][START_REF] Luna | Live exploration of dynamic rings[END_REF] considers another restriction on dynamicity by targeting T -interval-connected graphs, i.e., the graph is connected at each step and there exists a stability of this connectivity in any interval of time of length T [START_REF] Kuhn | Distributed computation in dynamic networks[END_REF]. The two first papers [START_REF] Ilcinkas | Exploration of the t-interval-connected dynamic graphs: The case of the ring[END_REF][START_REF] Ilcinkas | Exploration of constantly connected dynamic graphs based on cactuses[END_REF] investigate an off-line version of the exploration meaning that the single agent knows in advance the evolution of the graph over time and uses it to compute its route before the beginning of the execution. In both papers, the authors provide lower and upper bounds on the exploration time in this context. The first one focuses on ring-shaped graphs, the second one on cactus-shaped (i.e., trees of rings). Finally, [START_REF] Luna | Live exploration of dynamic rings[END_REF] deals with the exploration with stop of 1-interval-connected rings by several robots. The authors study the impact of numerous assumptions (like the synchrony assumption, the anonymity of the graph, the chirality of robots, or the knowledge of some characteristic of the graph) on the solvability of the problem depending on the number of robots involved. They particularly show that these assumptions may influence the capacity of robots to detect the end of the exploration and hence to systematically terminates their execution or not.

In summary, previous work on exploration of dynamic graphs restricts strongly the dynamic of the considered graph. The notable exception is a recent work on perpetual exploration of highly dynamic rings [START_REF] Bournat | Computability of perpetual exploration in highly dynamic rings[END_REF]. This paper shows that, three (resp. two) synchronous anonymous robots are necessary and sufficient to perpetually explore highly dynamic rings of size greater (resp. equals) to four (resp. three). Nonetheless, algorithms from [START_REF] Bournat | Computability of perpetual exploration in highly dynamic rings[END_REF] do not tolerate initial memory corruption nor arbitrary initial positions of robots. In other words, they are not self-stabilizing. Moreover, to the best of our knowledge, there exist no self-stabilizing algorithm for exploration either in a static or a dynamic environment. Note that there exist such fault-tolerant solutions in static graphs to other problems (e.g., naming and leader election [START_REF] Blin | On the self-stabilization of mobile robots in graphs[END_REF]).

Our Contribution. The main contribution of this paper is to prove that the necessary and sufficient numbers of robots for perpetual exploration of highly dynamic rings exhibited in [START_REF] Bournat | Computability of perpetual exploration in highly dynamic rings[END_REF] also hold in a self-stabilizing setting at the price of the loss of anonymity of robots.

More precisely, this result is achieved through the following technical achievements. Section 3 presents two impossibility results establishing that at least two (resp. three) self-stabilizing robots are necessary to perpetually explore highly dynamic rings of size greater than 3 (resp. 4) even if robots are not anonymous. Note that these necessity results are not implied by the ones of [START_REF] Bournat | Computability of perpetual exploration in highly dynamic rings[END_REF] (that focuses on anonymous robots). Then, Sections 4 and 5 present and prove two algorithms showing the sufficiency of these conditions.

Model

In this section, we propose an extension of the classical model of robot networks in static graphs introduced by [START_REF] Klasing | Gathering asynchronous oblivious mobile robots in a ring[END_REF] to the context of dynamic graphs.

Dynamic graphs. In this paper, we consider the model of evolving graphs introduced in [START_REF] Xuan | Computing shortest, fastest, and foremost journeys in dynamic networks[END_REF]. We hence consider the time as discretized and mapped to N. An evolving graph G is an ordered sequence {G 0 , G 1 , G 2 , . . .} of subgraphs of a given static graph G = (V, E). The (static) graph G is called the footprint of G. In the following, we restrict ourselves to evolving graphs whose footprints are anonymous, bidirectional, unoriented, and simple graphs. For any i ≥ 0, we have G i = (V, E i ) and we say that the edges of E i are present in G at time i. The underlying graph of G, denoted U G , is the static graph gathering all edges that are present at least once in G (i.e., U G = (V, E G ) with E G = ∞ i=0 E i ). An eventual missing edge is an edge of E G such that there exists a time after which this edge is never present in G. A recurrent edge is an edge of E G that is not eventually missing. The eventual underlying graph of G, denoted U ω G , is the static graph gathering all recurrent edges of G (i.e., U ω G = (V, E ω G ) where E ω G is the set of recurrent edges of G). In this paper, we chose to make minimal assumptions on the dynamicity of our graph since we restrict ourselves on connectedover-time evolving graphs. The only constraint we impose on evolving graphs of this class is that their eventual underlying graph is connected [START_REF] Dubois | Enabling minimal dominating set in highly dynamic distributed systems[END_REF] (intuitively, that means that any node is infinitely often reachable from any other one). For the sake of the proof, we also consider the weaker class of edge-recurrent evolving graphs where the eventual underlying graph is connected and matches to the footprint. In the following, we consider only connected-over-time evolving graphs whose footprint is a ring of arbitrary size called connected-over-time rings for simplicity. We call n the size of the ring. Although the ring is unoriented, to simplify the presentation and discussion, we, as external observers, distinguish between the clockwise and the counter-clockwise direction in the ring.

For the sake of some proofs in this paper, we need to introduce an operator denoted \ that removes some edges of an evolving graph for some time ranges. More formally, from an evolving graph G = {(V, E 0 ), (V, E 1 ), (V, E 2 ), . . .}, we define the evolving graph G\{(e 1 , τ 1 ), . . . (e k , τ k )} (with for any i ∈ {1, . . . , k}, e i ∈ E and τ i ⊆ N) as the evolving graph

{(V, E 0 ), (V, E 1 ), (V, E 2 ), . . .} such that: ∀t ∈ N, ∀e ∈ E G , e ∈ E t ⇔ e ∈ E t ∧ (∀i ∈ {1, . . . , k}, e = e i ∨ t / ∈ τ i ).
Robots. We consider systems of autonomous mobile entities called robots moving in a discrete and dynamic environment modeled by an evolving graph G = {(V, E 1 ), (V, E 2 ) . . .}, V being a set of nodes representing the set of locations where robots may be, E i being the set of bidirectional edges representing connections through which robots may move from a location to another one at time i. Robots are uniform (they execute the same algorithm), identified (each of them has a distinct identifier), have a persistent memory but are unable to directly communicate with one another by any means. Robots are endowed with local strong multiplicity detection (i.e., they are able to detect the exact number of robots located on their current node). They have no a priori knowledge about the ring they explore (size, diameter, dynamicity, . . . ) nor on the robots (number, bound on size of identifiers. . . ). Finally, each robot has its own stable chirality (i.e., each robot is able to locally label the two ports of its current node with left and right consistently over the ring and time but two different robots may not agree on this labeling). We assume that each robot has a variable dir that stores a direction (either left or right). At any time, we say that a robot points to left (resp. right) if its variable dir is equal to this (local) direction. We say that a robot considers the clockwise (resp., counter-clockwise) direction if the (local) direction pointed to by this robot corresponds to the (global) direction seen by an external observer.

Execution. The configuration of the system at time t (denoted γ t ) captures the position (i.e., the node where the robot is currently located) and the state (i.e., the value of every variable of the robot) of each robot at a given time. We say that robots form a tower on a node v in γ t if at least two robots are co-located on v in γ t . Given an evolving graph G = {G 0 , G 1 , G 2 , . . .}, an algorithm A, and an initial configuration γ 0 , the execution E of A on G starting from γ 0 is the infinite sequence (G 0 , γ 0 ), (G 1 , γ 1 ), (G 2 , γ 2 ), . . . where, for any i ≥ 0, the configuration γ i+1 is the result of the execution of a synchronous round by all robots from (G i , γ i ) as explained below.

The round that transitions the system from (G i , γ i ) to (G i+1 , γ i+1 ) is composed of three atomic and synchronous phases: Look, Compute, Move. During the Look phase, each robot gathers information about its environment in G i . More precisely, each robot updates the value of the following local predicates: (i) N umberOf RobotsOnN ode() that returns the exact number of robots present at the node of the robot; (ii) ExistsEdgeOnLef t() that returns true if an edge in the left direction of the robot is present, false otherwise; (iii) ExistsEdgeOnRight() that returns true if an edge in the right direction of the robot is present, false otherwise; (iv) ExistsAdjacentEdge() returns true if an edge adjacent to the current node of the robot is present, false otherwise. During the Compute phase, each robot executes the algorithm A that may modify some of its variables (in particular dir) depending on its current state and on the values of the predicates updated during the Look phase. Finally, the Move phase consists of moving each robot trough one edge in the direction it points to if there exists an edge in that direction, otherwise, i.e., if the edge is missing at that time, the robot remains at its current node. Note that the i th round is entirely executed on G i and that the transition from G i to G i+1 occurs only at the end of this round. We say that a robot is edge-activated during a round if there exists at least one edge adjacent to its location during that round. To simplify the pseudo-code of the algorithms, we assume that the robots have access to two predicates: ExistsEdgeOnCurrentDirection() (that returns true if an edge is present at the direction currently pointed by the robot, false otherwise) and ExistsEdgeOnOppositeDirection() (that returns true if an edge is present in the direction opposite to the one currently pointed by the robot, false otherwise). Both of these two predicates depend on the values of the predicates ExistsRightEdge() and ExistsLef tEdge(), and on the value of the variable dir.

Self-Stabilization. Intuitively, a self-stabilizing algorithm is able to recover in a finite time a correct behavior from any arbitrary initial configuration (that captures the effect of an arbitrary transient fault in the system). More formally, an algorithm A is self-stabilizing for a problem on a class of evolving graphs C if and only if it ensures that, for any configuration γ 0 , the execution of A on any G ∈ C starting from γ 0 contains a configuration γ i such that the execution of A on G starting from γ i satisfies the specification of the problem. Note that, in the context of robot networks, this definition implies that robots must tolerate both arbitrary initialization of their variables and arbitrary initial positions (in particular, robots may be stacked in the initial configuration).

Perpetual Exploration. Given an evolving graph G, a perpetual exploration algorithm guarantees that every node of G is infinitely often visited by at least one robot (i.e., a robot is infinitely often located at every node of G). Note that this specification does not require that every robot visits infinitely often every node of G.

Necessary Number of Robots

This section is devoted to the proof of the necessity of two (resp. three) self-stabilizing identified robots to perform perpetual exploration of highly dynamic rings of size at least 3 (resp. 4). To reach this goal, we provide two impossibility results.

First, we prove (see Theorem 3.1) that two robots with distinct identifiers are not able to perpetually explore in a self-stabilizing way connected-over-time rings of size greater than 4. Then, we show that we can borrow arguments from [START_REF] Bournat | Computability of perpetual exploration in highly dynamic rings[END_REF] to prove Theorem 3.2 that states that only one robot cannot complete the self-stabilizing perpetual exporation of connected-over-time rings of size greater than 3.

Highly Dynamic Rings of Size 4 or More

The proof of Theorem 3.1 makes use of a generic framework proposed in [START_REF] Braud-Santoni | The next 700 impossibility results in time-varying graphs[END_REF]. Note that, even if this generic framework is designed for another model (namely, the classical message passing model), it is straightforward to borrow it for our current model. Indeed, its proof only relies on the determinism of algorithms and indistinguishability of dynamic graphs, these arguments being directly translatable in our model. We present briefly this framework here. The interested reader is referred to [START_REF] Braud-Santoni | The next 700 impossibility results in time-varying graphs[END_REF] for more details.

This framework is based on a theorem that ensures that, if we take a sequence of evolving graphs with ever-growing common prefixes (that hence converges to the evolving graph that shares all these common prefixes), then the sequence of corresponding executions of any deterministic algorithm also converges. Moreover, we are able to describe the execution to which it converges as the execution of this algorithm on the evolving graph to which the sequence converges. This result is useful since it allows us to construct counter-example in the context of impossibility results. Indeed, it is sufficient to construct an evolving graphs sequence (with ever-growing common prefixes) and to prove that their corresponding execution violates the specification of the problem for ever-growing time to exhibit an execution that never satisfies the specification of the problem.

In order to build the evolving graphs sequence suitable for the proof of our impossibility result, we need the following technical lemma. Lemma 3.1. Let A be a self-stabilizing deterministic perpetual exploration algorithm in connectedover-time rings of size 4 or more using 2 robots r 1 and r 2 with distinct identifiers. Any execution of A satisfies: For any time t, for any states s 1 and s 2 , for any distinct identifiers id 1 and id 2 , it exists t such that if r 1 , of identifier id 1 , is on node u 1 in state s 1 , and r 2 , of identifier id 2 , is on node u 2 in state s 2 such that there exists only one adjacent edge to each position of the robots continuously present from time t to time t , then r 1 and/or r 2 moves at time t . This lemma holds even if the robots have the same chirality.

Proof. Consider a self-stabilizing algorithm A that solves deterministically the perpetual exploration problem for connected-over-time rings of size 4 or more using two robots with distinct identifiers. Let G = {G 0 , G 1 , . . .} be a connected-over-time ring whose footprint G is a ring of size 4 or more, and such that ∀i ∈ N, G i = G. Let r 1 and r 2 be two robots executing A on G.

By contradiction, assume that there exists a time t, two states s 1 and s 2 , and two distinct identifiers id 1 and id 2 such that at time t, r 1 of identifier id 1 is in state s 1 on a node u 1 of G, r 2 of identifier id 2 is in state s 2 on a node u 2 (it is possible to have u 2 = u 1 ) of G, such that, for any time t ≥ t, if there exists only one adjacent edge to each position of the robots continuously present from time t to time t , then none of the robots move.

Consider the graph G such that G = G and such that G = G\{(e, {0, . . . , +∞})}, where e is the edge linking u 1 and its adjacent node in the clockwise direction. Note that G is a connectedover-time ring, since it only possesses one eventual missing edge.

In the case where at time t in G, r 1 and r 2 are on the same node, since A is a self-stabilizing algorithm, we can initially place r 1 and r 2 on node u 1 of G in state s 1 and s 2 respectively.

In the case where at time t in G, r 1 and r 2 are not on the same node, since A is a self-stabilizing algorithm, we can initially place r 1 on node u 1 of G in state s 1 and r 2 on the adjacent node of node u 1 in the clockwise direction in state s 2 .

In these two cases, by construction, there is only one adjacent edge to each position of the robots continuously present from time 0 to +∞, and r 1 and r 2 are respectively in state s 1 and s 2 .

Then, by assumption, r 1 and r 2 does not leave their respective nodes after time 0. As G counts 4 nodes or more, we obtain a contradiction with the fact that A is a self-stabilizing algorithm solving deterministically the perpetual exploration problem for connected-over-time rings of size 4 or more using two robots. Theorem 3.1. There exists no deterministic algorithm satisfying the perpetual exploration specification in a self-stabilizing way on the class of connected-over-time rings of size 4 or more with two fully synchronous robots possessing distinct identifiers.

Proof. By contradiction, assume that there exists a deterministic algorithm A satisfying the perpetual exploration specification in a self-stabilizing way on any connected-over-time rings of size 4 or more using two robots r 1 and r 2 possessing distinct identifiers.

Consider the connected-over-time graph G = {G 0 , G 1 , . . .} whose footprint G is a ring of size strictly greater than 3 and such that ∀i ∈ N, G i = G.

Consider four nodes u, v, w and x of G, such that node v is the adjacent node of u in the clockwise direction, w is the adjacent node of v in the clockwise direction, and x is the adjacent node of w in the clockwise direction. We denote respectively e ur and e ul the clockwise and counter clockwise adjacent edges of u, e vr and e vl the clockwise and counter clockwise adjacent edges of v, e wr and e wl the clockwise and counter clockwise adjacent edges of w, and e xr and e xl the clockwise and counter clockwise adjacent edges of x. Note that e ur = e vl , e vr = e wl , and e wr = e xl .

Let ε be the execution of A on G starting from the configuration where r 1 (resp. r 2 ) is located on node v (resp. w).

We construct a sequence of connected-over-time graphs (G m ) m∈N such that G 0 = G and for any i ≥ 0, if G i exists, it is a connected-over-time ring, and at time t i only nodes among {v, w, x} have been visited, then we can define G i+1 as shown on Figure 1, and as explained in the following paragraph (denote by ε i the execution of A on G i starting from the same configuration as ε).

Since G i is a connected-over-time ring, and since A is a deterministic algorithm solving the perpetual exploration algorithm in a self-stabilizing way on connected-over-time rings of size 4 or more using 2 robots possessing distinct identifiers, when the configuration γ i at time t i is such that the two robots possess exactly one adjacent edge present, we use Lemma 3.1 to exhibit time t i ≥ t i such that if the configuration γ i last from time t i to time t i , then one or both of the robots move. Similarly, since G i is a connected-over-time ring, and since A is a deterministic algorithm solving the perpetual exploration algorithm in a self-stabilizing way on connected-over-time rings of size 4 or more using 2 robots possessing distinct identifiers, when the configuration γ i at time t i is such that there is only one missing edge, and that only one robot is adjacent to this missing edge, then we can also exhibit a time t i at which at least one of the robots move. Indeed, if this configuration lasts from time t i to time +∞, G i is a connected-over-time ring, and if none of the robot move in this configuration, the exploration cannot be solved. Therefore such a time t i exists. In the following we show how we construct the dynamic graph G i+1 , in function of t i and G i . If the two robots are on two distinct nodes in G i then:

• if one of the robot is on node v and the other robot is on node w then we define G i+1 such that G i+1 and G i have the same footprint, and G i+1 = G i \{(e vl , {t i , . . . , t i })}.

• if one of the robot is on node x and the other robot is on node w then we define G i+1 such that G i+1 and G i have the same footprint, and G i+1 = G i \{(e xr , {t i , . . . , t i })}. • if one of the robot is on node v and the other robot is on node x then we define G i+1 such that G i+1 and G i have the same footprint, and G i+1 = G i \{(e vl , {t i , . . . , t i }), (e xr , {t i , . . . , t i })}.

If the two robots are on the same node in G i then:

• if the two robots are on node v, then we define G i+1 such that G i+1 and G i have the same footprint, and G i+1 = G i \{(e vl , {t i , . . . , t i })}.

• if the two robots are on node w then we define G i+1 such that G i+1 and G i have the same footprint, and G i+1 = G i \{(e wr , {t i , . . . , t i })}.

• if the two robots are on node x, then we define G i+1 such that G i+1 and G i have the same footprint, and G i+1 = G i \{(e xr , {t i , . . . , t i })}.

Note that G i and G i+1 are indistinguishable for robots before time t i . This implies that, at time t i , r 1 and r 2 are on the same node in ε i and in ε i+1 . By construction of t i , either r 1 or r 2 or both of the two robots move at time t i in ε i+1 . G i+1 is a connected-over-time ring (since it is indistinguishable from G after t i + 1). Moreover, even if one or both of the robots move during the Move phase of time t i , at time t i + 1 the robots are still on nodes among {v, w, x}, by assumption on G i and since from time t i to time t i the edges permitting to go on a node other than the nodes among {v, w, x} are missing.

Let t i+1 = t i + 1. Then we can construct recursively each dynamic ring of (G m ) m∈N by applying the argues above on all the possible configurations reached by the movements of the robots at time

t i on G i+1 .
Note that the recurrence can be initiated, since G 0 exists, is a connected-over-time ring and that at time t 0 = 0 only nodes among {v, w, x} have been visited. In other words, (G m ) m∈N is well-defined.

We can then define the evolving graph G ω such that G ω and G 0 have the same footprint, and such that for all i ∈ N, G ω shares a common prefix with G i until time t i .

Note that among the configurations presented in Figure 1, only Configuration 4 contains 2 missing edges. However, if this configuration is reached in G ω the following configuration reached in G ω is either Configuration 13 or Configuration 14 or Configuration 15. Since these three configurations possess only one missing edge, this implies that G ω is a connected-over-time ring.

As the sequence (t m ) m∈N is increasing by construction, this implies that the sequence (G m ) m∈N converges to G ω .

Applying the theorem of [START_REF] Braud-Santoni | The next 700 impossibility results in time-varying graphs[END_REF], we obtain that, until time t i , the execution of A on G ω is identical to the one on G i . This implies that, executing A on G ω (whose footprint is a ring of size strictly greater than 3), r 1 and r 2 only visit the nodes among {v, w, x}. This is contradictory with the fact that A satisfies the perpetual exploration specification on connected over time rings of size strictly greater than 3 using 2 robots.

Highly Dynamic Rings of Size 3 or More

In [START_REF] Bournat | Computability of perpetual exploration in highly dynamic rings[END_REF], the authors prove (in Theorem V.1) that a single anonymous and synchronous robot cannot perpetually explore connected-over-time rings of size 3 or more in a fault-free setting. We can do two observations. First, any fault-free synchronous execution is possible in a self-stabilizing setting. Second, in the case of a single robot, the anonymous and the identified model are equivalent.

These observations are sufficient to directly state the following result:

Theorem 3.2. There exists no deterministic algorithm satisfying the perpetual exploration specification in a self-stabilizing way on the class of connected-over-time rings of size 3 or more using one robot possessing an identifier.

4 Sufficiency of Three Robots for n ≥ 4

In this section, we present our self-stabilizing deterministic algorithm for the perpetual exploration of any connected-over-time ring of size greater than 4 with three robots. In this context, the difficulty to complete the exploration is twofold. First, in connected-over-time graphs, robots must deal with the possible existence of some eventual missing edge (without the guarantee that such edge always exists). Note that, in the case of a ring, there is at most one eventual missing edge in any execution (otherwise, we have a contradiction with the connected-over-time property). Second, robots have to handle the arbitrary initialization of the system (corruption of variables and arbitrary position of robots).

Presentation of the algorithm

Principle of the algorithm. The main idea behind our algorithm is that a robot does not change its direction (arbitrarily initialized) while it is isolated. This allows robots to perpetually explore connected-over-time rings with no eventual missing edge regardless of the initial direction of the robots. Obviously, this idea is no longer sufficient when there exists an eventual missing edge since, in this case, at least two robots will eventually be stuck (i.e., they point to an eventual missing edge that they are never able to cross) forever at one end of the eventual missing edge. When two (or more) robots are located at the same node, we say that they form a tower. In this case, our algorithm succeed (as we explain below) to ensure that at least one robot leaves the tower in a finite time. In this way, we obtain that, in a finite time, a robot is stuck at each end of the eventual missing edge. These two robots located at two ends of the eventual missing edge play the role of "sentinels" while the third one (we call it a "visitor") visits other nodes of the ring in the following way. The "visitor" keeps its direction until it meets one of these "sentinels", they then switch their roles: After the meeting, the "visitor" still maintains the same direction (becoming thus a "sentinel") while the "sentinel" robot changes its direction (becoming thus a "visitor" until reaching the other "sentinel").

In fact, robots are never aware if they are actually stuck at an eventual missing edge or are just temporarily stuck on an edge that will reappear in a finite time. That is why it is important that the robots keep consider their directions and try to move forward while there is no meeting in order to track a possible eventual missing edge. Our algorithm only guarantees a convergence in a finite time towards a configuration where a robot plays the role of "sentinel" at each end of the eventual missing edge if such an edge exists. Note that, in the case where there is no eventual missing edge, this mechanism does not prevent the correct exploration of the ring since it is impossible for a robot to be stuck forever.

Our algorithm easily deals with the initial corruption of its variables. Indeed, all variables of a robot (at the exception of a counter and the variable dir whose initial respective values have no particular impact) store information about the environment of this robot in the previous round it was edge-activated. These variables are updated each time a robot is edge-activated. Since we consider connected-over-time rings, it can only exist one eventual missing edge, therefore all robots are infinitely often edge-activated. The initial values of these variables are hence reset in a finite time. The main difficulty to achieve self-stabilization is to deal with the arbitrary initial position of robots. In particular, the robots may initially form towers. In the worst case, all robots of a tower may be stuck at an eventual missing edge and be in the same state. They are then unable to start the "sentinels"/"visitor" scheme explained above. Our algorithm needs to "break" such a tower in a finite time (i.e., one robot must leave the node where the tower is located). In other words, we tackle a classical problem of symmetry breaking. We succeed by providing each robot with a function that returns, in a finite number of invocations, different global directions to two robots of the tower based on the private identifier of the robot and without any communication among the robots. More precisely, this is done thanks to a transformation of the robot identifier: each bit of the binary representation of the identifier is duplicated and we add the bits "010" at the end of the sequence of these duplicated bits. Then, at each invocation of the function, a robot reads the next bit of this transformed identifier. If the robot reads zero, it try to move to its left. Otherwise, it try to move to its right. Doing so, in a finite number of invocation of this function, at least one robot leaves the tower. If necessary, we repeat this "tower breaking" scheme until we are able to start the "sentinels"/"visitor" scheme.

The main difficulty in designing this algorithm is to ensure that these two mechanisms ("sentinels"/"visitor" and "tower breaking") do not interfere with each other and prevent the correct exploration. We solve this problem by adding some waiting at good time, especially before starting the procedure of tower breaking by identifier to ensure that robots do not prematurely turn back and "forget" to explore some parts of the ring.

Formal presentation of the algorithm. Before presenting formally our algorithm, we need to introduce the set of constants (i.e., variables assumed to be not corruptible) and the set of variables of each robot. We also introduce three auxiliary functions.

As stated in the model, each robot has an unique identifier. We denote it by id and represent it in binary as b 1 b 2 . . . b |id| . We define, for the purpose of the "breaking tower" scheme, the constant T ransf ormedIdentif ier by its binary representation b 1 b 1 b 2 b 2 . . . b |id| b |id| 010 (each bit of id is duplicated and we add the three bits 010 at the end). We store the length of the binary representation of T ransf ormedIdentif ier in the constant and we denote its ith bit by T ransf ormedIdentif ier[i] for any 1 ≤ i ≤ .

In addition to the variable dir defined in the model, each robot has the following three variables: (i) the variable i ∈ N corresponds to an index to store the position of the last bit read from T ransf ormedIdentif ier; (ii) the variable N umberRobotsP reviousEdgeActivation ∈ N stores the number of robots that were present at the node of the robot during the Look phase of the last round where it was edge-activated; and (iii) the variable HasM ovedP reviousEdgeActivation ∈ {true, f alse} indicates if the robot has crossed an edge during its last edge-activation.

Our algorithm makes use of a function Update that updates the values of the two last variables according to the current environment of the robot each time it is edge-activated. We provide the pseudo-code of this function in Algorithm 1. Note that this function also allows us to deal with the initial corruption of the two last variables since it resets them in the first round where the robot is edge-activated.

We already stated that, whenever robots are stuck forming a tower, they make use of a function to "break" the tower in a finite time. The pseudo-code of this function GiveDirection appears in Algorithm 1 Function Update

1: function Update 2:
if ExistsAdjacentEdge() then 3:

N umberRobotsP reviousEdgeActivation ← N umberOf RobotsOnN ode() 4:

HasM ovedP reviousEdgeActivation ← ExistsEdgeOnCurrentDirection() 5:

end if 6: end function Algorithm 2. It assigns the value lef t or right to the variable dir of the robot depending on the ith bit of the value of T ransf ormedIdentif ier. The variable i is incremented modulo (that implicitly resets this variable when it is corrupted) to ensure that successive calls to GiveDirection will consider each bit of T ransf ormedIdentif ier in a round-robin way. As shown in the next section, this function guarantees that, if two robots are stuck together in a tower and invoke repeatedly their own function GiveDirection, then two distinct global directions are given in finite time to the two robots regardless of their chirality. This property allows the algorithm to "break" the tower since at least one robot is then able to leave the node where the tower is located.

Finally, we define the function OppositeDirection that simply affects the value lef t (resp. right) to the variable dir when dir = right (resp. dir = lef t).

There are two types of configurations in which the robots may change the direction they consider. So, our algorithm needs to identify them. We do so by defining a predicate that characterizes each of these configurations.

The first one, called W eAreStuckInT heSameDirection(), is dedicated to the detection of configurations in which the robot must invoke the "tower breaking" mechanism. Namely, the robot is stuck since at least one edge-activation with at least another robot and the edge in the direction opposite to the one considered by the robot is present. More formally, this predicate is defined as follows: W eAreStuckInT heSameDirection() ≡ (N umberOf RobotsOnN ode() > 1) ∧ (N umberOf RobotsOnN ode() = N umberRobotsP reviousEdgeActivation) ∧ ¬ExistsEdgeOnCurrentDirection() ∧ ExistsEdgeOnOppositeDirection() ∧ ¬HasM ovedP reviousEdgeActivation The second predicate, called IW asStuckOnM yN odeAndN owW eAreM oreRobots(), is designed to detect configurations in which the robot must transition from the "sentinel" to the "visitor" role in the "sentinel"/"visitor" scheme. More precisely, such configuration is characterized by the fact that the robot is edge-activated, stuck during its previous edge-activation, and there are strictly more robots located at its node than at its previous edge-activation. More formally, this predicate is defined as follows: IW asStuckOnM yN odeAndN owW eAreM oreRobots() ≡ (N umberOf RobotsOnN ode() > N umberRobotsP reviousEdgeActivation) ∧ ¬HasM ovedP reviousEdgeActivation ∧ ExistsAdjacentEdge() Now, we are ready to present the pseudo-code of the core of our algorithm (see Algorithm 3). The basic idea of the algorithm is the following. The function GiveDirection is invoked when W eAreStuckInT heSameDirection() is true (to try to "break" the tower after the appropriate Algorithm 2 Function GiveDirection waiting), while the function OppositeDirection is called when IW asStuckOnM yN odeAnd-N owW eAreM oreRobots() is true (to implement the "sentinel"/"visitor" scheme). Afterwards, the function Update is called (to update the state of the robot according to its environment).

Preliminaries to the Correctness Proof

First, we introduce some definitions and preliminary results that are extensively used in the proof.

We saw previously that the notion of tower is central in our algorithm. Intuitively, a tower captures the simultaneous presence of all robots of a given set on a node at each time of a given interval. We require either the set of robots or the time interval of each tower to be maximal. Note that the tower is not required to be on the same node at each time of the interval (robots of the tower may move together without leaving the tower).

We distinguish two kinds of towers according to the agreement of their robots on the global direction to consider at each time there exists an adjacent edge to their current location (excluded the last one). If they agreed, the robots form a long-lived tower while they form a short-lived tower in the contrary case. This implies that a short-lived tower is broken as soon as the robots forming the tower are edge-activated, while the robots of a long-lived tower move together at each edge activation of the tower (excluded the last one). Definition 4.1 (Tower). A tower T is a couple (S, θ), where S is a set of robots (|S| > 1) and θ = [t s , t e ] is an interval of N, such that all the robots of S are located at a same node at each instant of time t in θ and S or θ are maximal for this property. Moreover, if the robots of S move during a round t ∈ [t s , t e [, they are required to traverse the same edge. Definition 4.2 (Long-lived tower). A long-lived tower T = (S, [t s , t e ]) is a tower such that there is at least one edge-activation of all robots of S in the time interval [t s , t e [. Definition 4.3 (Short-lived tower). A short-lived tower T is a tower that is not a long-lived tower.

For k > 1, a long-lived (resp., a short-lived) tower T = (S, θ) with |S| = k is called a k-long-lived (resp., a k-short-lived) tower.

As there are only three robots on our system, and that in each round each of them consider a global direction, we can make the following observation. Observation 4.1. There are at least two robots having the same global direction at each instant time.

In the remainder of this section, we consider an execution E of Algorithm 3 executed by three robots r 1 , r 2 , and r 3 on a connected-over-time ring G of size n ∈ N, with n ≥ 4, starting from an arbitrary configuration.

For the sake of clarity, the value of a variable or a predicate name of a given robot r after the Look phase of a given round t is denoted by the notation name(r, t).

We say that a robot r has a coherent state at time t, if the value of its variable N umber-RobotsP reviousEdgeActivation(r, t) corresponds to the value of its predicate N umberOf Robots-OnN ode() at its previous edge-activation and the value of its variable HasM ovedP reviousEdge-Activation(r, t) corresponds to the value of its predicate ExistsEdgeOnCurrentDirection() at its previous edge-activation. The following lemma states that, for each robot, there exists a suffix of the execution in which the state of the robot is coherent. Lemma 4.1. For any robot, there exists a time from which its state is always coherent.

Proof. Consider a robot r performing SELF-STAB PEF 3.

G belongs to the class of connected-over-time rings, hence at least one adjacent edge to each node of G is infinitely often present. This implies that r is infinitely often edge-activated, whatever its location is. Let t be the first time at which r is edge-activated.

Variables can be updated only during Compute phases of rounds. When executing SELF-STAB PEF 3, the variables N umberRobotsP reviousEdgeActivation and HasM ovedP reviousEdge-Activation of r are updated with the current values of its predicates N umberOf RobotsOnN ode() and ExistsEdgeOnCurrentDirection() only when it is edge-activated.

Therefore from time t + 1, r is in a coherent state.

Let t 1 , t 2 , and t 3 be respectively the time at which the robots r 1 , r 2 , and r 3 , respectively are in a coherent state. Let t max = max{t 1 , t 2 , t 3 }. From Lemma 4.1, the three robots are in a coherent state from t max . In the remaining of the proof, we focus on the suffix of the execution after t max .

The two following lemmas (in combination with Lemma 4.5 and Corollary 4.1) aim at showing that, regardless of the chirality of the robots and the initial values of their variables i, a finite number of synchronous invocations of the function GiveDirection by two robots of a long-lived tower returns them a distinct global direction. This property is shown by looking closely to the structure of the binary representation of the transformed identifiers of the robots.

To state these lemmas, we need to introduce some vocabulary and definitions from combinatorics on words. We consider words as (possibly infinite) sequence of letters from the alphabet A = {0, 1}. Given a word u, we refer to its i-th letter by u[i]. The length of a word u (denoted |u|) is its number of letters. Given two words u

= u[1] . . . u[k] and v = v[1] . . . v[ ] (with k = |u| and = |v|), the concatenation of u and v (denoted u.v) is the word u[1] . . . u[k]v[1] . . . v[ ] (with |u.v| = k + ).
Given a finite word u, the word u 1 is u itself and the word u z (z > 1) is the word u.u z-1 . Given a finite word u, the word u ω is the infinite word u.u.u. . . .. A prefix u 1 of a word u is a word such that there exists a word u 2 satisfying u = u 1 .u 2 . A suffix u 2 of a word u is a word such that there exists a word u 1 satisfying u = u 1 .u 2 . A factor u 2 of a word u is a word such that there exists a prefix u 1 and a suffix u 3 of u satisfying u = u 1 .u 2 .u 3 . The factor of u starting from the i th bit of u and ending to the j th bit of u included is denoted u[i . . . j]. A circular permutation of a word u is a word of the form u 2 .u 1 where u = u 1 .u 2 . Lemma 4.2. Let u and v be two distinct transformed identifiers. If u ω and v ω share a common factor X, then X is finite.

Proof. Consider two distinct transformed identifiers u and v such that u = v.

By definition, the transformed identifier u is either equal to 00.010 or to 11.Π

α(u) d=1 (Π β(u,d) 1 00.Π γ(u,d) 1
11).010 ( * ) with α(u) a function giving the number of blocks (Π

β(u,d) 1 00.Π γ(u,d) 1
11) contained in u, β(u, d) a function giving the number of pair of bits 00 contained in the d th block of u, and γ(u, d) a function giving the number of pair of bits 11 contained in the d th block of u.

Similarly, by definition v is either equal to 00.010 or to 11.Π

α(v) d=1 (Π β(v,d) 1 00.Π γ(v,d) 1
11).010 ( * * ). Let U = u ω and V = v ω . Assume by contradiction that U and V share a common factor X of infinite size. Hence U = x.X and V = y.X, with x (respectively y) the prefix of U (respectively of V ). We have X = ũω , where ũ is a circular permutation of the word u, and X = ṽω , where ṽ is a circular permutation of the word v.

By definition of a common factor we have Let U = u ω and W = w ω . Assume by contradiction that U and W share a common factor X of infinite size. Hence U = x.X and W = y.X, with x (respectively y) the prefix of U (respectively of W ). We have X = ũω , where ũ is a circular permutation of the word u, and X = wω , where w is a circular permutation of the word w.

∀h ∈ N * , U [|x| + h] = V [|y| + h] ( * * * ). Let k ∈ N * such that k > |x|
< |v|. Since V [|y|+k+3 . . . |y|+k+|v|+2] is equal to v, this implies that V [|y|+k+3] = v[1], and V [|y| + k + |u|] = V [|y| + k + 2w + 3] = v[i]
By definition of a common factor we have

∀h ∈ N * , U [|x| + h] = W [|y| + h] ( * * * ). Let k ∈ N * such that k > |x|

Tower Properties

We are now able to state a set of lemmas that show some interesting technical properties of towers under specific assumptions during the execution of our algorithm. These properties are extensively used in the main proof of our algorithm.

Lemma 4.4. The robots of a long-lived tower T = (S, [t s , t e ]) consider a same global direction at each time between the Look phase of round t s and the Look phase of round t e included.

Proof. Consider a long-lived tower T = (S, [t s , t e ]).

Call t act the first time in [t s , t e [ at which the robots of S are edge-activated. Since T is a long-lived tower, t act exists.

When executing SELF-STAB PEF 3, a robot can change the global direction it considers only when it is edge-activated. Moreover a robot does not change the global direction it considers if it has moved during its previous edge-activation. Besides, during the Look phase of a time t a robot considers the same global direction than the one it considers during the Move phase of time t -1.

Therefore, during the Look phase of time t s the robots of S consider the same global direction, otherwise the robots of S consider different global directions during the Move phase of time t s -1, and so move during this phase (otherwise T is not formed at time t s ), therefore they separate during the Move phase of time t act . This leads to a contradiction with the fact that T is a long-lived tower.

Consider a time t ∈]t s , t e [. If at time t the robots of S are not edge-activated, then during the Move phase of time t the robots of S do not change the global direction they consider.

T is a long-lived tower from time t s to time t e included. Therefore if at time t ∈]t s , t e [ the robots of S are edge-activated, then, by definition of a long-lived tower, during the Move phase of time t, the robots of S consider the same global direction.

Since at time t s the robots of S consider the same global direction using the two previous arguments by recurrence on each time t ∈]t s , t e [ and the fact that robots change the global directions they consider only during Compute phases, we can conclude that the robots of S consider a same global direction from the Look phase of time t s to the Look phase of time t e .

The following lemma is used to prove, in combination with Lemmas 4.2 and 4.3, the "tower breaking" mechanism since it proves that robots of a long-lived tower synchronously invoke their GiveDirection function after their first edge-activation. Lemma 4.5. For any long-lived tower T = (S, [t s , t e ]), any (r i , r j ) in S 2 , and any t less or equal to t e , we have W eAreStuckInT heSameDirection()(r i , t) = W eAreStuckInT heSameDirection()(r j , t) and IW asStuckOnM yN odeAndN owW eAreM oreRobots()(r i , t) = IW asStuckOn-M yN odeAndN owW eAreM oreRobots()(r j , t) if all robots of S have been edge-activated between t s (included) and t (not included).

Proof. Consider a long-lived tower T = (S, [t s , t e ]). Let t act be the first time in [t s , t e [ where the robots of S are edge-activated. By definition of a long-lived tower, this time exists.

By definition of a long-lived tower and by lemma 4.4, from the Look phase of time t s to the Look phase of time t e included, all the robots of S are on a same node and consider a same global direction. Therefore the values of their respective predicates N umberOf RobotsOnN ode(), Exists-EdgeOnCurrentDirection(), ExistsEdgeOnOppositeDirection() and ExistsAdjacentEdge() are identical from the Look phase of time t s to the Look phase of time t e included.

When executing SELF-STAB PEF 3, a robot updates its variables N umberRobotsP revious-EdgeActivation and HasM ovedP reviousEdgeActivation respectively with the values of its predicates N umberOf RobotsOnN ode() and ExistsEdgeOnCurrentDirection(), only during Compute phases of times where it is edge-activated. By the observation made at the previous paragraph, this implies that from the Compute phase of time t act to the Look phase of time t e included, the robots of S have the same values for their variables N umberRobotsP reviousEdgeActivation and HasM ovedP reviousEdgeActivation.

Then, by construction of the predicates W eAreStuckInT heSameDirection() and IW asStuck-OnM yN odeAndN owW eAreM oreRobots(), the lemma is proved.

From the Lemmas 4.5, 4.2 and 4.3, we can then deduce the following corollary. Proof. First, note that if two robots possess two distinct identifiers, then their transformed identifiers are also distinct.

Consider a long-lived tower T = (S, θ) with θ = [t s , +∞[. Call t act ≥ t s the first time after t s where the robots of S are edge-activated. By definition of a long-lived tower, t act exists. By Lemma 4.5, after time t act , the robots of S consider the same values of predicates W eAreStuckInT heSameDirection() and IW asStuckOnM yN odeAndN ow-W eAreM oreRobots().

Assume by contradiction that after t act the predicates W eAreStuckInT heSameDirection() of the robots of S are infinitely often true. Then by construction of SELF-STAB PEF 3, after time t act , all the robots of S call the function GiveDirection infinitely often and at the same instants of times.

If among the robots of S two have the same chirality, to keep forming T they need to consider the same values of bits each time the function GiveDirection is called. Here the robots have to consider the same values of bits infinitely often (since the two robots call the function GiveDirection infinitely often). Each time a robot executes the function GiveDirection it reads the next bit (in a round robin way) of the bit read during its previous call to the function GiveDirection. Call i 1 and i 2 the two respective transformed identifiers of two robots forming T such that these two robots possess the same chirality. By the previous observations, to keep forming T , i ω 1 and i ω 2 must share an infinite common factor. However according to Lemma 4.2 this is not possible. Therefore there exists a time t end at which these two robots consider two different bits. When the robots call the function GiveDirection, they are edge-activated (by definition of the predicate W eAreStuckInT heSameDirection()), therefore at time t end , T is broken.

Similarly, if among the robots of S two have not the same chirality, to keep forming T they need to consider different values of bits each time the function GiveDirection is called. Here the robots have to consider different values of bits infinitely often (since the two robots call the function reach node u in finite time. However e is missing forever, hence in finite time, the predicates W eAreStuckInT heSameDirection() of all the robots are true. This leads to a contradiction.

Case 2: |S| = 2. Assume, without lost of generality, that T is formed of r 1 and r 2 .

If, after t f alse , the 2-long-lived tower does not meet r 3 , then by similar arguments than the one used for the case 1 we prove that there is a contradiction. Now consider the case where the 2-long-lived tower meets r 3 . If at a time t > t f alse , the robots of S meet r 3 it is either because the two entities (the tower and r 3 ) move during the Move phase of time t -1 while considering two opposed global directions or because the two entities consider the same global direction but one of the entity cannot move (an edge is missing in its direction) during the Move phase of round t -1. Let t act ≥ t be the first time after time t included where the three robots are edge-activated. All the edges of G except e are infinitely often present therefore t act exists. In both cases, thanks to the update at time t -1 of the variables HasM ovedP reviousEdgeActivation and N umberRobotsP re-viousEdgeActivation of the robots, during the Move phase of time t act the robots of the two entities consider opposed global directions. The two entities separate them during the Move phase of this time. Moreover, from this separation, as long as r 3 is alone on its node it does not change the global direction it considers. Similarly, from this separation, as long as the robots of S do not meet r 3 , their predicates IW asStuckOnM yN odeAndN owW eAreM oreRobots() are false, and since from time t f alse their predicates W eAreStuckInT heSameDirection() are false, they do not change the global direction they consider.

Hence, in finite time after time t act the two entities are located respectively on the two extremities of e. However e is missing forever, therefore in finite time, the predicates W eAre-StuckInT heSameDirection() of the robots of T are true. This leads to a contradiction.

In both cases a contradiction is highlighted. Therefore, after t f alse all the robots of S have their predicates W eAreStuckInT heSameDirection() infinitely often true. Then we can use Corollary 4.1 to prove that T is broken, which leads to a contradiction with the fact that θ = [t s , +∞[. Lemma 4.7. No execution containing only configurations without long-lived tower reaches a configuration where three robots form a tower. Proof. Assume that there is no long-lived tower in the execution. The robots can cross at most one edge at each round. Each node has at most 2 adjacent edges in G. Moreover each robot considers at each instant time a direction. Assume, by contradiction that 3 robots form a tower T at a time t. Let t ≥ t be the first time after time t where the robots of T are edge-activated. There is no 3-long-lived tower in the execution, therefore during the Move phase of time t , the robots of T consider two opposed global directions. However there are three robots, and two different global directions, hence, during the Move phase of time t , two robots consider the same global direction. Therefore there exists a 2-long-lived tower, which leads to a contradiction. Lemma 4.8. In every execution, if a tower involving 3 robots is formed at time t, then at time t -1 a 2-long-lived tower is present in ε.

Proof. Assume that a tower T of 3 robots is formed at time t.

First note that if there exists a 2-long-lived tower T = (S, [t s , t e ]) such that t -1 ∈ [t s , t e [, it is possible for T to be formed. Now we prove that if there is no 2-long-lived tower at time t -1 then T cannot be formed at time t. Assume that at time t -1 there is no 2-long-lived tower. Let us consider the three following cases.

Case 1: There is a tower T of 3 robots at time t -1. The tower T must break at time t -1, otherwise there is a contradiction with the fact that T is formed at time t. Hence the robots of T are edge-activated at time t -1. While executing SELF-STAB PEF 3 the robots consider a direction at each round. There are only two possible directions. Therefore, for the tower T to break at time t -1, two robots of T consider a same global direction, while the other robot of T considers the opposite global direction. This implies that the three robots cannot be present on a same node at time t, since n ≥ 4.

Case 2: There is a 2-short-lived tower T at time t -1. For the three robots to form T at time t, they must be edge-activated at time t -1. By definition of a 2-short-lived tower, the two robots of T consider two opposed global directions during the Move phase of time t -1.

Since the robots can cross at most one edge at each round, it is not possible for the three robots to be on a same node at time t, which leads to a contradiction with the fact that T is formed at time t.

Case 3: There are 3 isolated robots at time t -1. For the three robots to form T at time t, they must be edge-activated at time t -1. The robots can cross at most one edge at each round. Each node has at most 2 adjacent edges present in G. Moreover each robot considers at each instant time a direction. Therefore it is not possible for the three robots to be on a same node at time t, which leads to a contradiction with the fact that T is formed at time t.

Lemma 4.9. Every execution starting from a configuration without a 3-long-lived tower cannot reach a configuration with a 3-long-lived tower.

Proof. Assume that E starts from a configuration which does not contain a 3-long-lived tower. By contradiction, let γ be the first configuration of E containing a 3-long-lived tower T = (S, [t s , t e ]). Let t act ≥ t s be the first time after time t s where the 3 robots of T are edge-activated. By definition of a long-lived tower, t act exists. Lemma 4.8 implies that the configuration at time t s -1 contains a 2-long-lived tower. Hence, since γ contains the first 3-long-lived tower of E, at time t s a 2-long-lived tower and a robot meet to form T . The meeting between these two entities can happen either because both of them move in opposed global directions during the Move phase of time t s -1, or because, during the Move phase of time t s -1, the two entities consider the same global direction but one of the entity cannot move (an edge is missing in its direction). In both cases; thanks to the update of the variables HasM ovedP reviousEdgeActivation and N umberRobotsP reviousEdgeActivation at time t s -1; during the Move phase of time t act the two entities consider opposed global directions. Hence, the two entities separate during the Move phase of time t act , therefore there is a contradiction with the fact that T is a 3-long-live tower. Lemma 4.10. Let γ be a configuration such that all but one robots consider the same global direction. Then starting from γ, no execution without long-lived tower can reach a configuration where all robots consider the same global direction.

Proof. Assume that E does not contain long-lived tower and starts from a configuration where all robots but one consider the same global direction. For the three robots to consider the same global direction at least one robot must change the global direction it considers. While executing SELF-STAB PEF 3, the only way for a robot to change the global direction it considers is to form a tower and to be edge-activated. By Lemma 4.7, there is no tower of 3 robots in E. Therefore, for at least one robot to change the global direction it considers, a 2-short-lived tower must be formed and the robots of this tower must be edge-activated. However, by definition of a 2-short-lived tower, once edge-activated, the two robots composing the 2-short-lived tower consider two opposed global directions. Therefore after the edge-activation, the three robots do not consider the same global direction.

Lemma 4.11. Consider an execution containing no 3-long-lived tower. If a 2-long-lived tower T = (S, [t s , t e ]), where t e is finite, is located at a node u at round t e , then the robot that does not belong to S cannot be located at node u during the Look phase of round t e . Moreover, during the Look phase of round t e + 1, one robot of S located at u considers a global direction opposite to the one considered by the other robot of S (which is no longer on u).

Proof. Assume that E does not contain 3-long-lived tower. Assume that r 1 and r 2 are involved in a 2-long-lived tower T = (S, [t s , t e ]).

After the Compute phase of time t e , r 1 and r 2 consider two opposed global directions, otherwise there is a contradiction with the fact that T is broken at time t e . Directions of robots can be modified only during Compute phases of rounds, therefore during the Look phase of time t e + 1, the robots of T still consider two opposed global directions.

Let t act ∈ [t s , t e [ be the first time after time t s where the robots of T are edge-activated. By definition of a 2-long-lived tower t act exists. By Lemma 4.5, from the Look phase of time t act + 1 to the Look phase of time t e included, r 1 and r 2 have the same values of predicates W eAreStuck-InT heSameDirection() and IW asStuckOnM yN odeAndN owW eAreM oreRobots(). Therefore, while executing SELF-STAB PEF 3, the only way for r 1 and r 2 to consider two opposed global directions during the Move phase of time t e is to execute the function GiveDirection and hence to have their predicates W eAreStuckInT heSameDirection() true. Therefore, at time t e the condition ¬ExistsEdgeOnCurrentDirection() ∧ ExistsEdgeOnOppositeDirection() is true. Hence, since during the Move phase of time t e , r 1 and r 2 consider two opposed global directions, during the Look phase of time t e + 1, one of the robot of T is still on node u, while the other robot of T is on an adjacent node of u. Now assume, by contradiction that r 3 is on node u during the Look phase of time t e . Let t last be the last time in [t s , t e [, where the robots of T are edge-activated. By definition of a 2-long-lived tower t last exists. There is no 3-long-lived tower, hence if r 3 is on node u at time t e , it forms a 3-short-lived tower with the robots of T at time t last + 1.

Note that at time t last , r 3 cannot be located on the same node as the robots of T , otherwise since n ≥ 4 the three robots cannot form a 3-short-lived tower at time t last + 1. This implies that at time t last the function Update, updates the variables N umberRobotsP reviousEdgeActivation of the robots of T to 2. Since the variables are updated only during the Compute phases of times where the robots are edge-activated, during the Look phase of time t e , the robots of T have their variables N umberRobotsP reviousEdgeActivation still equal to 2. Since r 3 is on node u during the Look phase of time t e , the predicates N umberOf RobotsOnN ode() of the robots of T are not equal to their variables N umberRobotsP reviousEdgeActivation. Therefore the robots of T cannot execute the function GiveDirection at time t e , and hence are not able to separate them, which leads to a contradiction with the fact that T is broken at time t e . Lemma 4.12. Consider an execution E without any 3-long-lived tower. If a 2-long-lived tower T is formed at a time t s , then during the Look phase of time t s -1, a tower T of 2 robots involving only one robot of T is present. Moreover, during the Move phase of time t s -1, the robot of T involved in T does not move while the other robot of T moves.

Proof. Consider an execution E without any 3-long-lived tower. Assume that at time t s a 2-longlived tower T = (S, [t s , t e ]) is formed.

First note that if there exists a tower T of 2 robots at time t s -1, such that only one robot of T is involved in T and such that this robot does not move during the Move phase of time t s -1, then it is possible for T to be formed. Now we prove that T can be formed at time t s only in this situation.

Assume, by contradiction, that there is no tower of 2 robots during the Look phase of time t s -1. This implies that, at time t s -1 either the three robots are involved in a 3-short-lived tower T 3 (case 1) or the three robots are isolated (case 2).

Case 1: Call t, the time of the formation of T 3 . By Lemma 4.8, at time t-1, there is a 2-long-lived tower T " = (S", θ") in E such that t ∈ θ". Call r the robot that does not belong to T ". Note that S" = S, otherwise there is a contradiction with the fact that T starts at time t s . This implies that T is composed of one robot of T " and of r. However by lemma 4.11, we know that as long as r is on a same node as the robots of T " then T " cannot be broken. This implies that the three robots form a 3-long-lived tower, which leads to a contradiction with the fact that there is no 3-long-lived tower in E. Hence this case cannot happen.

Case 2: At time t s -1 the robots of T must be edge-activated, otherwise there is a contradiction with the fact that T starts at time t s .

Since there is no long-lived tower at time t s -1 then by Lemma 4.8, at time t s it is not possible to have a tower of 3 robots. Then since at time t s , T is formed, it exists at time t s a tower of 2 robots. For two robots to form a tower at time t s , during the Move phase of time t s -1, they either both move while considering two opposed global directions or they consider the same global direction but one of the robot cannot move (an edge is missing in its direction). In both cases, thanks to the update of their variables N umberRobotsP reviousEdgeActivation and HasM ovedP reviousEdgeActivation during the Compute phase of time t s -1, during the Move phase of the first time greater or equal to t s where these two robots are edge-activated, they consider opposed global directions and separate them. Therefore there is a contradiction with the fact that T is a 2-long-lived tower starting at time t s .

Therefore there exists a tower of 2 robots T during the Look phase of time t s -1. Now assume, by contradiction that the two robots of T are involved in T . If T is a 2-long-lived tower then during the Move phase of time t s -1 the two robots of T are edge-activated and consider two opposed global directions, otherwise there is a contradiction with the fact that T starts at time t s . If T is a 2-short-lived tower then during the Move phase of time t s -1 the two robots of T are edge-activated (otherwise T cannot be a 2-long-lived tower), and they consider two opposite global directions (by definition of a 2-short-lived tower).

A robot can cross only one edge at each instant time. Since n ≥ 4 whatever the situation (only one of the robots of T moves or both of the robots of T move during the Move phase of time t s -1) the two robots of T cannot be again on a same node at time t s . In conclusion, only one robot of T is involved in T .

Finally, assume by contradiction, that during the Move phase of time t s -1, either both the robots of T move (in this case, during the Move phase of time t s -1 the two robots consider two opposed global directions otherwise they cannot meet to form T ) or only the robot of T involved in T moves while the other robot of T does not move (in this case, during the Move phase of time t s -1 the two robots consider the same global direction otherwise they cannot meet to form T ). In both cases, thanks to the update of the variables HasM ovedP reviousEdgeActivation and N umberRobotsP reviousEdgeActivation during the Compute phase of time t s -1, during the Move phase of the first time after time t s where the robots of T are edge-activated, they consider two opposed global directions. Therefore there is a contradiction with the fact that T is a 2-long-lived tower starting at time t s .

The next two lemmas show that the whole ring is visited between two consecutive 2-long-lived towers if these two towers satisfy some properties. Lemma 4.13. Consider an execution E without any 3-long-lived tower but containing a 2-long-lived tower T = (S, [t s , t e ]). If there exists another 2-long-lived tower T = (S , [t s , t e ]), with t s > t e + 1 and such that T is the first 2-long-lived tower after T in E, then all the nodes of G have been visited by at least one robot between time t e and time t s -1.

Proof. Consider an execution E without any 3-long-lived tower but containing a 2-long-lived tower T = (S, [t s , t e ]). Assume that there exists another 2-long-lived tower T = (S , [t s , t e ]), with t s > t e + 1 and such that T is the first 2-long-lived tower after T in E.

Since by assumption there is no long-lived tower between the Look phase of time t e + 1 and the Look phase of time t s -1 included, then by Lemma 4.7, from the Look phase of time t e + 1 to the Look phase of time t s -1 included, if some robots meet they only form 2-short-lived towers. Therefore, by Lemma 4.12, at time t s -1 there exists a 2-short-lived tower T short .

To form T , by Lemma 4.12, the configuration C reached is such that T short and the robot of T not involved in T short are on two adjacent nodes, the adjacent edge to the location of T short in the global direction d is missing at time t s -1, and the two robots of T are edge-activated and consider the global direction d during the Move phase of time t s -1. During the Move phase of time t e the configuration C is such that the two robots of T are on a same node considering two opposed global direction. Moreover, from the Look phase of time t e + 1 to the Look phase of time t s -1 included, if two robots meet they separate once they are edge-activated considering two opposed global directions. Besides, while executing SELF-STAB PEF 3, a robot does not change the global direction it considers if it is isolated. All this implies that to reach C from C all the nodes of G have been visited by at least one robot between time t e and time t s -1.

Lemma 4.14. Consider an execution E without any 3-long-lived tower, and let T i = (S i , [t s i , t e i ]) be the i th 2-long-lived tower of E, with i ≥ 2. If T i+1 = (S i+1 , [t s i+1 , t e i+1 ]) exists and satisfies t s i+1 = t e i + 1, then all the nodes of G have been visited by at least one robot between time t s i -1 and time t s i+1 -1.

Proof. Consider an execution E without any 3-long-lived tower but containing a 2-long-lived tower T i = (S i , [t s i , t e i ]), with i ≥ 2. Assume that there exists another 2-long-lived tower T i+1 = (S i+1 , [t s i+1 , t e i+1 ]), with t s i+1 = t e i + 1. By Lemma 4.12, to form T i+1 , a tower of 2 robots involving only one robot of T i+1 must be present at time t s i+1 -1. Moreover T i is a tower of 2 robots which is present in G from time t s i to time t s i+1 -1. Therefore S i+1 = S i .

To form T i , by Lemma 4.12, the configuration C reached at time t s i -1 is such that there is a tower T of 2 robots involving only one robot of T i and the other robot of T i which are on two adjacent nodes Similarly, by Lemma 4.12, and since t s i+1 = t e i + 1, to form T i+1 , the configuration C reached at time t s i+1 -1 is such that T i and the robot of T i+1 not involved in T i are on two adjacent nodes, the adjacent edge to the location of T i in the global direction d is missing at time t s i+1 -1, and the two robots of T i+1 are edge-activated and consider the global direction d during the Move phase of time t s i+1 -1. Moreover, since there is no 3-long-lived tower in E, from the Look phase of time t s i to the Look phase of time t s i+1 -1 included, if T i meets the other robot of the system, they form a 3-short-lived tower and hence they separate once they are edge-activated considering two opposed global directions. Besides, while executing SELF-STAB PEF 3, a robot does not change the global direction it considers if it is isolated. All this implies that to reach C from C all the nodes of G have been visited by at least one robot between time t s i -1 and time t s i+1 -1.

Correctness Proof

Upon establishing all the above properties of towers, we are now ready to state the main lemmas of our proof. Each of these three lemmas below shows that after time t max our algorithm performs the perpetual exploration in a self-stabilizing way for a specific subclass of connected-over-time rings. Lemma 4.15. SELF-STAB PEF 3 is a perpetual exploration algorithm for the class of static rings of arbitrary size using three robots.

Proof. Assume that G is a static ring. While executing SELF-STAB PEF 3, a robot considers a direction at each round. Moreover, a robot does not change the global direction it considers if its variable HasM ovedP reviousEdgeActivation is true. The variables of a robot are updated during Compute phases of times where it is edge-activated. Since G is static, this implies that in each round all the robots are edge-activated and are able to move whatever the direction they consider. So, after t max their variables HasM ovedP reviousEdgeActivation are always true. Hence, the robots never change their directions.

As (i) the robots have a stable direction, (ii) they always consider respectively the same global direction, and (iii) there always exists an adjacent edge to their current locations in the global direction they consider, the robots move infinitely often in the same global direction. Moreover, as G has a finite size, this implies that all the robots visit infinitely often all the nodes of G. Lemma 4.16. SELF-STAB PEF 3 is a perpetual exploration algorithm for the class of edgerecurrent but non static rings of arbitrary size using three robots.

Proof. Assume that G is an edge-recurrent but non static ring. Let us study the following cases.

Case 1: There exists at least one 3-long-lived tower in E.

Case 1.1: One of the 3-long-lived towers of E has an infinite duration.

Denote by T = (S, [t s , +∞[) the 3-long-lived tower of E that has an infinite duration. Call t ≥ t s the first time after time t s where the robots of T are edge-activated. The variables of a robot are updated during Compute phases of times where it is edgeactivated. Therefore, since there are three robots in the system, from time t act + 1, the condition "N umberOf RobotsOnN ode() > N umberRobotsP reviousEdgeActivation" is false for the three robots of T . Therefore from time t act + 1 the predicate IW asStuck-OnM yN odeAndN owW eAreM oreRobots() of each robot of T is false. By Corollary 4.1, eventually, the predicates W eAreStuckInT heSameDirection() of the robots of T are always false, otherwise T is broken in finite time, which leads to a contradiction. Since eventually the predicates IW asStuckOnM yN odeAndN owW eAreM oreRobots() and W eAreStuckInT heSameDirection() of the robots of T are always false, then eventually they consider always the same global direction. G is edge-recurrent, therefore there exists infinitely often an adjacent edge to the location of T in the global direction considered by the robots of T , then the robots are able to move infinitely often in the same global direction. Moreover, as G has a finite size, all the robots visit infinitely often all the nodes of G.

Case 1.2: Any 3-long-lived tower of E has a finite duration. By Lemma 4.9, once a 3-long-lived tower is broken, it is impossible to have another 3-long-lived tower in E. Then, E admits an infinite suffix that matches either case 2 or 3.

Case 2: There exists at least one 2-long-lived tower in E.

Case 2.1: There exists a finite number of 2-long-lived towers in E.

Let T = (S , [t s , t e ]) be the last 2-long-lived tower of E.

There is no 3-long-lived tower in E at time t s (otherwise Case 1 is considered), hence by Lemma 4.9 there is no 3-long-lived tower in E. Moreover, if T has a finite duration, then E admits an infinite suffix with no long-lived tower, hence matching case 3. Otherwise, (i.e., T has an infinite duration), as in Case 1.1, the robots of T eventually have their predicates W eAreStuckInT heSameDirection() always false, otherwise, T is broken in finite time. Let t f alse be the time from which the robots of T have their predicates W eAreStuckInT heSameDirection() always false. After time t f alse , the only case when the robots of T change the global direction they consider, is when they meet the third robot of the system.

Case 2.1.1: The robots of T meet the third robot finitely often.

After the time when the last tower of 3 robots is broken, the robots of T have their predicates IW asStuckOnM yN odeAndN owW eAreM oreRobots() always false. Let t break be the time when the last tower of 3 robots if broken. From time t = max{t break , t f alse } + 1 the robots of T have their predicates IW asStuckOnM y-N odeAndN owW eAreM oreRobots() and W eAreStuckInT heSameDirection() always false, therefore they always consider the same global direction. Since G is edge-recurrent, there is infinitely often an adjacent edge to the location of T in the direction considered by the robots of T . This implies that they are able to move infinitely often in the same global direction. Moreover, as G has a finite size, this implies that all the robots visit infinitely often all the nodes of G.

Case 2.1.2: The robots of T meet the third robot infinitely often.

Consider the execution after time t f alse . The robot not involved in T does not change its direction while it is isolated. Similarly, the robots of T maintain their directions until they meet the third robot. Moreover, when the robots of T meet the third robot of the system, they form a 3-short-lived tower. Therefore once they are edge-activated, they separate them considering opposed global directions. Then, we can deduce that all the nodes of G are visited between two consecutive meetings of T and the third robot. As T and the third robot infinitely often meet, all the nodes of G are infinitely often visited.

Case 2.2:

There exist an infinite number of 2-long-lived towers in E. By Lemmas 4.13 and 4.14, we know that between two consecutive 2-long-lived towers (from the second one), all the nodes of G are visited. As there is an infinite number of 2-long-lived towers, the nodes of G are infinitely often visited.

Case 3: There exist no long-lived tower in E.

Then, we know, by Lemma 4.7, that E contains only configurations with either three isolated robots or one 2-short-lived tower and one isolated robot.

We want to prove the following property. If during the Look phase of time t, a robot r is located on a node u considering the global direction gd, then there exists a time t ≥ t such that, during the Look phase of time t , a robot is located on the node v adjacent to u in the global direction gd and considers the global direction gd.

Let t" ≥ t be the smallest time after time t where the adjacent edge of u in the global direction gd is present in G. As all the edges of G are infinitely often present, t" exists.

(i) If r crosses the adjacent edge of u in the global direction gd during the Move phase of time t", then the property is verified.

(ii) If r does not cross the adjacent edge of u in the global direction gd during the Move phase of time t", this implies that r changes the global direction it considers during the Look phase of a time t. This prove the property. By applying recurrently this property to any robot, we prove that all the nodes are infinitely often visited.

Thus, we obtain the desired result in every cases.

Lemma 4.17. SELF-STAB PEF 3 is a perpetual exploration algorithm for the class of connectedover-time but not edge-recurrent rings of arbitrary size using three robots.

Proof. Consider that G is a connected-over-time but not edge-recurrent ring. This implies that there exists exactly one eventual missing edge e in G. Denote by E 1 the maximal suffix of E in which the eventual missing edge never appears. Let t missing the time after which e never appears again. Let us study the following cases.

Case 1: There exists at least one 3-long-lived tower in E 1 .

According to Lemma 4.6, this 3-long-liver tower is broken in finite time. Moreover, once this tower is broken, according to Lemma 4.9, it is impossible to have a configuration containing a 3-long-lived tower. Then, E 1 admits an infinite suffix that matches either case 2 or 3.

Case 2: There exists at least one 2-long-lived tower in E 1 .

Case 2.1: There exists a finite number of 2-long-lived towers in E 1 .

According to Lemma 4.6, the last 2-long-lived tower is broken in finite time. Since by Lemma 4.9, it cannot exists 3-long-lived tower in E 1 , then E 1 admits an infinite suffix with no long-lived tower hence matching Case 3.

Case 2.2:

There exist an infinite number of 2-long-lived towers in E 1 . By Lemmas 4.13 and 4.14, we know that between two consecutive 2-long-lived towers (from the second one), all the nodes of G are visited. As there is an infinite number of 2-long-lived towers, all the nodes of G are infinitely often visited.

Case 3: There exist no long-lived tower in E 1 .

By Lemma 4.7, all configurations in E 1 contain either three isolated robots or one 2-short-lived tower and one isolated robot.

(1) We want to prove the following property. If during the Look phase of a time t in E 1 , a robot considers a global direction gd and is located on a node at a distance d = 0 in G (G is the footprint of G) from the extremity of e in the global direction gd, then it exists a time t ≥ t such that, during the Look phase of time t , a robot is on a node at distance d -1 in G from the extremity of e in the global direction gd and considers the global direction gd. Let v be the adjacent node of u in the global direction gd.

Let t" ≥ t be the smallest time after time t where the adjacent edge of u in the global direction gd is present in G. As all the edges of G except e are infinitely often present and as u is at a distance d = 0 in G from the extremity of e in the global direction gd, then the adjacent edge of u in the global direction gd is infinitely often present in G. Hence, t" exists.

(i) If r crosses the adjacent edge of u in the global direction gd during the Move phase of time t", then the property is verified.

(ii) If r does not cross the adjacent edge of u in the global direction gd during the Move phase of time t", this implies that r changes the global direction it considers during the Look phase of a time t. Assume that at time t reachExtremities , r" is on node u and considers the global direction gd. Then by applying recurrently the property (1) we can prove that, in finite time, all the nodes between the current node of r" at time t reachExtremities and v in the global direction gd are visited and that r" reaches v. Call t act ≥ t reachExtremities , the first time after time t reachExtremities where there are two robots on node v that are edge-activated. At time t act , the robot that is on node v and pointing to e at time t reachExtremities changes the global direction it considers (hence considers gd) by construction of SELF-STAB PEF 3 and since the tower formed is a 2-short-lived tower.

We can then repeat this reasoning (with v and v alternatively in the role of u and with v and v alternatively in the role of v) and prove that all nodes are infinitely often visited. Thus, we obtain the desired result in every cases.

To conclude the proof, first note that even if the robots can start in a non coherent state, it exists a time t max from which all the robots of the system are in a coherent state (by Lemma 4.1). Then it is sufficient to observe that a connected-over-time ring is by definition either static, edge-recurrent but non static, or connected-over-time but not edge-recurrent. As we prove the correctness of our algorithm from the time the robots are in a coherent state in these three cases in Lemmas 4.15, 4.16, and 4.17 respectively, we can claim the following final result. Theorem 4.1. SELF-STAB PEF 3 is a self-stabilizing perpetual exploration algorithm for the class of connected-over-time rings of arbitrary size (greater or equal to four) using three robots with distinct identifiers.

Sufficiency of Two Robots for n = 3

In this section, we present SELF-STAB PEF 2, a self-stabilizing algorithm solving deterministically the perpetual exploration problem on connected-over-time rings of size equal to 3, using two robots possessing distinct identifiers.

To present this algorithm we add a new predicate, named IAmStuckAloneOnM yN ode() defined as follows. IAmStuckAloneOnM yN ode() ≡ (N umberOf RobotsOnN ode() = 1) ∧¬ExistsEdgeOnCurrentDirection() ∧ExistsEdgeOnOppositeDirection() The pseudo-code of SELF-STAB PEF 2 is given in Algorithm 4.

Proof of correctness. We now prove the correctness of this algorithm.

First, note that Lemmas 4.1, 4.2, 4.3 are also true for SELF-STAB PEF 2.

To show the correctness of SELF-STAB PEF 2, we need to introduce some lemmas. We consider that the two robots executing SELF-STAB PEF 2 are r 1 and r 2 . Let t 1 , and t 2 be respectively the time at which the robot r 1 and r 2 are in a coherent state. Let t max = max{t 1 , t 2 }. From Lemma 4.1, the two robots are in a coherent state from t max . In the remaining of the proof, we focus on the suffix of the execution after t max . The other notations correspond to the ones introduced in Section 4.

Lemma 5.1. Every execution starting from a configuration without a 2-long-lived tower cannot reach a configuration with a 2-long-lived tower.

Proof. Assume that E starts from a configuration which does not contain a 2-long-lived tower. By contradiction, let C be the first configuration of E containing a 2-long-lived tower T = (S, [t s , t e ]).

Let t act ≥ t s be the first time after time t s where the 2 robots of T are edge-activated. By definition of a long-lived tower, t act exists.

For a 2-long-lived tower to be formed at time t s , r 1 and r 2 must meet at time t s . While executing SELF-STAB PEF 2, the two robots can meet at time t s only because they are moving considering opposed global directions during the Move phase of time t s -1. Therefore, since the variables of a robot are updated only during Compute phases of time where it is edge-activated, during the Look phase of time t act , the predicates W eAreStuckInT heSameDirection() of the two robots are false (since their variables HasM ovedP reviousEdgeActivation are true). Moreover, during the Look phase of time t act the predicates IAmStuckAloneOnM yN ode() of the two robots are false (since their predicates N umberOf RobotsOnN ode() is not equal to 1). Hence during the Move phase of time t act the two robots still consider two opposed global directions. Therefore T is broken at time t act , which leads to a contradiction with the fact that T is a 2-long-lived tower. This proves the lemma.

Let t act1 (resp. t act2 ) be the first time in the execution at which the robot r 1 (resp. r 2 ) is edge-activated. By definition, we have t 1 = t act1 + 1 and t 2 = t act2 + 1. By Lemma 5.1, if there exists a 2-long-lived tower in E, then this 2-long-lived tower is present in the execution from time t 0 = 0. In this case t 1 = t 2 = t max and at time t max -1 the robots are edge-activated for the first time of the execution.

Lemma 5.2. The robots of a long-lived tower T = (S, [t s , t e ]) consider a same global direction at each time between the Look phase of round t max and the Look phase of round t e included.

Proof. Consider a long-lived tower T = (S, [t s , t e ]). We know that t s = t 0 = 0, that t 1 = t 2 = t max and that at time t max -1 the robots are edge-activated for the first time of the execution. During the Move phase of time t max -1, the two robots consider the same global direction, otherwise there is a contradiction with the fact that T is a 2-long-lived tower.

When executing SELF-STAB PEF 2, a robot can change the global direction it considers only when it is edge-activated. Besides, during the Look phase of a time t a robot considers the same global direction than the one it considers during the Move phase of time t -1.

Consider a time t ∈ [t max , t e [. If at time t the robots of S are not edge-activated, then during the Move phase of time t the robots of S do not change the global direction they consider.

If at time t the robots of S are edge-activated, then during the Move phase of time t, since t = t e , the robots of S consider the same global direction, otherwise there is a contradiction with the fact that T is a long-lived tower from time t s to time t e .

Since at time t max -1 the robots of S consider the same global direction using the two previous arguments by recurrence on each time t ∈ [t max , t e [ and the fact that robots change the global directions they consider only during Compute phases, we can conclude that the robots of S consider a same global direction from the Look phase of time t max to the Look phase of time t e included. Lemma 5.3. For any long-lived tower T = (S, [t s , t e ]), and any t ≤ t e , such that the robots of S have been edge-activated twice between t s included and t not included, we have W eAreStuckIn-T heSameDirection()(r 1 , t) = W eAreStuckInT heSameDirection()(r 2 , t).

Proof. Consider a long-lived tower T = (S, [t s , t e ]). We know that t s = t 0 = 0, that t 1 = t 2 = t max and that at time t max -1 the robots are edge-activated for the first time of the execution. Assume that between t s included and t e not included, the robots of T are edge-activated two or more times.

By definition of a long-lived tower and by lemma 5.2, from the Look phase of time t max to the Look phase of time t e included, all the robots of S are on a same node and consider a same global direction. Therefore the values of their respective predicates N umberOf RobotsOnN ode(), Exists-EdgeOnCurrentDirection() and ExistsEdgeOnOppositeDirection() are identical from the Look phase of time t max to the Look phase of time t e included.

Let t act ≥ t max be the first time after t max such that the robots of T are edge-activated. By assumption, t act exists. When executing SELF-STAB PEF 2, a robot updates its variables Has-M ovedP reviousEdgeActivation and N umberRobotsP reviousEdgeActivation respectively with the values of its predicates ExistsEdgeOnCurrentDirection() and N umberOf RobotsOnN ode(), only during Compute phases of times when it is edge-activated. Therefore, from the Look phase of time t act + 1 to the Look phase of time t e included, the robots of S have the same values for their variables HasM ovedP reviousEdgeActivation and N umberRobotsP reviousEdgeActivation.

The predicate W eAreStuckInT heSameDirection() depends only on the values of the variables HasM ovedP reviousEdgeActivation, N umberRobotsP reviousEdgeActivation and on the values of the predicates N umberOf RobotsOnN ode(), ExistsEdgeOnCurrentDirection(), and Exists-EdgeOnOppositeDirection(). As seen previously, all these values are identical for all the robots of S from the Look phase of time t act + 1 until the Look phase of time t e included. This prove the lemma.

From the Lemmas 5.3, 4.2 and 4.3, by noticing that the robots of a long-lived tower T cannot have their predicates IAmStuckAloneOnM yN ode() true as long as their are involved in T , we can again obtain the corollary 4.1 (the proof is not exactly the same since the predicate IW asStuckOn-M yN odeAndN owW eAreM oreRobots() does not exist in SELF-STAB PEF 2, however the proof is very similar, therefore not repeated in this section).

Theorem 5.1. SELF-STAB PEF 2 is a deterministic self-stabilizing perpetual exploration algorithm for the class of connected-over-time rings of size equals to 3 using 2 fully synchronous robots possessing distinct identifiers.

Proof. Consider that G is a connected-over-time ring of size 3. First note that even if the robots can start in a non coherent state, by Lemma 4.1, it exists a time t max from which all the robots are in a coherent state. Let us study the following cases occurring when the robots are in a coherent state.

Case 1 : There exists at least one 2-long-lived tower in E. By Lemma 5.1, once a 2-long-lived tower is broken, it is not possible to have again a 2-longlived tower in E. Therefore there exists only one 2-long-lived tower in E.

If the 2-long-lived tower of E has a finite duration, then by Lemma 5.1, E admits an infinite suffix with no long-lived tower hence matching Case 2.

If the 2-long-lived tower T of E has an infinite duration, the robots of T eventually have their predicates W eAreStuckInT heSameDirection() always false, otherwise, by Corollary 4.1 T is broken in finite time, which leads to a contradiction. Let t f alse be the time from which the robots of T have their predicates W eAreStuckInT heSameDirection() always false. After time t f alse the robots of T always consider the same global direction (since their predicates IAmStuckAloneOnM yN ode() cannot be true). Moreover, after time t f alse there exists infinitely often an adjacent edge to the location of T in the global direction considered by the robots of T , otherwise there exists a time t f alse when the predicates W eAreStuckIn-T heSameDirection() of the robots of T are true, which is a contradiction. Hence after time t f alse the robots of T are infinitely often able to move in the same global direction. Since G has a finite size, all the robots visit infinitely often all the nodes of G.

Case 2: There exist no long-lived tower in E.

If there is no long-lived tower, this implies that if a tower is formed, then it is a 2-short-lived tower. By the connected-over-time assumption, each node has at least one adjacent edge infinitely often present. This implies that any short-lived tower is broken in finite time. Two cases are now possible.

Case 2.1: There exists infinitely often a 2-short-lived tower in the execution.

Note that, if a tower is formed at a time t, then the three nodes have been visited between time t -1 and time t. Then, the three nodes are infinitely often visited by a robot in the case where there exists infinitely often a 2-short-lived tower in the execution.

Case 2.2: There exists a time t isolated after which the robots are always isolated. By contradiction, assume that there exists a time t such that a node u is never visited after t . This implies that, after time max{t isolated , t }, either the robots are always switching their position or they stay on their respective nodes. In the first case, during the Look phase of each time greater than max{t isolated , t }, the respective variables dir of the two robots contain the direction leading to u (since each robot previously moves in this direction). As at least one of the adjacent edges of u is infinitely often present, a robot crosses it in a finite time, that is contradictory with the fact that u is not visited after t . The second case implies that both adjacent edges to the location of both robots are always absent after time t isolated (since an isolated robot moves as soon as it is possible, by definition of the predicate IAmStuckAloneOnM yN ode()), that is contradictory with the connected-over-time assumption.

Thus, we obtain the desired result in every cases.

Conclusion

In this paper, we addressed the open question: "What is the minimal size of a swarm of selfstabilizing robots to perform perpetual exploration of highly dynamic graphs?". We give a first answer to this question by exhibiting the necessary and sufficient numbers of such robots to perpetually explore any connected-over-time ring, i.e., any dynamic ring with very weak assumption on connectivity: every node is infinitely often reachable from any another one without any recurrence, periodicity, nor stability assumption. More precisely, we showed that necessary and sufficient numbers of robots proved in [START_REF] Bournat | Computability of perpetual exploration in highly dynamic rings[END_REF] in a fault-free setting (2 robots for rings of size 3 and 3 robots for rings of size greater than 4) still hold in the self-stabilizing setting at the price of the loss of anonymity of robots.

In addition to the above contributions, our results overcome the robot networks state-of-the-art in a couple of ways. First, at the exception of the algorithms from [START_REF] Bournat | Computability of perpetual exploration in highly dynamic rings[END_REF], it is the only algorithms dealing with highly dynamic graphs. All previous solutions made some assumptions on periodicity or on all-time connectivity of the graph. Second, it is the first self-stabilizing algorithm for the problem of exploration, either for static or for dynamic graphs.

This work opens an interesting field of research with numerous open questions. First, we should investigate the necessity of every assumption made in this paper. For example, we assumed that robots are synchronous. Is this problem solvable with asynchronous robots? Second, it would be worthwhile to explore other problems in this rather complicated environment, e.g., gathering, leader election, etc.. It may also be interesting to consider other classes of dynamic graphs and other classes of faults, e.g., crashes of robots, Byzantine failures, etc..

Figure 1 :

 1 Figure 1: Construction of G in proof of Lemma 3.1.

  and such that U [|x|+k] = 0, U [|x|+k+1] = 1 and U [|x|+k+2] = 0. By ( * ) and since U = x.X = x.ũ ω , k exists. By ( * ) and by construction of U , we know that U [|x| + k + 3 . . . |x| + k + |u| + 2] is equal to u and U [|x| + k + 3 . . . |x| + k + |u| -1] is either equal to 00 or to 11.Π * * ), we have V [|y| + k] = 0, V [|y| + k + 1] = 1 and V [|y| + k + 2] = 0. By ( * * ) and by construction of V , we know that V [|y| + k + 3 . . . |y| + k + |v| + 2] is equal to v and V [|y| + k + 3 . . . |y| + k + |v| -1] is either equal to 00 or to 11.Π

Case 1 :

 1 |u| = |v|. If |u| = |v|, then by ( * * * ) we have U [|x|+k+3 . . . |x|+k+|u|+2] = V [|y|+k+3 . . . |y|+k+|v|+2]. This implies that u = v, which leads to a contradiction with the fact that u and v are distinct. Case 2: |u| = |v|. Without lost of generality assume that |u| < |v|. We have U [|x| + k + |u|] = 0, U [|x| + k + |u| + 1] = 1 and U [|x| + k + |u| + 2] = 0. Therefore by ( * * * ) we have V [|y| + k + |u|] = 0, V [|y| + k + |u| + 1] = 1 and V [|y| + k + |u| + 2] = 0. Note that |u| = 2w + 3 with w ∈ N * . Similarly |v| = 2z + 3, with z ∈ N * , and z > x since |u|

  where i is odd and such that 1 ≤ i ≤ 2z. Hence by ( * * ), necessarilyV [|y| + k + |u|] = V [|y| + k + |u| + 1], which leads to a contradiction with the fact that V [|y| + k + |u|] = 0 and V [|y| + k + |u| + 1] = 1.Let us introduce the notation w which given a word w is defined such that w = i∈{0,...,|w|-1} w[i]where if w[i] = 1 then w[i] = 0, and if w[i] = 0 then w[i] = 1.Proof. Consider two distinct transformed identifiers u and v such that u = v.By definition, the transformed identifier u is either equal to 00.010 or to 11.Π with α(u) a function giving the number of blocks (Πβ(u,d) 1 00.Π γ(u,d)111) contained in u, β(u, d) a function giving the number of pair of bits 00 contained in the d th block of u, and γ(u, d) a function giving the number of pair of bits 11 contained in the d th block of u.Similarly, by definition v is either equal to 00.010 or to 11.Π w = v. This implies that |w| = |v| and w is either equal to 11.101 or to 00.Π ). Note that u and w are distinct. Indeed, if |u| = |v| then, w and u are distinct since |w| = |v|. If |u| = |v| then, since the suffix of size 3 of u is the word 010, and the suffix of size 3 of w is the word 101, then u and w are distinct.

  and such that U [|x|+k] = 0, U [|x|+k+1] = 1 and U [|x|+k+2] = 0. By ( * ) and since U = x.X = x.ũ ω , k exists. By ( * ) and by construction of U , we know that U [|x| + k + 3 . . . |x| + k + |u| + 2] is equal to u. By ( * * * ), we have W [|y| + k] = 0, W [|y| + k + 1] = 1 and W [|y| + k + 2] = 0. By ( * * ) and by construction of W , we know that either W [|y| + k + 4 . . . |y| + k + |w| + 3] = w (in the case where W [|y| + k + 1] = w[|w| -2]) or W [|y| + k + 2 . . . |y| + k + |w| + 1] = w (in the case where W [|y| + k + 1] = w[|w|]).Case 1: W[|y| + k + 4 . . . |y| + k + |w| + 3] = w. In this case W [|y| + k + 3] = 1, then necessarily by ( * * * ) U [|x| + k + 3] = 1. By ( * ), and since U [|x| + k + 3 . . . |x| + k + |u| + 2] = u, this implies that U [|x| + k + 4] = 1. Therefore by ( * * * ), necessarily W [|y| + k + 4] = 1. Since W [|y| + k + 4 . . . |y| + k + |w| + 3] = w, and by ( * * ), this implies that w = 11.101, otherwise W [|y| + k + 4] = 0, which leads to a contradiction with the fact that U [|x| + k + 4] = 1. This implies by ( * * * ), that U [|x|+k +3 . . . |x|+k +8] = 111101. Therefore by ( * ), necessarily U [|x| + k + 9] = 0. However by construction of W , since W [|y| + k + 4 . . . |y| + k + |w| + 3] = w, and since |w| = 5, we have W [|y|+k+9 . . . |y|+k+14] = w. This implies that W [|y|+k+9] = 1 since w = 11.101, which leads to a contradiction with the fact that U [|x| + k + 9] = 0. Case 2: W[|y| + k + 2 . . . |y| + k + |w| + 1] = w. In this case, since W [|y| + k + 2] = 0, this implies by ( * * ) that W [|y| + k + 3] = 0. Therefore by ( * * * ) we have U [|x| + k + 3] = 0. Hence, since U [|x| + k + 3 . . . |x| + k + |u| + 2] = u, then by ( * ), we have u = 00.010, otherwise U [|x| + k + 3] = 1 which leads to a contradiction with the fact that W [|y| + k + 3] = 0. This implies by ( * * * ), that W [|y|+k+2 . . . |x|+k+7] = 000010. Therefore by ( * * ), necessarily W [|x| + k + 8] = 1. However by construction of U , since U [|x| + k + 3 . . . |x| + k + |u| + 2] = u, and since |u| = 5, we have U [|x|+k +8 . . . |y|+k +13] = u which implies that U [|x|+k +8] = 0 since u = 00.010, which leads to a contradiction with the fact that W [|y| + k + 8] = 1.

Corollary 4 . 1 .

 41 Consider a long-lived tower T = (S, θ) with θ = [t s , +∞[. The predicates W e-AreStuckInT heSameDirection() of the robots of S cannot be infinitely often true, otherwise T is broken in finite time.

  While executing SELF-STAB PEF 3, a robot can change the global direction it considers only during Compute phases of times where it is edge-activated and involved in a tower. Let t act ≥ t be the first time after time t such that during the Move phase of time t act , r does not consider the global direction gd. Let r the robot involved in a tower with r at time t act . Since there are only 2-short-lived towers in the execution, the two robots r and r consider two opposed global directions during the Move phase of time t act . Therefore during the Move phase of time t act , r is on node u considering the global direction gd. By applying case (ii) by recurrence, we can say that from the Move phase of time t to the Move phase of time t" there always exists a robot on node u considering the global direction gd. Therefore during the Move phase of time t" a robot moves on node v. Since the robot does not change the global direction they consider during Look phases, during the Look phase of time t" + 1 this robot still considers the global direction gd.

  While executing SELF-STAB PEF 3, a robot can change the global direction it considers only during Compute phases of times where it is edge-activated and involved in a tower. Let t act ≥ t be the first time after time t such that during the Move phase of time t act , r does not consider the global direction gd. Let r the robot involved in a tower with r at time t act . Since there are only 2-short-lived towers in the execution, the two robots r and r consider two opposed global directions during the Move phase of time t act . Therefore during the Move phase of time t act , r is on node u considering the global direction gd. By applying case (ii) by recurrence, we can say that from the Move phase of time t to the Move phase of time t" there always exists a robot on node u considering the global direction gd. Therefore during the Move phase of time t" a robot moves on node v. Since the robot does not change the global direction they consider during Look phases, during the Look phase of time t" + 1 this robot still considers the global direction gd. We now want to prove that there exists a time t reachExtremities in E 1 from which one robot is forever located on each extremity of e pointing to e.First, we want to prove that a robot reaches one of the extremities of e in a finite time after t missing and points to e at this time. If it is not the case at time t missing , then there exists at this time a robot considering a global direction gd and located on a node u at distance d = 0 in G from the extremity of e in the global direction gd. By applying d times the property (1), we prove that, during the Look phase of a time t reach ≥ t missing , a robot (denote it r) reaches the extremity of e in the global direction gd from u (denote it v and let v be the other extremity of e), and that this robot considers the global direction gd during the Look phase of time t reach .Then, we can prove that from time t reach there always exists a robot on node v considering the global direction gd. Indeed, note that no robot can cross e in the global direction gd from time t reach since e is missing from time t missing . Moreover while executing SELF-STAB PEF 3, a robot can change the global direction it considers only during Compute phases of times where it is edge-activated and involved in a tower. Therefore if at a time t change ≥ t missing , r changes the global direction it considers at time t reach this is because it is involved in a tower. Since there are only 2-short-lived towers in the execution, at time t change , r is involved in a tower with a robot r , and r and r consider two opposed global directions during the Move phase of time t change . Therefore during the Move phase of time t change , r is on node v considering the global direction gd. By applying this argument by recurrence, we can say that from time t reach there always exists a robot on node v considering the global direction gd. Now we prove that this is also true for the extremity v of e. If there exists at time t reach a robot on node v considering the global direction gd, or if it exists a robot considering the global direction gd on a node u at distance d = 0 in G from v in the global direction gd, then by using similar arguments than the one used for v, we can prove the property (2). If this is not the case, this implies that at time t reach all the robots consider the global direction gd. Then in finite time (after time t reach ) by the property (1), a robot reaches node v. Since from time t reach there is always a robot on node v, there is a 2-short-lived tower formed. Then by definition of a 2-short-lived tower, there exists a time at which one of the robots of this tower considers the global direction gd while the other considers the global direction gd. Then we can use the same arguments as the one used previously to prove the property (2).(3) It stays to prove that in the Case 3 all the nodes are infinitely often visited. We know that from time t

	Algorithm 4 SELF-STAB PEF 2
	1: if W eAreStuckInT heSameDirection() then
	2:	GiveDirection
	3: end if
	4: if IAmStuckAloneOnM yN ode() then
	5:	OppositeDirection
	6: end if
	7: Update
		This prove the property.
		(2) 29

reachExtremities one robot is forever located on each extremity of e pointing to e. Call r" the robot that is not on node v (resp. v ) and pointing to e at time t reachExtremities .

A preliminary version of this work appears This work has been partially supported by the ANR project ESTATE and was initiated while the second author was visiting professor at UPMC Sorbonne Universités.

The authors want to thank Florence Levé from Université de Picardie-Jules Verne (France

GiveDirection infinitely often). Each time a robot executes the function GiveDirection it reads the next bit (in a round robin way) of the bit read during its previous call to the function GiveDirection. Call j 1 and j 2 the two respective transformed identifiers of two robots forming T such that these two robots possess a different chirality. By the previous observations, to keep forming T , j ω 1 must possess an infinite suffix S such that an infinite suffix of j ω 2 is equal to S. This is equivalent to say that j ω 1 and j ω 2 must possess an infinite common factor. However according to Lemma 4.3 this is not possible. Therefore there exists a time t end at which these two robots consider two identical bits. When the robots call the function GiveDirection, they are edge-activated, therefore at time t end , T is broken.

Hence in both cases the long-lived tower T is broken, which leads to a contradiction with the fact that θ = [t s , +∞[. Lemma 4.6. If there exists an eventual missing edge, then all long-lived towers have a finite duration.

Proof. Consider that there exists an edge e of G which is missing forever from time t missing . Consider the execution from time t missing .

Call u and v the two adjacent nodes of e, such that v is the adjacent node of u in the clockwise direction.

By contradiction assume that there exists a long-lived tower T = (S, θ) such that θ = [t s , +∞[. Exactly 3 robots are executing SELF-STAB PEF 3, so |S| is either equals to 2 or 3. We want to prove that all the robots of T have their predicates W eAreStuckInT heSameDirection() infinitely often true. By contradiction, assume that there exists a robot r i of S, such that it exists a time t i in θ such that for all time t greater or equal to t i its predicate W eAreStuckInT heSameDirection() is false.

Call t act ≥ t s , the first time after time t s where the robots are edge-activated. Since T is a long-lived tower, t act exists. By Lemma 4.5, from time t act + 1 the robots of S possess the same values of predicates W eAreStuckInT heSameDirection(). By assumption of contradiction, from time t f alse = max{t act + 1, t i } the predicates W eAreStuckInT heSameDirection() of all the robots of S are false.

We recall that by definition of a long-lived tower and by Lemma 4.4 all the robots of S are on a same node and consider a same global direction from the Look phase of time t s to the Look phase of time t e included.

Case 1: |S| = 3. From time t s the predicates N umberOf RobotsOnN ode() of the robots of S are equal to 3. When executing SELF-STAB PEF 3, a robot updates its variables N umber-RobotsP reviousEdgeActivation with the value of its predicate N umberOf RobotsOnN ode(), only during Compute phases of times where it is edge-activated. Therefore from time t f alse the robots of S have their variables N umberRobotsP reviousEdgeActivation equal to 3. Hence, from time t f alse their predicates IW asStuckOnM yN odeAndN owW eAreM oreRobots() are false, since the condition N umberOf RobotsOnN ode() > N umberRobotsP reviousEdgeActivation is false.

Since from time t f alse , the predicates W eAreStuckInT heSameDirection() of the robots of S are also false, then from time t f alse the robots of S always consider the same global direction.

Without lost of generality, assume that, from time t f alse , the robots of S consider the clockwise direction. All the edges of G except e are infinitely often present, therefore the robots of S