{'fraction_non_alphanumeric': 0.03478950560644469, 'fraction_numerical': 0.01241038242018009, 'mean_word_length': 3.7975826307543086, 'pattern_counts': {'":': 0, '<': 1, '<?xml version=': 0, '>': 21, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 11, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
RoboCast: Asynchronous Communication in Robot Networks

This paper introduces the \emph{RoboCast} communication abstraction. The RoboCast allows a swarm of non oblivious, anonymous robots that are only endowed with visibility sensors and do not share a common coordinate system, to asynchronously exchange information. We propose a generic framework that covers a large class of asynchronous communication algorithms and show how our framework can be used to implement fundamental building blocks in robot networks such as gathering or stigmergy. In more details, we propose a RoboCast algorithm that allows robots to broadcast their local coordinate systems to each others. Our algorithm is further refined with a local collision avoidance scheme. Then, using the RoboCast primitive, we propose algorithms for deterministic asynchronous gathering and binary information exchange.


Introduction
Existing studies in robots networks focus on characterizing the computational power of these systems when robots are endowed with visibility sensors and communicate using only their movements without relying on any sort of agreement on a global coordinate system. Most of these studies [1,5,4] assume oblivious robots (i.e. robots have no persistent memory of their past actions), so the "memory" of the network is implicit and generally deduced from the current positions of the robots. Two computation models are commonly used in robot networks: ATOM [9] and CORDA [7]. In both models robots perform in Look-Compute-Move cycles. The main difference is that these cycles are executed in a fully asynchronous manner in the CORDA model while each phase of the Look-Compute-Move cycle is executed in a lock step fashion in the ATOM model. These computation models have already proved their limitations. That is, the deterministic implementations of many fundamental abstractions such as gathering or leader election are proved impossible in these settings without additional assumptions ( [8,3]). The purpose of this paper is to study how the addition of bounded memory to each individual robot can increase the computational power of an asynchronous swarm of robots. We focus on an all-to-all communication primitive, called RoboCast, which is a basic building block for the design of any distributed system. A positive answer to this problem is the open gate for solving fundamental problems for robot networks such as gathering, scattering, election or exploration.
In robot networks, using motion to transmit information is not new [9,10,6]. In [9], Suzuki and Yamashita present an algorithm for broadcasting the local coordinate system of each robot (and thus build a common coordinate system) under the ATOM model. The algorithm heavily relies on the phase atomicity in each Look-Compute-Move cycle. In particular, a robot a that observes another robot b in four distinct positions has the certitude that b has in turn already seen a in at least two different positions. The situation becomes more intricate in the asynchronous CORDA model. Indeed, the number of different positions observed for a given robot is not an indicator on the number of complete cycles executed by that robot since cycles are completely uncorrelated. By contrast, our implementation of RoboCast is designed for the more general CORDA model and uses a novel strategy: the focus moves from observing robots in different positions to observing robots moving in different directions. That is, each robot changes its direction of movement when a particular stage of the algorithm is completed; this change allows the other robots to infer information about the observed robot.
Roadmap The paper is made up of six sections. Section 2 describes the computing model and presents the formal specification of the RoboCast problem. Section 3 presents our protocol and its complexity. The algorithm is enhanced in Section 4 with a collision-avoidance scheme. Using the Robocast primitive, Section 5 proposes algorithms for deterministic asynchronous gathering and binary information exchange. Finally, Section 6 provides concluding remarks. Some proofs are relegated to the appendix.

Model
We consider a network that consists of a finite set of n robots arbitrarily deployed in a two dimensional space, with no two robots located at the same position. Robots are devices with sensing, computing and moving capabilities. They can observe (sense) the positions of other robots in the space and based on these observations, they perform some local computations that can drive them to other locations.
In the context of this paper, the robots are anonymous, in the sense that they can not be distinguished using their appearance and they do not have any kind of identifiers that can be used during the computation. In addition, there is no direct mean of communication between them. Hence, the only way for robots to acquire information is by observing their positions. Robots have unlimited visibility, i.e. they are able to sense the entire set of robots. We assume that robots are non-oblivious, i.e. they can remember observations, computations and motions performed in previous steps. Each robot is endowed with a local coordinate system and a local unit measure which may be different from those of other robots. This local coordinate system is assumed to be fixed during a run unless it is explicitly modified by the corresponding robot as a result of a computation. We say in this case that robots remember their own coordinate systems. This is a common assumption when studying non-oblivious robot networks [9,6].
A protocol is a collection of n programs, one operating on each robot. The program of a robot consists in executing Look-Compute-Move cycles infinitely many times. That is, the robot first observes its environment (Look phase). An observation returns a snapshot of the positions of all robots within the visibility range. In our case, this observation returns a snapshot of the positions of all robots. The observed positions are relative to the observing robot, that is, they use the coordinate system of the observing robot. Based on its observation, a robot then decides -according to its program -to move or to stay idle (Compute phase). When a robot decides a move, it moves to its destination during the Move phase.
The local state of a robot is defined by the content of its memory and its position. A configuration of the system is the union of the local states of all the robots in the system. An execution e = (c 0 , . . . , c t , . . .) of the system is an infinite sequence of configurations, where c 0 is the initial configuration of the system, and every transition c i → c i+1 is associated to the execution of a non empty subset of actions. The granularity (or atomicity) of those actions is model-dependent and is defined in the sequel of this section.
A scheduler is a predicate on computations, that is, a scheduler defines a set of admissible computations, such that every computation in this set satisfies the scheduler predicate. A scheduler can be seen as an entity that is external to the system and selects robots for execution. As more power is given to the scheduler for robot scheduling, more different executions are possible and more difficult it becomes to design robot algorithms. In the remainder of the paper, we consider that the scheduler is fair and fully asynchronous, that is, in any infinite execution, every robot is activated infinitely often, but there is no bound on the ratio between the most activated robot and the least activated one. In each cycle, the scheduler determines the distance to which each robot can move in this cycle, that is, it can stop a robot before it reaches its computed destination. However, a robot r i is guaranteed to be able to move a distance of at least δ i towards its destination before it can be stopped by the scheduler.
We now review the main differences between the ATOM [9] and CORDA [7] models. In the ATOM model, whenever a robot is activated by the scheduler, it performs a full computation cycle. Thus, the execution of the system can be viewed as an infinite sequence of rounds. In a round one or more robots are activated by the scheduler and perform a computation cycle. The fully-synchronous ATOM model refers to the fact that the scheduler activates all robots in each round, while the regular ATOM model enables the scheduler to activate only a subset of the robots. In the CORDA model, robots may be interrupted by the scheduler after performing only a portion of a computation cycle. In particular, phases (Look, Compute, Move) of different robots may be interleaved. For example, a robot a may perform a Look phase, then a robot b performs a Look-Compute-Move complete cycle, then a computes and moves based on its previous observation (that does not correspond to the current configuration anymore). As a result, the set of executions that are possible in the CORDA model are a strict superset of those that are possible in the ATOM model. So, an impossibility result that holds in the ATOM model also holds in the CORDA model, while an algorithm that performs in the CORDA model is also correct in the ATOM model. Note that the converse is not necessarily true.
The RoboCast Problem The RoboCast communication abstraction provides a set of robots located at arbitrary positions in a two-dimensional space the possibility to broadcast their local information to each other. The RoboCast abstraction offers robots two communication primitives: RoboCast(M) sends Message M to all other robots, and Deliver(M) delivers Message M to the local robot. The message may consists in the local coordinate system, the robot chirality, the unit of measure, or any binary coded information.
Consider a run at which each robot r i in the system invokes RoboCast(m i ) at some time t i for some message m i . Let t be equal to max{t 1 , . . . , t n }. Any protocol solving the RoboCast Problem has to satisfy the following two properties: Validity: For each message m i , there exists a time t ′ i > t after which every robot in the system has performed Deliver(m i ). Termination: There exists a time t T ≥ max{t ′ 1 , . . . , t ′ n } after which no robot performs a movement that causally depends on the invocations of RoboCast(m i ).

Local Coordinate System RoboCast
In this section we present algorithms for robocasting the local coordinate system. For ease of presentation we first propose an algorithm for two-robots then the general version for systems with n robots. The local coordinate system is defined by two axes (abscissa and ordinate), their positive directions and the unity of measure. In order to robocast this information we use a modular approach. That is, robots invoke first the robocast primitive (LineRbcast1 hereafter) to broadcast a line representing their abscissa. Then, using a parametrized module (LineRbcast2), they robocast three successive lines encoding respectively their ordinate, unit of measure and the positive direction of axes. This invocation chain is motivated by the dependence between the transmitted lines. When a node broadcasts a line, without any additional knowledge, two different points have to be sent in order to uniquely identify the line at the destination. However, in the case of a coordinate system, only for the first transmitted axis nodes need to identify the two points. The transmission of the subsequent axes needs the knowledge of a unique additional point.

Line RoboCast
In robot networks the broadcast of axes is not a new issue. Starting with their seminal paper [9], Suzuki and Yamashita presented an algorithm for broadcasting the axes via motion that works in the ATOM model. Their algorithm heavily relies on the atomicity of cycles and the observation focus on the different positions of the other robots during their Move phase.
This type of observation is totally useless in asynchronous CORDA model. In this model, when a robot r moves towards its destination, another robot r ′ can be activated k > 1 times with k arbitrarily large, and thus observe r in k different positions without having any clue on the number of complete cycles executed by r. In other words, the number of different positions observed for a given robot is not an indicator on the number of complete executed cycles since in CORDA cycles are completely uncorrelated.
Our solution uses a novel strategy. That is, the focus moves from observing robots in different positions to observing their change of direction: each robot changes its direction of movement when a particular stage of the algorithm is completed; this change allows the other robots to infer information about the observed robot.
Line RoboCast Detailed Description Let r 0 and r 1 be the two robots in the system. In the sequel, when we refer to one of these robots without specifying which, we denote it by r i and its peer by r 1−i . In this case, the operations on the indices of robots are performed modulo 2. For ease of presentation we assume that initially each robot r i translates and rotates its local coordinate system such that its x-axis and origin coincide with the line to be broacast and its current location respectively. We assume also that each robot is initially located in the origin of its local coordinate system.
At the end of the execution, each robot must have broadcast its own line and have received the line of its peer. A robot "receives" the line broadcast by its peer when it knows at least two distinct positions of this line. Thus, to send its line, each robot must move along it (following a scheme that will be specified later) until it is sure that it has been observed by the other robot.
The algorithm idea is simple: each robot broadcasts its line by moving along it in a certain direction (considered to be positive). Simultaneously, it observes the different positions occupied by its peer r 1−i . Once r i has observed r 1−i in two distinct positions, it informs it that it has received its line by changing its direction of movement, that is, by moving along its line in the reverse direction (the negative direction if the first movement have been performed in the positive direction of the line). This change of direction is an acknowledgement for the reception of the peer line. A robot finishes the algorithm once it changed its direction and observed that the other robot also changed its direction. This means that both robots have sent their line and received the other's line.
The algorithm is described in detail as Algorithm 1. Due to space limitations, its proof is given in the Appendix. Each robot performs four stages referred in Algorithm 1 as states: state S 1 : This is the initial state of the algorithm. At this state, the robot r i stores the position of its peer in the variable pos 1 and heads towards the position (1.0) of its local coordinate system. That is, it moves along its line in the positive direction. Note that r i stays only one cycle in this state and then goes to state S 2 . and pos 2 . Before finishing the algorithm, r i must be sure that also r 1−i knows its line. Therefore, it observes r 1−i until it detects a change of direction (the condition of line 3.a). If this is not the case and if r i is still in the positive part of its x-axis, then it goes to the position (−1, 0) of its local coordinate system (line 3.b). Otherwise (if r i is already in the negative part of its xaxis), it performs a null movement (line 3.c). When r i is in state S 3 one is sure, as we shall show later, that r 1−i knows at least one position of l i , say p. Recall that l i corresponds to the x-axis of r i . It turns out that p is located in the positive part of this axis. In moving towards the negative part of its x-axis, r i is sure that it will eventually be observed by r 1−i in a position distinct from p which allows r 1−i to compute l i . -state S 4 : At this stage, both r i and r 1−i received the line sent by each others.
That is, r i has already changed its own direction of movement, and observed that r 1−i also changed its direction. But nothing guarantees that at this step r 1−i knows that r i changed its direction of movement. If r i stops now, r 1−i may remain stuck forever (in state S 3 ). To announce the end of the algorithm to its peer, r i heads towards a position located outside l i , That is, it will move on a line nextl i (distinct from l i ) which is given as parameter to the algorithm. During the move from l i to nextl i , r i should avoid points outside these lines. To this end, r i must first pass through myIntersectwhich is the intersection of l i and nextl i -before moving to a point located in nextl i but not on l i (refer to lines 3.a.2, 3.a.3 and 4.a of the code). Note that the robocast of a line is usually followed by the robocast of other information (e.g. other lines that encode the local coordinate system). To helps this process the end of the robocast of l i should mark the beginning of the next line, nextl i , robocast. Therefore, once r i reaches myIntersect, r i rotates its local coordinate system such that its x-axis matches now with nextl i , and then it moves toward the point of (1,0) of its (new) local coordinate system. When r 1−i observes r i in a position that is not on l i , it learns that r i knows that r 1−i learned l 1−i , and so it can go to state S 4 (lines 3.a. * ) and finish the algorithm.
1. r i rotates its coordinate system such that its x-axis and the origin match with nextl i and myIntersect respectively.

Line RoboCast: a Composable Version
Line RoboCast primitive is usually used as a building block for achieving more complex tasks. For example, the RoboCast of the local coordinate system requires the transmission of four successive lines representing respectively the abscissa, the ordinate, the value of the unit measure and a forth line to determine the positive direction of axes. In stigmergic communication a robot has to transmit at least a line for each binary information it wants to send. In all these examples, the transmitted lines are dependent one of each other and therefore their successive transmission can be accelerated by directly exploiting this dependence. Indeed, the knowledge of a unique point (instead of two) is sufficient for the receiver to infer the sent line. In the following we propose modifications of the Line RoboCast primitive in order to exploit contextual information that are encoded in a set of predicates that will be detailed in the sequel.
In the case of the local coordinate system, the additional information the transmission can exploit is the fact that the abscissa is perpendicular to the ordinate. Once the abscissa is transmitted, it suffices for a robot to simply send a single position of its ordinate, say pos1. The other robots can then calculate the ordinate by finding the line that passes through pos1 and which is perpendicular to the previously received abscissa. In the modified version of the Line RoboCast algorithm the predicate isP erpendicular encodes this condition.
For the case of stigmergy, a robot transmits a binary information by robocasting a line whose angle to the abscissa encodes this information. The lines transmitted successively by a single robot are not perpendicular to each others. However, all these lines pass through the origin of the coordinate system of the sending robot. In this case, it suffices to transmit only one position located on this line as long as it is distinct from the origin. We say in this case that the line satisfies the predicate passT hrOrigin.
A second change we propose relates to the asynchrony of the algorithm. In fact, even if robots execute in unison, they are not guaranteed to finish the execution of LineRbcast1 at the same time (by reaching S 4 ). A robot r i can begin transmitting its k-th line l i when its peer r 1−i is still located in its (k − 1)th line ancientl 1−i that r i has already received. r i should ignore the positions transmitted by r 1−i until it leaves ancientl 1−i for a new line. It follows that to make the module composable, the old line that the peer has already received from its peer should be supplied as an argument (ancientl 1−i ) to the function. Thus, it will not consider the positions occupied by r 1−i until the latter leaves ancientl 1−i .
In the following, we present the code of the new Line RoboCast function that we denote by LineRbcast2. Its description and its formal proof are omitted since they follow the same lines as those of LineRbcast1.

RoboCast of the Local Coordinate System
To robocast their two axes (abscissa and ordinate), robots call LineRbcast1 to robocast the abscissa, then LineRbcast2 to robocast the ordinate. The parameter = myOrdinate of LineRbcast2 stands for the next line to be robocast and it can be set to any line different from myOrdinate. The next line to robocast (unitLine) is a line whose angle with the x-axis encodes the unit of measure. This angle will be determined during the execution LineRbcast2.
1. peerAbscissa ← LineRbcast1(myAbscissa, myOrdinate) 2. peerOrdinate ← LineRbcast2(myOrdinate, = myOrdinate, peerAbscissa, isP erpendicular) After executing the above code, each robot knows the two axes of its peer coordinate system but not their positive directions neither their unit of measure. To robocast the unit of measure we use a technique similar to that used by [9]. The idea is simple: each robot measures the distance d i between its origin and the peer's origin in terms of its local coordinate system. To announce the value of d i to its peer, each robot robocast via LineRbcast2 a line, unitLine, which passes through its origin and whose angle with its abscissa is equal to f (d i ) where for x > 0, f (x) = (1/2x) × 90 • is a monotonically increasing function with range (0 • , 90 • ). The receiving robot r 1−i can then infer d i from f (d i ) and compute the unit measure of r i which is equal to d 1−i /d i . The choice of (0 • , 90 • ) as a Algorithm 2 Line RoboCast LineRbcast2 for two robots: Algorithm for robot r i Inputs: l i : the line to robocast nextl i : the next line to robocast after l i precedentl 1−i : the line robocast precedently by r 1−i predicate: a predicate on the output l 1−i , for example isP erpendicular and passT hrOrigin.
range for f (x) (instead of (0 • , 360 • )) is motivated by the fact that the positive directions of the two axes are not yet known to the robots. It is thus impossible to distinguish between an angle α with α ∈ (0 • , 90 • ) and the angles Π − α, −α, and Π + α. To overcome the ambiguity and to make f (x) injective, we restrict the range to (0 • , 90 • ). In contrast, Suzuki and Yamashita [9] use a function f ′ (x) slightly different from ours: (1/2x)×360 • . That is, its range is equal to (0 • , 360 • ). This is because in ATOM, robots can robocast at the same time the two axis and their positive directions, for example by restricting the movement of robots to only the positive part of their axes. Since the positive directions of the two axes are known, unitLine can be an oriented line whose angle f ′ (x) can take any value in (0 • , 360 • ) without any possible ambiguity.
Positive directions of axes Once the two axes are known, determining their positive directions amounts to selecting the upper right quarter of the coordinate system that is positive for both x and y. Since the line used to robocast the unit of distance passes through two quarters (the upper right and the lower left), it remains to choose among these two travelled quarters which one corresponds to the upper right one. To do this, each robot robocast just after the line encoding the unit distance another line which is perpendicular to it such that their intersection lays inside the upper right quarter.
Generalization to n robots The generalization of the solution to the case of n > 2 robots has to use an additional mechanism to allow robots to "recognize" other robots and distinguish them from each others despite anonymity. Let us consider the case of three robots r 1 , r 2 , r 3 . When r 1 looks the second time, r 2 and r 3 could have moved (or be moving), each according to its local coordinate system and unit measure. At this point, even with memory of past observations, r 1 may be not able to distinguish between r 2 and r 3 in their new positions given the fact that robots are anonymous. Moreover, r 2 and r 3 could even switch places and appear not to have moved. Hence, the implementation of the primitive observe(i) is not trivial. For this, we use the collision avoidance techniques presented in the next section to instruct each robot to move only in the vicinity of its initial position. This way, other robots are able to recognize it by using its past positions. The technical details of this mechanism are given at the end of the next section.
Apart from this, the generalization of the protocol with n robots is trivial. We present its detailed description in the Appendix.

Motion Complexity Analysis
Now we show that the total number of robot moves in the coordinate system RoboCast is upper bounded. For the sake of presentation, we assume for now that the scheduler does not interrupt robots execution before they reach their planned destination. Each robot is initially located at the origin of its local coordinate system. To robocast each axis, a robot must visit two distinct positions: one located in the positive part of this axis and the other one located in its negative part. For example, to robocast its x-axis, a robot has first to move from its origin to the position (1.0) i , then from (1.0) i to the (−1, 0) i . Then, before initiating a robocast for the other axis, the robot must first return back to its origin. Hence, at most 3 movements are needed to robocast each axis. This implies that to robocast the whole local coordinate system, at most 12 movements have to be performed by a particular robot.
In the general CORDA model, the scheduler is allowed to stop robots before they reach their destination, as long as a minimal distance of δ i has been traversed. In this case, the number of necessary movements is equal to at most 8 * (1 + 1/δ i ). This worst case is obtained when a robot is not stopped by the scheduler when moving from its origin towards another position (thus letting it go the farthest possible), but stopped whenever possible when returning back from this (far) position to the origin. This contrasts with [9] and [6] where the number of positions visited by each robot to robocast a line is unbounded (but finite). This is due to the fact that in both approaches, robots are required to make a non null movement whenever activated until they know that their line has been received. Managing an arbitrary large number of movements in a restricted space to prevent collisions yields severe requirements in [6]: either robots are allowed to perform infinitely small movements (and such movements can be seen by other robots with infinite precision), or the scheduler is restricted in its choices for activating robots (no robot can be activated more than k times, for a given k, between any two activations of another robot) and yields to a setting that is not fully asynchronous. Our solution does not require any such hypothesis.

Collision-free RoboCast
In this section we enhance the algorithms proposed in Section 3 with the collisionfree feature. In this section we propose novel techniques for collision avoidance that cope with the system asynchrony.
Our solution is based on the same principle of locality as the Voronoi Diagram based schemes. However, acceptable moves for a robot use a different geometric area. This area is defined for each robot r i as a local zone of movement and is denoted by ZoM i . We require that each robot r i moves only inside ZoM i . The intersection of different ZoM i must remain empty at all times to ensure collision avoidance. We now present three possible definitions for the zone of movement: ZoM 1 i , ZoM 2 i and ZoM 3 i . All three ensure collision avoidance in CORDA, but only the third one can be computed in a model where robots do not know the initial position of their peers.
Let P (t) = {p 1 (t), p 2 (t) . . . , p n (t)} be the configuration of the network at time t, such that p i (t) denotes the position of robot r i at time t expressed in a global coordinate system. This global coordinate system is unknown to individual robots and is only used to ease the presentation and the proofs. Note that P (t 0 ) describes the initial configuration of the network.

Definition 1. (Voronoi Diagram)[2]
The Voronoi diagram of a set of points P = {p 1 , p 2 , . . . , p n } is a subdivision of the plane into n cells, one for each point in P . The cells have the property that a point q belongs to the Voronoi cell of point p i iff for any other point p j ∈ P , dist(q, p i ) < dist(q, p j ) where dist(p, q) is the Euclidean distance between p and q. In particular, the strict inequality means that points located on the boundary of the Voronoi diagram do not belong to any Voronoi cell.
be the Voronoi diagram of the initial configuration P (t 0 ). For each robot r i , the zone of movement of r i at time t, ZoM 1 The zone of movement of r i at time t, ZoM 2 i (t), is the circle centered in p i (0) and whose diameter is equal to i ) For each robot r i , define the distance d i (t) = min{dist(p i (t 0 ), p j (t)) with r j = r i } at time t. The zone of r i at time t, ZoM 3 i (t), is the circle centered in p i (t 0 ) and whose diameter is equal to Note that ZoM 1 and ZoM 2 are defined using information about the initial configuration P (t 0 ), and thus cannot be used with the hypotheses of Algorithm 2. In contrast, robot r i only needs to know its own initial position and the current positions of other robots to compute ZoM 3 i . As there is no need for r i to know the initial positions of other robots, ZoM 3 i can be used with Algorithm 2. It remains to prove that ZoM 3 i guarantees collision avoidance. We first prove that ZoM 1 i does, which is almost trivial because its definition does not depend on time. Then, it suffices to prove that ZoM 3 i ⊆ ZoM 2 i ⊆ ZoM 1 i . Besides helping us in the proof, ZoM 2 i can be interesting in its own as a cheap collision avoidance scheme in the ATOM model, as computing a cycle of radius half the distance to the nearest neighbor is much easier that computing a full blown Voronoi diagram.
Lemma 41 If ∀t, for each robot r i , the destination point computed by r i at t remains inside ZoM 1 i (t), then collisions are avoided.
Proof. By definition of Voronoi diagram, different Voronoi cells do not overlap. Moreover, for a given i, ZoM 1 i is static and does not change over time. Hence, Clearly, ZoM 2 i ⊆ ZoM 1 i which means that ZoM 2 i ensures also collision avoidance.
Lemma 42 If ∀t, for each robot r i , the destination point computed by r i at t always remains inside ZoM 2 i (t), then collisions are avoided.
The proof of the above lemma follows directly from the fact that ∀tZoM 2 i (t) ⊆ ZoM 1 i (t) and Lemma 41.
Proof. Fix some robot r i and let r j be the closest robot from r i at time t 0 . Let d 0 denote the initial distance between r i and r j , that is, We assume that all robots move only inside their ZoM 3 i computed as explained in Definition 4. Let t 1 ≥ t 0 be the first time at which a robot in {r i , r j }, say e.g. r i , finishes a Look phase after t 0 . The destination computed by r i in this cycle is located inside ZoM 3 i (t 1 ), which is a circle centered at p i (t 0 ) and whose diameter is ≤ d 0 /3. Hence, the destination computed by r i is distant from p i (0) by at most d 0 /3. Let t 2 ≥ t 1 be the first time after t 1 at which a robot, say r j , finishes a Look phase. Between t 1 and t 2 , r i may have finished its Move phase or not. In any case, the observed configuration by r j at t 2 is such that r i is distant from p j (t 0 ) by at most d 0 + d 0 /3. This implies that ZoM 3 j (t 2 ) has a diameter of at most (d 0 + d 0 /3)/3, which implies that the destination point computed by r j in this cycle is distant from p j (t 0 ) by at most d 0 + d 0 /3 + d 0 /9.
Repeating the argument, we get that ∀t, Reducing the formula, we obtain that ZoM 3 Ensuring Collision-freedom in Line Robocast Algorithms To make LineR-bcast1 and LineRbcast2 collision-free, it is expected that any destination computed by a robot r i at t be located within its ZoM 3 i (t). The computation of destinations is modified as follows: Let dest i (t) be the destination computed by a robot r i at time t. Based on dest i (t), r i computes a new destination dest ′ i (t) that ensures collision avoidance. dest ′ i (t) can be set to any point located in [p i (t 0 ), dest i (t)] ∩ ZoM 3 i (t). For example, we can take dest ′ i (t) to be equal to the point located in the line segment [p i (t 0 ), dest i (t)] and distant from p i (t 0 ) by a distance of d i (t)/2 with d i (t) computed as explained in Definition 4.
This modification of the destination computation method does not impact algorithms correctness since it does not depend on the exact value of computed destinations, but on the relationship between the successive positions occupied by each robot. The algorithms remain correct as long as robots keep the capability to freely change their direction of movement and to move in both the positive and the negative part of each such direction. This capability is not altered by the collision avoidance scheme since the origin of the coordinate system of each robot -corresponding to its original position -is strictly included in its zone of movement, be it defined by ZoM 1 , ZoM 2 or ZoM 3 .
Generalisation of the Protocols to n Robots As explained at the end of Section 3, the generalisation of our algorithms to the case of n robots has to deal with the issue of distinguishing robots from each others despite their anonymity. The solution we use is to instruct each robot to move in the close neighbourhood of its original position. Thus, other robots can recognize it by comparing its current position with past ones. For this solution to work, it is necessary that each robot always remains the closest one to all the positions it has previously occupied. Formally speaking, we define the zone of movement ZoM 4 in a similar way as ZoM 3 except that the diameter is this time equal to d i (t)/6 (vs. d i (t)/3). We now show that ZoM 4 provides the required properties. Let r i and r j be an arbitrary pair of robots and Let d ij denotes the distance between their initial positions. It can easily shown, using the same arguments as the proof of Lemma 43, that: 1. Neither of the two robots moves away from its initial position by a distance greater than d ij /4. This implies that each robot remains always at a distance strictly smaller than d ij /2 from all the positions it has previously held. 2. The distance between r i (resp. r j ) and all the positions held by r j (r i ) is strictly greater than d ij /2.
Hence, r i can never be closer than r j to a position that was occupied by r j , and vice versa. This implies that it is always possible to recognize a robot by associating it with the position which is closest to it in some previously observed configuration.

Asynchronous Deterministic 2-Gathering
Given a set of n robots with arbitrary initial locations and no agreement on a global coordinate system, n-Gathering requires that all robots eventually reach the same unknown beforehand location. n-Gathering was already solved when n > 2 in both ATOM [9] and CORDA [4] oblivious models. The problem is impossible to solve for n = 2 even in ATOM, except if robots are endowed with persistent memory [9]. In this section we present an algorithm that uses our RoboCast primitive to solve 2-Gathering in the non-oblivious CORDA model. A first "naive" solution is for each robot to robocast its abscissa and ordinate axes and to meet the other robot at the midpoint m of their initial positions. RoboCasting the two axes is done using our Line RoboCast function described above in conjunction with the ZoM 3 −based collision avoidance scheme.
A second possible solution is to refine Algorithm ψ f −point(2) of [9, 10] by using our Line RoboCast function to "send" lines instead of the one used by the authors. The idea of this algorithm is that each robot which is activated for the first time translates and rotates its coordinate system such that the other robot is on its positive y-axis, and then it robocasts its (new) x-axis to the other robot using our Line Robocast function. In [9], the authors give a method that allows each robot to compute the initial position of one's peer by comparing their two robocast x-axes defined above. Then each robot moves toward the midpoint of their initial positions. Our Line RoboCast routine combined with the above idea achieves gathering in asynchronous systems within a bounded (vs. finite in [9]) number of movements of robots and using only two (vs. four) variables in their persistent memory.
Theorem 51 There is an algorithm for solving deterministic gathering for two robots in non-oblivious asynchronous networks (CORDA).

Asynchronous Stigmergy
Stigmergy [6] is the ability of a group of robots that communicate only through vision to exchange binary information. Stigmergy comes to encode bits in the movements of robots. Solving this problem becomes trivial when using our Robo-Cast primitive. First, robots exchange their local coordinate system as explained in Section 3. Then, each robot that has a binary packet to transmit robocasts a line to its peers whose angle with respect to its abscissa encodes the binary information. Theoretically, as the precision of visual sensors is assumed to be infinite, robots are able to observe the exact angle of this transmitted line, hence the size of exchanged messages may be infinite also. However, in a more realistic environment in which sensor accuracy and calculations have a margin of error, it is wiser to discretize the measuring space. For this, we divide the space around the robot in several sectors such that all the points located in the same sector encode the same binary information (to tolerate errors of coding). For instance, to send binary packets of 8 bits, each sector should have an angle equal to u = 360 • /2 8 . Hence, when a robot moves through a line whose angle with respect to the abscissa is equal to α, the corresponding binary information is equal to ⌊α/n⌋. Thus, our solution works in asynchronous networks, uses a bounded number of movements and also allows robots to send binary packets and not only single bits as in [6].

Conclusion and Perspectives
We presented a new communication primitive for robot networks, that can be used in fully asynchronous CORDA networks. Our scheme has the additional properties of being motion, memory, and computation efficient. We would like to raise some open questions: 1. The solution we presented for collision avoidance in CORDA can be used for protocols where robots remain in their initial vicinity during the whole protocol execution. A collision-avoidance scheme that could be used with all classes of protocol is a challenging issue. 2. Our protocol assumes that a constant number of positions is stored by each robot. Investigating the minimal number of stored positions for solving a particular problem would lead to interesting new insights about the computing power that can be gained by adding memory to robots.

Appendix A Correctness Analysis of LineRbcast1
In the following we prove that Algorithm 1 satisfies the specification of a Robo-Cast, namely validity and termination. First we introduce some notations that will be further used in the proofs of the algorithm. For each variable v, and each robot r i , we denote r i .v(t) the value of the variable v in the local memory of r i at time t. When the time information can be derived from the context, we use simply r i .v.
Proof of the Validity property. We start by the validity property. For this, we first prove a series of technical lemmas. The following two lemmas state the existence of a time instant at which both robots have reached S 2 and a following time instant at which at least one of them have reached S 3 .
Lemma A1 Eventually, both robots reach state S 2 .
Proof. Thanks to the fairness assumption of the scheduler, every robot is activated infinitely often. The first time each robot is activated, it executes the lines (1.a, 1.b, 1.c) of Algorithm 1 and it reaches the state S 2 .
Lemma A2 Eventually, at least one robot reaches state S 3 .
Proof. Let r 1 and r 2 be two robots executing Algorithm 1, and assume towards contradiction that neither of them reaches state S 3 . But according to Lemma A1, they both eventually reach S 2 . Consider for each robot r i the cycle in which it reaches state S 2 , and define t i to be the time of the end of the Look phase of this cycle. Without loss of generality, assume t 1 ≤ t 2 (the other case is symmetric). Hence, the variable r 1 .pos 1 describes the position of robot r 2 at t 1 expressed in the local coordinate system of robot r 1 . Let t 3 > t 2 be the time at which robot r 2 finishes its cycle that leads it to state S 2 . Between t 2 and t 3 , robot r 2 performed a non null movement because it moved towards the point (1.0) of its local coordinate system (line 1.b of the code). Hence, the position of r 2 at t 3 is different from its position at t 1 ≤ t 2 which was recorded in the variable r 1 .pos 1 . By assumption, r 2 never reaches state S 3 , so each time it is activated after t 3 it keeps executing the lines 2.a and 2.c of the code and never moves from its current position (reached at t 3 ). By fairness, there is a time t ≥ t 3 at which robot r 1 is activated again. At this time, it observes r 2 in a position different from r 1 .pos 1 . This means that for r 1 the condition of line 2.a is false. Hence, r 1 executes the else block of the condition (2.b. * ) and reaches state S 3 which contradicts the assumption and proves the lemma.
The next lemma expresses the fact that our algorithm exhibits some kind of synchrony in the sense that robots advance in the execution of the algorithm through the different states in unisson. That is, neither of them surpasses the other by more than one stage (state).
Lemma A3 If at some time robot r i is in state S j and robot r 1−i is in state S k then |j − k| ≤ 1.
Proof. The proof of the lemma is divided into two parts: -If robot r i is in state S 3 and robot r 1−i is in state S j then j ≥ 2.
proof: Since robot r i is in state S 3 , it has necessarily executed the lines (1.a . . . 1.d) and (2.b. * ) of the code. Hence, the value of variable r i .pos 1 is different from that of r i .pos 2 . This means that r i has seen r 1−i in at least two different positions which implies that r 1−i has been activated at least once. Hence, r 1−i has necessarily executed the lines (1.a . . . 1.c) and has reached S 2 . -If robot r i is in state S 4 and robot r 1−i is in state S j then j ≥ 3.
proof: For a robot r 1−i to reach state S 4 , it must execute the line 3.a of the code and detect that the other robot r 1−i has changed its direction of movement (it moved toward the negative part of its x-axis). Thus, robot r 1−i has necessarily executed lines (2.b.2 . . . 2.c) of the code which means that r 1−i is in state S 3 . Before this, robot r 1−i moved only in one direction, that is, in the positive direction of its x-axis.
This proves the lemma.
The following lemma states that each robot r i is guaranteed to be observed by its peer at least once in a position located in the positive part of its local x-axis. The observed position is stored in r 1−i .pos 1 . Expressed otherwise, this means that each robot "send" a position located in its positive x-axis to its peer. This property is important for proving validity which correspond to both robots eventually reaching S 3 (Lemmas A5 and A6). Indeed, since each robot r i is guaranteed that a point located in its local x-axis was received by its peer r 1−i , it suffices for r i to send its line to head toward the negative part of its x-axis and to stay there until it is observed by r 1−i . That is, until a position located in its negative x-axis (and thus distinct from r 1−i .pos 1 ) is received by Lemma A4 For each robot r i , the variable r i .pos 1 describes a position located in the positive axis of the other robot r 1−i .
Proof. The value of the variable r i .pos 1 is assigned for the first time in line 1.a when r i is still in state S 1 . At this time, according to Lemma A3, r 1−i is necessarily in state S 1 or S 2 (Otherwise, this would contradict Lemma A3 since we would have a time at which a robot (r 1−i ) is in a state S j with j ≥ 3 concurrently with another robot (r i ) that is in state S 1 ). This means that the variable r i .pos 1 describes a position held by robot r 1−i while it was in state S 1 or S 2 . But according to the algorithm, when a robot is in state S 1 or S 2 , it is still located in a position of its positive x-axis (or the origin). Hence, the variable r i .pos 1 describes a position located in the positive x-axis of robot r 1−i which proves the lemma.
Lemma A5 Eventually, both robots reach state S 3 .
Proof. According to Lemmas A2 and A3, there is a time at which some robot, say r i , reaches S 3 and the other one (r 1−i ) is at a state S j with j ≥ 2. If j ≥ 3 then the lemma holds and we are done. So we assume in what follows that r 1−i is at S 2 and we prove that it eventually reaches S 3 . Assume for the sake of contradiction that this is not the case, that is, r 1−i remains always stuck in S 2 . This implies, according to Lemma A3, that r i remains also stuck in state S 3 . When r i is in state S 3 , it keeps executing the line 3.b of the code until it reaches a position located in the negative part of its x-axis. Denote by t 1 the first time at which r i reaches its negative x-axis. Each time r i is activated after t 1 , it executes the line 3.c of the code corresponding to a null movement and it never moves from its current position (located in the negative x-axis). This is because we assumed that r i remains stuck in S 3 forever. By fairness, there is a time t 2 ≥ t 1 at which r 1−i is activated. This time, the condition of line 2.a does not hold for robot r 1−i because the position returned by observe(i) is located in the negative x-axis of r i and is different from r 1−i .pos 1 which is located in the positive part of the x-axis of r 1 (as stated in Lemma A4). Hence, r 1−i executes the part 2.b. * of the code and changes its status to S 3 . Now we are ready to prove the validity property.
Lemma A6 Algorithm 1 satisfies the validity property of the Line Robocast Problem for two robots.
Proof. Eventually both robots reach state S 3 according to Lemma A5. Each robot r i in state S 3 has necessarily executed the blocks 1. * and 2.b. * of the algorithm and thus delivered the line defined by the positions r i .pos 1 and r i .pos 2 . Now we prove that this line is well defined and that it does correspond to l 1−i , the line sent by r 1−i . r i .pos 1 and r i .pos 2 are well defined since they are assigned a value in lines 1.a and 1.b.1 respectively before r i delivers the line. The assigned values correspond to two positions of r 1−i . Moreover, by the condition of line 2.b. we have that these two positions are distinct. It remains to prove that they belong to l 1−i .
The values of variables r i .pos 1 and r i .pos 2 are assigned when r i is in state S 1 and S 2 respectively. Hence, according to Lemma A3, when r i .pos 1 and r i .pos 2 are defined, r 1−i did not yet reach S 4 and moved only through its x-axis. This means that r i .pos 1 and r i .pos 2 correspond to two distinct positions of the x-axis of r 1−i . Hence, r i delivered l 1−i . Since both robots eventually reach S 3 , both lines l i and l 1−i are eventually delivered.
Proof of the Termination property. Now we prove that the algorithm actually terminates. Before terminating, each robot r i must be sure that its peer r 1−i has received its sent line, that is, r 1−i has reached the state S 3 . As already explained, r i can infer the transition of r 1−i to S 3 by detecting a change of its direction of movement. Upon this, r i can go on to state S 4 and terminates safely. In the following two lemmas, we prove that at least one robot reaches S 4 . To do this, we first prove in Lemma A7 that at least one robot, say r 1−i , is observed by its peer in two distinct positions located in the positive part of its x-axis. Later, when r 1−i moves to its negative x-axis and r i observes it there, r i learns that r 1−i changed its direction of movement which allows the transition of r i to state S 4 . This is proved in Lemma A8.
Lemma A7 For at least one robot, say r i , the two variables r i .pos 1 and r i .pos 2 describe two positions located in the positive x-axis of r 1−i and such that r i .pos 2 > r i .pos 1 with respect to the local coordinate system of r 1−i .
Proof. Let r i be the first robot to enter state S 3 . The other robot (r 1−i ) is in state S 2 in accordance with Lemma A3. Hence, r 1−i moved only through the positive direction of its x-axis, so the variables r i .pos 1 and r i .pos 2 correspond to two different positions in the positive x-axis of robot r 1−i or in its origin. But since r i .pos 2 was observed after r i .pos 1 and r 1−i moves in the positive direction of its x-axis, then r i .pos 2 > r i .pos 1 with respect to the local coordinate system of r 1−i .
Lemma A8 Eventually, at least one robot reaches state S 4 .
Proof. We assume towards contradiction that no robot ever reach S 4 . But according to Lemma A5, both robots eventually reach S 3 . Hence we consider a configuration in which both robots are in S 3 and we derive a contradiction by proving that at least one of them does reach S 4 . Let r i be the robot induced by Lemma A7. The variables r i .pos 1 and r i .pos 2 of r i correspond to two different positions occupied by r 1−i while it was on the positive part of its x-axis. By assumption, r 1−i eventually reaches state S 3 . At the end of this cycle, r 1−i is either located in a position of its negative x-axis or it keeps executing lines 3.b. * each time it is activated until it reaches such a position, let's call it p. The next cycles it is activated, r 1−i executes the line 3.c of the code because we assumed that r 1−i never reaches S 4 . It results that r 1−i never quits p. Hence, r 1−i is guaranteed to be eventually observed by r i in a position that is smaller than r i .pos 2 with respect to the local coordinate system of r 1−i . At this point, the condition of line 3.4 becomes true for robot r i , which executes the block of the code labelled by 3.4. * and sets is state to S 4 .
Lemma A9 Eventually, both robots reach state S 4 .
Proof. According to Lemma A8 at least one robot, say r i , eventually reaches S 4 . When r i reaches S 4 , r 1−i is in a state S j with j ≥ 3 according to Lemma A3. If j = 4 the lemma holds trivially, so we consider in the following a configuration in which r 1−i is in state S 3 and we prove that it eventually joins r i in state . myIntersect is the point located at the intersection of l i and nextl i and its distance from p i is finite. Since r i is guaranteed to move a minimal distance of δ i at each cycle in which it is activated, it reaches myIntersect after a finite number of cycles. The next cycle, r i chooses a destination located outside l i (4.b.2) and moves towards it before finishing the algorithm. Let t i be the time of the end of the Move phase of this cycle and let q i be the position occupied by r i at t i . q i / ∈ l i means that q i / ∈ line(r 1−i .pos 1 , r 1−i .pos 2 ). It follows that r 1−i .pos 2 / ∈ line(r 1−i .pos 1 , q i ). By fairness, there is a time t > t i at which r 1−i is activated again, and at which it observes r i in the position q i . But we showed that q i is such that r 1−i .pos 2 / ∈ line(r 1−i .pos 1 , q i ). Hence the condition of line 3.a is true for robot r 1−i in t and it reaches state S 4 in this cycle.
Lemma A10 Algorithm 1 satisfies the termination property of the Line Robocast Problem for two robots.
Proof. Eventually, both robots reach S 4 as proved by Lemma A9. Let r i be a robot in state S 4 and let p i be its position at the end of the cycle in which it reaches S 4 , Let d i be the distance between p i and myIntersect i . Since the scheduler is fair and a robot is allowed to move in each cycle a minimal distance of σ i before it can be stopped by the scheduler, it follows that r i is guaranteed to cover the distance d i and to reach myIntersect after at most d i /σ i cycles. The next cycle, r i moves outside l i and terminates.
Theorem A11 Algorithm 1 solves the Line Robocast Problem for two robots in unoblivious CORDA systems.

B Generic RoboCast
In this section, we describe the RoboCast Algorithm for the general case of n robots. Then we give its formal proof of correctness.

B.1 Description of the Algorithm
The Line RoboCast algorithm for the general case of n processes is a simple generalization of the algorithm for two robots. The code of this algorithm is in Algorithm 3. It consists in the following steps: The first time a robot r i is activated in state . Hence, r i delivers line(r i , r j ) which corresponds to l j . r i does not move from its current position until it assigns a value to all the cells of pos 2 [] (apart from the one associated with itself which is meaningless). That is, until it delivers all the lines sent by its peers. Upon this, it transitions to S 3 and heads to the point (−1, 0). At state S 3 , r i waits until it observes that all other robots changed the direction of their movement or moved outside their sent line. Then, it moves towards a position located outside its current line l i . In particular, it goes to a position located in nextl i , the next line it will robocast. Hence r i first passes by the intersection of l i and nextl i . Then, it moves outside l i and terminates the algorithm.

B.2 A Correctness Argument
We prove the correctness of our algorithm by proving that it satisfies the validity and termination property of the RoboCast Problem specification. The general idea of the proof is similar to that of the two robots algorithms even if it is a little more involved.

Proof of the Validity property.
Lemma B1 Eventually, all robots reach state S 2 .
Proof. Similar to the proof of Lemma A1.
Lemma B2 Eventually, at least one robot reaches state S 3 .
Proof. Let R = {r 1 , r 2 , . . . , r n } be a set of n robots executing Algorithm 3. We assume towards contradiction that neither of them ever reach S 3 . But according to Lemma B1, all robots eventually reach state S 2 . Thus we proceed in the following way: we consider a configuration in which all robots are in S 2 and we prove that at least one of them eventually reaches S 3 which leads us to a contradiction. Consider for each robot r i ∈ R the cycle in which it reaches the Thus, the position of each robot at t ′ i is different from its position at t k which is stored in r k .pos 1 [i]. We have by assumption that no robot ever reaches S 3 . So each time a robot r i is activated after t ′ i , it keeps executing the lines 2.b and 2.d of the code and never moves from its current position reached at t ′ i . Define t end to be equal to max{t ′ 1 , . . . , t ′ n }. It follows that at ∀t ≥ t end , the position of each robot r i at t is different from r k .pos 1 [i]. But by fairness, there is a time t a ≥ t end at which r k is activated again. At this cycle, r k observes that each robot r i is located in a position different from r k .pos 1 [i]. Consequently, if there exists a robot r i such that r k .pos 2 [i] was equal to ⊥ before this cycle, then r k assigns the current observed position of r i to r k .pos 2 [i]. This implies that the condition of line 2.b is now false for r k . Hence r k executes the else block of the condition and reaches state S 3 . This is the required contradiction that proves the lemma. Proof. The proof follows the same lines as that of Lemma A4.
Lemma B4 If at some time robot r i is in state S j and robot r ′ i is in state S k then |j − k| ≤ 1.
Proof. The lemma can be proved by generalising the proof of Lemma A3 to the case of n robots. We divide the analysis into two subcases: -If robot r i is in state S 3 and robot r ′ i is in state S j then j ≥ 2. proof: If r i is in state S 3 , this means that it observed all other robots in at least two distinct positions. This means that all other robots started a Move phase, which implies that they all finished a complete Compute phase in which they executed the lines 1.a . . . 1.c of the code and reached S 2 .
-If robot r i is in state S 4 and robot r ′ i is in state S j then j ≥ 3. proof: For a robot to reach S 4 , it must detect a change of direction by all other robots in the network which is captured by the condition of line 3.a. We prove that this condition cannot be true unless all robots have reached S 3 and no robot in the network is still in state S 2 . Indeed, robots in state S 1 move in the positive direction of their x-axis and those in state S 2 does not move. So, a robot cannot change its direction before reaching state S 3 . This change of direction is reflected by the choice of point (−1, 0) as a destination in line 2.c.1 of the code before the transition to state S 3 in line 2.c.2.
Corollary B5 If at some time t, ∃i, j such that robots r i and r j are respectively in state S k and S k+1 at t with k ∈ {1, 2, 3}, then all the robots of the network are either in state S k or S k+1 at t.
Proof. Since r i is in state S k , no robot in the network can be in a state S l with l ≥ k + 2 according to Lemma B4. Similarly, the fact that r j is in state S k+1 implies that no robot in the network can be in a state S l with l ≤ k − 1. By the conjunction of the two facts, we obtain that all robots are either in state S k or S k+1 .
The following lemma proves the fact that if at time t a , some robots of the network are in state S 2 and others are in state S 3 , then at least one robot that is in state S 2 at t a eventually reaches S 3 .
Lemma B6 Let G 2 (t), G 3 (t) be the groups of robots that are respectively in state S 2 and S 3 at time t. If at some time t a G 2 (t a ) > 0 and G 3 (t a ) > 0, then there exists a time t ≥ t a at which G 3 (t) ≥ G 3 (t a ) + 1.
Proof. Since by assumption G 2 (t a ) > 0 and G 3 (t a ) > 0, it follows from Corollary B5 that R = G 2 (t a ) ∪ G 3 (t a ). We assume toward contradiction that ∀t ≥ t a G 2 (t) = G 2 (t a ) = G 2 , that is, no robot that is in S 2 at t a ever reach S 3 . But by assumption we have G 2 > 0. Hence ∀t > t a G 2 (t) = G 2 > 0. This implies, in accordance with Lemma B4, that no robot of the network can reach -As discussed above, we have by assumption that all robots have reached S 2 at t a . This means that all robots have executed the line 1.a of the code at t a . Consequently, at t a , ∀r i ∈ R, ∀r j ∈ R with j = i, r i .pos 1 [j] =⊥. Moreover, according to Lemma B3 all these positions stored in the arrays pos 1 [] describe positions located in the positive x-axis of the corresponding robots.
-By assumption we have that ∀t > t a G 3 (t) = G 3 . This means that no robot in G 3 ever reach S 4 . Hence robots of G 3 never execute the block 3.a. * of the code and they keep executing the line 3.b each time they are activated until they reach a position in their negative x-axes. Then, once a robot of G3 arrives to the negative part of its x-axis, it keeps executing the line 3.c of the code each time it is activated. As we showed above, the positions stored in the different arrays pos 1 [] are different from ⊥ and correspond to points located in the positive x-axes of the corresponding robots. Since robots of G 3 eventually get to positions in their negative x-axes and stay there, they eventually get observed by each robot in the network in a position different from the one that is stored in its local variable pos 1 [] which correspond to a positive x-axis position. Formally, there is a time t v > t at which ∀r i ∈ G 3 , ∀r j ∈ R with r j = r i r j .pos 2 [i] =⊥. -Let r 1 , . . . , r m be the robots of G 2 . Consider for each robot r i ∈ G 2 the cycle in which it reaches the state S 2 , and define t i and t ′ i to be respectively the time of the end of the Look and the Move phase and of this cycle. Let t k be equal to min{t 1 , t 2 , . . . , t m } and let r k ∈ G 2 be the corresponding robot. That is, at t k , robot r k finishes to execute a Look phase and at the end of this cycle it reaches state S 2 . This means that for robot r k , r k .pos 1 [] describes the configuration of the network at time t k . Following the lines of the proof of Lemma B2 we obtain that there exist a time t u > t at which ∀r j ∈ G 2 \ {r k }, r k .pos 2 [j] = ⊥. Now, let t x = max{t v , t u }. From the discussion above it results that at time t x , for robot r k ∈ G 2 it holds that ∀r j ∈ G 3 , r k .pos 2 [j] = ⊥ and ∀r j ∈ G 2 \ {r k }, r k .pos 2 [j] = ⊥. Hence, at t x , ∀j ∈ R \ {r k }, r k .pos 2 [j] = ⊥. This means that the condition of line 2.a is false for r k at t x , so r k executes the else block of this condition when activated after t x and reaches state S 3 which contradicts the assumption that ∀t > t a G 2 (t) = G 2 .
Lemma B7 Eventually, all robots of the network reach state S 3 Proof. Follows from Lemmas B1, B2 and B6.
Lemma B8 Algorithm 3 satisfies the validity property.
Proof. The idea of the proof is similar to Lemma A6. According to Lemma B7, all robots eventually reach state S 3 . Each robot that reach state S 3 has necessarily executed the block 1. * and the line 2.c of Algorithm 3. Hence, this robot has its two arrays pos

Proof of the Termination property.
Lemma B9 Eventually, at least one robot reaches state S 4 Proof. We assume for the sake of contradiction that no robot ever reach S 4 . However, according to Lemma B7, all robots eventually reach state S 3 . Hence we consider a configuration in which all robots are in state S 3 and we prove that at least one of them eventually reaches S 4 which leads us to a contradiction. The idea of the proof is similar to that of Lemma B2: we consider the first robot r k that executes a Look phase of a cycle leading it from S 2 to S 3 . Let t k be the time of the end of this Look phase. Clearly, ∀r i ∈ R \ {r k }, r k .pos 1 [i] and r k .pos 2 [i] describe two positions of r i located in its positive x-axis. This is because these two positions were observed by r k before r i reaches S 3 and changes its direction of movement towards its negative x-axis. Moreover, r k .pos 2 [i] > r k .pos 1 [i] with respect to the local coordinate system of r i since r i was observed in r k .pos 1 [i] and then in r k .pos 2 [i] while it was moving along the positive direction of its x-axis. The claim can be proved formally as in Lemma A7. After t k , all other robots of the network perform a transition from S 2 to S 3 . Then, they head towards the negative part of their local x-axes (lines 2.c.1 and 3.b of the code) and stay there (line 3.c) since they cannot reach S 4 by assumption. Each robot r i that reaches the negative part of its x-axis is located in a position p i such that r k .pos 2 [i] is outside the line segment [r k .pos 2 [i], p i ]. Hence the condition of line 3.a eventually becomes true for robot r k , and it reaches S 4 after executing the block 3.a. * of the code. This is the required contradiction.
Lemma B10 Eventually, all robots of the network reach S 4 .
Proof. The proof is similar to that of Lemma A9. The intuition behind it is as follows: we proved in Lemma B9 that at least one robot, say r i , eventually reaches S 4 . After reaching S 4 , and after a finite number of executed cycles, r i quits l i (line 4.b.2). When they observe r i outside l i , the other robots transition to state S 4 . Lemma B11 Algorithm 3 satisfies the termination property.
Proof. The proof is similar to that of Lemma A10 Theorem B12 Algorithm 1 solves the Line Robocast Problem for n robots in unoblivious CORDA systems.