Asynchronous Arbitrary Pattern Formation: the effects of a rigorous   approach

Serafino Cicerone; Gabriele Di Stefano; Alfredo Navarra

arXiv:1706.02474·cs.DC·February 7, 2018

Asynchronous Arbitrary Pattern Formation: the effects of a rigorous approach

Serafino Cicerone, Gabriele Di Stefano, Alfredo Navarra

PDF

Open Access

TL;DR

This paper introduces a rigorous, logic-based distributed algorithm for asynchronous arbitrary pattern formation without chirality, revealing flaws in previous approaches and establishing its equivalence with leader election.

Contribution

It provides the first fully rigorous algorithm for APF without chirality, using logical predicates to ensure correctness and challenge prior unverified results.

Findings

01

The new algorithm fully characterizes APF and its equivalence with leader election.

02

Previous algorithms in the literature lack rigorous correctness proofs.

03

Some established results in the literature are shown to be incorrect.

Abstract

Given any multiset F of points in the Euclidean plane and a set R of robots such that |R|=|F|, the Arbitrary Pattern Formation (APF) problem asks for a distributed algorithm that moves robots so as to reach a configuration similar to F. Similarity means that robots must be disposed as F regardless of translations, rotations, reflections, uniform scalings. Initially, each robot occupies a distinct position. When active, a robot operates in standard LCM cycles. Robots are asynchronous, oblivious, anonymous, silent and execute the same distributed algorithm. So far, the problem has been mainly addressed by assuming chirality, that is robots share a common left-right orientation. We are interested in removing such a restriction. While working on the subject, we faced several issues that required close attention. We deeply investigated how such difficulties were overcome in the literature,…

Figures15

Click any figure to enlarge with its caption.

Tables7

Table 1. Table 1: The basic Boolean variables used to define all the phases’ invariants. In the first column, the phase in which the corresponding variables are mainly used. Missing notations can be found in the corresponding sections. The table contains a formal definition for all variants except 𝚚 𝚚 \mathtt{q} and 𝚒 1 , … , 𝚒 6 subscript 𝚒 1 … subscript 𝚒 6 \mathtt{i}_{1},\ldots,\mathtt{i}_{6} . Such variables are formally defined in Section 6.4 , where they are used to recognize the guards in different scenarios when guards have to be moved in the finalization phase.

phase	var	definition
*	$𝚊$	$R$ is a leader configuration
$ℱ 1$	$𝚜_{2}$	$\| \partial C (R) \| = 2$
	$𝚜_{3}$	$\| \partial C (R) \| = 3$
	$𝚜_{+}$	$\| \partial C (R) \| > 3$
	$𝚌$	$\| {c (R)} \cap R \| = 1$
	$𝚝_{0}$	$𝚜_{3} \land$ points in $\partial C (R)$ form a triangle of angles all different from $90^{\circ}$
	$𝚝_{1}$	$𝚜_{3} \land$ points in $\partial C (R)$ form a triangle of angles equal to $30^{\circ}$ , $60^{\circ}$ , and $90^{\circ}$
	$𝚕$	$\| \partial C_{↓}^{1} (R) \| \geq 2 \lor δ_{1} \leq δ_{0, 2}$
	$𝚖_{0}$	$\| {c (F)} \cap F \| = k$ , $k > 1$
	$𝚖_{1}$	$𝚖_{0} \land \| {c (R)} \cap R \| = k - 1$
$ℱ 2$	$𝚐_{0}$	$\| \partial C^{g} (R) \| = 1$
	$𝚐_{1}$	$𝚐_{0} \land \exists! g^{'} \in \partial C (R) : ∢ (g, c (R), g^{'}) = α$
	$𝚐_{2}$	$𝚐_{1} \land \exists g^{''} \in \partial C (R)$ antipodal to $g ’$
	$𝚏_{2}$	$(𝚖_{0} \Rightarrow 𝚖_{1}) \land 𝚜_{2} \land 𝚕$
$ℱ 3$	$𝚍_{0}$	$\partial C^{t} (R) = {r}$
	$𝚍_{1}$	$𝚍_{0} \land \exists f^{} \in F^{} : r = [c (F), f^{*}] \cap C^{t} (R)$
	$𝚍_{2}$	$C^{t} (R) \cap (r, μ (r)] \neq \emptyset$ , where $r = min_view (R_{η}^{\neg m})$
	$𝚏_{3}$	$(𝚖_{0} \Rightarrow 𝚖_{1}) \land 𝚐_{2}$
$ℱ 4$	$𝚚$	$\partial C (F) = F$ , $F$ without multiplicities, and $\| F \| - 1$ points of $F$ are on the same semi-circle
	$𝚒_{1}, \dots, 𝚒_{6}$	guards $g$ , $g^{'}$ and $g^{''}$ are detectable $\land R ∖ {g, g^{''}}$ is similar to $F ∖ {μ (g), μ (g^{''})}$
	$𝚏_{4}$	$\neg 𝚚 \land (𝚒_{1} \lor 𝚒_{2}) \lor 𝚚 \land (𝚒_{3} \lor 𝚒_{4} \lor 𝚒_{5} \lor 𝚒_{6})$
$ℱ 5$	$𝚋_{0}$	$R$ is symmetric
	$𝚋_{1}$	$\exists$ a reflection axis $ℓ$ for $R$ : $\| R \cap ℓ \| = 1$
	$𝚋_{2}$	$\exists$ a reflection axis $ℓ$ for $R$ : $\| R \cap ℓ \| \geq 2$ $\land$ at least two robots in $R \cap ℓ$ are not critical
	$𝚋_{3}$	$\exists$ a reflection axis $ℓ$ for $R$ : $\| R \cap ℓ \| = 2$ $\land$ exactly one robot in $R \cap ℓ$ is critical
	$𝚋_{4}$	$\exists$ a reflection axis $ℓ$ for $R$ : $\| R \cap ℓ \| = 3$ $\land$ exactly two robots in $R \cap ℓ$ are critical
	$𝚋_{5}$	$\exists$ a reflection axis $ℓ$ for $R$ : $\| R \cap ℓ \| = 2$ $\land$ both robots in $R \cap ℓ$ are critical
	$𝚎$	$R$ does not contain multiplicities
	$𝚣_{1}$	let $\partial C (R) = {r, r 1, r 2}$ with $r$ faraway robot, and let $t$ be the point on $C (R)$ closest to $r$ s.t. points $t$ , $r_{1}$ , and $r_{2}$ form a right-angled triangle: $\exists$ a reflection axis $ℓ$ for $R^{'} = R ∖ {r}$ that reflects $r_{1}$ to $r_{2}$ $\land$ $r$ belongs to the smallest arc of $C (R)$ between $ℓ$ and $t$ (excluded) $\land$ $R^{'} \cap ℓ = \emptyset$
	$𝚣_{2}$	$\exists r \in R$ : $\partial C_{↑}^{1} (R) = {r}$ $\land$ $R ∖ {r}$ is symmetric $\land$ [ either $𝚌$ or ( $\neg 𝚋_{0}$ $\land$ $\neg 𝚒_{2}$ $\land$ $d (c (R), r) < δ (C^{g} (R))$ $\land$ $\forall r^{'} \in \partial C (R), ∢ (r, c (R), r^{'}) \neq α$ )]
	$𝚞_{1}$	$\exists i > 0$ : $\partial C_{↑}^{i} (R) = {r^{(2)}}$ $\land$ $d (r^{(2)}, c (R)) = 1 / 2 [δ (C_{↑}^{i - 1} (R)) + δ (C_{↑}^{i + 1} (R))]$
	$𝚞_{2}$	$r^{(2)} \notin [t^{60}, t^{55}] \lor r^{(2)} = t^{x} \lor r^{(2)} = t^{55}$
	$𝚏_{5}$	$(𝚋_{0} \lor 𝚣_{1} \lor 𝚣_{2}) \land 𝚎$
*	$𝚠$	$R$ is similar to $F$

Table 2. Table 2: Each label on the first column specifies a different phase. In column ‘start’, for each phase it is specified the invariant that holds while a configuration belongs to the corresponding phase. In column ‘end’, it is specified the possible phases outside the considered one that can be reached or whether 𝚠 𝚠 \mathtt{w} may hold.

phase	start	end
$ℱ 1$	$\neg 𝚏_{2} \land \neg 𝚏_{3} \land \neg 𝚏_{4} \land \neg 𝚏_{5} \land \neg 𝚠$	$ℱ 2_{s} \lor ℱ 3_{s} \lor ℱ 4_{s} \lor ℱ 5_{s} \lor 𝚠$
$ℱ 2$	$𝚏_{2} \land \neg 𝚏_{3} \land \neg 𝚏_{4} \land \neg 𝚏_{5} \land \neg 𝚠$	$ℱ 3_{s} \lor ℱ 4_{s} \lor 𝚠$
$ℱ 3$	$𝚏_{3} \land \neg 𝚏_{4} \land \neg 𝚏_{5} \land \neg 𝚠$	$ℱ 4_{s}$
$ℱ 4$	$𝚏_{4} \land \neg 𝚏_{5} \land \neg 𝚠$	$𝚠$
$ℱ 5$	$𝚏_{5} \land \neg 𝚠$	$ℱ 1_{s} \lor ℱ 2_{s} \lor ℱ 4_{s} \lor 𝚠$

Table 3. Table 3: (left) Invariants and moves for all the sub-phases of ℱ 1 ℱ 1 \mathcal{F}1 . Each label on the first column specifies a different sub-phase to which a configuration belongs to. Then, with respect to each sub-phase, in the upper (shaded) side it is specified the invariant that the configuration satisfies at the beginning of the phase (start), and which sub-phase within ℱ 1 ℱ 1 \mathcal{F}1 can be reached (end). In the lower side, it is specified the corresponding move performed by the algorithm, and on the last column the possible phases outside ℱ 1 ℱ 1 \mathcal{F}1 that can be reached or whether 𝚠 𝚠 \mathtt{w} may hold. (right) Description of the moves performed by the algorithm in ℱ 1 ℱ 1 \mathcal{F}1 .

phase	start	end
$𝒜 1$	$𝚜_{+} \land 𝚕$	$𝒜_{s} \lor 𝒞_{s} \lor 𝒟_{s} \lor ℰ 1_{s}$
	$m_{1}$	$ℱ 4_{s} \lor 𝚠$
$𝒜 2$	$(𝚜_{+} \lor 𝚜_{3}) \land \neg 𝚕$	$𝒜_{s} \lor 𝒞_{s} \lor 𝒟_{s} \lor ℰ 1_{s}$
	$m_{2}$	$ℱ 4_{s} \lor 𝚠$
$ℬ$	$𝚜_{2} \land 𝚖_{0} \land \neg 𝚖_{1}$	$𝒞_{s} \lor 𝒟_{s}$
	$m_{3}$
$𝒞 1$	$𝚜_{3} \land 𝚝_{0} \land 𝚕$	$𝒞 2_{s} \lor 𝒟_{s} \lor ℰ 1_{s}$
	$m_{4}$	$ℱ 4_{s} \lor ℱ 5_{s} \lor 𝚠$
$𝒞 2$	$𝚜_{3} \land \neg 𝚝_{0} \land \neg 𝚝_{1} \land 𝚕 \land 𝚖_{0} \land \neg 𝚖_{1}$	$𝒟_{s}$
	$m_{5}$
$𝒟$	$𝚜_{3} \land 𝚝_{1} \land 𝚕 \land 𝚖_{0} \land \neg 𝚖_{1}$	$ℰ 1_{s}$
	$m_{6}$	$ℱ 3_{s}$
$ℰ 1$	$𝚜_{3} \land \neg 𝚝_{0} \land 𝚕 \land (𝚖_{0} \Rightarrow 𝚖_{1})$	$ℰ 2$
	$m_{1}$	$ℱ 2_{s} \lor ℱ 4_{s} \lor 𝚠$
$ℰ 2$	$𝚜_{2} \land \neg 𝚕 \land (𝚖_{0} \Rightarrow 𝚖_{1})$
	$m_{2}$	$ℱ 2_{s} \lor ℱ 4_{s} \lor 𝚠$

Table 4. Table 4: Invariants and moves for all the sub-phases of ℱ 2 ℱ 2 \mathcal{F}2 .

phase	start	end
$𝒢 1$	$\neg 𝚐_{0} \land (𝚌 \Rightarrow 𝚖_{1})$	$𝒢 2_{s}$
	$m_{7}$	$ℱ 3_{s} \lor ℱ 4_{s} \lor 𝚠$
$𝒢 2$	$𝚐_{0} \land \neg 𝚐_{1} \land (𝚌 \Rightarrow 𝚖_{1})$
	$m_{8}$	$ℱ 3_{s} \lor ℱ 4_{s}$
$ℋ$	$𝚌 \land \neg 𝚖_{0}$	$𝒢 2_{s}$
	$m_{9}$

Table 5. Table 5: Invariants and moves for all the sub-phases of ℱ 3 ℱ 3 \mathcal{F}3 .

phase	start	end
$ℳ$	$𝚍_{0} \land \neg 𝚍_{1}$	$𝒪_{s}$
	$m_{10}$
$𝒩$	$(𝚍_{0} \Rightarrow 𝚍_{1}) \land 𝚍_{2}$	$ℳ_{s} \lor 𝒪_{s}$
	$m_{11}$
$𝒪$	$(𝚍_{0} \Rightarrow 𝚍_{1}) \land \neg 𝚍_{2}$	$𝒩_{s} \lor 𝒪_{s}$
	$m_{12}$	$ℱ 4_{s}$

Table 6. Table 6: Invariants and moves for all the sub-phases of ℱ 4 ℱ 4 \mathcal{F}4 .

phase	start	end
$𝒫 1$	$\neg 𝚚 \land 𝚒_{1}$	$𝒫 2_{s}$
	$m_{13}$
$𝒫 2$	$\neg 𝚚 \land 𝚒_{2}$
	$m_{14}$	$𝚠$
$𝒬 1$	$𝚚 \land 𝚒_{3}$	$𝒬 2_{s} \lor 𝒬 3_{s}$
	$m_{15}$
$𝒬 2$	$𝚚 \land 𝚒_{4}$	$𝒬 3_{s}$
	$m_{16}$
$𝒬 3$	$𝚚 \land 𝚒_{5}$	$𝒬 4_{s}$
	$m_{17}$	$𝚠$
$𝒬 4$	$𝚚 \land 𝚒_{6}$
	$m_{13}$	$𝚠$

Table 7. Table 7: Invariants and moves for all the sub-phases of ℱ 5 ℱ 5 \mathcal{F}5 .

phase	start	end
$𝒯$	$𝚋_{0} \land \neg 𝚌 \land 𝚋_{1} \land \neg 𝚣_{1}$	$𝒰_{s} \lor 𝒲_{s}$
	$m_{18}$	$𝚠$
$𝒰$	$𝚣_{1}$
	$m_{19}$	$ℱ 1_{s} \lor 𝚠$
$𝒱 1$	$𝚋_{0} \land (\neg 𝚌 \lor \neg 𝚞_{1}) \land 𝚋_{2}$	$𝒲_{s}$
	$m_{20}$	$𝚠$
$𝒱 2$	$𝚋_{0} \land (\neg 𝚌 \lor \neg 𝚞_{2}) \land 𝚋_{3}$	$𝒲_{s}$
	$m_{21}$	$𝚠$
$𝒱 3$	$𝚋_{0} \land \neg 𝚌 \land 𝚋_{4}$	$𝒲_{s}$
	$m_{22}$	$𝚠$
$𝒱 4$	$𝚋_{0} \land \neg 𝚌 \land 𝚋_{5}$	$𝒱 2_{s}$
	$m_{23}$	$𝚠$
$𝒲$	$𝚣_{2} \land \neg 𝒱 1_{s} \land \neg 𝒱 2_{s}$
	$m_{24}$	$ℱ 1_{s} \lor ℱ 2_{s} \lor ℱ 4_{s}$

Equations4

α = \frac{1}{3} \cdot min {∢ (x, c (F), y) : x, y \in \partial C (F), x \neq = y} .

α = \frac{1}{3} \cdot min {∢ (x, c (F), y) : x, y \in \partial C (F), x \neq = y} .

G 1_{s} \lor G 2_{s} = \neg g_{1} \land (c \Rightarrow m_{1}) .

G 1_{s} \lor G 2_{s} = \neg g_{1} \land (c \Rightarrow m_{1}) .

Peer Reviews

No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.

Videos

No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.

Taxonomy

TopicsOptimization and Search Problems · Distributed systems and fault tolerance · Modular Robots and Swarm Intelligence

Full text

∎

11institutetext: S. Cicerone 22institutetext: Department of Information Engineering, Computer Science and Mathematics - University of L’Aquila, Via Vetoio, I–67100, L’Aquila, Italy. 22email: [email protected] 33institutetext: G. Di Stefano 44institutetext: Department of Information Engineering, Computer Science and Mathematics - University of L’Aquila, Via Vetoio, I–67100, L’Aquila, Italy. 44email: [email protected] 55institutetext: A. Navarra 66institutetext: Department of Mathematics and Computer Science, University of Perugia, Via Vanvitelli 1, I–06123, Perugia, Italy.

66email: [email protected]

Asynchronous Arbitrary Pattern Formation: the effects of a rigorous approach††thanks: The work has been supported in part by the European project

“Geospatial based Environment for Optimisation Systems Addressing Fire Emergencies” (GEO-SAFE), contract no. H2020-691161, and by the Italian National Group for Scientific Computation (GNCS-INdAM).

Serafino Cicerone

Gabriele Di Stefano

Alfredo Navarra

(Received: date / Accepted: date)

Abstract

Given any multiset $F$ of points in the Euclidean plane and a set $R$ of robots such that $|R|=|F|$ , the Arbitrary Pattern Formation ( $APF$ ) problem asks for a distributed algorithm that moves robots so as to reach a configuration similar to $F$ . Similarity means that robots must be disposed as $F$ regardless of translations, rotations, reflections, uniform scalings. Initially, each robot occupies a distinct position. When active, a robot operates in standard Look-Compute-Move cycles. Robots are asynchronous, oblivious, anonymous, silent and execute the same distributed algorithm. So far, the problem has been mainly addressed by assuming chirality, that is robots share a common left-right orientation. We are interested in removing such a restriction.

While working on the subject, we faced several issues that required close attention. We deeply investigated how such difficulties were overcome in the literature, revealing that crucial arguments for the correctness proof of the existing algorithms have been neglected. The systematic lack of rigorous arguments with respect to necessary conditions required for providing correctness proofs deeply affects the validity as well as the relevance of strategies proposed in the literature.

Here we design a new deterministic distributed algorithm that fully characterizes $APF$ showing its equivalence with the well-known Leader Election problem in the asynchronous model without chirality. Our approach is characterized by the use of logical predicates in order to formally describe our algorithm as well as its correctness. In addition to the relevance of our achievements, our techniques might help in revising previous results. In fact, it comes out that well-established results like [Fujinaga et al., SIAM J. Comp. 44(3) 2015], more recent approaches like [Bramas et al., PODC and SSS 2016] and ‘unofficial’ results like [Dieudonné et al., arXiv:0902.2851] revealed to be not correct.

Keywords:

Distributed Algorithms Mobile Robots Asynchrony Pattern Formation

1 Introduction

In distributed computing, one of the most studied problem is certainly the Pattern Formation ( $PF$ ) which is strictly related to Consensus and Leader Election. Given a team of robots (agents or entities) and a geometric pattern in terms of points in the plain with respect to an ideal coordinate system, the goal is to design a distributed algorithm that works for each robot to guide it so that eventually all robots together form the pattern if possible. As the global coordinate system might be unknown to the robots, a pattern is declared formed as soon as robots are disposed similarly to the input pattern, that is regardless of translations, rotations, reflections, uniform scalings.

The $PF$ problem has been largely investigated in the last years under different assumptions. Here we refer to the standard Look-Compute-Move model. When active, a robot operates in Look-Compute-Move (LCM) cycles. In one cycle a robot takes a snapshot of the current global configuration (Look) in terms of robots’ positions according to its own coordinate system. Successively, in the Compute phase it decides whether to move toward a specific target or not, and in the positive case it moves (Move).

Different characterizations of the environment consider whether robots are fully-synchronous, semi-synchronous (cf. SY99 ; YS10 ; YUKY17 ) or asynchronous (cf. BCM16 ; DFSY15 ; FYOKY15 ; FPSW08 ; GM10 ):

•

Fully-synchronous (FSync): The activation phase (i.e. the execution of a Look-Compute-Move cycle) of all robots can be logically divided into global rounds. In each round all the robots are activated, obtain the same snapshot of the environment, compute and perform their move.

•

Semi-synchronous (SSync): It coincides with the FSync model, with the only difference that not all robots are necessarily activated in each round.

•

Asynchronous (Async): The robots are activated independently, and the duration of each phase is finite but unpredictable. As a result, robots do not have a common notion of time. Moreover, they can be seen while moving, and computations can be made based on obsolete information about positions.

One of the latest and most important results for $PF$ , see FYOKY15 , solves the problem for robots endowed with few capabilities. Initially, no robots occupy the same location, and they are assumed to be:

•

Dimensionless: modeled as geometric points in the plane;

•

Anonymous: no unique identifiers;

•

Autonomous: no centralized control;

•

Oblivious: no memory of past events;

•

Homogeneous: they all execute the same deterministic algorithm;

•

Silent: no means of direct communication;

•

Asynchronous: there is no global clock that synchronizes their actions;

•

Non-rigid: robots are not guaranteed to reach a destination within one move;

•

Chiral: they share a common left-right orientation.

Since Async robots are considered, it is worth to remark they are activated independently, and the duration of each phase is finite but unpredictable, i.e., the time between Look, Compute, and Move phases is finite but unbounded. This is decided by an adversary for each robot and for each phase. As a result, robots do not have a common notion of time. Moreover, they can be seen while moving even though a robot does not perceive whether other robots are moving or not. It follows that the computations and hence the moves performed by robots can be made on the base of obsolete information about robots’ positions as these can refer to outdated perceptions. In fact, due to asynchrony, by the time a robot takes a snapshot of the configuration, this might have drastically changed when it starts moving. The adversary determining the Look-Compute-Move cycles timing is assumed to be fair, that is, each robot becomes active and performs its cycle within finite time and infinitely often.

During the Look phase, robots can perceive multiplicities, that is whether a same point is occupied by more than one robot, and how many robots compose a multiplicity.

The distance traveled within a move is neither infinite nor infinitesimally small. More precisely, the adversary has also the power to stop a moving robot before it reaches its destination, but there exists an unknown constant $\nu>0$ such that if the destination point is closer than $\nu$ , the robot will reach it, otherwise the robot will be closer to it of at least $\nu$ . Note that, without this assumption, an adversary would make impossible for any robot to ever reach its destination.

The main open question left in FYOKY15 within Async concerns the resolution of the more general $PF$ problem in the described setting but without chirality. So far, the only sub-problems solved within the weakest setting are the gathering problem CFPS12 , where all robots must move toward a common point, and the circle-formation problem FPSV14 ; MV16 , where $n$ robots must form a regular $n$ -gon.

Another interesting question represents the so-called Arbitrary Pattern Formation ( $APF$ ), that is, from which initial configurations it is possible to form any pattern? In DPV10 , $APF$ has been solved for a number $n\geq 4$ of asynchronous robots with chirality but excluding patterns with multiplicities. The answer to this restricted setting for $APF$ provided a nice characterization of the problem that was shown to be equivalent to Leader Election within the same set of assumptions. In particular, the configurations from which the proposed algorithm could output any pattern (without multiplicities) are the so-called leader configurations. These are configurations of robots from which it is possible to elect a leader. Clearly, if one provides an algorithm to solve $APF$ for some input configurations, then also $PF$ can be solved for all such configurations.

The contribution of this work is threefold: (1) to provide counter-examples to the correctness of algorithms for the $PF$ and $APF$ problems proposed in well-established and in recent papers; (2) to solve $APF$ (and consequently $PF$ ) with any number of asynchronous robots without chirality when the initial configurations are leader configurations, hence generalizing the equivalence of $APF$ and Leader Election also within our setting for any number of robots without chirality, including patterns with multiplicities; (3) to use a rigorous approach for handling problems in the asynchronous environment able to provide accurate arguments to state the correctness of the designed algorithms.

1.1 Motivation and related work

Starting with CDN16 , we kept on studying $PF$ without chirality but we faced several issues mainly related to asynchrony that required close attention. Since the main difficulties were not depending on the lack of chirality, we deeply investigated how such problems were overcome in the literature. In particular, we closely explored FYOKY15 – that can be considered as a milestone in the advancement of $PF$ study within Async – and we found that surprisingly our difficulties with $PF$ have not been addressed at all. Actually, we are able to devise fundamental counter-examples to the correctness of FYOKY15 . We contacted the authors of FYOKY15 and they confirmed us that the provided counter-example and most importantly the rationale behind it represents a main issue that requires deep investigation.

In order to catch a first idea of our findings, it is necessary to understand what should be carefully analyzed when dealing with asynchrony and robots that do not share a common coordinate system. The first problem arising when approaching $PF$ is where robots should form the pattern $F$ , that is how to embed $F$ on the area occupied by robots so as each point of $F$ can be seen as a ‘landmark’. Both in FYOKY15 and in our strategy, the algorithms are logically divided into phases. Usually the first phase is devoted to move a few of robots in such a way the embedding becomes easy. Then, there is an intermediate phase where all robots but those placed in the first phase are moved in order to form $F$ . Finally there is a third phase where the ‘special’ robots are moved to finalize $F$ . While in the second phase it is relatively easy to move robots to partially form $F$ because the embedding is well defined, this is not the case for the other two phases. For instance, if not carefully managed, it may happen that during a move the configuration changes its membership to a different phase, especially from the first phase. In order to provide the correctness proof of an algorithm under the sketched scheme, it is not sufficient to define some invariants that exclusively define the membership of a configuration to a phase (as sometimes has been done in the literature), but it is mandatory to prove that the defined moves cannot change the membership of the current configuration while robots are moving. In the Async model a change of membership is possible, if not carefully considered, as robots can be seen while moving. If such a situation happens, other robots ‘believing to be in a different phase’ may start moving and then the situation becomes sometimes intractable or even they prevent the algorithm to accomplish the $PF$ . Unfortunately this is the case for FYOKY15 , where the authors neglected such situations, and we can provide counter-examples where their algorithm fails. It is worth to remark, that the systematic lack of arguments with respect to such events completely invalidates the correctness and the relevance of the strategy proposed in FYOKY15 . Moreover, it is not possible to recover the algorithm with some easy patches as it requires structural intervention.

On this base, and in order to better understand the problem, we started restricting our attention to the case where initial configurations are asymmetric. An asymmetric configurations of robots is meant as a disposal on the Euclidean plane not admitting axis of symmetries nor rotations. Even if solving this ‘restricted’ version of the $PF$ problem may be perceived to be an easy task, the analysis of the literature revealed the following state of the art:

•

A first study can be found in GM10 . The authors provide a distributed algorithm that can form many patterns, subject to significant restrictions in the input configurations. One of such constraints almost coincides with asymmetry, but it is not the only one. Unfortunately, the way it is presented does not allow to exactly specify from which kind of configurations robots can start and which patterns are formable.

•

A formal characterization that includes asymmetric configurations has been conducted in DPV10-2 ; DPV10 . Actually the problem considered is $APF$ and the authors show the equivalence of $APF$ and the Leader Election problems under some circumstances. Still the results are based on chirality for a number of robots greater than or equal to 4. Moreover, the patterns considered are not exactly ‘arbitrary’ because they do not allow multiplicities, that is the points of any given pattern to be formed by $n$ robots compose a set of $n$ distinct elements. In our study, as well as in FYOKY15 , patterns may allow multiplicities, and this deeply affects the design of resolution algorithms.

•

Other approaches found in the literature to solve $PF$ are probabilistic, see BT15 ; BT16b ; YY14 . In particular, in BT15 ; BT16b the authors claim to solve $APF$ (and hence $PF$ ) with a strategy that is divided into two main phases: the first phase is probabilistic and is used to make asymmetric the input configuration; the second phase is deterministic and solves $PF$ from asymmetric configurations even without assuming any form of multiplicity detection. Basically, the strategy in the second phase solves $APF$ from asymmetric configurations. Unfortunately, the proposed strategy suffers of some lack of rigorous arguments supporting the correctness of the proposed algorithm. We are able to provide counter-examples that affect the rationale behind the proposed strategy, and then also in this case the proposed algorithm is not correct. An extended version of those papers can be found in BT16 .

•

Further ‘unofficial’ results can be found in CGJM14 ; DPVarx09 . Concerning CGJM14 , not all patterns are considered but only asymmetric ones. Concerning DPVarx09 , the authors claim to solve $APF$ by slightly modifying the results of DPV10 . There are three main issues about this paper. First of all, the main proof is given by a sketchy description, whereas we show how formal arguments are extremely necessary in this context. In fact, we are able to provide counter-examples that invalidate the proposed strategy, hence discovering a further algorithm which is not correct.

Secondly, the patterns considered in DPVarx09 do not allow multiplicities. In our study, as well as in FYOKY15 , patterns may allow multiplicities, and this deeply affects the design of resolution algorithms. In fact, also the gathering becomes a sub-problem of $PF$ where it is required to solve the so-called point formation. It is well-known how difficult is the resolution of the gathering problem CFPS12 . Finally, the minimum number of robots required by the proposed algorithm is $5$ . Note that in robot based computing systems, instances with small numbers of robots usually require very different and non-trivial arguments with respect to the general algorithm. This is the case for instance for the square formation MV16 and for gathering both in the Euclidean plane CFPS12 or in discrete rings DDN12tr ; DDN11 ; DMN15 ; BPT16 and grids DDKN12 .

Such an analysis along with a useful interaction with anonymous referees, motivated us to study not only asymmetric configurations but also leader configurations, in order to see whether $APF$ is equivalent to Leader Election also in our more general setting.

Nevertheless, our investigation inspired the third aim of this paper, that is to provide a rigorous approach for designing algorithms in Async. The need of new ways of expressing algorithm in Async is widely recognized. For instance, in BLP16 ; DBO17 ; MPST14 a formal model to describe mobile robot protocols under synchrony and asynchrony assumptions is provided. So far, these only concern robots operating in a discrete space i.e., with a finite set of possible robot positions.

1.2 Our results

We provide fundamental arguments affecting the correctness of FYOKY15 , BT15 ; BT16b and DPVarx09 . The relevance of our finding is given not only by the fact that we re-open the $PF$ and the $APF$ problems in some Async contexts, but also that possibly other tasks may suffer of the same arguments. It follows that problems considered already solved, like for $PF$ in the case of robots with chirality or like $APF$ in the case of robots without chirality, must be carefully revised. We show that the resolution of such problems might be really difficult, especially for providing correctness proofs with an adeguate level of formalism.

We fully characterize the $APF$ problem (and hence $PF$ ) from initial leader configurations, that is for any number of robots we can form any pattern, including symmetric ones and those with multiplicities. Since we do not assume chirality, symmetries to be considered for the robots and for the patterns are not only rotations as in FYOKY15 ; DPV10-2 ; DPV10 , but also reflections and symmetries due to multiplicities. The proposed algorithm shows the equivalence between $APF$ and Leader Election within our setting, generalizing previous results in terms of number of robots that now can be any, in terms of robots capability as we removed the chirality assumption, and in terms of formable patterns that now can include multiplicities and symmetries. Our main result can be stated as follows:

Theorem 1.1

Let $R$ be an initial configuration of Async robots without chirality. $APF$ is solvable from $R$ if and only if Leader Election is solvable in $R$ .

To reach this result, we design our algorithm according to a rigorous approach. Such an approach is based on basic predicates that composed in a Boolean logic way provides all the invariants needed to be checked during the execution of the algorithm. Differently to previous approaches used in the literature, we make a careful use of invariants to describe properties holding during the movements of robots. As already observed, the technique of specifying formal invariants to define the different phases of an algorithm is something that other authors have adopted. However in this paper the level of details reached to describe every single move and the corresponding trajectory is something new. In turn, this implies that for each single move the algorithm may require three different invariants (to describe properties at the start, during, and at the end of the move). Hence, our algorithm is organized as a set of moves, each associated to up to three invariants. Moves are grouped and associated to a phase, where a phase represents a general task of the algorithm. Summarizing, the approach leads to a greater level of detail that provides us rigorous arguments to state the correctness of the algorithm. This approach itself represents a result of this paper, as it highlights crucial properties in Async contexts that so far have been underestimate in the literature.

As further remarks, it is worth to note that differently from FYOKY15 , we do not require that the local coordinate system specific of a single robot remains the same among different Look-Compute-Move cycles. Moreover, the trajectories traced during a move specified by our algorithm are always well-defined either as straight lines or as rotations along specified circles.

Finally, our algorithm does not require to specify the pattern to be formed as a set of coordinates in a Cartesian system. There are two possible options. As in GM10 , the pattern can be specified as a list of ratios of its sides and angles between the sides. Another option is to provide the list of distances among all points. In both cases, each robot can locally evaluate a possible set of points consistent with the input and its local coordinate system. Clearly, it turns out that doing this way robots do not share the same information about the pattern but each one acquires its own representation.

1.3 Outline

In the next section, some further details on the considered robots’ model are provided. In Section 3, useful notation and definitions are introduced. Section 4 provides a first description of our strategy to solve $APF$ in Async without chirality and starting from initial leader configurations. Section 5 contains a description of some counter-examples about previous strategies for $PF$ and $APF$ in Async, hence re-opening some of these problems. Section 6, provides our new distributed algorithm. It is given in terms of various sub-phases where different moves are performed. The correctness of the algorithm is given in Section 7. Finally, Section 8 concludes the paper.

2 Robot Model

The robot model is mainly borrowed from FYOKY15 and CDN16 . We consider a system composed by a set $\mathcal{R}$ of $n$ mobile robots. Let $\mathbb{R}$ be the set of real numbers, at any time the multiset $R=\{r_{1},r_{2},\ldots,r_{n}\}$ , with $r_{i}\in\mathbb{R}^{2}$ , contains the positions of all the robots.

We arbitrarily fix an $x$ - $y$ coordinate system $Z_{0}$ and call it the global coordinate system. A robot, however, does not have access to it: it is used only for the purpose of description, including for specifying the input. All actions taken by a robot are done in terms of its local $x$ - $y$ coordinate system, whose origin always indicates its current position. Let $r_{i}(t)\in\mathbb{R}^{2}$ be the location of robot $r_{i}$ (in $Z_{0}$ ) at time $t$ . Then a multiset $R(t)=\{r_{1}(t),r_{2}(t),\ldots,r_{n}(t)\}$ is called the configuration of $R$ at time $t$ (and we simply write $R$ instead of $R(t)$ when we are not interested in any specific time).

A robot is said to be stationary in a configuration $R(t)$ if at time $t$ it is:

•

inactive, or

•

active, and:

–

it has not taken the snapshot yet;

–

it has taken snapshot $R(t)$ ;

–

it has taken snapshot $R(t^{\prime})$ , $t^{\prime}<t$ , which leads to a null movement.

A configuration $R(t)$ is said to be stationary111The definition of stationary robot provided in FYOKY15 is slightly different but also inaccurate. In fact, it does not catch the third scenario about active robots described by our definition. If removing such a case, no configuration might be declared stationary during an execution. Similarly, the definition of static robot from BT16b does not describe for instance the case where a robot is not moving but has already performed the Look phase. if all robots are stationary in $R(t)$ .

If two or more robots occupy the same position, then there is an element $r\in R$ occurring more than once. In such a case $r$ is said to belong to (or compose) a multiplicity.

Definition 1

A configuration $R$ is said initial if it is stationary and all elements in $R$ are distinct, that is, no multiplicity occurs.

Each robot $r_{i}$ has a local coordinate system $Z_{i}$ , where the origin always points to its current location. Let $Z_{i}(p)$ be the coordinates of a point $p\in\mathbb{R}^{2}$ in $Z_{i}$ . If $r_{i}$ takes a time interval $[t_{0},t_{1}]$ for performing the Look phase, then it obtains a multiset $Z_{i}(R(t))=\{Z_{i}(r_{1}(t)),Z_{i}(r_{2}(t)),...,Z_{i}(r_{n}(t))\}$ for some $t\in[t_{0},t_{1}]$ , where $Z_{i}(r_{i}(t))=(0,0)$ . That is, $r_{i}$ has the (strong) multiplicity detection ability and can count the number of robots sharing a location. More generally, if $P$ is a multiset of points, for any $x$ - $y$ coordinate system $Z$ , by $Z(P)$ we denote the multiset of the coordinates $Z(p)$ in $Z$ for all $p\in P$ .

Let $\{t_{i}:i=0,1,\ldots\}$ be the set of time instants at which a robot takes the snapshot $R(t_{i})$ during the Look phase. Without loss of generality, we assume $t_{i}=i$ for all $i=0,1,\ldots$ . Then, an infinite sequence $\mathbb{E}:R(0),R(1),\ldots$ is called an execution with an initial configuration $I=R(0)$ that by definition is stationary and without multiplicities. Actually, depending on the algorithm, multiplicities may be created in $R(i)$ , with $i>0$ .

Let $P_{1}$ and $P_{2}$ be two multisets of points: if $P_{2}$ can be obtained from $P_{1}$ by translation, rotation, reflection, and uniform scaling, then $P_{2}$ is similar to $P_{1}$ . Given a pattern $F$ expressed as a multiset $Z_{0}(F)$ , an algorithm $A$ forms $F$ from an initial configuration $I$ if for any execution $\mathbb{E}:R(0)(=I),R(1),R(2),\ldots$ , there exists a time instant $i>0$ such that $R(i)$ is similar to $F$ and no robots move after $i$ , i.e., $R(t)=R(i)$ hold for all real numbers $t\geq i$ .

Unlike the initial configuration, in general, not all robots are stationary in $R(i)$ when $i>0$ , but at least one robot that takes the snapshot $R(i)$ is stationary by definition. Whether or not a given configuration $R$ is stationary (or a robot is stationary at $R$ ) depends not only on $R$ but also on the execution history, in general. Let $\mathbb{E}:R(0),R(1),\ldots,R(f)$ and $\mathbb{E}^{\prime}:R^{\prime}(0),R^{\prime}(1),\ldots$ be two executions, and assume $R(f)=R^{\prime}(0)$ . Then $\mathbb{E}\mathbb{E}^{\prime}:R(0),R(1),\ldots,R(f)(=R^{\prime}(0)),R^{\prime}(1),\ldots$ is always a correct execution for SSync (and hence for FSync) robots since $R(f)$ is stationary by the definition of SSync robots. However, this is not the case for Async robots, since in $\mathbb{E}^{\prime}$ , $R^{\prime}(0)$ is assumed to be stationary, but in $\mathbb{E}$ , $R(f)$ may not be; the transition from $R^{\prime}(0)$ to $R^{\prime}(1)$ may be caused by the Look of a robot $r$ which is moving at $R(f)$ and hence cannot observe $R(f)$ . If an algorithm can guarantee that $R(f)$ is stationary, like for SSync robots, then we can safely concatenate $\mathbb{E}$ and $\mathbb{E}^{\prime}$ to construct a legitimate execution even for Async robots. An execution fragment that starts and ends at a stationary configuration is called a phase.

Consider an execution of an algorithm $A$ , and assume that at a given time $t$ algorithm $A$ produces a stationary configuration $R(t)$ . As observed in the Introduction, $A$ should use some invariants to decide which move to apply to $R(t)$ . According to the invariants, a given move is then applied to a subset $S$ of robots in $R(t)$ in order to produce a new stationary configuration. In this general case, a phase is realized by the move, and we could say that the phase is a consequence of the invariants verified at $R(t)$ .

In order to provide the correctness proof for $A$ , it is not sufficient to define the invariants associated to a phase, but it is mandatory to prove that the defined moves do not affect the stationarity of robots not belonging to $S$ . In fact, if such a situation happens, robots not in $S$ may ‘believe to be in a different phase’ and hence may start moving (possibly producing intractable cases).

For addressing correctly this problem, we introduce the following definition of transition-safe algorithm.

Definition 2

Let $R$ be a configuration and $S\subseteq R$ be the robots allowed to move according to a move $m$ dictated by algorithm $A$ . Let $[t_{1},t_{2}]$ be any time interval in which some robots in $S$ are moving but at least one has not yet reached its target, and let $R^{\prime}$ be any configuration observed during $[t_{1},t_{2}]$ .

We say that $m$ is safe if in $R\textquoteright$ algorithm $A$ allows only robots in $S$ to move; $A$ is transition-safe if each move in $A$ is safe.

Note that, in the situation described by the above definition, if $R^{\prime}$ is stationary and has been obtained from $R$ by means of move $m$ , necessarily the adversary has stopped some moving robots in $S$ (while the other moving robots have reached their targets). From there, if $A$ is transition-safe then either move $m$ is again performed by robots in $S$ or still robots in $S$ move according to a move $m^{\prime}\neq m$ (possibly toward different targets).

3 Notation and basic properties

Given two distinct points $u$ and $v$ in the Euclidean plane, let $d(u,v)$ denote their distance, let $\mathit{line}(u,v)$ denote the straight line passing through these points, and let $(u,v)$ ( $[u,v]$ , resp.) denote the open (closed, resp.) segment containing all points in $\mathit{line}(u,v)$ that lie between $u$ and $v$ . The half-line starting at point $u$ (but excluding the point $u$ ) and passing through $v$ is denoted by $\mathit{hline}(u,v)$ . We denote by $\sphericalangle(u,c,v)$ the angle centered in $c$ and with sides $\mathit{hline}(c,u)$ and $\mathit{hline}(c,v)$ . The angle $\sphericalangle(u,c,v)$ is measured from $u$ to $v$ in clockwise or counter-clockwise direction, the measure is always positive and ranges from [math] to less than $360$ degrees, and the direction in which it is taken will be clear by the context.

Given an arbitrary multiset $P$ of points in $\mathbb{R}^{2}$ , $C(P)$ and $c(P)$ denote the smallest enclosing circle of $P$ and its center, respectively. Let $C$ be any circle concentric to $C(P)$ . We say that a point $p\in P$ is on $C$ if and only if $p$ is on the circumference of $C$ ; $\partial C$ denotes all the points of $P$ that are on $C$ . We say that a point $p\in P$ is inside $C$ if and only if $p$ is in the area enclosed by $C$ but not in $\partial C$ ; $\mathit{int}(C)$ denotes all the points inside $C$ . The radius of $C$ is denoted by $\delta(C)$ . The smallest enclosing circle $C(P)$ is unique and can be computed in linear time M83 . A useful characterization of $C(P)$ is expressed by the following property.

Property 1

Welz91 $C(P)$ passes either through two of the points of $P$ that are on the same diameter (antipodal points), or through at least three points. $C(P)$ does not change by eliminating or adding points to $\mathit{int}(P)$ . $C(P)$ does not change by adding points to $\partial C(P)$ . However, it may be possible that $C(P)$ changes by either eliminating or changing positions of points in $\partial C(P)$ .

Given a multiset $P$ , we say that a point $p\in P$ is critical if and only if $C(P)\neq C(P\setminus\{p\})$ 222Note that in this work we use operations on multisets.. It easily follows that if $p\in P$ is a critical point, then $|\partial C(P)\cap\{p\}|=1$ .

Property 2

CieliebakP02 If $|\partial C(P)|\geq 4$ then there exists at least one point in $\partial C(P)$ which is not critical.

Given a multiset $P$ , consider all the concentric circles that are centered in $c(P)$ and with at least one point of $P$ on them: $C_{\uparrow}^{i}(P)$ denotes the $i$ -th of such circles, and they are ordered so that by definition $C_{\uparrow}^{0}(P)=c(P)$ is the first one, $C(P)$ is the last one, and the radius of $C_{\uparrow}^{i}(P)$ is greater than the radius of $C_{\uparrow}^{j}(P)$ if and only if $i>j$ . Additionally, $C_{\downarrow}^{i}(P)$ denotes one of the same concentric circles, but now they are ordered in the opposite direction: $C_{\downarrow}^{0}(P)=C(P)$ is the first one, $c(P)$ by definition is the last one, and the radius of $C_{\downarrow}^{i}(P)$ is greater than the radius of $C_{\downarrow}^{j}(P)$ if and only if $i<j$ .

The radius of three of such circles will play a special role in the remainder: $\delta_{0}(P)=\delta(C_{\downarrow}^{0}(P))$ , $\delta_{1}(P)=\delta(C_{\downarrow}^{1}(P))$ , and $\delta_{2}(P)=\delta(C_{\downarrow}^{2}(P))$ (with $\delta_{1}$ and $\delta_{2}$ equal to zero when the corresponding circles do not exist).

Definition 3

Let $R$ be a configuration. We define $\delta_{0,1}=(\delta_{0}(R)+\delta_{1}(R))/2$ and $\delta_{0,2}=(\delta_{0}(R)+\delta_{2}(R))/2$ , and we denote by $C^{0,1}(R)$ and $C^{0,2}(R)$ the circles centered in $c(R)$ and with radii $\delta_{0,1}$ and $\delta_{0,2}$ , respectively.

Definition 4

Let $R$ be a configuration and $F$ a pattern. Assuming $C(R)=C(F)$ , let $d=\delta(C_{\uparrow}^{1}(F))$ . The guard circle $C^{g}(R)$ and the teleporter circle $C^{t}(R)$ are defined as the circles centered in $c(R)$ of radii equal to $d/2^{i}$ and $d/2^{(i-1)}$ , respectively, with $i>1$ being the minimum integer such that the following conditions hold:

•

$\mathit{int}(C^{g}(R))\setminus c(C^{g}(R))=\emptyset$ ;

•

$|\mathit{int}(C^{t}(R))\setminus\mathit{int}(C^{g}(R))|\leq 1$ ;

•

$|\partial C^{t}(R)|\leq 1.$

Circles $C^{g}(R)$ and $C^{t}(R)$ are not defined for any configuration. For a visualization see Figure 1. Circle $C^{g}(R)$ will be used by our algorithm as the place where a specific robot $g$ is moved in order to establish a common reference coordinate system by which robots can embed $F$ on the area occupied by robots. Circle $C^{t}(R)$ , which is larger than $C^{g}(R)$ , represents the place closest to $c(R)$ where a robot deviates in case its trajectory should traverse $C^{g}(R)$ . Doing so, no robots can be confused with $g$ .

Definition 5

Let $F$ be a pattern, the reference angle $\alpha$ is defined as the following value:

[TABLE]

Such a reference angle will be used to correctly place robot $g$ on $C^{g}(R)$ during the formation of pattern $F$ .

3.1 View of a point and symmetries

We now introduce the concept of view of a point in the plane; it can be used by robots to determine whether a configuration $R$ and/or a pattern $F$ is symmetric or not.

Given a set of robots $\mathcal{R}$ , the distance $d(r,s)$ between two robots $r$ , $s\in\mathcal{R}$ is the length of the segment connecting their positions in the plane. A map $\varphi:\mathcal{R}\rightarrow\mathcal{R}$ is called an isometry or distance preserving if for any $r,s\in\mathcal{R}$ one has $d(\varphi(r),\varphi(s))=d(r,s)$ . If $\mathcal{R}$ admits only the identity isometry, then $\mathcal{R}$ is said asymmetric, otherwise it is said symmetric. These definitions naturally extend to the corresponding configuration $R$ of robots in $\mathcal{R}$ , and in general to a generic multiset of points $P$ . Notice that, whenever a configuration (or a pattern) contains a multiplicity, then it is symmetric, no matter where the multiplicity is. In fact, two distinct robots (or target points of a pattern) in the multiplicity can be always mapped to each other.

Let $P$ be a generic multiset of points. For $p\in P$ , with $p\neq c(P)$ , we denote by $V^{+}(p)$ the counter-clockwise view of $P$ computed from $p$ . Essentially, $V^{+}(p)$ is a string whose elements are the polar coordinates of all points in $P$ . The elements in $V^{+}(p)$ are arranged as follows: first $p$ , then in order and starting from $c(P)$ all the points in the ray $\mathit{hline}(c(P),p)$ , and finally all the points in the other rays, with rays processed in counter-clockwise fashion. Similarly, $V^{-}(p)$ denotes the clockwise view of $P$ computed from $p$ . By assuming a lexicographic order for polar coordinates, the view of $p$ is defined as $V(p)=\min\{V^{+}(p),V^{-}(p)\}$ .

If $c(P)\in P$ then $c(P)$ is said the point in $P$ of minimum view, otherwise any $p=\arg\!\min\{V(p^{\prime}):p^{\prime}\in P\}$ is said of minimum view in $P$ . Given $P$ and $P^{\prime}\subseteq P$ , we use the notation $\textit{min\_view}(P^{\prime})$ to denote any point $p$ with minimum view in $P^{\prime}$ .

The possible symmetries that $P$ can admit are reflections, rotations and those due to multiplicities. $P$ admits a reflection if and only if there exist two points $p,q\in P$ , $p,q\neq c(P)$ , not necessarily distinct, such that $V^{+}(p)=V^{-}(q)$ ;333When chirality can be exploited, reflections can be ignored as $V^{+}(p)$ can be always discriminated from $V^{-}(q)$ . $P$ admits a rotation if and only if there exist two distinct points $p,q\in P$ , $p,q\neq c(P)$ , such that $V^{+}(p)=V^{+}(q)$ . It follows that if $P$ is asymmetric then there exists a unique multipoint with minimum view. The above properties can be exploited by robots to detect whether the observed configuration during the Look phase is symmetric or not. When $P$ is symmetric, in general, it cannot be guaranteed the existence of a single point of minimum view. However, if $P$ admits exactly one axis of reflection $\ell$ with $P\cap\ell\neq\emptyset$ and at least a single point on $\ell$ , then among all the single points on $\ell$ there exists one of minimum view (otherwise $P$ would admit another axis of reflection). Similarly, if $P$ admits a rotation with $c(P)\in P$ and $c(P)$ is a single point, then $c(P)$ can be uniquely determined. In all such cases basically a leader can be elected in $P$ .

Definition 6

A configuration $R$ is said a leader configuration if there exists a robot $r\in R$ such that for each isometry $\varphi$ , $\varphi(x)=x$ .

In this work we assume any initial configuration $R(0)$ to be a leader configuration. In Figure 2 relationships among different kinds of configurations are shown.

We now redefine the concept of clockwise (and hence of counter-clockwise) direction for a multiset of points $P$ so as to make it independent of a global coordinate system.444Indeed, this is not necessary when chirality is assumed. If $P$ is asymmetric and $p=\textit{min\_view}(P\setminus c(P))$ , then the direction used to compute $V(p)$ during the analysis of all the rays starting from $c(P)$ is the clockwise direction of $P$ . If $P$ is symmetric, there might be many multipoints of minimum view. Symmetries we take care of are of three types: rotations, reflections and those due to multiplicities. If $P$ is reflexive, any direction can be assumed as the clockwise direction of $P$ since they are indistinguishable. In any other case the direction used to compute $V(p)$ from any point $p\neq c(P)$ of minimum view determines the clockwise direction of $P$ .

We can now apply the redefined concept of clockwise direction to a configuration $R$ and/or a pattern $F$ . For instance, in Figure 3. $(a)$ , the multiset $R$ is asymmetric, hence its clockwise direction coincides with that used to compute $V(r)$ , with $r=\textit{min\_view}(R)$ ; whereas in Figure 3. $(b)$ , the set $F$ is rotational and reflexive, hence its clockwise direction does not distinguish a left-right orientation.

4 The strategy

In this section, we provide a general description of the strategy underlying our algorithm for the resolution of $APF$ starting from initial leader configurations. It is based on a functional decomposition approach: the problem is divided into five sub-problems denoted as $\mathtt{RefSys}$ (Reference System), $\mathtt{ParForm}$ (Partial Formation), $\mathtt{Fin}$ (Finalization), $\mathtt{SymBreak}$ (Symmetry Breaking), and $\mathtt{Membership}$ . For each sub-problem but $\mathtt{Membership}$ an algorithm is provided. Each algorithm is defined in a way that its execution consists of a sequence of phases, whereas $\mathtt{Membership}$ crosses different phases. The whole strategy is then realized by composing the algorithms of each phase.

We now provide a high-level description of the four sub-problems.

Problem $\mathtt{RefSys}$ : It concerns the main difficulty arising when the pattern formation problem is addressed: the lack of a unique embedding of $F$ on $R$ that allows each robot to uniquely identifying its target (the final destination point to form the pattern).555In the literature, this is sometime realized by inducing a common coordinate system. This method can be effective only if $F$ is specified by coordinates and not by distances. In particular, $\mathtt{RefSys}$ can be described as the problem of moving some (minimal number of) robots into specific positions such that they can be used by any other robot as a common reference system. Such a reference system should imply a unique mapping from robots to targets, and should be maintained along all the movements of robots (except for the finalization phase, where the algorithm moves the robots forming the reference system).

Our strategy solves $\mathtt{RefSys}$ by using three robots (called guards). Such guards are positioned as described in Figure 1: the boundary guards are denoted as $g^{\prime}$ and $g^{\prime\prime}$ and are two antipodal robots on $C(R)$ , the internal guard is denoted as $g$ and is the unique robot on $C^{g}(R)$ (the guard circle). The internal guard is placed so that the angle $\sphericalangle(g,c(R),g^{\prime})$ is equal to $\alpha$ (the reference angle) whose value only depends on $F$ . Once $\mathtt{RefSys}$ is solved, each robot can use the guards to univocally determine its target position in the subsequent phases.

Notice that in specific cases the presence of $C^{g}(R)$ implies a refinement to the strategy defined for the sub-problem $\mathtt{RefSys}$ . In fact, in case of a multiplicity in $c(F)$ , all the robots in $c(R)$ (but one) must be placed before $C^{g}(R)$ (and hence the internal guard $g$ ) is used. Then, two distinct phases are designed for addressing $\mathtt{RefSys}$ :

•

phase $\mathcal{F}1$ , responsible for setting the external guards $g^{\prime}$ and $g^{\prime\prime}$ and, if required, for placing the multiplicity in $c(R)$ ;

•

phase $\mathcal{F}2$ , responsible for setting the internal guard $g$ .

Problem $\mathtt{ParForm}$ : This sub-problem concerns moving all the non-guards robots (i.e., $n-3$ robots) toward the targets. In our strategy, phase $\mathcal{F}3$ is designed to solve this problem. The difficulties in this phase are the following: (1) during the phase, the reference system must be preserved, (2) the movements must be performed by avoiding undesired multiplicities (collision-free routes), and (3) the movements must be performed without entering into the guard circle (routing through the teleporter circle).

Once the guards are placed, a unique robot per time is chosen to be moved toward its target: it is the one not on a target, closest to an unoccupied target, and of minimum view in case of tie. We are ensured that always one single robot $r$ will be selected since the configuration is maintained a leader configuration by the guards. The selected robot is then moved toward one of the closest targets until it reaches such a point. All moves must be performed so as to avoid the occurrence of undesired multiplicities; hence, it follows that sometimes the movements are not straightforward toward the target point but robots may deviate their trajectories. To this aim, the strategy makes use of a procedure called CollisionFreeMove designed ad-hoc for computing alternative trajectories. Moreover, according to the role of the internal guard $g$ , robots cannot enter into the circle $C^{g}(R)$ , otherwise the reference system induced by the guards is lost. The latter implies that, in case of a possible route passing through $C^{g}(R)$ , a robot avoids entering into the guard circle by deviating along the boundary of $C^{t}(R)$ (the teleporter circle); such a circle is centered in $c(R)$ and its radius is opportunely chosen so that in its interior there is only $g$ and in $\partial C^{t}(R)$ there is at most one robot.

Problem $\mathtt{Fin}$ : It refers to the so-called finalization phase, where the last three robots (the guards) must be moved to their targets to complete the formation of pattern $F$ . In our strategy, a phase $\mathcal{F}4$ is designed to solve this problem. This phase must face a complex task, since (1) moving the guards leads to the loss of the common reference system, and (2) moving without a common reference system makes hard to finalize the pattern formation.

In order to solve $APF$ , two additional problems must be faced. The first one concerns the case where the initial configuration in symmetric.

Problem $\mathtt{SymBreak}$ : Consider the case in which the initial leader configuration admits a symmetry while the pattern to be formed is asymmetric. In this situation it is mandatory for each solving algorithm to break the symmetry (i.e., to transform the initial configuration into an asymmetric one). In fact, without breaking the symmetry, any pair of symmetric robots may perform the same kind of movements and this prevent the arbitrary pattern formation. In our strategy, phase $\mathcal{F}5$ is used to address this sub-problem. It carefully moves the robot away from the center (in case of rotational symmetry) or one robot away from the unique axis (in case of reflections) until to obtain a stationary asymmetric configuration.

The main difficulties in this sub-problem are: (1) to avoid the formation of other kind of symmetries that could prevent the pattern formation (e.g., rotational symmetries), and (2) to correctly face the situation in which multiple steps are necessary to reach the target. In the latter case, the algorithm must recognize the obtained asymmetric configuration as a “configuration originated from a symmetric one where some robot has not yet reached a designed target”.

The second problem that crosses different phases is that described in the Introduction.

Problem $\mathtt{Membership}$ : This is the problem of avoiding that moves defined in the algorithm can change the membership of the current configuration while robots are moving. In fact, if such a situation happens, other robots believing to be in a different phase may start moving and then the situation becomes sometimes intractable or even they prevent the algorithm to accomplish the $PF$ (for instance, this is the case for the algorithm proposed in FYOKY15 ). In contrast, our strategy correctly addresses such a general problem by making use of two ingredients: safe moves and an ad-hoc procedure called StationaryMove. By using only moves that are safe, we obtain an algorithm which is transition-safe. This means that while robots are moving according to a move $m$ , only robots planned by $m$ can move until all robots correctly reached the target. By using Procedure StationaryMove, the algorithm can control each move that potentially could lead to non-stationary configurations, and hence to change the membership of the current configuration in an uncontrolled manner.666The technique adopted by means of Procedure StationaryMove is similar to the so-called cautious move in FPSV14 ; MV16 . Among others, Procedure StationaryMove exploits two main properties of our algorithms that are ensured during the most of the computations: there is at most one moving robot and $C(R(0))=C(R(t))=C(F)$ , $t>0$ . Such properties do not hold only in a few of the cases handled by phase $\mathcal{F}5$ . For instance, while solving $\mathtt{RefSys}$ , the embedding of $F$ into $R$ is not yet defined but the property that $C(R)=C(F)$ might be exploited. In fact, in some cases StationaryMove can force the moving robots crossing circles $C^{i}_{\downarrow}(F)$ to stop on such circles (hence potentially on a point of $F$ ). In this way, we force the configuration to become stationary while its membership may have changed, because perhaps an embedding of $F$ that leads to a different phase holds.

5 Counter-examples

In this section we provide fundamental arguments affecting the correctness of FYOKY15 , BT15 ; BT16b and DPVarx09 . It is worth to remark that our algorithm does not fix all the problems arisen in this section, however our technique might be helpful as a guideline for approaching such inconsistencies.

5.1 A counter-example to the correctness of the algorithm presented in FYOKY15

In this section, we provide a counter-example to the correctness of the algorithm $\mathit{FORM}$ presented in FYOKY15 to solve $PF$ assuming chirality. $\mathit{FORM}$ is designed to form a pattern $F$ (possibly with multiplicities) from an initial configuration $I$ (without multiplicity) each time $\rho(I)$ divides $\rho(F)$ , where $\rho(\cdot)$ is the parameter that captures the symmetricity of a multiset of points in the plane (cf. FYOKY15 ). Since the algorithm assumes robots empowered with chirality, function $\rho(\cdot)$ only measures the number of possible rotations that the input set of points admits. In fact, dealing with chirality overcomes managing reflections.

An execution of algorithm $\mathit{FORM}$ is partitioned into four phases called the pattern embedding ( $\mathit{EMB}$ ), the embedded pattern formation ( $\mathit{FOR}$ ), the finishing ( $\mathit{FIN}$ ), and the gathering ( $\mathit{GAT}$ ) phases. Phase $\mathit{EMB}$ embeds a given pattern $F$ , phase $\mathit{FOR}$ forms a substantial part $\tilde{F}$ of $F$ , and phase $\mathit{FIN}$ forms the remaining $F\setminus\tilde{F}$ of $F$ to complete the formation. Phase $\mathit{GAT}$ treats a pattern $F$ with multiplicities. These phases occur in this order, but some of them may be skipped.

For each of the phases, the authors present an algorithm and an invariant (i.e., predicate) that every configuration in the phase satisfies. Each invariant $\mathit{INV}$ is considered as a set too; a configuration $R$ satisfies $\mathit{INV}$ if and only if $R\in\mathit{INV}$ . Authors show that the defined invariants are pairwise disjoint, so exactly one of the algorithms implementing the phases is executed.

We start by briefly recalling both the invariant $\mathit{INV}_{\!\!\mathit{EMB}}$ and the algorithm $A_{\mathit{EMB}}$ for the first phase $\mathit{EMB}$ . For a formal understanding of the arguments below, the reader is invited to refer to FYOKY15 for the definition of $\ell$ -stable configurations, which in turn defines a set $\Lambda\subseteq\partial C(R)$ :

•

$\mathit{INV}_{\!\!\mathit{EMB}}=\neg(\mathit{INV}_{\!\!\mathit{FOR}}\vee\mathit{INV}_{\!\!\mathit{FIN}})$ . Informally, $\mathit{INV}_{\!\!\mathit{FOR}}$ is the set of the so called $\ell$ -stable configurations $R$ such that not all robots in $R\setminus\Lambda$ are located at their final positions in $F$ , while $\mathit{INV}_{\!\!\mathit{FIN}}$ is the set of configurations $R$ such that all robots in $R\setminus\Lambda$ are located at their final positions in $F$ .

Figure 4.(a) shows an initial configuration $I$ such that $I\in\mathit{INV}_{\!\!\mathit{EMB}}$ . Notice that the number of robots in $I$ is odd and $\rho(I)=1$ (since $I$ is asymmetric).

•

$A_{\mathit{EMB}}$ consists of three algorithms $A_{1}$ , $A_{2}$ , and $A_{3}$ , that are devoted to three different cases. Such algorithms are responsible of forming a $\ell$ -stable configuration. In particular $A_{1}$ is responsible for forming a $T$ -stable configuration, that is a configuration $R$ with exactly three robots in $\partial C(R)$ such that two of them are antipodal and the third one is a midpoint of them. Actually, $A_{1}$ is invoked when $|\partial C(R)|=2$ (and this is the case in $I$ ), and it moves an additional robot on $C(R)$ to get a $T$ -stable configuration.

From $I$ , algorithm $A_{1}$ moves robot $r_{7}$ straightly toward the point $[c(I),r_{7}]\cap C(I)$ .

Both the invariant $\mathit{INV}_{\!\!\mathit{FIN}}$ and the algorithm $A_{\mathit{FIN}}$ for the third phase $\mathit{FIN}$ are also necessary to build our counter-example. The finishing phase consists of different invariants depending on the kind of $\ell$ -stable configuration obtained in the first phase. In particular, when the $T$ -stable configuration has been built according to algorithm $A_{1}$ , $\mathit{INV}_{\!\!\mathit{FIN}}$ consists of three invariants $\mathit{INV}_{\!\!a}$ , $\mathit{INV}_{\!\!b}$ , and $\mathit{INV}_{\!\!c}$ , each associated to an algorithm that moves one of the three robots on $C(R)$ . What we need to explore for the counter-example is $\mathit{INV}_{\!\!c}$ .

•

A configuration $R$ satisfies $\mathit{INV}_{\!\!c}$ if and only if $R\setminus F=\{r\}$ and $r$ is on $\tau_{c}$ , where $\tau_{c}$ is a route designed as follows:

–

Let $R=\{r_{1},r_{2},\ldots,r_{n}\}$ , $F=\{f_{1},f_{2},\ldots,f_{n}\}$ be the set of robots and pattern points ordered according to their distance from $c(R)$ and $c(F)$ , respectively. Assume that $c(R)=c(F)$ and that $R\setminus\{r_{n}\}$ is similar to $F\setminus\{f_{n}\}$ . In such a case, pattern $F$ can be formed from $R$ by moving just $r_{n}$ toward $f_{n}$ along a route $\tau_{c}$ defined as any route such that, for any point $p$ on $\tau_{c}$ , still $r_{n}$ is the unique robot to be moved (toward $f_{n}$ ) to form $F$ from $R^{\prime}$ , where $R^{\prime}$ is constructed from $R$ by replacing $r_{n}$ with $p$ .

Concerning the algorithm executed when $\mathit{INV}_{\!\!c}$ holds, it simply requires that robot $r_{n}$ traces the path $\tau_{c}$ .

We have recalled all the details necessary to describe the counter-example. Assume now that algorithm $A_{1}$ is moving $r_{7}$ to form a $T$ -stable configuration, and consider the pattern $F$ depicted in Figure 4.(b) composed by the black and white circles. Notice that $\rho(F)=1$ as $F$ is asymmetric. Since $A_{1}$ moves robot $r_{7}$ straightly toward the point $[c(I),r_{7}]\cap C(I)$ , at a certain time it is possible that robot $r_{9}$ observes (during a Look phase) the configuration $R$ depicted in Figure 4.(c). This means that during the movement of $r_{7}$ , robot $r_{9}$ starts moving toward $f_{9}$ according to the algorithm associated to the invariant $\mathit{INV}_{\!\!c}$ . If this happens, the following properties hold:

there are two moving robots; 2. 2.

each move is due to a different phase; 3. 3.

if both moving robots reach their current targets – see Figure 4.(d) – then the obtained configuration $R^{\prime}$ admits $\rho(R^{\prime})=3$ and from there it would be impossible to form $F$ . In fact, as proved in FYOKY15 , $F$ is formable from $R^{\prime}$ if and only if $\rho(R^{\prime})$ divides $\rho(F)$ , but here $\rho(F)=1$ .

By personal communications, the authors of FYOKY15 confirmed us that the provided counter-example and most importantly the rationale behind it represents a main issue that requires deep investigation. While it is possibly easy to find a patch to the counter-example by slightly modifying algorithm $A_{1}$ , it is not straightforward to provide general arguments that can ensure the correctness of the whole algorithm. The main question left is: how can be guaranteed among all the phases that the membership of a configuration to a phase does not change while a robot is moving?

As we are going to show in the correctness section, our algorithm does not suffer of such arguments as it prevents such scenarios. Actually, the authors of FYOKY15 are working to devise an erratum to solve the posed problems. The current version of such an erratum is available from FYOKY17 .

5.2 A counter-example to the correctness of the algorithm presented in BT15 ; BT16b

In this section, we show how missing arguments affect the correctness of BT15 ; BT16b . After our personal communications to the authors, a new version BT16 _v3 (i.e., version v3 of BT16 ) of the extended paper BT16 _v2 has been recently released which includes the case discussed here. Still we believe it is important to report the counter-example as it highlights how the lack of formalism may cause the missing of possible instances.

Similarly to our approach, the algorithm in BT16 _v2 selects a specific robot $r_{1}$ closest to $c(R)$ to serve as what we call guard. Such a robot is moved in a specific placement in order to be always recognized as such until the very last step that finalizes the formation of the input pattern $F$ .

Another ingredient of the algorithm presented in BT16 _v2 we need to describe for our purpose is how the authors get rid of any form of multiplicity detection. When $F$ contains multiplicities, the robots first form a different pattern $\tilde{F}$ obtained by the robots from $F$ as follows: for each point $p$ of multiplicity $k$ , $k-1$ further points $p_{1}$ , $\ldots$ , $p_{k-1}$ are added such that the distance of each $p_{i}$ from $c(F)$ equals the distance of $p$ from $c(F)$ , $\sphericalangle(p,c(F),p_{i})<p_{i}$ , and $|p_{i}-p|=\frac{d}{4i}$ , with $d=\min_{f,f^{\prime}\in F}|f-f^{\prime}|$ .

For all algorithm phases except Termination, $\tilde{F}$ is used instead of $F$ . To execute the Termination phase, the configuration must be totally ordered (using the set of points, excluding multiplicity information), and at least one robot must be located at each point of $F$ (except maybe the smallest one). If there exists a robot $r\neq r_{1}$ not located at a point in $F$ , then $r$ chooses the closest point in $F$ as its destination and rotates toward it while remaining in its circle. The global coordinate system remains unchanged because $r_{1}$ does not move. Eventually, $r_{1}$ becomes the only robot not located at its destination, then it moves toward it, and the pattern $F$ is formed.

As shown in the description of our strategy, and in particular in phase $\mathcal{F}2$ , before creating our internal guard $g$ , we ensure to move $k-1$ robots in $c(R)$ if $F$ admits a multiplicity of $k$ elements in $c(F)$ . Such type of patterns (with a multiplicity in $c(F)$ ) are completely ignored in BT16 _v2. In such a case, the general description provided above does not apply. First of all, $\tilde{F}$ is not well-defined. Secondly, once $r_{1}$ is correctly placed, $k$ robots should be moved close or perhaps in $c(R)$ . This is not clear but in any case there will be robots getting closer to $c(R)$ with respect to $r_{1}$ , hence affecting the global coordinate system.

The lack of details as well as of a rigorous approach led the authors to design a partial algorithm that cannot cope with all possible input. It is worth to remark that in our strategy, the case of a multiplicity in $c(F)$ required a separate phase due to the arisen difficulties. The design of such a phase might not be easy since, in general, several robots must be moved at or close to $c(R)$ before the global coordinate system is established.

5.3 A counter-example to the correctness of the algorithm presented in DPVarx09

In DPV10 , the authors show the equivalence of $APF$ and Leader Election for a number of robots greater than or equal to 4, endowed with chirality and for patterns without multiplicities. In DPVarx09 , the same authors claim to extend the results to a number of robots greater than or equal to 5 but without chirality. The need of one robot more is justified by the way they want to build a common reference system for all robots. This is done by making use of two robots instead of one, the closest two robots to the center. They claim that such two robots can be always selected since they start from initial leader configurations. Hence a leader and a ‘second leader’ can always be detected and moved close to the center so as they can be always recognized by all robots. Even though the description is rather sketchy, their strategy is clear. Unfortunately it is not correct. Just to provide a counter-example, we refer to Figure 5. The represented configuration is symmetric, admitting one axis of reflection $\ell$ with a robot $r$ on it. Such a robot can be elected as leader, that is, this is a leader configuration and the proposed algorithm should solve any pattern from it. Following the arguments in DPVarx09 , since the configuration admits an axis of reflection with one robot on it, $r$ should move close to $c(R)$ in order to become the unique robot closest to $c(R)$ . The authors wrongly argue that during its motion $r$ cannot lose its leadership because it is the unique robot on $\ell$ , and by moving along $\ell$ it always remains the unique robot on $\ell$ .

Even though during the movement it is true that $r$ remains the unique robot on $\ell$ , it cannot move toward $c(R)$ without creating further axes of reflection, (five axes in this case) once position $p$ is reached. Once $r$ is in position $p$ , all robots look the same as the configuration admits a rotation, that is the configuration is not a leader configuration anymore, hence preventing the resolution of $APF$ . As we are going to show in the correctness section, our algorithm carefully addresses the case by means of a sub-phase of phase $\mathcal{F}5$ .

6 The algorithm

In this section, a robot always means an oblivious Async robot. Recall that initially a configuration is an initial leader configuration, hence it does not contain multiplicities by definition. Concerning the number of robots $n$ , for $n=1$ the $APF$ problem is trivial. When $n=2$ the problem is unsolvable as the gathering of two robots has been shown to be unsolvable, see CFPS12 .

Concerning the pattern to form, it might contain multiplicities. The case of point formation (Gathering) is delegated to CFPS12 , so we do not consider such a case as input for our algorithm.

Similarly to FYOKY15 , for $n=3$ , we design an ad-hoc algorithm.

Theorem 6.1

Let $R=\{r_{1},r_{2},r_{3}\}$ be an initial leader configuration with three robots, and let $F=\{f_{1},f_{2},f_{3}\}$ be any pattern. Then, there exists an algorithm able to form $F$ from $R$ .

Proof

We assume that $F$ does not contain a point of multiplicity 3, otherwise the algorithm in CFPS12 for the Gathering problem can be used. Assume that the point in $F$ and in $R$ are not collinear and let $T_{R}$ and $T_{F}$ be the triangles formed by points in $R$ and $F$ respectively. Degenerate cases with collinear points or with $F$ admitting a multiplicity of cardinality two will be considered later.

Let $\alpha_{i}$ ( $\beta_{i}$ , resp.) be the internal angle of $T_{R}$ ( $T_{F}$ , resp.) associated with the vertex $r_{i}$ ( $f_{i}$ , resp.), for each $i=1,2,3$ . Since $R$ is a leader configuration, the case with $\alpha_{1}=\alpha_{2}=\alpha_{3}=60^{\circ}$ cannot occur. Without loss of generality, we assume $\alpha_{1}\leq\alpha_{2}\leq\alpha_{3}$ , and $\beta_{1}\leq\beta_{2}\leq\beta_{3}$ (hence $\alpha_{1}\leq 60^{\circ}$ and $\beta_{1}\leq 60^{\circ}$ ). We prove the thesis by showing an algorithm that forms $F$ by modifying angles of $T_{R}$ so that eventually $\alpha_{i}=\beta_{i}$ , for each $i=1,2,3$ .

According to such angles, the algorithm distinguishes among the following cases when $R$ is not similar to $F$ :

$(a)$

$\alpha_{2}=\alpha_{3},\alpha_{1}\neq\beta_{1}$ . In this case, robot $r_{1}$ lies on an axis of symmetry $\ell$ and the algorithm performs the following step: $r_{1}$ moves along $\ell$ toward the point that makes true the condition $\alpha_{1}=\beta_{1}$ . Notice that during the movement of $r_{1}$ no further symmetries can be created as $\alpha_{1}$ remains the smallest angle being $\beta_{1}\leq 60^{\circ}$ . Hence $r_{1}$ is always recognized as the robot to move until its target is reached. After this step, either $R$ and $F$ are similar (when $\alpha_{i}=\beta_{i}$ for each $i=2,3$ ) or the next case $(b)$ occurs. 2. $(b)$

$\alpha_{2}=\alpha_{3}$ , $\alpha_{1}=\beta_{1}$ . Like in case (a), robot $r_{1}$ lies on an axis of symmetry. Then robots embed $f_{2}$ and $f_{3}$ on $r_{2}$ and $r_{3}$ , respectively, and $r_{1}$ moves along the unique circle $C$ passing through all the three robots toward a point $p$ that makes the configuration similar to $F$ (since the configuration is symmetric there are two equivalent points toward which $r_{1}$ can move). For the analysis see case $(c)$ , since immediately after $r_{1}$ starts moving we have $\alpha_{2}<\alpha_{3}$ whereas $\alpha_{1}$ remains equal to $\beta_{1}$ . 3. $(c)$

$\alpha_{2}<\alpha_{3}$ , $\alpha_{1}=\beta_{1}$ . We analyze two sub-cases, according to the comparison of $\alpha_{2}$ with $\beta_{2}$ , and of $\alpha_{3}$ with $\beta_{3}$ .

If $\alpha_{2}\geq\beta_{2}$ and $\alpha_{3}\leq\beta_{3}$ , the algorithm is based on the following steps: (1) robots embed $f_{2}$ and $f_{3}$ on $r_{2}$ and $r_{3}$ , respectively, (2) robots elect $r_{1}$ as the only robot allowed to move, (3) like in case $(b)$ , $r_{1}$ moves along the unique circle $C$ passing through all the three robots toward the unique point $p$ that makes the configuration similar to $F$ (here $p$ is unique as the configuration is asymmetric). This case is described by Figure 6 (left side). During the movement: $\alpha_{1}$ does not change, $\alpha_{2}$ decreases (without exceeding $\beta_{2}$ ), and $\alpha_{3}$ increases (without exceeding $\beta_{3}$ ). As a consequence, the relationships between angles remain the same, the obtained configuration is recognized as belonging to case $(c)$ , and $r_{1}$ is always recognized as the moving robot. Once $r_{1}$ reaches $p$ , $R$ and $F$ become similar and the pattern is formed. Note that during the movement the configuration is asymmetric as $\alpha_{1}$ remains strictly less than $\alpha_{2}$ . Angle $\alpha_{1}$ can match $\alpha_{2}$ only if $F$ is symmetric and $r_{1}$ has reached its target $p$ .

If $\alpha_{2}\leq\beta_{2}$ and $\alpha_{3}\geq\beta_{3}$ , the algorithm remains the same. The only difference is the analysis of the angles during the movement of $r_{1}$ : $\alpha_{1}$ does not change, $\alpha_{2}$ increases, and $\alpha_{3}$ decreases. Anyway, as in the previous sub-case, $r_{1}$ is always recognized as the moving robot and the pattern is eventually formed. 4. $(d)$

$\alpha_{2}<\alpha_{3},\alpha_{1}\neq\beta_{1}$ . This case concerns different sub-cases that can be described by referring to Figure 6 (right side). Without loss of generality, in the figure we assume $dist(r_{1},r_{2})\geq dist(r_{1},r_{3})\geq dist(r_{2},r_{3})$ , and hence robot $r_{3}$ is inside the shaded area depicted in Figure 6. Notice that $r_{3}$ cannot be on the arc of the circle delimited by points $p$ and $r_{2}$ , otherwise $\alpha_{3}=\alpha_{2}$ against hypothesis, and cannot be in the segment $[q,r_{2}]$ as otherwise the three robots would be collinear. If $r_{3}$ is in the interior of the shaded area, then $\alpha_{1}<\alpha_{2}<\alpha_{3}$ and the initial configuration is asymmetric; if $r_{3}$ belongs to the open segment $(p,q)$ , we get $\alpha_{1}=\alpha_{2}<\alpha_{3}$ .

Assuming $dist(f_{1},f_{2})\geq dist(f_{1},f_{3})\geq dist(f_{2},f_{3})$ , the algorithm is based on the following steps: (1) robots embed $f_{1}$ and $f_{2}$ on $r_{1}$ and $r_{2}$ , respectively, (2) robots elect $r_{3}$ as the only robot allowed to move, (3) $r_{3}$ embeds $f_{3}$ as closer as possible to itself, and (4) $r_{3}$ moves straightly toward $f_{3}$ . According to step 3, it follows that $f_{3}$ is in the segment formed by intersecting the half-line $\ell=\mathit{hline}(r_{1}f_{3})$ with the shaded area. In particular, it is in the interior of the shaded area when $F$ is asymmetric, whereas it is on the boundary of that area if $F$ is symmetric. To conclude the analysis of $f_{3}$ , notice that this point cannot be on the half-line starting from $r_{1}$ and passing through $r_{3}$ since we assumed $\alpha_{1}\neq\beta_{1}$ .

It is clear that, during the movements, $r_{3}$ will be always elected as the only robot allowed to move and hence it eventually reaches the target to form $F$ .

Summarizing, when the algorithm handles a leader configuration in case $(a)$ , the generated configurations remain in the same case $(a)$ until a stationary leader configuration belonging to case $(b)$ is created or the pattern is formed. When the algorithm handles a leader configuration in cases $(b)$ , as soon as the moving robot starts its movement the configuration belongs to case $(c)$ where the same move is continued until forming the pattern. If a configuration is in case $(c)$ , or $(d)$ the generated configurations remain in the same case until the pattern is formed.

Now, let us consider the degenerated cases when $\alpha_{3}=180^{\circ}$ or $\beta_{3}=180^{\circ}$ and $F$ has no multiplicities. If $\alpha_{3}=180^{\circ}$ , the embedding is like in case $(d)$ and, referring to Figure 6, robot $r_{3}$ is in the segment $[q,r_{2})$ whereas $f_{3}$ is either in the same segment or in the interior of the shaded area, according to whether $\beta_{3}=180^{\circ}$ or not. The algorithm simply moves $r_{3}$ toward $f_{3}$ .

The case $\alpha_{3}\not=180^{\circ}$ and $\beta_{3}=180^{\circ}$ requires a deeper analysis. Obviously, $\alpha_{1}\not=\beta_{1}$ as $\beta_{1}=0$ whereas $\alpha_{1}\not=0$ . If $\alpha_{2}=\alpha_{3}$ the configuration is symmetric, but the algorithm cannot act as in cases $(a)$ since $r_{1}$ should go to infinity to make $\alpha_{1}=\beta_{1}=0$ . Then, if $\alpha_{1}<\alpha_{2}$ , $r_{1}$ moves along the circle $C$ until $\alpha_{1}=\alpha_{2}$ . If the robot is stopped during the movement, $\alpha_{1}<\alpha_{2}<\alpha_{3}$ holds, and $r_{1}$ is recognized as the robot to be moved on $C$ until $\alpha_{1}=\alpha_{2}$ . When $\alpha_{1}=\alpha_{2}$ , still referring to Figure 6, $T_{R}$ is symmetric and $r_{3}$ is in the segment $(p,q)$ . Robot $r_{3}$ moves toward $q$ maintaining $\alpha_{1}=\alpha_{2}$ , and then it is always recognizable if stopped. When $r_{3}$ reaches $q$ then $\alpha_{3}=180^{\circ}$ and the algorithm acts as above by moving $r_{3}$ toward $f_{3}$ .

Finally, if $F$ admits a multiplicity it is assumed $f_{2}\equiv f_{3}$ , hence $f_{1}$ is not in the multiplicity. Then the algorithm simply acts as in the above degenerate cases when $\beta_{3}=180^{\circ}$ . ∎

In the remainder, we will provide an algorithm able to form any pattern $F$ (which is not a single point) starting from any initial leader configuration with $n\geq 4$ . A possible input for the algorithm is shown in Figure 7. We construct our algorithm in such a way that the execution consists of a sequence of phases $\mathcal{F}1$ , $\mathcal{F}2$ , $\mathcal{F}3$ , $\mathcal{F}4$ , and $\mathcal{F}5$ not necessarily in this order (some of which might be skipped whereas some other might be repeated a finite number of times). To each phase, we assign an invariant such that every configuration satisfies exactly one of the invariants (hence robots can correctly recognize the phase in which they are). Since each algorithm associated to a phase is composed of different kinds of moves, each phase is divided into sub-phases. Each sub-phase is characterized by a single move. Moreover, apart for a few exceptions, each time robots switch to a different phase/sub-phase, the current configuration is stationary, that is the move performed in a sub-phase is initiated from a stationary configuration (this property is crucial to prove the correctness of our algorithm). Basically, whenever a robot becomes active, it can deduce from the acquired snapshot to which phase and sub-phase the observed configuration belongs to, and whether it is a robot designated to move. In case it is its turn to move, it applies the move associated to the sub-phase detected. As it will be shown in the proof of correctness, our algorithm always maintains the current configuration as a leader configuration until the pattern is formed. The algorithm also assures there will always be exactly one robot moving in phases $\mathcal{F}1-\mathcal{F}4$ and at most two robots moving concurrently in phase $\mathcal{F}5$ , however, all moves are safe. In turn we prove the algorithm is transition-safe.

Table 1 contains all predicates required by our algorithm, whereas Table 2 describes in which phase a configuration is, according to the specified properties. Notice that for each arbitrary phase/sub-phase $\mathcal{X}$ we need three predicates $\mathcal{X}_{s}$ , $\mathcal{X}_{d}$ , and $\mathcal{X}_{e}$ to distinguish between the invariant that the configuration satisfies at the beginning of the phase (start), once robots start to move (during), and once the moving robots have terminated to apply the same move (end), respectively. In the most cases, we have $\mathcal{X}_{d}=\mathcal{X}_{s}$ ; in the remaining cases, as it will be clarified in the correctness section, when $\mathcal{X}_{d}\neq\mathcal{X}_{s}$ , $\mathcal{X}_{d}$ and $\mathcal{X}_{e}$ always coincide. For this reason we omit $\mathcal{X}_{d}$ in the presented tables.

About moves, Table 3–7 contain a description of all moves applied by our algorithm for each phase. As described in Section 4, sometimes the trajectories defined by the proposed moves are opportunely manipulated so as to guarantee stationarity (by means of Procedure StationaryMove) and to avoid collisions (by means of Procedure CollisionFreeMove).

It is important to keep in mind that during the whole algorithm it is assumed a first embedding of $F$ such that $C(R)=C(F)$ . Actually $C(R)$ never changes in phases $\mathcal{F}1-\mathcal{F}4$ whereas in phase $\mathcal{F}5$ it might change, however within $\mathcal{F}5$ robots do not exploit the embedding, hence the assumption considering $C(R)=C(F)$ does not affect any reasoning. We are now ready to consider each phase separately to see how the desired behavior is obtained.

6.1 Phase $\mathcal{F}1$

As described in Section 4, this phase is responsible for setting the external guards $g^{\prime}$ and $g^{\prime\prime}$ and, if required, for placing robots in $c(F)$ . Due to its complexity, the algorithm for this phase is composed of many different moves, and each move is referred to a sub-phase. Table 3 describes all such sub-phases, and also the corresponding invariants and moves.

The first sub-phase $\mathcal{A}$ (logically divided into $\mathcal{A}1$ and $\mathcal{A}2$ ) leaves exactly three robots on $C(R)$ when more than three robots are there. This is realized by selecting any not critical robots for $C(R)$ but three (see Property 2). We remind that a robot is critical for $C(R)$ if its removal makes $C(R)$ changing. The selected robots are moved one by one inside $C(R)$ so as to maintain the configuration being asymmetric. This is realized by moving each of such robots toward a specific new circle $C_{\downarrow}^{1}(R)$ (hence concentric to $C(R)$ and inside it).

As an example, the configuration $R$ in Figure 7 belongs to the sub-phase $\mathcal{A}1$ (i.e., predicate $\mathcal{A}1_{s}=\mathtt{s}_{+}\wedge\mathtt{l}$ holds), and hence move $m_{1}$ (cf Table 3) is applied. As soon as a robot $r$ leaves $\partial C(R)$ , the obtained configuration switches to $\mathcal{A}2$ and hence move $m_{2}$ is applied until $r$ reaches the desired circle. In fact, if $r$ ends its movement before reaching its target, it is selected again by the algorithm and again move $m_{2}$ is applied. Once $r$ reaches its target, predicate $\mathcal{A}1_{s}=\mathtt{s}_{+}\wedge\mathtt{l}$ holds. Such moves are repeated so that the configuration with $|\partial C(R)|=3$ in Figure 8 left is obtained: this configuration belongs to $\mathcal{C}1$ since $\mathcal{C}1_{s}=\mathtt{s}_{3}\wedge\mathtt{t}_{0}\wedge\mathtt{l}$ holds.

Actually, both $m_{1}$ and $m_{2}$ are performed by invoking Procedure StationaryMove (see Algorithm 1). This is done because while moving, a robot $r$ may incur along the way in a point $p$ that makes the current configuration belonging to the finalization phase $\mathcal{F}4$ or even final, that is predicate $\mathtt{w}$ holds. Such situations may happen when according to some embedding of $F$ on $R$ , difficult to detect at this stage, $p$ coincides with a point in $F$ . If other robots perform their Look phase while $r$ is on $p$ , they may start moving according to a different rule specified by our strategy, hence violating the desired property to maintain stationarity among phases. In order to avoid such a behavior, we simply force $r$ to stop on points that potentially may cause the described situations. For $m_{1}$ and $m_{2}$ , such points belong to some $C_{\downarrow}^{i}(F)$ , see Lines 1-1 of StationaryMove. If after a stop, still the configuration belongs to $\mathcal{F}1$ , then the same robot $r$ will be selected again to keep on moving.

The sub-phase $\mathcal{B}$ is concerned with the case of just two robots in $\partial C(R)$ and $F$ admits a multiplicity in $c(F)$ . In such a case, a third robot is moved from $\mathit{int}(C(R))$ to $C(R)$ (see move $m_{3}$ of Table 3).

Sub-class $\mathcal{C}$ (logically divided into $\mathcal{C}1$ and $\mathcal{C}2$ ) processes configurations with exactly three robots in $\partial C(R)$ , and moves them so that they form a triangle with angles of $30^{\circ}$ , $60^{\circ}$ and $90^{\circ}$ . Now, assume that the three robots form a triangle with angles $\alpha_{1}\geq\alpha_{2}\geq\alpha_{3}$ and let $r_{1}$ , $r_{2}$ and $r_{3}$ be the three corresponding robots. $\mathcal{C}1$ takes care of the case in which all the angles are different from $90^{\circ}$ (see Figure 8, left side): by move $m_{4}$ , robot $r_{2}$ rotates on $C(R)$ in such a way that $\alpha_{1}$ becomes of $90^{\circ}$ (see Figure 8, right side).

Similarly to $m_{1}$ and $m_{2}$ , move $m_{4}$ is performed by invoking Procedure StationaryMove. The points in $F$ on which the moving robot $r_{2}$ must stop are now a bit different than before, as $m_{4}$ rotates $r_{2}$ along $C(R)$ rather than moving straightly. This may cause different situations: still incurring in points in $F$ (Lines 1-1), or creating an unexpected reference angle of $\alpha$ degrees (Lines 1-1), or creating an asymmetric configuration belonging to $\mathcal{F}5$ (Lines 1-1).

If $r_{2}$ completes move $m_{4}$ by making $\alpha_{1}=90^{\circ}$ like in Figure 8, then there are two antipodal robots on $C(R)$ that will be detected as $g^{\prime}$ and $g^{\prime\prime}$ in the subsequent phases. The third robot $r$ on $C(R)$ is now moved either along $C(R)$ or toward a position inside $C(R)$ , depending on whether $F$ admits a multiplicity in $c(F)$ of $k>1$ elements or not. In the former case (see Figure 8, right side), the algorithm is in sub-phase $\mathcal{C}2$ and by move $m_{5}$ it rotates $r$ on $C(R)$ along the shortest path in such a way the composed triangle admits the required angles of $30^{\circ}$ , $60^{\circ}$ and $90^{\circ}$ (see Figure 9, left side). In the latter case $r$ is moved inside $C(R)$ by means of sub-phase $\mathcal{E}$ .

Once the robots in $\partial C(R)$ have formed the required triangle (case in which $F$ admits a multiplicity of $k$ elements in $c(F)$ ), sub-phase $\mathcal{D}$ can move the $k-1$ robots closest to $c(R)$ toward it (cf move $m_{6}$ of Table 3 and Figure 9). The specific triangle formed by the robots in $\partial C(R)$ assures that during sub-phase $\mathcal{D}$ the configuration remains always a leader configuration.

The last sub-phase of $\mathcal{F}1$ (sub-phase $\mathcal{E}$ ) is applied after creating a multiplicity of $k-1$ robots in $c(R)$ if $F$ requires $k$ elements in $c(F)$ , and when exactly three robots are in $\partial C(R)$ . Among such robots, there are two antipodal ones $g^{\prime}$ and $g^{\prime\prime}$ plus a third one $r$ . Robot $r$ is moved inside $C(R)$ . Sub-phase $\mathcal{E}$ is logically divided into $\mathcal{E}1$ and $\mathcal{E}2$ ; this is because the same moves of $\mathcal{A}1$ and $\mathcal{A}2$ are used to perform the required task (cf Figure 9 right side with Figure 10 left side).

6.2 Phase $\mathcal{F}2$

This phase is responsible for setting the internal guard $g$ . In particular, $g$ is initially identified as the closest robot to $c(R)$ (excluding possible robots in $c(R)$ required to compose a multiplicity), and hence moved on the guard circle $C^{g}(R)$ (cf Definition 4). Such a move is performed either by sub-phase $\mathcal{G}$ (logically divided into $\mathcal{G}1$ and $\mathcal{G}2$ ) or by sub-phase $\mathcal{H}$ . Table 4 describes all such sub-phases, and also the corresponding invariants and moves.

Sub-phase $\mathcal{G}$ starts when the invariant $\mathcal{G}1_{s}=\neg\mathtt{g}_{0}\wedge(\mathtt{c}\Rightarrow\mathtt{m}_{1})$ holds, that is when $\mathtt{g}_{0}$ is false (i.e., the guard $g$ is not yet on $C^{g}(R)$ ) and $\mathtt{c}\Rightarrow\mathtt{m}_{1}$ is true (i.e., if there is one robot on the center $\mathtt{c}(R)=c(F)$ then this is due to the presence of a multiplicity in $c(F)$ ). An example of such a case is described in Figure 10 (right side). Sub-phase $\mathcal{G}1$ then repeatedly applies move $m_{7}$ (cf Table 4) to move the closest robot to $c(R)$ on $C^{g}(R)$ (cf Figure 11). Note that, similarly to moves $m_{1}$ and $m_{2}$ , move $m_{7}$ is performed by invoking Procedure StationaryMove.

When $\mathcal{G}1$ is terminated, the sub-phase $\mathcal{G}2$ starts with the aim of rotating the robot $g$ placed on $C^{g}(R)$ so that $g$ , $c(R)$ , and one of the antipodal robots on $C(R)$ , now detected as $g^{\prime}$ , form an angle equal to the reference angle $\alpha$ (cf Definition 5). Move $m_{8}$ performs this task. At the end of $\mathcal{G}2$ , the three guards $g$ , $g^{\prime}$ and $g^{\prime\prime}$ compose the required common reference system for all robots.

Sub-phase $\mathcal{H}$ handles the specific configurations in which the invariant $\mathcal{H}_{s}=\mathtt{c}\wedge\neg\mathtt{m}_{0}$ holds, that is the cases where there is one robot in $c(R)=c(F)$ and there is no multiplicity in $c(F)$ . In such a cases, $m_{9}$ moves the robot away from the center $c(R)$ , so that the obtained configuration is subsequently managed by $\mathcal{G}$ .

6.3 Phase $\mathcal{F}3$

This phase is responsible for moving all the non-guards robots (i.e., $n-3$ robots) toward the targets. It is composed of three sub-phases, as described in Table 5.

We remark that at the end of $\mathcal{F}2$ , the required common reference system for all robots has been established (based on the three guards $g$ , $g^{\prime}$ and $g^{\prime\prime}$ ). This implies that all robots can now embed $F$ on $C(R)$ . This embedding is obtained as follows:

•

as already observed, $C(F)$ is superimposed on $C(R)$ ;

•

the counter-clockwise direction for $R$ is assumed to be the one such that $g$ becomes collinear with $g^{\prime}$ and $c(R)$ by rotating of $\alpha$ degrees;

•

the counter-clockwise direction for $F$ is that defined in Section 3 for any multiset of points;

•

let $f^{\prime}$ be a point in $\partial C(F)$ such that $f^{\prime}$ is the second point appearing in $V(f)$ , being $f$ any point in $\textit{min\_view}(\partial C(F))$ ; $f^{\prime}$ is superimposed on $g^{\prime}$ , and any other point in $F$ is superimposed such that the clockwise direction of $F$ coincides with that of $R$ .

This embedding is shown in Figure 12 (left side). According to this embedding, each robot uses the following mapping $\mu:\{g^{\prime},g^{\prime\prime},g\}\to F$ for determining the final target of each guard:

•

$\mu(g^{\prime})=f^{\prime}$ ;

•

$\mu(g^{\prime\prime})=f^{\prime\prime}$ , where $f^{\prime\prime}$ is the point in $\partial C(F)$ closest to $g^{\prime\prime}$ (in case of tie, that reachable from $g^{\prime\prime}$ in the counter-clockwise direction);

•

$\mu(g)=f$ , where $f\in F\setminus\{f^{\prime},f^{\prime\prime}\}$ and if $c(F)\in F$ then $f=c(F)$ , else $f$ is the point in $\partial C_{\uparrow}^{1}(F)$ closest to $g$ (in case of tie, the first of such points reached by $\mathit{hline}(c(R),g)$ when this half-line is turned counter-clockwise around the center).

This embedding is maintained along all phase $\mathcal{F}3$ ; we remark that $g$ , $g^{\prime}$ and $g^{\prime\prime}$ are not moved during this phase. Any other robot, one by one, is moved toward its closest point of $F\setminus\{\mu(g),\mu(g^{\prime}),\mu(g^{\prime\prime})\}$ (see Figure 12, right side). At any time, each robot must determine (1) whether it is already on its target or not (i.e., whether it is matched or not), (2) if it is not matched, which is its target, and (3) whether it is its turn to move or not. To this aim, each robot computes the following data:

•

the sets of matched robots and matched targets, that is $R^{m}=R\cap(F\setminus\{\mu(g),\mu(g^{\prime}),\mu(g^{\prime\prime})\})$ and $F^{m}=F\cap R^{m}$ ;

•

the sets of unmatched robots and unmatched targets, that is $R^{\neg m}=R\setminus(R^{m}\cup\{g,g^{\prime},g^{\prime\prime}\})$ and $F^{\neg m}=F\setminus(F^{m}\cup\{\mu(g),\mu(g^{\prime}),\mu(g^{\prime\prime})\})$ ;

•

the minimum distance between unmatched robots and unmatched targets, that is $\eta=\min\{d(r,f):~{}r\in R^{\neg m},~{}f\in F^{\neg m}\}$ ;

•

the set of unmatched robots at minimum distance from unmatched targets, that is $R^{\neg m}_{\eta}=\{r\in R^{\neg m}:~{}d(r,F^{\neg m})=\eta\}$ ;

•

in a given turn, which is the robot $r$ that has to move toward its target, that is $r=\textit{min\_view}(R^{\neg m}_{\eta})$ , and which is the corresponding target $\mu(r)$ , that is any point in $\{f\in F^{\neg m}:\;d(r,f)=\eta\}$ .

According to the strategy described in Section 4, the robot that moves toward its target has two constraints: (1) avoiding undesired collisions (in case the trajectory meets an already matched robot), and (2) avoiding entering into the guard circle (to preserve the common reference system).

For the former constraint, a Procedure CollisionFreeMove is designed. The procedure is given in Algorithm 2 while its description can be found in the corresponding correctness proof provided in Lemma 1.

For the latter, in case the segment $[r,\mu(r)]$ meets the teleporter circle $C^{t}(R)$ , then an alternative trajectory is computed. For this computation, robots also need the following data: the set $F^{*}=\{f\in F^{\neg m}~{}:~{}d(f,c(F))~{}\text{is minimum}\}$ .

The new trajectory is divided into three parts (see Figure 13):

(a)

a collision free trajectory toward the closest point $p_{1}$ on the teleporter circle, that is $p_{1}=(r,\mu(r)]\cap C^{t}(R)$ ; 2. (b)

a rotation along $C^{t}(R)$ toward the closest point $p_{2}=[c(F),f^{*}]\cap C^{t}(R)$ , where $f^{*}\in F^{*}$ ; 3. (c)

a collision free trajectory toward $f^{*}$ .

Note that in case (c), the destination $f^{*}$ may differ from the original destination $\mu(r)$ computed in case (a), but this is not a problem since, as shown in the correctness section, no other robot is moved until $r$ reaches its final destination.

The algorithm (see Table 5) performs such a new trajectory by moving robots along the teleporter circle as follows. Sub-phase $\mathcal{M}$ concerns case (b) above, that is configurations fulfilling invariant $\mathcal{M}_{s}=\mathtt{d}_{0}\wedge\neg\mathtt{d}_{1}$ (i.e., configurations where there is a unique robot $r$ on the $C^{t}(R)$ but $r$ does not coincide with a point $p=[c(F),f^{*}]\cap C^{t}(R)$ , where $f^{*}\in F^{*}$ ). Then, move $m_{10}$ rotates $r$ toward such a point $p$ . Sub-phase $\mathcal{N}$ concerns case (a) above. Via move $m_{11}$ (that invokes CollisionFreeMove), $\mathcal{N}$ is in charge of leading $r$ on a point on $C^{t}(R)$ if needed (cf $\mathtt{d}_{2}$ in $\mathcal{N}_{s}=(\mathtt{d}_{0}\Rightarrow\mathtt{d}_{1})\wedge\mathtt{d}_{2}$ ). Finally, sub-phase $\mathcal{O}$ is concerned with case (c) above, that is when the trajectory from $r$ to its target $\mu(r)$ does not meet the teleporter circle. Move $m_{12}$ (that invokes CollisionFreeMove) performs this final task.

Lemma 1

Procedure CollisionFreeMove performed by a robot $r$ with input a target $f$ always moves $r$ avoiding collisions with other robots either toward $f$ , if there are no robots between $r$ and $f$ , or toward a point $p$ fulfilling the following conditions:

$p$ * is inside both $C(R)$ and the cell $D_{f}$ of the Voronoi diagram induced by $F^{\neg m}$ where $f$ lies;* 2. 2.

there is no robot between $p$ and $f$ ; 3. 3.

$d(f,p)<d(f,r)$ .

Moreover, all the points $x$ reached by $r$ during its movement share the same properties of $p$ .

Proof

At Line 2, Procedure CollisionFreeMove moves $r$ toward $f$ when there are no robots between $r$ and $f$ . As the movement is straightforward and since both $D_{f}$ and the disk enclosed by $C(R)$ are convex, all the points $x$ reached by $r$ during its movement are inside $C(R)$ and $D_{f}$ .

If there are robots between $r$ and $f$ , among such robots the procedure, at Line 2, identifies as $\bar{r}$ the closest to $r$ . The point $p$ is calculated on one of the two half-lines perpendicular to $[r,f]$ in $\bar{r}$ , in accordance to the position of $c(R)$ , see Line 2. On $\ell$ , a set $P=\{p=\ell\cap\mathit{hline}(r,x):~{}p\neq\bar{r}~{}\mbox{and}~{}x\in R\setminus\{R\}\}$ is calculated at Line 2. The target $p$ is different by any point in $P$ : being these points on the lines between $r$ and any another robot, this will assure that the movement will be free by further collisions. To set the exact position of $p$ on $\ell$ , three other points are calculated at Lines 2, 2, and 2. The first one is $p^{\prime}$ , that is the intersection of $\ell$ and $C(R)$ . The target $p$ is such that $d(\bar{r},p)<d(\bar{r},p^{\prime})$ , then all the points $x$ reached by $r$ during its movement are inside $C(R)$ . The second one is $p^{\prime\prime}$ , that is the intersection between $\ell$ and the circle centered in $f$ of radius $[f,r]$ . The target $p$ is such that $d(\bar{r},p)<d(\bar{r},p^{\prime\prime})$ , then all the points $x$ reached by $r$ during its movement are closer and closer to $f$ . The third one, if exists, is $p^{\prime\prime\prime}$ , that is the intersection of $\ell$ and a side of cell $D_{f}$ . The target $p$ is such that $d(\bar{r},p)<d(\bar{r},p^{\prime\prime\prime})$ , then all the points $x$ reached by $r$ during its movement are inside this cell. This assures that the points $x$ reached by $r$ are closer to $f$ than any other target. Moreover, there is no robot between $x$ and $f$ . In fact, if such robot $r^{\prime}$ exists, the line $\mathit{hline}(r,x)$ would intersect $\ell$ in a point closest to $\bar{r}$ than each point in $P$ , a contradiction as the target $p$ is the closer one.

Finally, at Line 2, the point $p$ is set at a position fulfilling all the above constraints. In addition, notice that the choice of half-line $\ell$ ensures that $p$ cannot be on or inside $C^{t}(R)$ ; this implies that the procedure can be safely applied. In turn, all such properties prove that the claim holds. ∎

6.4 Phase $\mathcal{F}4$

This phase concerns the finalization steps, where the last three robots (the guards) must be moved to their targets to complete the formation of pattern $F$ . In particular, since in this phase we use the embedding defined in phase $\mathcal{F}3$ , $g^{\prime}$ is already matched and hence at most $g$ and $g^{\prime\prime}$ remain to be moved. Moving the guards leads to the loss of the common reference system, and hence ad-hoc moves must be designed to complete the pattern.

The algorithm for this phase is composed of two sub-phases denoted as $\mathcal{P}$ and $\mathcal{Q}$ (see Table 6). The former handles the majority of configurations by moving first $g^{\prime\prime}$ and then $g$ toward the respective targets. The latter manages some special cases where $g^{\prime\prime}$ is critical for $C(R)$ . In particular, predicate $\mathtt{q}$ (informally introduced in Table 1) is used to characterize such special cases. Formally:

Definition 7

Let $F=\{f_{1},f_{2},\ldots,f_{n}\}$ be a pattern to be formed. We say that the predicate $\mathtt{q}$ holds if $F$ fulfills the following conditions:

$\partial C(F)=F$ ; 2. 2.

$F$ does not contain multiplicities; 3. 3.

assuming $f_{1}=\textit{min\_view}(F)$ and $(f_{1},f_{2},\ldots,f_{n})$ as the counter-clockwise sequence of points on $C(F)$ , then $\sphericalangle(f_{n},c(F),f_{2})>180^{\circ}$ , where such an angle is obtained by rotating $\mathit{hline}(c(F),f_{n})$ counter-clockwise.

Figure 14. $(a)$ shows an embedding of a pattern $F$ in which $\mathtt{q}$ holds: note that $r_{1}$ is $g$ , $r_{2}$ is $g^{\prime\prime}$ and $f_{2}$ is matched with $g^{\prime}$ .

Sub-phase $\mathcal{P}$ is divided into $\mathcal{P}1$ and $\mathcal{P}2$ to manage the moves of $g^{\prime\prime}$ and $g$ , respectively. We now describe each sub-phase: its invariant, the task it performs, and the corresponding move.

In $\mathcal{P}1$ , $g^{\prime\prime}$ rotates along $C(R)$ toward $\mu(g^{\prime\prime})$ . Each robot can recognize this phase by performing, in order, the following steps:

test whether $\mathtt{g}_{1}$ holds; 2. 2.

if the previous test is passed, it uses the same embedding defined in phase $\mathcal{F}3$ : this embedding allows to recognize the guard $g^{\prime}$ , and, in turn, to determine $g^{\prime\prime}$ as the robot on $C(R)$ closest to the antipodal point of $g^{\prime}$ ; 3. 3.

finally, it tests whether such an embedding makes $R\setminus\{g,g^{\prime\prime}\}$ similar to $F\setminus\{\mu(g),\mu(g^{\prime\prime})\}$ and $g^{\prime\prime}\not=\mu(g^{\prime\prime})$ , where also the targets $\mu(g)$ and $\mu(g^{\prime\prime})$ are those defined in phase $\mathcal{F}3$ .

The result of test at Item 3 above can be seen as the value of an invariant $\mathtt{i}_{1}$ (cf phase $\mathcal{P}1$ at Table 6). When a robot checks that $\mathtt{i}_{1}$ holds and recognizes itself as $g^{\prime\prime}$ , it simply applies move $m_{13}$ to complete the rotation along $C(R)$ to reach its target $\mu(g^{\prime\prime})$ . For instance, referring to Figure 12 right side, once all non-guard robots are correctly placed during $\mathcal{F}3$ , the configuration belongs to $\mathcal{P}1$ , and $g^{\prime\prime}$ rotates in the clockwise direction along $C(R)$ to compose the multiplicity on the left. This is in fact the closest point on $C(R)$ to $g^{\prime\prime}$ (in the clockwise direction as there is a tie to break) with respect to the defined embedding of $F$ . Once also $g^{\prime\prime}$ is correctly positioned on its target, as we are going to see, $\mathtt{i}_{2}$ holds and only $g$ remains to move toward $\mu(g)$ to finalize $F$ . In the specific example of Figure 12, $\mu(g)=c(R)$ .

The movement of $g$ is realized in $\mathcal{P}2$ via a straight move of $g$ toward $\mu(g)$ . Each robot can recognize this phase by performing, in order, the following steps:

compute the set $E=\{(r,f):~{}(\{r\}=c(R)\vee\{r\}=\partial C^{1}_{\uparrow}(R))\wedge R\setminus\{r\}\mbox{ is similar to }F\setminus\{f\}\}$ ; 2. 2.

test whether there exists a pair $(r,f)\in E$ such that $f=c(F)\vee(c(F)\not\in F)\wedge f\in C^{1}_{\uparrow}(F)\wedge d(c(R),r)<d(c(F),f)$ ; 3. 3.

if there are many pairs $(r,f)$ that fulfill the previous test, it selects one for which $d(r,f)$ is minimum; 4. 4.

the pair $(r,f)$ selected in the previous step allows robots to recognizes the internal guard $g$ (i.e., $g$ coincides with $r$ ) and the target of $g$ (i.e., the point $f$ ).

The result of test at Item 2 above can be seen as the value of an invariant $\mathtt{i}_{2}$ . When a robot checks that $\mathtt{i}_{2}$ holds and recognizes itself as $g$ , it simply applies move $m_{14}$ to complete the movement toward the remaining unmatched target $f$ .

To ensure a correct finalization even when $\mathtt{q}$ holds and hence when $g^{\prime\prime}$ might be critical for $C(R)$ , the sub-phase $\mathcal{Q}$ is divided into four sub-phases. They are responsible for:

•

$\mathcal{Q}1$ : moving $g$ radially toward $C(R)$ ;

•

$\mathcal{Q}2$ : rotating $g^{\prime\prime}$ of at most $\alpha$ along $C(R)$ ;

•

$\mathcal{Q}3$ : rotating $g$ from the position acquired at $\mathcal{Q}1$ along $C(R)$ toward its target;

•

$\mathcal{Q}4$ : rotate again $g^{\prime\prime}$ if necessary along $C(R)$ toward its target.

The movement of $g$ toward its target performed in two steps guarantees to avoid possible symmetries. We now describe each sub-phase: its invariant, the task it performs, and the corresponding move. To recognize each phase among $\mathcal{Q}1,\ldots,\mathcal{Q}4$ , robots perform the following test:

test whether there exists an embedding of $F$ such that $r_{2},r_{3},\ldots,r_{n-1}$ are matched with $f_{2},f_{3},\ldots,f_{n-1}$ , respectively. We recall that here predicate $\mathtt{q}$ holds, hence points in $F$ fulfill all the conditions in Definition 7 (see Figure 14. $(a)$ ).

As we are going to show in the correctness section, in order to fulfill the required conditions $R$ must is asymmetric. Hence the above test always determines a unique ordering for the robots. After, robots perform two additional tests, according to the specific sub-phases to be recognized. Concerning $\mathcal{Q}1$ , the following additional tests are needed:

test whether both $\partial C^{1}_{\uparrow}(R)=\{r_{1}\}$ and $\sphericalangle(r_{1},c(R),f_{2})=\alpha$ hold;

3)

test whether $r_{n}$ is antipodal to $r_{2}$ (which coincides with $f_{2}$ ).

If all the previous tests are passed, robots recognize $g$ as $r_{1}$ , $g^{\prime}$ as $r_{2}$ , and $g^{\prime\prime}$ as the antipodal robot to $g^{\prime}$ . The result of such a process can be seen as the value of an invariant $\mathtt{i}_{3}$ . When a robot recognizes itself as $g$ and checks that $\mathtt{q}\wedge\mathtt{i}_{3}$ holds, it simply applies move $m_{15}$ to move radially toward $C(R)$ (cf cases $(a)$ and $(b)$ of Figure 14).

Concerning $\mathcal{Q}2$ , the following additional tests are needed:

test whether $r_{1}$ is on $C(R)$ between $f_{1}$ and $f_{2}$ such that $\sphericalangle(r_{1},c(R),f_{2})=\alpha$ ;

3)

test whether $r_{n}$ is on $C(R)$ such that $r_{n}\neq f_{n}$ and $\sphericalangle(r_{n},c(R),p)<\alpha$ , where $p$ is the antipodal point to $f_{2}$ .

If all the previous tests are passed, robots recognize $g$ as $r_{1}$ , $g^{\prime}$ as $r_{2}$ , and $g^{\prime\prime}$ as the closest robot to $p$ . The result of such a process can be seen as the value of an invariant $\mathtt{i}_{4}$ . When a robot checks that $\mathtt{q}\wedge\mathtt{i}_{4}$ holds and recognizes itself as $g^{\prime\prime}$ , it applies move $m_{16}$ to rotate of at most an angle $\alpha$ from $p$ or to reach its target $f_{n}$ if residing before $p$ . This is done to maintain $C(R)$ , being $g^{\prime\prime}$ critical (cf cases $(b)$ and $(c)$ of Figure 14).

Now, notice that according to the definition of view of $F$ given in Section 3.1 and according to Definition 7, $\sphericalangle(f_{1},c(F),f_{2})=3\alpha$ . Hence, for sub-phase $\mathcal{Q}3$ the following additional tests are needed:

test whether $r_{1}$ is on $C(R)$ between $f_{1}$ and $f_{2}$ such that $\alpha\leq\sphericalangle(r_{1},c(R),f_{2})<3\alpha$ ;

3)

test whether $r_{n}$ is on $C(R)$ such that $r_{n}=f_{n}$ or $\sphericalangle(r_{n},c(R),p)=\alpha$ , where $p$ is the antipodal point to $f_{2}$ .

If all the previous tests are passed, robots recognize $g$ as $r_{1}$ , $g^{\prime}$ as $r_{2}$ , and $g^{\prime\prime}$ as the closest robot to $p$ . The result of such a process can be seen as the value of an invariant $\mathtt{i}_{5}$ . When a robot checks that $\mathtt{q}\wedge\mathtt{i}_{5}$ holds and recognizes itself as $g$ , it applies move $m_{17}$ to complete the rotation along $C(R)$ to reach its target $f_{1}$ (cf cases $(c)$ and $(d)$ of Figure 14).

Finally, for $\mathcal{Q}4$ the following additional tests are needed:

test whether $r_{1}$ is matched with $f_{1}$ , according to the embedding defined at test 1;

3)

test whether $r_{n}$ is on $C(R)$ such that $r_{n}\neq f_{n}$ and $\alpha\leq\sphericalangle(r_{n},c(R),p)<\sphericalangle(f_{n},c(R),p)$ , where $p$ is the antipodal point to $f_{2}$ .

If all the previous tests are passed, robots recognize $g$ as $r_{1}$ , $g^{\prime}$ as $r_{2}$ , and $g^{\prime\prime}$ as the closest robot to $p$ . The result of such a process can be seen as the value of an invariant $\mathtt{i}_{6}$ . When a robot checks that $\mathtt{q}\wedge\mathtt{i}_{6}$ holds and recognizes itself as $g^{\prime\prime}$ , it applies move $m_{13}$ to reach $f_{n}$ (cf cases $(d)$ and $(e)$ of Figure 14).

6.5 Phase $\mathcal{F}5$

As remarked in Section 4, to solve $APF$ it is necessary to face the $\mathtt{SymBreak}$ sub-problem, that is to break possible symmetries in the initial leader configuration provided to the algorithm. We recall that the initial symmetric configurations handled by the algorithm consist of any configuration $R$ without multiplicities fulfilling one of the following conditions:

(1)

there exists a unique reflection axis $\ell$ for $R$ such that $|R\cap\ell|\geq 1$ ;

(2)

there exists a rotational symmetry in $R$ and $c(R)\in R$ .

The strategy used to address this sub-problem is to carefully move one robot away from the axis (if case (1) occurs) or the robot away from the center (if case (2) occurs), in order to obtain a stationary asymmetric configuration. In fact, during this phase multiplicities are not created. In particular, configurations with a reflection axis are always preliminary transformed by moving one robot along the axis $\ell$ toward $c(R)$ , if possible; otherwise (cf Figure 5), a robot on $\ell$ is moved ‘sufficiently faraway’ along $\ell$ and then rotated on $C(R)$ . Whereas, if $c(R)$ is reached or case (2) occurs, the robot in $c(R)$ is moved radially away from the center. In all the cases, in order to maintain stationarity, we aim to obtain a configuration different from those addressed in the other phases $\mathcal{F}1,\ldots,\mathcal{F}4$ until the moving robot does not reach a specific target.

The strategy for breaking the symmetries presents some complexities that lead the algorithm for this phase to be composed of many different moves. As in the previous phases, each of such moves is referred to a sub-phase; Table 7 describes all such sub-phases, and also the corresponding invariants and moves. We now provide a description of each sub-phase.

Sub-phase $\mathcal{T}$ concerns any configuration $R$ where predicate $\mathtt{b}_{0}\wedge\neg\mathtt{c}\wedge\mathtt{b}_{1}\wedge\neg\mathtt{z}_{1}$ holds. Informally, this means that $R$ is symmetric (cf $\mathtt{b}_{0}$ ), there is no robots in $c(R)$ (cf $\neg\mathtt{c}$ ) and hence $R$ must admit one single axis $\ell$ of reflection with robots on it. Actually, there exists a unique robot $r$ on $\ell$ (cf $\mathtt{b}_{1}$ ), and no robot has started to move away from $\ell$ (cf $\mathtt{z}_{1}$ ). Figure 15.(a) shows an example for such a configuration $R$ . Move $m_{18}$ moves $r$ toward $c(R\setminus\{r\})$ if possible. This movement can be performed only when $r$ admits a rotational-free path toward $c(R\setminus\{r\})$ . Such a path is defined as follows:

•

given a robot $r\in\ell$ , if in the segment $(r,c(R\setminus\{r\}))$ there are no robots and there is no point $t$ such that $R\setminus\{r\}\cup\{t\}$ has a rotational symmetry, then we say that there exists a rotational-free path for $r$ toward $c(R\setminus\{r\})$ .

If it is not possible for $r$ to reach $c(R\setminus\{r\})$ , that is $r$ does not admit a rotational-free path, then move $m_{18}$ moves $r$ along $\ell$ so that a faraway configuration $R^{\prime}$ is created.

A configuration $R$ is said to be a faraway configuration if in $R$ the following conditions hold:

•

$\mathtt{s}_{3}$ , that is $|\partial C(R)|=3$ ;

•

there exists a robot $r$ among the three on $C(R)$ such that $R\setminus\{r\}$ admits one axis of reflection $\ell$ that reflects to each other the other two robots on $C(R)$ , referred to as $r_{1}$ and $r_{2}$ ;

•

$r_{1}$ and $r_{2}$ are the furthest robots from $r$ ;

•

$\sphericalangle(r_{1},r,r_{2})\leq 59^{\circ}$ .

In such a case, robot $r$ is said to be a faraway robot.

Concerning the configuration shown in Figure 15.(a), since $r$ does not admit a rotational-free path, then move $m_{18}$ moves $r$ to create a faraway configuration $R^{\prime}$ . In Theorem 12, it is shown that $r$ becomes a faraway robot and that $\partial C(R^{\prime})=\{r,r_{1},r_{2}\}$ .

Sub-phase $\mathcal{U}$ handles any faraway configuration $R$ . These configurations are characterized by predicate $\mathtt{z}_{1}$ . In particular, since $\partial C(R)=\{r,r_{1},r_{2}\}$ , with $r$ being a faraway robot, then move $m_{19}$ moves robot $r$ along $C(R)$ so that eventually $r$ is antipodal to either $r_{1}$ or $r_{2}$ . It is worth to note that as soon as $r$ leaves the axis $\ell$ , the obtained configuration is no longer symmetric. Anyway, predicate $\mathtt{z}_{1}$ characterizes not only faraway configurations that are symmetric, but also configurations in which robot $r$ is stopped before reaching its target.

Sub-phases $\mathcal{V}1,\ldots,\mathcal{V}4$ are responsible for transforming configurations with one axis of reflection and at least two robots on it into configurations having one robot in $c(R)$ . In these sub-phases we use the following additional notation. Let $R$ be a configuration with one axis of reflection $\ell$ such that $|R\cap\ell|\geq 2$ . Then:

•

It is possible to total order the elements in $R\cap\ell$ by exploiting their distance from $c(R)$ and, in case of ties, by giving priority to robots being not critical, to those admitting rotational-free paths, and then of minimum view;

•

According to the above ordering, we denote by $r^{(1)}$ the first robot, and by $r^{(2)}$ the second robot. For instance, robot $r^{(1)}$ is the only robot moved by $m_{22}$ in sub-phase $\mathcal{V}3$ (cf Figure 15.(f)). Robots $r^{(1)}$ and $r^{(2)}$ will be possibly moved concurrently by move $m_{20}$ in sub-phase $\mathcal{V}1$ ;

•

When $|R\cap\ell|=2$ and exactly one robot in $R\cap\ell$ is critical (i.e., predicate $\mathtt{b}_{3}$ holds - cf Figure 15.(e)), we need some additional notation. Note that the unique critical robot on $\ell$ is by definition $r^{(2)}$ . Let $r^{\prime}$ , $r^{\prime\prime}$ be the closest robots to $r^{(2)}$ that belong to $\partial C(R)$ . We denote by $t^{60}$ and $t^{55}$ the points on $\ell$ such that $\sphericalangle(r^{\prime},t^{60},r^{\prime\prime})=60^{\circ}$ and $\sphericalangle(r^{\prime},t^{55},r^{\prime\prime})=55^{\circ}$ , respectively. Moreover, if it exists, let $t^{x}$ on $\ell$ be the point between $t^{60}$ and $t^{55}$ , closest to $t^{60}$ such that $|C(R\setminus\{r_{1}\}\cup\{t^{x}\})\cap R|>3$ . Move $m_{21}$ uses points $t^{60}$ , $t^{55}$ , and $t^{x}$ to define the movement of robot $r^{(2)}$ .

Sub-phase $\mathcal{V}1$ concerns any configuration $R$ where predicate $\mathtt{b}_{0}\wedge(\neg\mathtt{c}\vee\neg\mathtt{u}_{1})\wedge\mathtt{b}_{2}$ holds. Informally, this means that $R$ is symmetric (cf $\mathtt{b}_{0}$ ), there exist at least two robots on the axis of reflection $\ell$ and at least two of them are not critical for $C(R)$ (cf $\mathtt{b}_{2}$ ), there is no robot in $c(R)$ (cf $\neg\mathtt{c}$ ), or $r^{(2)}$ has not yet reached its target (cf $\neg\mathtt{u}_{1}$ ). Figures 15.(b)-(c) show examples for such a configuration $R$ . The move planned for this phase is $m_{20}$ . If $r^{(1)}$ admits a rotational-free path then $m_{20}$ moves $r^{(1)}$ toward the center of the current configuration, like in Figure 15.(b). Concurrently, move $m_{20}$ makes $r^{(2)}$ moving along the axis toward a point such that $r^{(2)}$ remains the unique robot on $C^{i}_{\uparrow}(R)$ at a distance form $c(R)$ which is in the middle between $C^{i-1}_{\uparrow}(R)$ and $C^{i+1}_{\uparrow}(R)$ . Concerning Figure 15.(c), notice that as soon as $r^{(2)}$ starts moving, a rotational-free path for $r^{(1)}$ is created; hence the two robots move concurrently. During the concurrent movements, $r^{(2)}$ must take care to not swap its role with $r^{(1)}$ , hence maintaining bigger its distance from $c(R)$ with respect to $r^{(1)}$ .

Sub-phase $\mathcal{V}2$ concerns any configuration $R$ where predicate $\mathtt{b}_{0}\wedge(\neg\mathtt{c}\vee\neg\mathtt{u}_{2})\wedge\mathtt{b}_{3}$ holds. Informally, this means that $R$ is symmetric (cf $\mathtt{b}_{0}$ ), there are two robots on the reflection axis $\ell$ and exactly one of them is critical for $C(R)$ (cf $\mathtt{b}_{3}$ ), there is no robots in $c(R)$ (cf $\neg\mathtt{c}$ ), or $r^{(2)}$ has not yet reached its target (cf $\neg\mathtt{u}_{2}$ ). Figures 15.(d)-(e) show examples for such a configuration $R$ . The move planned for this phase is $m_{21}$ . If $r^{(1)}$ admits a rotational-free path then $m_{21}$ moves $r^{(1)}$ toward $c(R)$ (cf Figure 15.(d)), else $r^{(1)}$ moves still in the direction of $c(R)$ but without reaching any circle $C^{i}_{\downarrow}$ where other robots resides. Concurrently, if $r^{(2)}$ lies in $[t^{60},t^{55})$ then move $m_{21}$ makes $r^{(2)}$ move along the axis toward $t^{x}$ if it exists, or $t^{55}$ like in Figure 15.(e). Notice that, like for $\mathcal{V}1$ , there might be two robots that move concurrently even though now they do not risk to swap their roles.

Sub-phase $\mathcal{V}3$ concerns any configuration $R$ where predicate $\mathtt{b}_{0}\wedge\neg\mathtt{c}\wedge\mathtt{b}_{4}$ holds, that is symmetric configurations (cf $\mathtt{b}_{0}$ ) with three robots on the reflection axis $\ell$ , and with exactly two of such robots critical for $C(R)$ (cf $\mathtt{b}_{4}$ ). Moreover, in $R$ there is no robot in $c(R)$ (cf $\neg\mathtt{c}$ ). An example of such configurations is provided in Figure 15.(f). In such a case it is easy to see that $r^{(1)}$ admits a rotational-free path. Consequently, move $m_{22}$ moves $r^{(1)}$ in $c(R)$ .

Sub-phase $\mathcal{V}4$ concerns any configuration $R$ where predicate $\mathtt{b}_{0}\wedge\neg\mathtt{c}\wedge\mathtt{b}_{5}$ holds, that is symmetric configurations (cf $\mathtt{b}_{0}$ ) with two robots only on the reflection axis $\ell$ that are both critical for $C(R)$ (cf $\mathtt{b}_{5}$ ), and with no robots in $c(R)$ (cf $\neg\mathtt{c}$ ). Assuming $R\cap\ell=\{r_{1},r_{2}\}$ , move $m_{23}$ moves the robot $r\in\{r_{1},r_{2}\}$ closest to $C(R\setminus\{r_{1},r_{2}\})$ . The target is the point $t\in\ell$ closest to $r$ that is not critical for $C(R\setminus\{r\}\cup t)$ . An example of such a case is provided in Figure 15.(g). Notice that when $r$ reaches the target $t$ , a configuration belonging to $\mathcal{V}2$ is obtained.

Finally, sub-phase $\mathcal{W}$ concerns any configuration $R$ where predicate $\mathtt{z}_{2}\wedge\neg\mathcal{V}1_{s}\wedge\neg\mathcal{V}2_{s}$ holds. This means that there are two possibilities for $R$ : either $R$ is symmetric with a robot $r$ in $c(R)$ , or $R$ is asymmetric, potentially obtained from a symmetric configuration by moving a robot $r$ away from $c(R)$ . The movement of $r$ toward $C^{g}(R)$ is dictated by move $m_{24}$ in a direction that does not form the reference angle $\alpha$ (used in Phase $\mathcal{F}2$ ) nor leaves symmetries. It follows that as soon as $r$ moves from $c(R)$ , the configuration is asymmetric. It is possible that the obtained configuration belongs to phase $\mathcal{F}4$ and in particular sub-phase $\mathcal{P}2$ in case $r$ is the unique robot left to be correctly moved toward the final target in order to form $F$ , that is predicate $\mathtt{i}_{2}$ holds. Since in phase $\mathcal{W}$ predicate $\mathtt{i}_{2}$ must be false when the configuration is asymmetric, robots can always recognize which phase the configuration belongs to, and that $r$ is the only moving robot.

7 Correctness

In this section, we provide all the results necessary to assess the correctness of our algorithm. To this end, we have to show that for each non-final configuration (that is configurations not satisfying $\mathtt{w}$ ) exactly one of the start predicates (predicates for stationary configurations) in Table 2 is true. We will show that a stationary configuration satisfying a starting predicate in Table 2 will be transformed by robots’ moves into a stationary configuration of another phase or in a stationary configuration satisfying $\mathtt{w}$ . To this end, for each phase (that is for each configuration that satisfies a starting predicate of Table 2), we have to show that exactly one of the starting predicates in the corresponding table (one among Table 3, 4, 5, 7, 6, and 7) is true. For each applied move, we have to show that during its implementation no undesired symmetry (and hence multiplicity) is created, and all robots but those involved by the move remain stationary. This assures that at the end of the move the configuration is necessarily stationary. Finally, we will show that during a move the starting predicate of Table 2 indicating the phase remains unchanged, with the exception of a few remarked situations which do not affect the correctness of the algorithm.

Lemma 2

Given an initial leader configuration $R$ and a pattern $F$ , if $\mathtt{w}$ does not hold then exactly one of the predicates defining a starting phase of Table 2 is true.

Proof

First, we show that each phase manages a different set of configurations, that is the logical conjunction of any two predicates among those defining the five starting phases in Table 2 is false. Then, we show that the logical disjunction of all the predicates defining the five phases of Table 2 along with predicate $\mathtt{w}$ is a tautology.

The conjunction of $\mathcal{F}1_{s}$ , with $\mathcal{F}2_{s}$ , $\mathcal{F}3_{s}$ , $\mathcal{F}4_{s}$ , and $\mathcal{F}5_{s}$ is false because of variables $\mathtt{f}_{2}$ , $\mathtt{f}_{3}$ , $\mathtt{f}_{4}$ , and $\mathtt{f}_{5}$ , respectively. Similarly, the conjunction of $\mathcal{F}2_{s}$ with $\mathcal{F}3_{s}$ , $\mathcal{F}4_{s}$ , and $\mathcal{F}5_{s}$ is false because of variables $\mathtt{f}_{3}$ , $\mathtt{f}_{4}$ , and $\mathtt{f}_{5}$ , respectively. The conjunction of $\mathcal{F}3_{s}$ with $\mathcal{F}4_{s}$ and $\mathcal{F}5_{s}$ is false because of $\mathtt{f}_{4}$ and $\mathtt{f}_{5}$ , respectively. Finally, the conjunction of $\mathcal{F}4_{s}$ with $\mathcal{F}5_{s}$ is false because of $\mathtt{f}_{5}$ .

For the second part of the proof, let us consider $\mathcal{F}1_{s}\vee\mathcal{F}2_{s}\vee\mathcal{F}3_{s}\vee\mathcal{F}4_{s}\vee\mathcal{F}5_{s}$ . This expression is equivalent to $\neg\mathtt{w}\wedge[(\neg\mathtt{f}_{2}\wedge\neg\mathtt{f}_{3}\wedge\neg\mathtt{f}_{4}\wedge\neg\mathtt{f}_{5})\vee(\mathtt{f}_{2}\wedge\neg\mathtt{f}_{3}\wedge\neg\mathtt{f}_{4}\wedge\neg\mathtt{f}_{5})\vee(\mathtt{f}_{3}\wedge\neg\mathtt{f}_{4}\wedge\neg\mathtt{f}_{5})\vee(\mathtt{f}_{4}\wedge\neg\mathtt{f}_{5})\vee\mathtt{f}_{5}]$ . Since the sub-expression in square brackets is true, the whole expression is equivalent to $\neg\mathtt{w}$ which is clearly true in disjunction with $\mathtt{w}$ . ∎

Lemma 2 basically shows that our algorithm can take as input any initial configuration for which it has been designed for, that is leader configurations.

Lemma 3

Given a configuration $R$ and a pattern $F$ , if $\mathcal{F}1_{s}$ is true then exactly one of the predicates for the starting phases in Table 3 is true.

Proof

We first show that at least one predicate among $\mathcal{A}1_{s}$ , $\mathcal{A}2_{s}$ , $\mathcal{B}_{s}$ , $\mathcal{C}1_{s}$ , $\mathcal{C}2_{s}$ , $\mathcal{D}_{s}$ , $\mathcal{E}1_{s}$ , and $\mathcal{E}2_{s}$ is true. By simple algebraic transformations, we obtain $\mathcal{A}1_{s}\vee\mathcal{A}2_{s}\vee\mathcal{B}_{s}\vee\mathcal{C}1_{s}\vee\mathcal{C}2_{s}\vee\mathcal{D}_{s}\vee\mathcal{E}1_{s}\vee\mathcal{E}2_{s}=\mathtt{s}_{+}\vee\mathtt{s}_{3}\vee(\mathtt{s}_{2}\wedge\neg((\mathtt{m}_{0}\Rightarrow\mathtt{m}_{1})\wedge\mathtt{l}))$ . Note that $\mathtt{s}_{+}\vee\mathtt{s}_{3}\vee\mathtt{s}_{2}$ is true for each configuration, since that expression is referred to all the possibilities about the number of robots on $C(R)$ as we assumed $|R|\geq 4$ . So it is sufficient to show that $\mathcal{F}1_{s}\Rightarrow\neg((\mathtt{m}_{0}\Rightarrow\mathtt{m}_{1})\wedge\mathtt{l})$ when $\mathtt{s}_{2}$ is true. As $\mathcal{F}1_{s}$ implies $\neg\mathtt{f}_{2}=\neg((\mathtt{m}_{0}\Rightarrow\mathtt{m}_{1})\wedge\mathtt{s}_{2}\wedge\mathtt{l})$ (see Table 2), when $\mathtt{s}_{2}$ holds we trivially get that $\neg(\mathtt{l}\wedge(\mathtt{m}_{0}\Rightarrow\mathtt{m}_{1}))$ holds.

We now show that at most one of the predicates for starting phases in Table 3 is true. To this end, it is sufficient to show that the logical conjunction of any two predicates is false. In most cases, this is obtained by showing that both the predicates imply the same variable, but with opposite logical values.

•

Concerning $\mathcal{A}1_{s}=\mathtt{s}_{+}\wedge\mathtt{l}$ , it is disjoint with $\mathcal{A}2_{s}$ because of $\mathtt{l}$ . Since $\mathtt{s}_{+}$ implies $\neg(\mathtt{s}_{2}\vee\mathtt{s}_{3})$ , then $\mathcal{A}1_{s}$ is disjoint with any of the remaining predicates, as for them either $\mathtt{s}_{2}$ or $\mathtt{s}_{3}$ is true.

•

Concerning $\mathcal{A}2_{s}=(\mathtt{s}_{+}\vee\mathtt{s}_{3})\wedge\neg\mathtt{l}$ , either it implies $\mathtt{s}_{+}$ (and then, as above, it differs from all the remaining predicates) or it implies $\mathtt{s}_{3}\wedge\neg\mathtt{l}$ . However, $\mathtt{l}$ is positive in all the remaining predicates where $\mathtt{s}_{3}$ holds; predicates $\mathcal{B}_{s}$ and $\mathcal{E}2_{s}$ are both disjoint with $\mathcal{A}2_{s}$ because of $\mathtt{s}_{2}$ .

•

Predicate $\mathcal{B}_{s}$ is disjoint with all the remaining predicate but $\mathcal{E}2_{s}$ because of $\mathtt{s}_{2}$ (the others require $\mathtt{s}_{3}$ ). $\mathcal{B}_{s}$ and $\mathcal{E}2_{s}$ are disjoint because of $\mathtt{m}_{0}\Rightarrow\mathtt{m}_{1}$ .

•

Concerning $\mathcal{C}1_{s}=\mathtt{s}_{3}\wedge\mathtt{t}_{0}\wedge\mathtt{l}$ , it is disjoint with both $\mathcal{C}2_{s}$ and $\mathcal{E}1_{s}$ because of $\mathtt{t}_{0}$ , with $\mathcal{D}_{s}$ because of $\mathtt{t}_{1}$ (since $\mathtt{t}_{0}$ implies $\neg\mathtt{t}_{1}$ ), and with $\mathcal{E}2_{s}$ because $\mathtt{s}_{3}$ implies $\neg\mathtt{s}_{2}$ .

•

Predicate $\mathcal{C}2_{s}$ is disjoint with $\mathcal{D}_{s}$ because of $\mathtt{t}_{1}$ , with $\mathcal{E}1_{s}$ because of $\mathtt{m}_{0}\Rightarrow\mathtt{m}_{1}$ , and with $\mathcal{E}2_{s}$ because $\mathtt{s}_{3}$ implies $\neg\mathtt{s}_{2}$ .

•

Predicate $\mathcal{D}_{s}$ is disjoint with $\mathcal{E}1_{s}$ because of $\mathtt{m}_{0}\Rightarrow\mathtt{m}_{1}$ , and with $\mathcal{E}2_{s}$ because $\mathtt{s}_{3}$ implies $\neg\mathtt{s}_{2}$ .

•

Predicate $\mathcal{E}1_{s}$ is disjoint with $\mathcal{E}2_{s}$ because $\mathtt{s}_{3}$ implies $\neg\mathtt{s}_{2}$ .

Summarizing, we get that exactly one of the predicates for the starting phases in Table 3 is true when $\mathcal{F}1_{s}$ holds. ∎

Lemma 4

Given a configuration $R$ and a pattern $F$ , if $\mathcal{F}2_{s}$ is true then exactly one of the predicates for the starting phases in Table 4 is true.

Proof

We first show that at most one of the predicates for starting phases in Table 4 is true. To this end, it is sufficient to show that the logical conjunction of any two predicates is false. This is obtained by showing that both the predicates imply the same variable, but with opposite logical values. In particular, $\mathcal{G}1_{s}$ and $\mathcal{G}2_{s}$ are disjoint because of $\mathtt{g}_{0}$ . Since $\mathtt{m}_{1}\Rightarrow\mathtt{m}_{0}$ , we can assume that both $\mathcal{G}1_{s}$ and $\mathcal{G}2_{s}$ imply $\mathtt{c}\Rightarrow\mathtt{m}_{0}=\neg\mathtt{c}\vee\mathtt{m}_{0}=\neg(\mathtt{c}\wedge\neg\mathtt{m}_{0})$ . Then, both $\mathcal{G}1_{s}$ and $\mathcal{G}2_{s}$ are disjoint with $\mathcal{H}_{s}$ because of $(\mathtt{c}\wedge\neg\mathtt{m}_{0})$ .

We now show that exactly one of the predicates for starting phases in Table 4 is true. To this end, we show that $\mathcal{G}1_{s}\vee\mathcal{G}2_{s}\vee\mathcal{H}_{s}$ is true when $\mathcal{F}2_{s}$ holds. We first analyze $\mathcal{G}1_{s}\vee\mathcal{G}2_{s}$ ; it corresponds to $[\neg\mathtt{g}_{0}\wedge(\mathtt{c}\Rightarrow\mathtt{m}_{1})]\vee[\mathtt{g}_{0}\wedge\neg\mathtt{g}_{1}\wedge(\mathtt{c}\Rightarrow\mathtt{m}_{1})]=[\neg\mathtt{g}_{0}\vee(\mathtt{g}_{0}\wedge\neg\mathtt{g}_{1})]\wedge(\mathtt{c}\Rightarrow\mathtt{m}_{1})=[\neg\mathtt{g}_{0}\vee\neg\mathtt{g}_{1}]\wedge(\mathtt{c}\Rightarrow\mathtt{m}_{1})$ . Since $\neg\mathtt{g}_{0}\Rightarrow\neg\mathtt{g}_{1}$ , the last expression can be simplified into

[TABLE]

Now, observe that $\mathcal{F}2_{s}$ implies both $\mathtt{f}_{2}=(\mathtt{m}_{0}\Rightarrow\mathtt{m}_{1})\wedge\mathtt{s}_{2}\wedge\mathtt{l}$ and $\neg\mathtt{f}_{3}=\neg[(\mathtt{m}_{0}\Rightarrow\mathtt{m}_{1})\wedge\mathtt{g}_{2}]=\neg(\mathtt{m}_{0}\Rightarrow\mathtt{m}_{1})\vee\neg\mathtt{g}_{2}$ . In turn, it follows that $\mathcal{F}2_{s}$ implies $(\mathtt{m}_{0}\Rightarrow\mathtt{m}_{1})$ , $\mathtt{s}_{2}$ , and $\neg\mathtt{g}_{2}$ . According to the definition of $\mathtt{g}_{2}$ , it follows that either $\mathtt{g}_{1}$ is false or $\not\exists g^{\prime\prime}\in\partial C(R)$ antipodal to $g\textquoteright$ . The latter condition cannot hold since $\mathcal{F}2_{s}$ implies $\mathtt{s}_{2}$ , and hence $\mathtt{g}_{1}$ is false. Concluding, Eq. 1 is equivalent to $\mathcal{G}1_{s}\vee\mathcal{G}2_{s}=\mathtt{c}\Rightarrow\mathtt{m}_{1}$ .

Finally, we get $\mathcal{G}1_{s}\vee\mathcal{G}2_{s}\vee\mathcal{H}_{s}=(\mathtt{c}\Rightarrow\mathtt{m}_{1})\vee(\mathtt{c}\wedge\neg\mathtt{m}_{0})=\neg\mathtt{c}\vee(\mathtt{m}_{0}\Rightarrow\mathtt{m}_{1})$ . Since in $\mathcal{F}2_{s}$ predicate $\mathtt{m}_{0}\Rightarrow\mathtt{m}_{1}$ holds, then the claim follows.

Summarizing, we get that exactly one of the predicates for the starting phases in Table 4 is true when $\mathcal{F}2_{s}$ holds. ∎

Lemma 5

Given a configuration $R$ and a pattern $F$ , if $\mathcal{F}3_{s}$ is true then exactly one of the predicates for the starting phases in Table 5 is true.

Proof

By observing that $\mathtt{d}_{0}\wedge\neg\mathtt{d}_{1}$ is equivalent to $\neg(\mathtt{d}_{0}\Rightarrow\mathtt{d}_{1})$ , it is easy to see that the logical conjunction of any two predicates among $\mathcal{M}_{s}$ , $\mathcal{N}_{s}$ , and $\mathcal{O}_{s}$ is false. Then at most one of these predicates is true for $R$ . On the other hand the logical disjunction of predicates $\mathcal{M}_{s}$ , $\mathcal{N}_{s}$ , and $\mathcal{O}_{s}$ is also trivially true. Then, exactly one of the predicates for the starting phases in Table 5 is true. ∎

Lemma 6

Given a configuration $R$ and a pattern $F$ , if $\mathcal{F}4_{s}$ is true then exactly one of the predicates for the starting phases in Table 6 is true.

Proof

We first show that at least one predicate among $\mathcal{P}1_{s}$ , $\mathcal{P}2_{s}$ , $\mathcal{Q}1_{s}$ , $\mathcal{Q}2_{s}$ , $\mathcal{Q}3_{s}$ , and $\mathcal{Q}4_{s}$ is true. Since $\mathcal{F}4_{s}=\mathtt{f}_{4}\wedge\neg\mathtt{f}_{5}\wedge\neg\mathtt{w}$ holds, then $\mathtt{f}_{4}$ holds as well. Since $\mathtt{f}_{4}=\neg\mathtt{q}\wedge(\mathtt{i}_{1}\vee\mathtt{i}_{2})~{}\vee~{}\mathtt{q}\wedge(\mathtt{i}_{3}\vee\mathtt{i}_{4}\vee\mathtt{i}_{5}\vee\mathtt{i}_{6})$ , then the logical disjunction $\mathcal{P}1_{s}\vee\mathcal{P}2_{s}\vee\mathcal{Q}1_{s}\vee\mathcal{Q}2_{s}\vee\mathcal{Q}3_{s}\vee\mathcal{Q}4_{s}$ is true.

We now show that $R$ is processed by exactly one sub-phase of $\mathcal{F}4$ . $\mathcal{P}1_{s}$ is disjoint with $\mathcal{P}2_{s}$ since $\mathtt{i}_{1}$ implies that exactly two robots are unmatched, while $\mathtt{i}_{2}$ implies that exactly one robot is unmatched. $\mathcal{P}1_{s}$ and $\mathcal{P}2_{s}$ are disjoint with (any sub-phase of) $\mathcal{Q}$ because of $\mathtt{q}$ . According to the formal definitions of predicates $\mathtt{i}_{3},\ldots,\mathtt{i}_{6}$ , it follows that $\mathcal{Q}1_{s}$ is disjoint with any other sub-phase of $\mathcal{Q}$ , since $\mathtt{i}_{3}$ implies $r_{1}$ inside $C(R)$ while $\mathtt{i}_{4},\ldots,\mathtt{i}_{6}$ all imply $R=\partial C(R)$ . $\mathcal{Q}4_{s}$ is disjoint with both $\mathcal{Q}2_{s}$ and $\mathcal{Q}3_{s}$ since $\mathtt{i}_{6}$ implies that exactly one robot is unmatched, while both $\mathtt{i}_{4}$ and $\mathtt{i}_{5}$ imply that exactly two robots are unmatched. Finally, $\mathcal{Q}2_{s}$ and $\mathcal{Q}3_{s}$ are disjoint because of the third items in the definitions of $\mathtt{i}_{4}$ and $\mathtt{i}_{5}$ . ∎

Lemma 7

Given a leader configuration $R$ and a pattern $F$ , if $\mathcal{F}5_{s}$ is true then exactly one of the predicates for the starting phases in Table 7 is true.

Proof

We first show that at least one predicate among $\mathcal{T}_{s}$ , $\mathcal{U}_{s}$ , $\mathcal{V}1_{s}$ , $\mathcal{V}2_{s}$ , $\mathcal{V}3_{s}$ , $\mathcal{V}4_{s}$ and $\mathcal{W}_{s}$ is true. $\mathcal{F}5_{s}$ implies $(\mathtt{b}_{0}\vee\mathtt{z}_{1}\vee\mathtt{z}_{2})\wedge\mathtt{e}$ . Hence, $R$ does not contain multiplicities. If $\mathtt{z}_{1}$ is true, then $\mathcal{U}_{s}$ is true. If $\mathtt{z}_{2}$ is true, then one predicate among $\mathcal{W}_{s}$ , $\mathcal{V}1_{s}$ , or $\mathcal{V}2_{s}$ is true. If both $\mathtt{z}_{1}$ and $\mathtt{z}_{2}$ are false, then necessarily $\mathtt{b}_{0}$ holds and $\mathtt{c}$ must be false as otherwise $\mathtt{z}_{2}$ is true. It follows that $R$ admits exactly one axis of reflection $\ell$ with robots on it. In such a case $\mathcal{T}\vee\mathcal{V}1_{s}\vee\mathcal{V}2_{s}\vee\mathcal{V}3_{s}\vee\mathcal{V}4_{s}=\mathtt{b}_{1}\vee\mathtt{b}_{2}\vee\mathtt{b}_{3}\vee\mathtt{b}_{4}\vee\mathtt{b}_{5}$ . Actually, such an expression is true as $\mathtt{b}_{1}$ , $\ldots$ , $\mathtt{b}_{5}$ cover all the possible cases concerning robots lying on $\ell$ .

We now show that at most one of the predicates for starting phases in Table 7 is true. To this end, it is sufficient to show that the logical conjunction of any two predicates is false.

•

Concerning $\mathcal{T}_{s}=\mathtt{b}_{0}\wedge\neg\mathtt{c}\wedge\mathtt{b}_{1}\wedge\neg\mathtt{z}_{1}$ , it is disjoint with $\mathcal{U}_{s}$ because of $\mathtt{z}_{1}$ . It is disjoint with $\mathcal{V}1_{s}$ , $\mathcal{V}2_{s}$ , $\mathcal{V}3_{s}$ and $\mathcal{V}4_{s}$ because of $\mathtt{b}_{1}$ ( $\mathcal{V}1_{s}$ , $\mathcal{V}2_{s}$ , $\mathcal{V}3_{s}$ and $\mathcal{V}4_{s}$ require that that at least one predicate among $\mathtt{b}_{2},\ldots,\mathtt{b}_{5}$ holds, while predicates $\mathtt{b}_{1},\ldots,\mathtt{b}_{5}$ are pairwise disjoint). It is disjoint with $\mathcal{W}_{s}$ because $\mathcal{T}_{s}$ implies that $\mathtt{b}_{0}\wedge\neg\mathtt{c}$ holds, whereas $\mathcal{W}_{s}$ implies that $\neg\mathtt{b}_{0}\vee\mathtt{c}$ holds.

•

Concerning $\mathcal{U}_{s}=\mathtt{z}_{1}$ , it is disjoint with $\mathcal{V}1_{s}$ , $\mathcal{V}2_{s}$ , $\mathcal{V}3_{s}$ and $\mathcal{V}4_{s}$ because such predicates require that that at least one among $\mathtt{b}_{2},\ldots,\mathtt{b}_{5}$ holds, and this implies that $R$ must have a reflection axis with at least two robots on the axis. Conversely $\mathtt{z}_{1}$ implies that $R$ is either asymmetric or reflexive with at most one robot on the axis. To prove that $\mathcal{U}_{s}$ is disjoint with $\mathcal{W}_{s}$ we show that $\mathtt{z}_{1}\Rightarrow\neg\mathtt{z}_{2}$ . Consider a configuration $R$ that fulfills $\mathtt{z}_{1}$ :

–

if $R$ is symmetric (i.e., $\mathtt{b}_{0}$ holds) then $c(R)$ is not occupied (i.e., $\neg\mathtt{c}$ holds) – since $\mathtt{z}_{2}$ implies $\mathtt{c}\vee\neg\mathtt{b}_{0}$ holds, then $\mathtt{z}_{2}$ is false;

–

if $R$ is asymmetric (i.e., $\neg\mathtt{b}_{0}$ holds), let $r$ be the faraway robot detected by predicate $\mathtt{z}_{1}$ . Since $R$ is asymmetric then $r$ is not on the axis $\ell$ given in the definition of predicate $\mathtt{z}_{1}$ . If $r^{\prime}=\partial C_{\uparrow}^{1}(R)$ , then $R\setminus\{r^{\prime}\}$ cannot be symmetric as the asymmetry of $R$ is due to $r$ . This means that $\mathtt{z}_{2}$ cannot hold.

•

Concerning $\mathcal{V}1_{s}=\mathtt{b}_{0}\wedge(\neg\mathtt{c}\vee\neg\mathtt{u}_{1})\wedge\mathtt{b}_{2}$ , it is disjoint with $\mathcal{V}2_{s}$ , $\mathcal{V}3_{s}$ and $\mathcal{V}4_{s}$ because of $\mathtt{b}_{2}$ . Moreover it is trivially disjoint with $\mathcal{W}_{s}$ ( $\mathcal{W}_{s}$ requires $\neg\mathcal{V}1_{s}$ ).

•

Concerning $\mathcal{V}2_{s}=\mathtt{b}_{0}\wedge(\neg\mathtt{c}\vee\neg\mathtt{u}_{2})\wedge\mathtt{b}_{3}$ , it is disjoint with $\mathcal{V}3_{s}$ and $\mathcal{V}4_{s}$ because of $\mathtt{b}_{3}$ . Moreover it is trivially disjoint with $\mathcal{W}_{s}$ ( $\mathcal{W}_{s}$ requires $\neg\mathcal{V}2_{s}$ ).

•

Concerning $\mathcal{V}3_{s}=\mathtt{b}_{0}\wedge\neg\mathtt{c}\wedge\mathtt{b}_{4}$ , it is disjoint with $\mathcal{V}4_{s}$ because of $\mathtt{b}_{4}$ . It is disjoint with $\mathcal{W}_{s}$ because if $R$ belongs to $\mathcal{W}$ then it fulfills $\mathtt{b}_{0}\wedge\neg\mathtt{c}$ holds, while we have already observed that $\mathtt{z}_{2}$ implies $\neg\mathtt{b}_{0}\vee\mathtt{c}$ .

•

Concerning $\mathcal{V}4_{s}=\mathtt{b}_{0}\wedge\neg\mathtt{c}\wedge\mathtt{b}_{5}$ , it is disjoint with $\mathcal{W}_{s}$ because we are in the same situation of $\mathcal{V}3_{s}$ vs $\mathcal{W}_{s}$ .

∎

We are now ready to provide the correctness proof of our algorithm for each phase, and then we combine all phases by means of the final theorem that provides the correctness of the whole algorithm. For each phase we consider all possible sub-phases. For each sub-phase we show all the possible scenarios where the corresponding moves lead. In particular, for each phase among $\mathcal{F}1$ , $\mathcal{F}2$ , $\mathcal{F}3$ , $\mathcal{F}4$ , $\mathcal{F}5$ , and for each move $m$ defined in the algorithm, we need to show several properties that guarantee to our algorithm to safely evolve until pattern $F$ is formed. For the first four phases $\mathcal{F}1$ , $\mathcal{F}2$ , $\mathcal{F}3$ , and $\mathcal{F}4$ all moves involve only one robot and we are going to prove the following properties:

$\mathit{H}_{0}$ :

at the beginning, $m$ involves only one robot;

$\mathit{H}_{1}$ :

while a robot is moving according to $m$ , the configuration is a leader configuration;

$\mathit{H}_{2}$ :

$m$ is safe, and in particular that while a robot is moving according to $m$ , all other robots are stationary;

$\mathit{H}_{3}$ :

while a robot is moving according to $m$ , no collisions are created;

$\mathit{H}_{4}$ :

if $m$ is associated to phase $\mathcal{X}$ , then the predicate $\mathcal{X}_{e}$ holds once a robot has terminated to apply $m$ ;

$\mathit{H}_{5}$ :

$m$ preserves stationarity.

Basically property $\mathit{H}_{2}$ is needed to correctly address the $\mathtt{Membership}$ problem described in Section 4.

About Property $\mathit{H}_{4}$ , the stop of a robot $r$ is due to three events. First, the adversary may stop $r$ before reaching its target. Second, the move might be subject to Procedures StationaryMove or CollisionFreeMove, hence $r$ reaches an intermediate target. Third, $r$ reaches the real target imposed by the current move. From the proofs, we omit the analysis of the first condition because the situation obtained once the adversary stops the moving robot $r$ always equals what can happen while $r$ is moving, that is the analysis of property $\mathit{H}_{2}$ holds.

About Property $\mathit{H}_{5}$ , we always omit this property form our proofs because it comes for free from the other properties once we have shown that there is always only one robot $r$ moving. So whenever $r$ stops moving, the configuration is stationary.

Lemma 8

Let $R$ be a stationary configuration in $\mathcal{F}1$ . From $R$ the algorithm eventually leads to a stationary configuration belonging to $\mathcal{F}2$ , $\mathcal{F}3$ , $\mathcal{F}4$ , $\mathcal{F}5$ or where $\mathtt{w}$ holds.

Proof

By Lemma 3, exactly one of the predicates for the starting phases in Table 3 is true. In turn, this implies that exactly one of the moves associated to the sub-phases of $\mathcal{F}1$ is applied to $R$ . We show that the properties $\mathit{H}_{0},\ldots,\mathit{H}_{4}$ hold for each possible move applied to $R$ .

Let us consider sub-phase $\mathcal{A}1$ where move $m_{1}$ is performed.

$\mathit{H}_{0}$ :

Move $m_{1}$ only concerns the not critical robot $r$ on $C(R)$ of minimum view.

$\mathit{H}_{1}$ :

During the movement of $r$ , the configuration remains a leader configuration. Actually it is asymmetric as there are no multiplicities yet and $r$ cannot participate to neither a rotation, being the only robot on $C_{\downarrow}^{1}(R)$ , or a reflection as the axis of symmetry should pass through $r$ , but then the starting configuration $R$ was symmetric, a contradiction.

$\mathit{H}_{2}$ :

We show that $m_{1}$ is safe. As soon as the robot moves, predicate $\mathcal{A}2=(\mathtt{s}_{+}\vee\mathtt{s}_{3})\wedge\neg\mathtt{l}$ holds, since from $\mathtt{s}_{+}$ by moving one robot either $\mathtt{s}_{+}$ or $\mathtt{s}_{3}$ holds and $\neg\mathtt{l}$ holds as the robot has not yet reached the target.

Any configurations $R^{\prime}$ observed during the move of $r$ cannot belong to $\mathcal{F}2$ as $\mathtt{s}_{2}$ does not hold. It cannot belong to $\mathcal{F}3$ as well because $\mathtt{f}_{3}$ does not hold. In fact, $\mathtt{f}_{3}$ does not hold in $\mathcal{A}1_{s}$ and move $m_{1}$ cannot change this status. Possibly, the $R^{\prime}$ falls in $\mathcal{F}4$ , in particular sub-phases $\mathcal{P}2$ and $\mathcal{Q}1$ . In fact, in $\mathcal{P}1$ predicate $\mathtt{g}_{1}$ should hold, but $r$ is certainly not on $C^{g}(R)$ ; in $\mathcal{Q}2$ , $\mathcal{Q}3$ , and $\mathcal{Q}4$ all robots should belong to $\partial C(R)$ , but $r$ does not. If $\mathcal{P}2_{s}$ holds, then only $r$ can be the remaining unmatched robot that moves in $\mathcal{P}2$ since $r$ is guaranteed to not meet a point in $F$ according to the use of Procedure StationaryMove. It follows that during the movement, in case $r$ is stopped by the adversary, it will be selected again by the algorithm as the unique robot that performs move $m_{14}$ . Similar arguments can be applied if $\mathcal{Q}1$ holds, where there is only one robot inside $C(R)$ .

Finally, we prove that $R^{\prime}$ cannot belong to $\mathcal{F}5$ by showing that $\neg\mathtt{f}_{5}=\neg\mathtt{e}\vee(\neg\mathtt{b}_{0}\wedge\neg\mathtt{z}_{1}\wedge\neg\mathtt{z}_{2})$ holds in $R^{\prime}$ . As the moving robot is alone on $C_{\downarrow}^{1}(R^{\prime})$ , $R^{\prime}$ is asymmetric, that is $\mathtt{b}_{0}$ does not hold. If predicate $\mathtt{s}_{+}$ holds then $\mathtt{z}_{1}$ is false. If $\mathtt{s}_{3}$ holds, then there should be a faraway robot $r^{\prime}$ on $C(R^{\prime})$ such that $R^{\prime}\setminus\{r^{\prime}\}$ admits an axis where $r$ resides (being alone on $C_{\downarrow}^{1}(R^{\prime})$ ), that is $\mathtt{z}_{1}$ is false. Now we show that $\mathtt{z}_{2}$ is false in $R^{\prime}$ . If $r$ is the closest robot to $c(R^{\prime})$ then its distance from $c(R^{\prime})$ is not less than $\delta(C^{g}(R^{\prime}))$ , that is $\mathtt{z}_{2}$ is false; else let $r^{\prime}$ be the robot closest to $c(R^{\prime})$ . It follows that if $R^{\prime\prime}=R^{\prime}\setminus\{r^{\prime}\}$ is symmetric, that is $r$ is on an axis of symmetry of $R^{\prime\prime}$ , then also $R\setminus\{r^{\prime}\}$ is symmetric. This contradicts the fact that $\mathtt{z}_{2}$ was false in $R$ as $\neg\mathtt{f}_{5}$ and $\mathtt{e}$ hold.

The above arguments also ensure that no other robot than $r$ can move from the reached configurations.

$\mathit{H}_{3}$ :

Move $m_{1}$ guarantees there are no robots between $r$ and its target.

$\mathit{H}_{4}$ :

Assume that $r$ stops moving because it reaches an intermediate target dictated by Procedure StationaryMove. In this case, predicates $\mathtt{w}$ , $\mathcal{P}1_{s}$ , or $\mathcal{P}2_{s}$ might hold because $\mathtt{i}_{1}$ or $\mathtt{i}_{2}$ become true (clearly, $\mathtt{i}_{3},\ldots,\mathtt{i}_{6}$ cannot become true as $F$ should equal $\partial F$ ). If this is not the case, $r$ is unmatched and the same considerations given for $\mathit{H}_{2}$ hold, that is the configuration belongs to phases $\mathcal{A}2$ or $\mathcal{P}2$ or $\mathcal{Q}1$ .

Assume that $r$ reaches the target $t=[r,c(R)]\cap C^{0,1}(R)$ . If the configuration remains in $\mathcal{F}1$ , then $\mathtt{l}$ holds and the configuration is either in $\mathcal{A}1$ if $\mathtt{s}_{+}$ holds, or in $\mathcal{A}2$ , $\mathcal{C}$ , $\mathcal{D}$ , or $\mathcal{E}1$ if $\mathtt{s}_{3}$ holds. If the configuration is not in $\mathcal{F}1$ , then by the above analysis it belongs to $\mathcal{F}4$ or $\mathtt{w}$ holds.

Sub-phase $\mathcal{A}2$ , where move $m_{2}$ is performed, is the continuation of sub-phase $\mathcal{A}1$ in case the moving robot $r$ stops before reaching its target on $C^{0,1}(R)$ to make predicate $\mathtt{l}$ newly true. Then the same analysis of move $m_{1}$ applies. Hence moves $m_{1}$ and $m_{2}$ are repeatedly applied in order to remove not critical robots from $\partial C(R)$ until there remain exactly three robots on $C(R)$ (unless the configuration reaches phase $\mathcal{F}4$ or satisfies $\mathtt{w}$ before). This can be done according to Properties 1 and 2. Once the resulting configuration satisfies $\mathtt{s}_{3}\wedge\mathtt{l}$ , it does not belong to sub-phase $\mathcal{A}$ anymore. This situation occurs in a finite number of steps. In fact, as shown above, move $m_{1}$ along with move $m_{2}$ bring not critical robots one by one to their designed targets. Since by assumption a robot is guaranteed to traverse at least distance $\nu$ each time it moves, then a finite number of steps suffices to reach the desired configuration.

Three robots on $C(R)$ are necessary to maintain the configuration a leader one in case a multiplicity should be formed in $c(R)$ , that is when predicate $\mathtt{m}_{0}\wedge\neg\mathtt{m}_{1}$ is true. If there are only two robots in $\partial C(R)$ , a third one from $\mathit{int}(C(R))$ is moved on $C(R)$ . This is done in sub-phase $\mathcal{B}$ by means of move $m_{3}$ .

$\mathit{H}_{0}$ :

The move only concerns robot $r$ on $C_{\downarrow}^{1}(R)$ with minimum view.

$\mathit{H}_{1}$ :

During the movement of $r$ the configuration remains a leader configuration. Actually it is asymmetric as there are no multiplicities yet, $r$ cannot participate to neither a rotation, being the only robot on $C_{\downarrow}^{1}(R)$ , or a reflection as the axis of symmetry should pass through $r$ , but then the starting configuration $R$ was symmetric too, a contradiction.

$\mathit{H}_{2}$ :

We show that $m_{3}$ is safe. Assuming that the configuration observed during the move of $r$ still belongs to $\mathcal{F}1$ , then $r$ is always detected as the unique robot on $C_{\downarrow}^{1}(R)$ and hence $\mathcal{B}_{s}$ still holds. The configuration observed while $r$ moves cannot belong neither to $\mathcal{F}2$ nor to $\mathcal{F}3$ as $\mathtt{m}_{0}\Rightarrow\mathtt{m}_{1}$ does not hold (we have $\mathtt{m}_{0}\wedge\neg\mathtt{m}_{1}$ by hypothesis). Similarly, it cannot belong to $\mathcal{F}4$ as a multiplicity in $c(R)$ must be created. Finally, it cannot belong to $\mathcal{F}5$ as the configuration is asymmetric, that is $\mathtt{b}_{0}$ is false; $\mathtt{s}_{2}$ holds hence $\mathtt{z}_{1}$ is false; $\mathtt{z}_{2}$ remains false because, by removing the closest robot to $c(R)$ , the configuration cannot be symmetric due to the movement of robot $r$ , as observed in $\mathit{H}_{1}$ .

The above arguments ensure that during the movement all robots but $r$ are stationary as the configuration remains in $\mathcal{B}$ .

$\mathit{H}_{3}$ :

No collision is possible as, by definition, there are no robots between $C_{\downarrow}^{1}(R)$ and $C(R)$ , and the target $t$ on $C(R)$ cannot coincide with one of the positions of the two robots on $C(R)$ .

$\mathit{H}_{4}$ :

Once $r$ reaches its target, the configuration cannot belong to $\mathcal{F}2$ , $\mathcal{F}3$ , $\mathcal{F}4$ for the same reasons as in $\mathit{H}_{2}$ . The configuration cannot belong to $\mathcal{F}5$ as it is asymmetric, that is $\mathtt{b}_{0}$ is false; $\mathtt{s}_{3}$ holds, but the robots on $C(R)$ form a right-angle triangle and then $\mathtt{z}_{1}$ is false; $\mathtt{z}_{2}$ remains false for the same reasons as in $\mathit{H}_{2}$ . It follows that the configuration remains in $\mathcal{F}1$ . In particular, the configuration is in $\mathcal{C}_{1}$ , $\mathcal{C}_{2}$ or $\mathcal{D}$ , depending on the kind of triangle formed by the robots on $C(R)$ , that is the status of predicates $\mathtt{t}_{0}$ and $\mathtt{t}_{1}$ .

When $|\partial C(R)|=3$ , we have to guarantee that two robots on $C(R)$ are antipodal before removing the third one, otherwise $C(R)$ could change its radius. This is done in sub-phase $\mathcal{C}1$ by means of move $m_{4}$ . The move involving one of the three robots on $C(R)$ makes the triangle they form containing a $90^{\circ}$ angle, and hence two antipodal robots.

$\mathit{H}_{0}$ :

As specified by the definition of $m_{4}$ , the only robot $r$ involved in this move is that on $C(R)$ corresponding to angle $\alpha_{2}$ if the triangle has angles $\alpha_{1}\geq\alpha_{2}\geq\alpha_{3}$ (in case of ties, the uniqueness of $r$ is guaranteed by using the view of robots).

$\mathit{H}_{1}$ :

$r$ remains always detectable because as soon as it starts moving we get $\alpha_{1}>\alpha_{2}>\alpha_{3}$ , that is the triangle formed by the three robots on $C(R)$ is asymmetric. Moreover the triangle remains asymmetric as during the movement and until the end, $\alpha_{1}$ increases, $\alpha_{2}$ maintains its value and $\alpha_{3}$ decreases.

$\mathit{H}_{2}$ :

We show that $m_{4}$ is safe. Assuming that the configuration observed during the move of $r$ still belongs to $\mathcal{F}1$ , as $\mathtt{s}_{3}\wedge\mathtt{t}_{0}$ remains true during the movement, then the configuration remains in $\mathcal{C}1$ . While $r$ moves the observed configuration cannot belong to $\mathcal{F}2$ as $\mathtt{s}_{2}$ does not hold. The same for $\mathcal{F}3$ , as there are no two antipodal robots and then $\mathtt{g}_{2}$ is false. Predicates $\mathcal{F}4_{s}$ cannot hold as the movement is controlled by StationaryMove which preventively calculates the possible points that could make $\mathcal{F}4_{s}$ true at the end of the movement. So, during the movement, $\mathcal{F}4_{s}$ remains false. Similarly, $\mathcal{F}5_{s}$ is false as it is controlled by StationaryMove. As the above defined angles are such that $\alpha_{1}>\alpha_{2}>\alpha_{3}$ during the move, then the robot $r$ on $\alpha_{2}$ is always uniquely determined;

$\mathit{H}_{3}$ :

No collisions are created as the robot moves on $C(R)$ having as target a point antipodal to one of the other two robots. The third robot cannot be on its trajectory as, otherwise, the smallest enclosing circle would be different from $C(R)$ .

$\mathit{H}_{4}$ :

If $r$ stops on a target specified by Procedure StationaryMove, the configuration can remain in $\mathcal{C}1$ . As in case $\mathit{H}_{2}$ , the configuration cannot belong to $\mathcal{F}2$ as $\mathtt{s}_{2}$ does not hold. The same for $\mathcal{F}3$ , as there are no two antipodal robots and then $\mathtt{g}_{2}$ is false. If Procedure StationaryMove computes a target specified at line 1, it could be possible that there exists an embedding satisfying $\mathtt{i}_{1}$ . Then the configuration can belong to sub-phase $\mathcal{P}1$ of $\mathcal{F}4$ . Moreover, predicate $\mathtt{w}$ might hold. If the computed target comes from line 1 of Procedure StationaryMove, an angle of $\alpha$ degrees is formed with a robot on $C^{g}(R)$ . In that case the configuration may belong to either sub-phase $\mathcal{P}1$ or sub-phase $\mathcal{P}2$ of $\mathcal{F}4$ . If the computed target comes from line 1 of Procedure StationaryMove, an asymmetric configuration where $\mathtt{z}_{1}$ holds is reached that may belong to sub-phase $\mathcal{U}$ of $\mathcal{F}5$ .

If the robot stops reaching the target of move $m_{4}$ , forming an angle of $90^{\circ}$ , $t_{0}$ is false and then the configuration can satisfy $\mathcal{C}2_{s}\vee\mathcal{D}_{s}\vee\mathcal{E}1_{s}$ . If the configuration is not in $\mathcal{F}1$ , as above, it can satisfy $\mathtt{w}$ , $\mathcal{F}4_{s}$ , or $\mathcal{F}5_{s}$ .

In case a multiplicity in $c(R)$ must be formed, in order to guarantee that the configuration remains a leader configuration, the algorithm ensures the triangle formed by the three robots on $C(R)$ is asymmetric. To guarantee the stationarity of the configuration, we impose that the triangle has angles equal to $30^{\circ}$ , $60^{\circ}$ , and $90^{\circ}$ degrees. This is done in sub-phase $\mathcal{C}2$ by means of move $m_{5}$ .

$\mathit{H}_{0}$ :

Among the three robots on $C(R)$ , only the one that does not admit an antipodal robot is moved (notice that the status of $\mathtt{t}_{0}$ in $\mathcal{C}2_{s}$ implies two antipodal robots on $C(R)$ ).

$\mathit{H}_{1}$ :

The configuration is always asymmetric because the triangle formed by the three robots can be symmetric only at the beginning.

$\mathit{H}_{2}$ :

We show that $m_{5}$ is safe. As predicate $\mathtt{m}_{0}\wedge\neg\mathtt{m}_{1}$ holds during the whole movement, that is a multiplicity in $c(R)$ must be formed, then the configuration observed during the movement remains in sub-phase $\mathcal{C}2$ until $\mathtt{t}_{1}$ becomes true. For the same reason, the configuration cannot belong to $\mathcal{F}2$ , $\mathcal{F}3$ , and $\mathcal{F}4$ . About $\mathcal{F}5$ , the configuration is asymmetric hence $\mathtt{b}_{0}$ is false; there are two antipodal robots, hence $\mathtt{z}_{1}$ is false; the configuration obtained by excluding the closest robot to $c(R)$ cannot be symmetric as the triangle on $C(R)$ is asymmetric, then $\mathtt{z}_{2}$ is false.

During the movement all other robots are stationary, for the same reason as in $\mathit{H}_{0}$ .

$\mathit{H}_{3}$ :

No collisions are created as the target of the moving robot is always between the antipodal robots on $C(R)$ .

$\mathit{H}_{4}$ :

As discussed in $\mathit{H}_{2}$ , the configuration remains in $\mathcal{F}1$ and in particular in $\mathcal{C}2$ or $\mathcal{D}$ depending on $\mathtt{t}_{1}$ .

Once the three robots on $C(R)$ form a triangle having angles equal to $30^{\circ}$ , $60^{\circ}$ , and $90^{\circ}$ degrees, the multiplicity in $c(R)$ can be safely formed with respect to undesired symmetries. This is done in sub-phase $\mathcal{D}$ by means of move $m_{6}$ .

$\mathit{H}_{0}$ :

The only moving robot $r$ is the closest to $c(R)$ , not in $c(R)$ , and of minimum view.

$\mathit{H}_{1}$ :

The configuration remains a leader configuration as predicate $\mathtt{t}_{1}$ remains true during the movement. In fact, none of the three robots on $C(R)$ is moved because at least two points in $F$ are on $C(F)$ , so the multiplicity to be formed is at most of $|F|-2$ elements. However the algorithm moves at most $|F|-3$ robots in $c(R)$ (see predicate $\mathtt{m}_{1}$ ).

$\mathit{H}_{2}$ :

We show that $m_{6}$ is safe. Predicate $\mathtt{t}_{1}\wedge\mathtt{m}_{0}\wedge\neg\mathtt{m}_{1}$ holds during the whole movement, then the configuration remains in $\mathcal{D}$ until $\mathtt{m}_{1}$ becomes true. As long as $\mathtt{m}_{1}$ is false, the configuration cannot be in $\mathcal{F}2$ , $\mathcal{F}3$ , and $\mathcal{F}4$ . It cannot be in $\mathcal{F}5$ because either $\mathtt{e}$ is false or $\mathtt{b}_{0}\vee\mathtt{z}_{1}\vee\mathtt{z}_{2}$ is false. In fact, if $\mathtt{e}$ is true, the configuration is asymmetric, that is $\mathtt{b}_{0}$ is false. During the movement predicate $\mathtt{z}_{1}$ remains false as the three robots on $C(R)$ form a right-angle triangle. The configuration without $r$ is asymmetric, that is $\mathtt{z}_{2}$ is false.

During the movement all other robots are stationary, for the same reason as in $\mathit{H}_{0}$ .

$\mathit{H}_{3}$ :

No collisions are created as the moving robot is the closest to the target.

$\mathit{H}_{4}$ :

Once the robot reaches $c(R)$ , either another robot must be moved in $c(R)$ because $\mathtt{m}_{1}$ is still false and then the configuration is still in $\mathcal{D}$ , or $\mathtt{m}_{1}$ holds. In the latter case the configuration can be in $\mathcal{E}1$ . It cannot be in $\mathcal{F}2$ , as $\mathtt{s}_{3}$ holds, and $\mathtt{w}$ cannot be satisfied as at least one robot must be still moved in $c(R)$ . The configuration can be in any sub-phase of $\mathcal{F}3$ as, by chance, $\mathtt{g}_{2}$ might hold. Moreover the configuration can belong to $\mathcal{F}4$ , sub-phase $\mathcal{P}$ , but not $\mathcal{Q}$ as predicate $\mathtt{q}$ is false. Finally, the configuration cannot be in $\mathcal{F}5$ for the same reasons as in $\mathit{H}_{2}$ .

As soon as phase $\mathcal{D}$ terminates and the configuration is in $\mathcal{E}1$ , move $m_{1}$ is applied to remove one robot from $C(R)$ leaving only the two antipodal robots.

$\mathit{H}_{0}$ :

The only not critical robot $r$ on $C(R)$ is moved.

$\mathit{H}_{1}$ :

During the movement of $r$ the configuration remains a leader configuration as $r$ cannot participate to neither a rotation, being the only robot on $C_{\downarrow}^{1}(R)$ , nor a reflection as the axis of symmetry should pass through $r$ , but then the starting configuration $R$ was symmetric too, a contradiction.

$\mathit{H}_{2}$ :

We prove that $m_{1}$ in $\mathcal{E}1$ is safe. Assuming that the configuration $R^{\prime}$ observed during the movement of $r$ still belongs to $\mathcal{F}1$ , then as soon as $r$ starts moving, predicate $\mathcal{E}2_{s}=\mathtt{s}_{2}\wedge\neg\mathtt{l}\wedge(\mathtt{m}_{0}\Rightarrow\mathtt{m}_{1})$ holds. In fact, in $\mathcal{E}1$ predicate $\mathtt{s}_{3}$ holds and by moving one robot, $\mathtt{s}_{2}$ becomes true while $\mathtt{l}$ becomes false as the robot has to reach its target.

The configuration while $r$ moves cannot belong to $\mathcal{F}2$ as $\mathtt{l}$ does not hold. It cannot belong to $\mathcal{F}3$ as well because $\mathtt{f}_{3}$ does not hold in $\mathcal{E}1$ and $m_{1}$ cannot change this status. Possibly, the configuration falls in $\mathcal{F}4$ , in particular only in sub-phase $\mathcal{P}2$ . In fact, in $\mathcal{P}1$ predicate $\mathtt{i}_{1}$ should hold, but since $\mathtt{s}_{2}$ holds, $g^{\prime\prime}$ should be on $\mu(g^{\prime\prime})$ . In $\mathcal{Q}$ , there must be at least three robots on $C(R)$ . If $\mathcal{P}2$ holds then only $r$ can be the remaining unmatched robot that moves in $\mathcal{P}2$ since $r$ is guaranteed to not meet a point in $F$ according to the use of Procedure StationaryMove. It follows that during the movement and once $r$ is stopped by the adversary, it will be selected again by the algorithm as the unique robot that performs move $m_{14}$ .

The configuration $R^{\prime}$ cannot belong to $\mathcal{F}5$ as either $\mathtt{e}$ is false or we now show that $\mathtt{b}_{0}\vee\mathtt{z}_{1}\vee\mathtt{z}_{2}$ is false. As the moving robot is alone on $\mathcal{C}_{\downarrow}^{1}(R^{\prime})$ , the configuration is asymmetric, that is $\mathtt{b}_{0}$ is false. Since $\mathtt{s}_{2}$ holds $\mathtt{z}_{1}$ is false. Finally as $\mathtt{z}_{2}$ is false in $R$ , then, by removing the closest robot to $c(R^{\prime})$ , the obtained configuration cannot be symmetric, hence $\mathtt{z}_{2}$ remains false.

The above arguments also ensure that no other robot than $r$ can move from the reached configurations.

$\mathit{H}_{3}$ :

Move $m_{1}$ guarantees there are no robots between $r$ and its target.

$\mathit{H}_{4}$ :

If $r$ stops because it reaches an intermediate target dictated by Procedure StationaryMove, then $\mathtt{w}$ or $\mathcal{P}2$ might hold, because $\mathtt{i}_{2}$ becomes true. For the same reasons as above, $\mathcal{P}1$ and $\mathcal{Q}$ cannot be reached. If $r$ reaches the target $t=[r,c(R)]\cap C^{0,1}(R)$ , the obtained configuration is not in $\mathcal{F}1$ anymore, as $\mathtt{f}_{2}$ holds. Then, it can be in $\mathcal{F}2$ as $\mathtt{f}_{2}$ is now true, and as above it can be in $\mathcal{F}4$ or $\mathtt{w}$ holds.

Similarly to sub-phases $\mathcal{A}1$ and $\mathcal{A}2$ , sub-phase $\mathcal{E}2$ is the continuation of sub-phase $\mathcal{E}1$ in case the moving robot $r$ stops before reaching its target on $C^{0,1}(R)$ to make predicate $\mathtt{l}$ newly true. Then the same analysis of move $m_{1}$ for $\mathcal{E}1$ applies. Once $r$ reaches its target, predicate $\mathtt{f}_{2}$ holds, and the configuration can be in $\mathcal{F}2$ , $\mathcal{F}4$ or $\mathtt{w}$ holds. ∎

Lemma 9

Let $R$ be a stationary configuration in $\mathcal{F}2$ . From $R$ the algorithm eventually leads to a stationary configuration belonging to $\mathcal{F}3$ , $\mathcal{F}4$ or where $\mathtt{w}$ holds.

Proof

Recall that the aim of $\mathcal{F}2$ is the formation of a configuration satisfying predicate $\mathtt{g}_{2}$ (cf definition of predicate $\mathtt{f}_{3}$ in $\mathcal{F}3_{s}$ ). That is, the target configuration has three robots acting as guards such that two of them, $g^{\prime}$ and $g^{\prime\prime}$ , are antipodal on $C(R)$ and the third one $g$ is on $C^{g}(R)$ forming an angle of $\alpha$ degree with $g^{\prime}$ .

By Lemma 4, exactly one of the predicates for the starting phases in Table 4 is true. In turn, this implies that exactly one of the moves associated to the sub-phases of $\mathcal{F}2$ is applied to $R$ . We show that the properties $\mathit{H}_{0},\ldots,\mathit{H}_{4}$ hold for each possible move applied to $R$ .

We analyze move $m_{7}$ : it is performed in sub-phase $\mathcal{G}1$ to bring a robot $r$ on $C^{g}(R)$ .

$\mathit{H}_{0}$ :

The move selects only one robot: the robot $r$ on $C^{1}_{\uparrow}(R)$ of minimum view.

$\mathit{H}_{1}$ :

During the movement of $r$ , the configuration remains a leader configuration as $r$ cannot participate to neither a rotation, being the only robot on $C_{\uparrow}^{1}(R)$ , or a reflection as the axis of symmetry should pass through $r$ , but then the starting configuration $R$ was symmetric too, a contradiction.

$\mathit{H}_{2}$ :

We show that $m_{7}$ is safe. During the movement of $r$ , as $\mathtt{f}_{2}$ remains true, the observed configuration cannot belong to $\mathcal{F}1$ . Assuming the observed configuration still belongs to $\mathcal{F}2$ , predicate $\mathcal{G}1_{s}$ remains true. Since $r$ has not yet reached the target, $\mathtt{g}_{2}$ is still false and hence the observed configuration cannot belong to $\mathcal{F}3$ . Possibly, the configuration falls in $\mathcal{F}4$ , in particular sub-phase $\mathcal{P}2$ . In fact, in $\mathcal{P}1$ predicate $\mathtt{g}_{1}$ should hold, but $r$ is certainly not on $C^{g}(R)$ (target of the current move). In $\mathcal{Q}$ there should be at least three robots in $\partial C(R)$ , but $\mathtt{s}_{2}$ holds. If $\mathcal{P}2$ holds then only $r$ can be the remaining unmatched robot that moves in $\mathcal{P}2$ since $r$ is guaranteed to not meet a point in $F$ according to the use of Procedure StationaryMove. The configuration cannot belong to $\mathcal{F}5$ as either $\mathtt{e}$ is false or $\mathtt{b}_{0}\vee\mathtt{z}_{1}\vee\mathtt{z}_{2}$ is false. In fact, if $\mathtt{e}$ is true then the configuration is asymmetric, that is $\mathtt{b}_{0}$ is false; $\mathtt{z}_{1}$ cannot hold as $\mathtt{s}_{2}$ holds; $\mathtt{z}_{2}$ remains false as $m_{7}$ moves $r$ toward $C^{g}(R)$ . It follows that during the movement and once $r$ is stopped by the adversary, it will be selected again by the algorithm as the unique robot that performs move $m_{14}$ .

Summarizing, while $r$ is moving the configuration can be in sub-phase $\mathcal{G}1$ of $\mathcal{F}2$ or in sub-phase $\mathcal{P}2$ of $\mathcal{F}4$ . In both cases $r$ is always recognized as the only robot allowed to move.

$\mathit{H}_{3}$ :

no collisions are created as there is no robot between $r$ and $C^{g}(R)$ .

$\mathit{H}_{4}$ :

Assume that $r$ stops moving because it reaches an intermediate target dictated by Procedure StationaryMove. Then, $\mathtt{w}$ can hold or the configuration is still in $\mathcal{G}1$ . In fact, by the analysis in $\mathit{H}_{2}$ , the configuration might be in $\mathcal{P}2$ , but this is excluded as the robot is on $C^{i}_{\uparrow}(F)$ , for some $i>0$ , while $\mathtt{i}_{2}$ does not hold because it requires that $d(c(R),r)<d(c(F),f)$ , where $f$ is a point on $C^{1}_{\uparrow}(F)\cap F$ .

Assume $r$ reaches its target on $C^{g}(R)$ . Then, $\mathtt{w}$ cannot hold because there are no points of $F$ on $C^{g}(R)$ by definition. The configuration is not in $\mathcal{F}1$ as $\mathtt{f}_{2}$ holds. As $\mathtt{g}_{0}$ holds, the configuration can be in $\mathcal{G}2$ and in $\mathcal{F}3$ in case also $\mathtt{g}_{1}$ holds. The configuration can be in $\mathcal{F}4$ , in particular in $\mathcal{P}1$ or $\mathcal{P}2$ depending on $\mathtt{i}_{1}$ or $\mathtt{i}_{2}$ . It cannot be in $\mathcal{Q}$ because $\mathtt{s}_{2}$ holds. The configuration cannot be on $\mathcal{F}5$ by the same analysis in $\mathit{H}_{2}$ .

Once there is a robot $r$ on $C^{g}(R)$ , to make $\mathtt{g}_{1}$ true, that is to correctly place guard $g$ , it should be rotated on $C^{g}(R)$ . This is done in sub-phase $\mathcal{G}2$ by move $m_{8}$ .

$\mathit{H}_{0}$ :

$r$ is the unique robot on $C^{g}(R)$ ;

$\mathit{H}_{1}$ :

During the movement of $r$ , the configuration remains a leader configuration as $r$ cannot participate to neither a rotation, being the only robot on $C^{g}(R)$ , or a reflection as the axis of symmetry should pass through $r$ , and through the antipodal robots $g^{\prime}$ and $g^{\prime\prime}$ or between them. These cases can happen only if $r$ is collinear with $g^{\prime}$ and $g^{\prime\prime}$ or if it lies on the line perpendicular to the segment $[g^{\prime},g^{\prime\prime}]$ . In any other case, the movement of $g$ cannot generate an axis of reflection as it would imply the existence of a point $t^{\prime}$ , representing the reflection of $t$ with respect to the axis, such that $d(g,t^{\prime})<d(g,t)$ . This contradicts the hypothesis that $t$ is the required closest point.

$\mathit{H}_{2}$ :

We show that $m_{8}$ is safe. During the movement of $r$ , as $\mathtt{f}_{2}$ remains true, the observed configuration cannot belong to $\mathcal{F}1$ . Assuming the configuration still belongs to $\mathcal{F}2$ , predicate $\mathcal{G}2_{s}$ remains true. As $\mathtt{g}_{2}$ is still not true, the configuration cannot belong to $\mathcal{F}3$ . The observed configuration does not fall in $\mathcal{F}4$ . In particular: as $\mathtt{g}_{1}$ is false, it is not in $\mathcal{P}1$ ; it is not in $\mathcal{P}2$ otherwise $\mathtt{i}_{2}$ true during the movement of $r$ implies $\mathtt{i}_{2}$ true in the starting configuration $R$ too, a contradiction; it is not in $\mathcal{Q}$ as $\mathtt{s}_{2}$ still holds during the movement of $r$ , while $\mathcal{Q}$ handles configurations with at least $n-1$ robots on $C(R)$ . The configuration does not fall in $\mathcal{F}5$ . In particular: either $\mathtt{e}$ is false or $\mathtt{b}_{0}\vee\mathtt{z}_{1}\vee\mathtt{z}_{2}$ is false. In fact, if $\mathtt{e}$ is true then the configuration is asymmetric, that is $\mathtt{b}_{0}$ is false. $\mathtt{z}_{1}$ cannot hold as $\mathtt{s}_{2}$ holds. $\mathtt{z}_{2}$ does not hold as $r$ is on $C^{g}(R)$ .

As the configuration remains in $\mathcal{G}2$ by the above analysis, robot $r$ is always detected as the only moving one.

$\mathit{H}_{3}$ :

No collisions are created as there is only $r$ on $C^{g}(R)$ .

$\mathit{H}_{4}$ :

If $r$ reaches its target on $C^{g}(G)$ , $\mathtt{w}$ cannot hold because there are no points of $F$ on $C^{g}(R)$ by definition. The configuration is not in $\mathcal{F}1$ as $\mathtt{f}_{2}$ holds. As $\mathtt{g}_{2}$ holds, the configuration can be in $\mathcal{F}3$ . The configuration can be in $\mathcal{F}4$ , in particular in $\mathcal{P}1$ as $\mathtt{i}_{1}$ might hold. It cannot be in $\mathcal{P}2$ or in $\mathcal{Q}$ by the same analysis in $\mathit{H}_{2}$ . It cannot be in $\mathcal{F}5$ by the same analysis in $\mathit{H}_{2}$ .

In case a robot $r$ is in $c(R)$ , but there is no multiplicity in $c(F)$ , then $r$ will be moved on $C^{g}(R)$ in sub-phase $\mathcal{H}$ by means of move $m_{9}$ .

$\mathit{H}_{0}$ :

$r$ is clearly the only robot to move;

$\mathit{H}_{1}$ :

the configuration is always a leader configuration by the same analysis provided for move $m_{8}$ in sub-phase $\mathcal{G}2$ .

$\mathit{H}_{2}$ :

We show that $m_{9}$ is safe. As soon as $r$ starts moving, the observed configuration can only belong in $\mathcal{G}$ . In fact, during the movement of $r$ , $C^{g}(R)$ changes, but $r$ is recognized as the unique robot on $C^{1}_{\uparrow}(R)$ . It follows that the configuration is in $\mathcal{G}2$ or $\mathcal{G}1$ depending whether $r$ is on the current circle $C^{g}(R)$ or not. The configuration cannot be in $\mathcal{F}1$ as $\mathtt{f}_{2}$ holds. It cannot be in $\mathcal{H}$ as $\mathtt{c}$ is false, and it cannot be in $\mathcal{F}3$ as $\mathtt{g}_{2}$ is false. It cannot be in $\mathcal{F}4$ as $\mathtt{g}_{1}$ remains false and this excludes $\mathcal{P}1$ , $\mathtt{i}_{2}$ remains false and this excludes $\mathcal{P}2$ , and $\mathcal{Q}$ is excluded by $\mathtt{s}_{2}$ . It cannot be in $\mathcal{F}5$ as the configuration is asymmetric with $c(R)$ occupied, which means both $\mathtt{z}_{1}$ and $\mathtt{z}_{2}$ are false.

In any of the reachable sub-phases described, $r$ is the only moving robot.

$\mathit{H}_{3}$ :

No collisions are created as there are no further robots between $c(R)$ and $C^{g}(R)$ .

$\mathit{H}_{4}$ :

Once $r$ reaches $C^{g}(R)$ , $\mathtt{w}$ cannot hold because there are no points of $F$ on $C^{g}(R)$ by definition. The obtained configuration is not in $\mathcal{F}1$ as $\mathtt{f}_{2}$ holds, and is not in $\mathcal{F}3$ as $\mathtt{g}_{1}$ is false. The obtained configuration is not in $\mathcal{F}4$ nor in $\mathcal{F}5$ as both $\mathtt{f}_{4}$ and $\mathtt{f}_{5}$ remain false, for similar reasons as in $\mathit{H}_{2}$ . It means the configuration can only be in phase $\mathcal{F}2$ , in particular it cannot be in $\mathcal{G}1$ as $\mathtt{g}_{0}$ is true, and it cannot be in $\mathcal{H}$ as $\mathtt{c}$ is false. So it can only be in $\mathcal{G}2$ .

∎

Lemma 10

Let $R$ be a stationary configuration in $\mathcal{F}3$ . From $R$ the algorithm eventually leads to a stationary configuration belonging to $\mathcal{F}4$ .

Proof

By Lemma 5, exactly one of the predicates for the starting phases in Table 5 is true. In turn, this implies that exactly one of the moves associated to the sub-phases of $\mathcal{F}3$ is applied to $R$ . We show that the properties $\mathit{H}_{0},\ldots,\mathit{H}_{4}$ hold for each possible move applied to $R$ .

Let $P^{*}=\{[c(F),f^{*}]\cap C^{t}(R)~{}|~{}f^{*}\in F^{*}\}$ , and let $d$ be the distance from any point in $P^{*}$ to any target in $F^{*}$ . Let us start the analysis of moves $m_{10}$ , $m_{11}$ , and $m_{12}$ by assuming there is exactly one robot $r$ on $C^{t}(R)$ and that $r$ is not on a point of $P^{*}$ , that is $\mathtt{d}_{0}$ holds while $\mathtt{d}_{1}$ is false. In this case, the configuration is in sub-phase $\mathcal{M}$ and move $m_{10}$ is applied.

$\mathit{H}_{0}$ :

The only moved robot is that on $C^{t}(R)$ , that by assumption is $r$ .

$\mathit{H}_{1}$ :

The configuration is maintained a leader configuration by the position of the three guards $g$ , $g^{\prime}$ , and $g^{\prime\prime}$ . In fact, as $g$ is the only robot on $C^{g}(R)$ , the configuration cannot be rotational. Moreover, the only possible reflection axis should pass through $g$ , but there is no robot that can be reflected to $g^{\prime}$ as, by predicate $\mathtt{g}_{1}$ , $g^{\prime}$ is the only robot such that $\sphericalangle(g,c(R),g^{\prime})=\alpha$ .

$\mathit{H}_{2}$ :

We show that $m_{10}$ is safe. As $\mathtt{f}_{3}$ holds during the movement of $r$ , the observed configuration cannot be in $\mathcal{F}1$ and $\mathcal{F}2$ . Moreover, during the move, both robots $r$ and $g$ do not stay neither on a target of $F$ nor on $C(R)$ . As each predicate among $\mathtt{i}_{1},\ldots,\mathtt{i}_{6}$ requires that at most two robots are not on target and at least one of them is on $C(R)$ , they are all false and then the observed configuration is not in $\mathcal{F}4$ . The configuration does not fall in $\mathcal{F}5$ . In particular: either $\mathtt{e}$ is false or $\mathtt{b}_{0}\vee\mathtt{z}_{1}\vee\mathtt{z}_{2}$ is false. In fact, if $\mathtt{e}$ is true then the configuration is asymmetric due to guard $g$ , that is $\mathtt{b}_{0}$ is false. $\mathtt{z}_{1}$ cannot hold as $\mathtt{g}_{2}$ holds which implies the existence of antipodal robots on $C(R)$ . $\mathtt{z}_{2}$ does not hold as there is $g$ on $C^{g}(R)$ . Hence, as $\mathtt{d}_{0}\wedge\neg\mathtt{d}_{1}$ holds, the observed configuration remains in $\mathcal{F}3$ , sub-phase $\mathcal{M}$ . Robot $r$ remains the only robot on $C^{t}(R)$ , then all the other robots are stationary.

$\mathit{H}_{3}$ :

Collisions are impossible as $r$ rotates on $C^{t}(R)$ and it is the only robot on it.

$\mathit{H}_{4}$ :

Once $r$ reaches the target on $C^{t}(R)$ , by the analysis done in $\mathit{H}_{2}$ , the configuration remains in $\mathcal{F}3$ , but now $\mathtt{d}_{1}$ holds. If still $r=\textit{min\_view}(R^{\neg m}_{\eta})$ , then $\mathtt{d}_{2}$ is false as the current target $\mu(r)\in F^{*}$ is reachable without intersecting $C^{t}(R)$ . If another robot $r^{\prime}=\textit{min\_view}(R^{\neg m}_{\eta})$ (this can happen only the first time phase $\mathcal{F}3$ is applied, and there was already $r$ on $C^{t}(R)$ ), then again $\mathtt{d}_{2}$ is false because otherwise the distance from $r^{\prime}$ to $\mu(r^{\prime})$ would be greater than $d$ , a contradiction. Hence, the obtained configuration is in sub-phase $\mathcal{O}$ .

When $\mathtt{d}_{0}\Rightarrow\mathtt{d}_{1}$ holds, the configuration is in sub-phase $\mathcal{N}$ or $\mathcal{O}$ depending on whether $\mathtt{d}_{2}$ is true or not. Let us assume that $\mathtt{d}_{2}$ is true, that is $C^{t}(R)\cap(r,\mu(r)]\neq\emptyset$ , where $r=\textit{min\_view}(R^{\neg m}_{\eta})$ . Then, move $m_{11}$ is applied and $r$ is moved toward the closest point $p_{1}$ in $C^{t}(R)\cap(r,\mu(r)]$ according to Procedure CollisionFreeMove.

$\mathit{H}_{0}$ :

The only moved robot is $r$ that is the one with minimum view in $R^{\neg m}_{\eta}$ . It is unique as the configuration is a leader configuration and hence there cannot be two robots in $R^{\neg m}_{\eta}$ with the same view.

$\mathit{H}_{1}$ :

As in the analysis done for move $m_{10}$ , the configuration is maintained a leader configuration by the guards.

$\mathit{H}_{2}$ :

We show that $m_{11}$ is safe. During the movement of $r$ , the configuration remains in $\mathcal{F}3$ by the same analysis done for move $m_{10}$ . In particular, it can still belong to sub-phase $\mathcal{N}$ or to sub-phase $\mathcal{O}$ . In fact, if there are robots between $r$ and $p_{1}$ , then $r$ receives an intermediate target $p$ by procedure CollisionFreeMove and hence $\mathtt{d}_{2}$ may remain true or not. By Lemma 1, condition $3)$ , robot $r$ reduces its distance to $p_{1}$ and then to $\mu(r)$ , being $p_{1}$ an intermediate point between the initial position of $r$ and $\mu(r)$ . Then the distance $\eta^{\prime}$ of $r$ to $\mu(r)$ is such that $\eta^{\prime}<\eta$ , and hence it remains the only robot in $R^{\neg m}_{\eta^{\prime}}$ . All the other robots remain stationary as their distance to any target is at least $\eta$ .

$\mathit{H}_{3}$ :

Collisions are impossible as $r$ is moved according to Procedure CollisionFreeMove.

$\mathit{H}_{4}$ :

By the analysis provided for $m_{10}$ , the configuration remains in $\mathcal{F}3$ while $r$ is moving. Here there are three possible cases: (i) $r$ reaches target $p_{1}$ ; (ii) $r$ has reached the new target $p$ (or it has been stopped before by the adversary) and the trajectory toward $\mu(r)$ does not intersect $C^{t}(R)$ anymore; (iii) $r$ has reached the new target $p$ (or it has been stopped before by the adversary) and still the trajectory toward $\mu(r)$ intersects $C^{t}(R)$ . In case (i) $r$ is now the only robot on $C^{t}(R)$ , and the configuration is in sub-phase $\mathcal{M}$ . In case (ii), $\mathtt{d}_{2}$ is false and the configuration is in $\mathcal{O}$ , and by Lemma 1, $r$ will be selected again to move. In case (iii), the configuration is still in $\mathcal{N}$ and robot $r$ will be selected again by the algorithm. In fact, by condition $3)$ of Lemma 1, $r=\textit{min\_view}(R^{\neg m}_{\eta^{\prime}})$ , with $\eta^{\prime}<\eta$ . Moreover, by condition $1)$ of Lemma 1, $C(R)$ and the target $\mu(r)$ do not change. Let $p^{\prime}\neq p$ be the closest point to $r$ on $(r,\mu(r)]\cap C^{t}(R)$ . By condition $2)$ of Lemma 1, there are no robots between $r$ and $p^{\prime}$ , that is there will not be a deviation by means of CollisionFreeMove when $r$ applies again $m_{11}$ . Note that, in case (iii), still $r$ applies $m_{11}$ , so predicate $\mathcal{N}_{e}$ does not hold, but now $p^{\prime}$ is assured to be reached within a finite number of steps because in each step $r$ moves of at least $\nu$ .

Let us assume that $\mathtt{d}_{2}$ is false, that is $C^{t}(R)\cap(r,\mu(r)]=\emptyset$ , where $r=\textit{min\_view}(R^{\neg m}_{\eta})$ . Then, the configuration is in $\mathcal{O}$ , move $m_{12}$ is applied and $r$ is moved toward $\mu(r)$ according to Procedure CollisionFreeMove.

$\mathit{H}_{0}$ :

As in move $m_{11}$ , the only moved robot is that with minimum view $r=R^{\neg m}_{\eta}$ . Robot $r$ is unique as the configuration is a leader configuration.

$\mathit{H}_{1}$ :

As in the analysis done for move $m_{10}$ , the configuration is maintained a leader configuration by the guards.

$\mathit{H}_{2}$ :

During the movement of $r$ , the configuration remains in $\mathcal{F}3$ by the same analysis done for move $m_{10}$ . In particular, it can only belong to $\mathcal{O}$ as the trajectory from $r$ to $\mu(r)$ cannot intersect $C^{t}(R)$ , even if Procedure CollisionFreeMove assigns a new target. By Lemma 1 condition $3)$ , robot $r$ reduces its distance to $\mu(r)$ . Then the distance $\eta^{\prime}$ of $r$ to $\mu(r)$ is such that $\eta^{\prime}<\eta$ , and hence it remains the only robot in $R^{\neg m}_{\eta^{\prime}}$ . All the other robots remain stationary as their distance to any target is at least $\eta$ .

$\mathit{H}_{3}$ :

Collisions are impossible as $r$ is moved according to Procedure CollisionFreeMove.

$\mathit{H}_{4}$ :

If $r$ reaches a new target $p$ assigned by CollisionFreeMove (or it has been stopped before by the adversary), the configuration is still in $\mathcal{O}$ but now, by condition $2)$ of Lemma 1, there are no robots between $r$ and $\mu(r)$ . By condition $1)$ of the same lemma both $C(R)$ and $\mu(r)$ do not change, and by condition $3)$ , robot $r$ reduces its distance to $\mu(r)$ . So $r$ applies again $m_{12}$ , predicate $\mathcal{O}_{e}$ does not hold, but now $\mu(r)$ is assured to be reached within a finite number of steps because in each step $r$ moves of at least $\nu$ .

If $r$ reaches $\mu(r)$ and there are still unmatched points in $F\setminus\{\mu(g),\mu(g^{\prime\prime})\}$ then the configuration remains in $\mathcal{F}3$ as $\mathtt{f}_{3}\wedge\neg\mathtt{f}_{4}\wedge\neg\mathtt{f}_{5}\wedge\neg\mathtt{w}$ holds. In particular, it belongs either to $\mathcal{N}$ or to $\mathcal{O}$ depending on $\mathtt{d}_{2}$ . It cannot belong to $\mathcal{M}$ as a robot on $C^{t}(R)$ would move before $r$ .

If $r$ reaches $\mu(r)$ and all points in $F\setminus\{\mu(g),\mu(g^{\prime\prime})\}$ are matched, then $\mathtt{w}$ does not hold as $g$ is not on $\mu(g)$ . The configuration is not in $\mathcal{F}5$ by the same analysis done for $\mathit{H}_{2}$ of move $m_{10}$ . Hence, the configuration is in $\mathcal{F}4$ . In particular it can be in sub-phases $\mathcal{P}1$ , $\mathcal{P}2$ , or $\mathcal{Q}1$ , as $g$ is not on $C(R)$ .

Clearly, the fact that from $\mathcal{O}$ the configuration can go back to $\mathcal{N}$ or to $\mathcal{O}$ can happen only a finite number of times, until all points in $F\setminus\{\mu(g),\mu(g^{\prime\prime})\}$ become matched.

In conclusion, moves $m_{10}$ , $m_{11}$ , and $m_{12}$ can be applied only a finite number of times, then eventually the configuration leaves phase $\mathcal{F}3$ and, following the above analysis, phase $\mathcal{F}4$ is reached. ∎

Lemma 11

Let $R$ be a stationary configuration in $\mathcal{F}4$ . From $R$ the algorithm eventually leads to a stationary configuration where $\mathtt{w}$ holds.

Proof

By Lemma 5, exactly one of the predicates for the starting phases in Table 6 is true. In turn, this implies that exactly one of the moves associated to the sub-phases of $\mathcal{F}4$ is applied to $R$ . We show that the properties $\mathit{H}_{0},\ldots,\mathit{H}_{4}$ hold for each possible move applied to $R$ .

We recall that in this phase only guards $g$ and $g^{\prime\prime}$ need to be moved to complete the formation of the pattern. As guards move, the embedding exploited in phase $\mathcal{F}3$ cannot be always recognized, at least not straightforwardly. Each sub-phase refers in fact to a different embedding that tries to reconstruct where the configuration comes from.

Sub-phases $\mathcal{P}1$ and $\mathcal{P}2$ manage the case where $\mathtt{q}$ is false. In sub-phase $\mathcal{P}1$ , guard $g^{\prime\prime}$ rotates along $C(R)$ in order to reach $\mu(g^{\prime\prime})$ , performing move $m_{13}$ . Since $\mathtt{q}$ is false, we are guaranteed that $C(R)$ does not change while $g^{\prime\prime}$ moves. In fact, let $p$ be the antipodal point to $\mu(g^{\prime\prime})$ . If $\mathtt{q}$ is false because of the first condition that is $\partial C(F)\neq F$ , then all points in $\partial C(F)\setminus\mu(g^{\prime\prime})$ are occupied by robots as $\mu(g)$ is inside $C(R)$ . Without loss of generality, let us assume that $g^{\prime\prime}$ needs to rotate in the clockwise direction to reach $\mu(g^{\prime\prime})$ . Since $C(F)=C(R)$ , there must exist a point $f\in\partial C(F)$ , which is occupied, that either coincides with $p$ or it can be met in the clockwise direction by rotating on $C(R)$ from $p$ . Robot $g^{\prime\prime}$ moves in between $\mu(g^{\prime\prime})$ and $f$ , and hence it is not critical. Similar arguments hold if $\mathtt{q}$ is false because of the second condition that is $F$ contains multiplicities since $\mu(g)$ is either inside $C(R)$ or on a multiplicity. If $\mathtt{q}$ is false because of the third condition, then $\sphericalangle(f_{2},c(R),f_{n})\leq 180^{\circ}$ . If $\mu(g^{\prime\prime})$ is reached by $g^{\prime\prime}$ in the counter-clockwise direction, then by the disposal of the points on $C(F)$ and the minimality of $f_{1}$ , $g^{\prime\prime}$ can safely move without affecting $C(R)$ . If $\mu(g^{\prime\prime})$ is reached by $g^{\prime\prime}$ in the clockwise direction, then the condition on $\mathtt{q}$ assures that $f_{n}$ lies in the counter-clockwise direction from $g^{\prime\prime}$ , it is occupied, and it is closer than $p$ to $\mu(g^{\prime\prime})$ .

$\mathit{H}_{0}$ :

Only $g^{\prime\prime}$ is involved in move $m_{13}$ . Even though $g^{\prime\prime}$ moves, $\mathtt{i}_{1}$ ensures to always recognize the same robot as $g^{\prime\prime}$ .

$\mathit{H}_{1}$ :

As in $\mathcal{F}3$ , the configuration is maintained always a leader configuration by the positioning of $g$ on $C^{g}(R)$ .

$\mathit{H}_{2}$ :

We show that $m_{13}$ is safe. As $\mathtt{q}$ only depends on $F$ , it is always false. During the movement of $g^{\prime\prime}$ , $\mathtt{i}_{1}$ remains true hence, by Lemma 6, the observed configuration always belongs to $\mathcal{P}1$ and it cannot belong to any other sub-phase of $\mathcal{F}4$ . The configuration cannot belong to $\mathcal{F}5$ because either $\mathtt{e}$ is false or we have to show that $\mathtt{b}_{0}\vee\mathtt{z}_{1}\vee\mathtt{z}_{2}$ is false. Assuming $\mathtt{e}$ true, the configuration is asymmetric because of the guards, that is $\mathtt{g}_{2}$ holds. $\mathtt{z}_{1}$ is false because $\mathtt{s}_{3}$ should hold and there should exist an axis of reflection $\ell$ as defined in $\mathtt{z}_{1}$ . The axis $\ell$ cannot exist because of the chosen angle $\alpha$ formed by the guard $g$ . Predicate $\mathtt{z}_{2}$ is false because guard $g$ is on $C^{g}(R)$ . It follows that the configuration cannot belong to any other phase because $\mathtt{f}_{4}$ holds and that $g^{\prime\prime}$ is the only moving robot.

$\mathit{H}_{3}$ :

No collisions are created as there are no robots between $g^{\prime\prime}$ and $\mu(g^{\prime\prime})$ on $C(R)$ .

$\mathit{H}_{4}$ :

Once $g^{\prime\prime}$ reaches the target, predicate $\mathtt{i}_{1}$ does not hold anymore as $g^{\prime\prime}=\mu(g^{\prime\prime})$ but predicate $\mathtt{i}_{2}$ holds, that is by Lemma 6 the configuration is in $\mathcal{P}2$ . The configuration cannot satisfy $\mathtt{w}$ as $g$ is on $C^{g}(R)$ . It is not in any other phase because the same arguments as in $\mathit{H}_{2}$ .

From $\mathcal{P}1$ only guard $g$ remains to be positioned in order to form $F$ . Now the embedding of $F$ on $R$ is more difficult to detect and $g$ moves according to move $m_{14}$ in phase $\mathcal{P}2$ .

$\mathit{H}_{0}$ :

Only $g$ is involved in the move. Even though $g$ moves, $\mathtt{i}_{2}$ ensures to always recognize the same robot as $g$ since the distance to the target always decreases.

$\mathit{H}_{1}$ :

The configuration is maintained always a leader configuration during the movement because $g$ is the only robot on $\mathcal{C}_{\uparrow}^{1}(R)$ . So it cannot participate to a rotation. Moreover, the configuration cannot admit a reflection as the axis of symmetry should pass through $g$ . This means that there exists another embedding of $F$ such that the target of $g$ would be closer than that it has currently calculated, but this contradicts predicate $\mathtt{i}_{2}$ that chooses the target that minimizes the distance.

$\mathit{H}_{2}$ :

We show that $m_{14}$ is safe. As $\mathtt{q}$ only depends on $F$ , it is always false. During the movement $\mathtt{i}_{2}$ remains true, hence, by Lemma 6, the configuration always belongs to $\mathcal{P}2$ and it cannot belong to any other sub-phase of $\mathcal{F}4$ . The configuration cannot belong to $\mathcal{F}5$ because either $\mathtt{e}$ is false and we are done, or we have to show that $\mathtt{b}_{0}\vee\mathtt{z}_{1}\vee\mathtt{z}_{2}$ is false. Assuming $\mathtt{e}$ true, the configuration is asymmetric because of the movement of $g$ . $\mathtt{z}_{1}$ is false because $\mathtt{s}_{3}$ should hold and there should exist an axis of reflection $\ell$ as defined in $\mathtt{z}_{1}$ . Such an axis cannot exist as $g$ should be on it being the only robot on $\mathcal{C}_{\uparrow}^{1}$ . Predicate $\mathtt{z}_{2}$ is false because of $\mathtt{i}_{2}$ . Moreover, it cannot belong to any other phase because $\mathtt{f}_{4}$ holds. It follows that $g$ is the only moving robot.

$\mathit{H}_{3}$ :

No collisions are created as there are no robots between $g$ and its target since $g$ always moves inside $C_{\uparrow}^{1}(F)$ toward its border or toward $c(F)$ . In any case no further robot is met as all of them are already positioned according to $F$ .

$\mathit{H}_{4}$ :

Once $g$ reaches the target, predicate $\mathtt{w}$ holds, that is $F$ has been formed and the configuration does not belong to any phase.

Sub-phases $\mathcal{Q}1$ – $\mathcal{Q}4$ manage the case where $\mathtt{q}$ is true. The main difficult here is to maintain $C(R)$ unchanged while guards are moving. In fact, if $g^{\prime\prime}$ rotates toward $\mu(g^{\prime\prime})$ as in sub-phase $\mathcal{P}1$ , $C(R)$ could change.

As first move, in $\mathcal{Q}1$ guard $g$ is moved radially on $C(R)$ by means of move $m_{15}$ .

$\mathit{H}_{0}$ :

Only $g$ is involved in the move. As it moves radially toward $C(R)$ , angle $\alpha$ is maintained along all the movement, hence $g$ is easily recognizable.

$\mathit{H}_{1}$ :

The configuration is maintained always asymmetric as $F$ does not require multiplicities and $g$ is the only robot inside $C(R)$ . So it cannot participate to neither a rotation, nor a reflection as the axis of symmetry should pass through $g$ , but then the starting configuration $R$ was symmetric, a contradiction.

$\mathit{H}_{2}$ :

We show that $m_{15}$ is safe. As $\mathtt{q}$ only depends on $F$ , it is always true. During the movement of $g$ , $\mathtt{i}_{3}$ remains true and hence the observed configuration always belongs to $\mathcal{Q}1$ . By Lemma 6, it cannot belong to any other sub-phase of $\mathcal{F}4$ . The configuration cannot belong to $\mathcal{F}5$ because $\mathtt{e}$ is true, and the configuration is asymmetric because of the movement of $g$ . $\mathtt{z}_{1}$ is false because $\mathtt{s}_{3}$ should hold and there should exist an axis of reflection $\ell$ as defined in $\mathtt{z}_{1}$ . Such an axis cannot exist as $g$ should be on it being the only robot on $\mathcal{C}_{\uparrow}^{1}$ . Predicate $\mathtt{z}_{2}$ is false because of the radial movement of $g$ from $\mathcal{C}^{g}(R)$ . Moreover, the configuration cannot belong to any other phase because $\mathtt{f}_{4}$ holds.

It follows that $g$ is the only moving robot.

$\mathit{H}_{3}$ :

No collisions are created as $g$ is the only robot inside $C(R)$ and there are no robots forming an angle of $\alpha$ degrees on $C(R)$ as they are all well positioned according to $F$ but for $g^{\prime\prime}$ that by construction is not on the way of $g$ .

$\mathit{H}_{4}$ :

Once $g$ reaches the target, predicate $\mathtt{i}_{3}$ becomes false while either $\mathtt{i}_{4}$ or $\mathtt{i}_{5}$ become true, depending whether $g^{\prime\prime}$ is already on target or not. By Lemma 6, this means the configuration may belong to $\mathcal{Q}2$ or $\mathcal{Q}3$ and it cannot belong to any other sub-phase of $\mathcal{F}4$ . The configuration cannot belong to $\mathcal{F}5$ because $\mathtt{e}$ is true, and the configuration is asymmetric because of $g$ . $\mathtt{z}_{1}$ is false because $\mathtt{s}_{3}$ is false. Predicate $\mathtt{z}_{2}$ is false because all robots are far from $\mathcal{C}^{g}(R)$ . Moreover, the configuration cannot belong to any other phase because $\mathtt{f}_{4}$ holds.

Sub-phase $\mathcal{Q}2$ is applied if $g^{\prime\prime}$ is not yet on its target. Since now all robots are in $\partial C(R)$ , $g^{\prime\prime}$ cannot freely move toward $\mu(g^{\prime\prime})$ as this could change $C(R)$ . A safe place to reach is the antipodal point $p$ to $g$ . Move $m_{16}$ rotates $g^{\prime\prime}$ on $C(R)$ toward the closest point among $p$ and $\mu(g^{\prime\prime})$ .

$\mathit{H}_{0}$ :

Only $g^{\prime\prime}$ is involved in the move. The angle $\alpha$ between $g$ and $g^{\prime}$ maintains $g^{\prime\prime}$ easily recognizable along all the movement.

$\mathit{H}_{1}$ :

The configuration is maintained always asymmetric as the angle $\alpha$ between $g$ and $g^{\prime}$ guarantees no rotations. Moreover, the only axis of reflection should cut $\alpha$ . Since $\mathtt{q}$ holds, $|F|-1$ points occupy a semi-circle. As all robots but $g$ and $g^{\prime\prime}$ are not yet positioned according to $F$ , it follows that $g$ is the only robot in the semi-circle between $g^{\prime}$ and $g^{\prime\prime}$ in the clockwise direction. Since by assumption there are at least four robots, this situation cannot hold as there cannot be a robot specular to one which is not a guard.

$\mathit{H}_{2}$ :

We show that $m_{16}$ is safe. As $\mathtt{q}$ only depends on $F$ , it is always true. During the movement of $g^{\prime\prime}$ , $\mathtt{i}_{4}$ remains true. As a consequence, by Lemma 6, the observed configuration belongs to $\mathcal{Q}2$ and it cannot belong to any other sub-phase of $\mathcal{F}4$ . The configuration cannot belong to $\mathcal{F}5$ because $\mathtt{e}$ is true, and the configuration is asymmetric because of $g$ . $\mathtt{z}_{1}$ is false because $\mathtt{s}_{3}$ is false. Predicate $\mathtt{z}_{2}$ is false because all robots are far from $\mathcal{C}^{g}(R)$ . Moreover, the configuration cannot belong to any other phase because $\mathtt{f}_{4}$ holds. It follows that $g^{\prime\prime}$ is the only moving robot.

$\mathit{H}_{3}$ :

No collisions are created as by construction the path between $g^{\prime\prime}$ and its target along $C(R)$ does not contain further robots.

$\mathit{H}_{4}$ :

Once $g^{\prime\prime}$ reaches the target, predicate $\mathtt{i}_{4}$ becomes false while predicate $\mathtt{i}_{5}$ becomes true. By Lemma 6, this means the configuration may belong to $\mathcal{Q}3$ and it cannot belong to any other sub-phase of $\mathcal{F}4$ . Moreover, it cannot belong to any other phase because of the same arguments as in $\mathit{H}_{2}$ .

In sub-phase $\mathcal{Q}3$ , guard $g$ can freely move toward its final target by means of move $m_{17}$ . In fact, because of predicate $\mathtt{q}$ , the move does not affect $C(R)$ .

$\mathit{H}_{0}$ :

Only $g$ is involved in the move. Robot $g$ is always recognizable as the only robot of minimum view.

$\mathit{H}_{1}$ :

The configuration is maintained always asymmetric as $g$ is the only one with minimum view and its clockwise view is different from its anti-clockwise view.

$\mathit{H}_{2}$ :

We show that $m_{17}$ in phase $\mathcal{Q}3$ is safe. As $\mathtt{q}$ only depends on $F$ , it is always true. During the movement of $g$ , $\mathtt{i}_{5}$ remains true. Hence, by Lemma 6, the observed configuration belongs to $\mathcal{Q}3$ and it cannot belong to any other sub-phase of $\mathcal{F}4$ . Moreover, it cannot belong to any other phase because of the same arguments as for move $m_{13}$ . It follows that $g$ is the only moving robot.

$\mathit{H}_{3}$ :

No collisions are created as by construction the path between $g$ and its target along $C(R)$ does not contain further robots.

$\mathit{H}_{4}$ :

Once $g$ reaches the target, predicate $\mathtt{i}_{5}$ becomes false while either $\mathtt{w}$ or $\mathtt{i}_{6}$ become true, depending whether $g^{\prime\prime}$ is already on target or not. This means either $F$ is formed or the obtained configuration $R^{\prime}$ belongs to $\mathcal{Q}4$ according to Lemma 6. We now show that the configuration cannot belong to $\mathcal{F}5$ since $\mathtt{b}_{0}\vee\mathtt{z}_{1}\vee\mathtt{z}_{2}$ is false, that is $\mathtt{f}_{5}$ is false. $R^{\prime}$ is asymmetric (i.e. $\mathtt{b}_{0}$ is false) because $\mathtt{q}$ holds and hence $R^{\prime}$ cannot be rotational and does not admit multiplicities. The only possible axis of reflection in $R^{\prime}$ should reflect $g$ with $g^{\prime\prime}$ . In turn, this implies that there must be another robot $r$ specular to $g^{\prime}$ such that $\sphericalangle(r,c(R^{\prime}),g^{\prime\prime})=3\alpha$ with $\mu(g^{\prime\prime})$ being on the smaller arc of $C(R^{\prime})$ between $g^{\prime\prime}$ and $r$ . It follows that $\sphericalangle(r,c(R^{\prime}),\mu(g^{\prime\prime}))<3\alpha$ , contradicting the definition of $\alpha$ . Predicate $\mathtt{z}_{1}$ is false because $\mathtt{s}_{3}$ is false. Predicate $\mathtt{z}_{2}$ is false because all robots are far from $\mathcal{C}^{g}(R^{\prime})$ . The configuration cannot belong to any other phase as either $\mathtt{f}_{4}$ or $\mathtt{w}$ holds.

In sub-phase $\mathcal{Q}4$ , guard $g^{\prime\prime}$ can freely move toward its final target by means of move $m_{13}$ . In fact, predicate $\mathtt{q}$ guarantees that the target of $g^{\prime\prime}$ does not overcome the antipodal point to $g$ , hence the movement does not affect $C(R)$ .

$\mathit{H}_{0}$ :

Only $g^{\prime\prime}$ is involved in the move. Robot $g^{\prime\prime}$ is always recognizable as $\mathtt{i}_{6}$ holds and $g^{\prime\prime}$ is the only robot not on target.

$\mathit{H}_{1}$ :

During the movement, the configuration cannot admit a rotation as the arc from $g^{\prime}$ to $g^{\prime\prime}$ in the clockwise direction is greater than half of $C(R)$ . There cannot be an axis of symmetry that makes $g$ specular to $g^{\prime}$ . In fact, $g^{\prime\prime}$ cannot admit a specular robot with respect to such an axis as it is closer to the axis than $g$ which contradicts the property of $g$ being the robot of minimum view. There cannot be an axis making specular $g$ to $g^{\prime\prime}$ . In fact, $g$ cannot admit a specular robot $r$ with respect to such an axis as $\sphericalangle(r,c(R),g^{\prime\prime})$ should be equal to $\sphericalangle(g,c(R),g^{\prime})=3\alpha$ , but this is possible only once $g^{\prime\prime}$ has reached its target being $g$ the robot of minimum view.

$\mathit{H}_{2}$ :

We show that $m_{13}$ in phase $\mathcal{Q}4$ is safe. As $\mathtt{q}$ only depends on $F$ , it is always true. During the movement of $g^{\prime\prime}$ , $\mathtt{i}_{6}$ remains true. Hence, by Lemma 6, the configuration belongs to $\mathcal{Q}3$ and it cannot belong to any other sub-phase of $\mathcal{F}4$ . Moreover, it cannot belong to any other phase because of the same arguments as for move $m_{17}$ holds. It follows that $g^{\prime\prime}$ is the only moving robot.

$\mathit{H}_{3}$ :

No collisions are created as by construction the path between $g^{\prime\prime}$ and its target along $C(R)$ does not contain further robots.

$\mathit{H}_{4}$ :

Once $g^{\prime\prime}$ reaches the target, predicate $\mathtt{w}$ becomes true. This means the configuration does not belong to any phase.

∎

Concerning phase $\mathcal{F}5$ , for each move $m$ defined in Table 7 we need to show several properties (similar to those used for $\mathcal{F}1,\mathcal{F}2,\mathcal{F}3$ , and $\mathcal{F}4$ ) that guarantee to our algorithm to safely evolve until a different phase is reached:

$\mathit{H}^{\prime}_{0}$ :

at the beginning, $m$ involves at most two robots;

$\mathit{H}^{\prime}_{1}$ :

while robots are moving according to $m$ , the configuration remains a leader configuration;

$\mathit{H}^{\prime}_{2}$ :

$m$ is safe, and in particular that while robots are moving according to $m$ , all other robots are stationary;

$\mathit{H}^{\prime}_{3}$ :

while robots are moving according to $m$ , no collisions are created;

$\mathit{H}^{\prime}_{4}$ :

if $m$ is associated to any phase $\mathcal{X}$ , then the predicate $\mathcal{X}_{e}$ holds once the robots have terminated to apply $m$ ;

$\mathit{H}^{\prime}_{5}$ :

$m$ preserves stationarity.

Note that, in this case we cannot get rid of property $\mathit{H}_{5}^{\prime}$ as we did with $\mathit{H}_{5}$ for phases $\mathcal{F}1$ , $\mathcal{F}2$ , $\mathcal{F}3$ , $\mathcal{F}4$ as now there might be two robots moving concurrently.

Moreover, during phase $\mathcal{F}5$ it is possible that by chance a robot makes true predicate $\mathtt{w}$ while moving. For the sake of clarity, and in order to not overcharge Procedure StationaryMove, we prefer to ignore such occurrences. This simply implies that the pattern will be formed successively by following the designed transitions, and from there on robots will not move anymore. Differently, if a stationary configuration is reached where $\mathtt{w}$ holds, then no move will be performed anymore. As described in Table 7, all sub-phases of $\mathcal{F}5$ with the exception of $\mathcal{W}$ may lead to stationary configurations where $\mathtt{w}$ holds. In the subsequent analysis we omit to mention all the times such possibilities.

Lemma 12

Let $R$ be a stationary configuration in $\mathcal{F}5$ . From $R$ the algorithm eventually leads to a stationary configuration belonging to $\mathcal{F}1$ , $\mathcal{F}2$ , $\mathcal{F}4$ or where $\mathtt{w}$ holds.

Proof

By Lemma 7, exactly one of the predicates for the starting phases in Table 7 is true. Then, exactly one of the moves associated to the sub-phases of $\mathcal{F}5$ is applied to $R$ . We show that the properties $\mathit{H}^{\prime}_{0},\ldots,\mathit{H}^{\prime}_{5}$ hold for each possible move applied to $R$ .

Let us consider sub-phase $\mathcal{T}$ where move $m_{18}$ is performed.

$\mathit{H}^{\prime}_{0}$ :

As $\mathtt{b}_{1}$ holds, there is only one robot $r$ on the axis $\ell$ moved by $m_{18}$ .

$\mathit{H}^{\prime}_{1}$ :

If $r$ admits a rotational-free path, then move $m_{18}$ makes $r$ move toward $c(R\setminus\{r\})$ . Since $r$ moves along the axis $\ell$ , then the obtained configuration remains a leader configuration. Moreover, $r$ is always recognizable as the moving robot.

If $r$ does not admit a rotational-free path, let $p^{\prime}$ be the point on $\ell$ toward $c(R\setminus\{r\})$ such that, if reached by $r$ , the new configuration $R^{\prime}$ becomes rotational. In this case $r$ is moved to become a faraway robot, that is ‘sufficiently’ far from $c(R)$ . We now show that during the movement no configuration admitting a rotation can be created. By contradiction, let us assume that that there exists a point $p^{\prime\prime}$ such that, if reached by $r$ the new configuration $R^{\prime\prime}$ admits a rotation. If in $p^{\prime\prime}$ the robot $r$ is not critical, then $R^{\prime\prime}$ has the same center of $R$ and cannot admit a rotation as in $p^{\prime}$ there is not a robot. So, in $p^{\prime\prime}$ robot $r$ must be critical. In this case, the center is not maintained and, if $R^{\prime\prime}$ is rotational, the robots on $C(R^{\prime\prime})$ must form a regular triangle (as in any other $n$ -gon the robots are not critical). Let $r_{1}$ and $r_{2}$ be the other two robots on $C(R^{\prime\prime})$ . As they are at the same distance from $\ell$ , they are also on a same circle $C^{i}_{\uparrow}(R^{\prime})$ . If $r_{1}$ and $r_{2}$ are antipodal on $C^{i}_{\uparrow}(R^{\prime})$ then to make $R^{\prime}$ rotational, $r$ should be in $c(R^{\prime})$ , but it is not possible by hypothesis. If $r_{1}$ and $r_{2}$ are not antipodal on $C^{i}_{\uparrow}(R^{\prime})$ , then there are $k$ equidistant robots on $C^{i}_{\uparrow}(R^{\prime})$ , with $k$ odd, as the robots on $C^{i}_{\uparrow}(R^{\prime})$ consist of $r$ and pairs of symmetric robots with respect to $\ell$ . Moreover, $k>3$ as the case $k=3$ is realized when $r$ is in $p^{\prime\prime}$ . This implies that there should be robots on $C^{i}_{\uparrow}(R^{\prime})$ in the arc between $r_{1}$ and $r_{2}$ external to $C(R^{\prime\prime})$ , a contradiction to the definition of $C(R^{\prime\prime})$ . Hence, also in this case the obtained configuration remains a leader configuration.

$\mathit{H}^{\prime}_{2}$ :

Move $m_{18}$ is safe as $\mathtt{b}_{0}$ and $\mathtt{e}$ are both true during the movement and then the configuration cannot be in $\mathcal{F}1$ , $\mathcal{F}2$ , $\mathcal{F}3$ , $\mathcal{F}4$ . Moreover, as $\mathtt{b}_{1}\wedge\neg\mathtt{z}_{1}$ remains true, the configuration cannot be in the other sub-phases of $\mathcal{F}5$ and $r$ remains the only moving robot.

$\mathit{H}^{\prime}_{3}$ :

No collisions are created as $r$ moves on $\ell$ and it is the only robot on $\ell$ .

$\mathit{H}^{\prime}_{4}$ :

As $\mathtt{b}_{0}\wedge\mathtt{e}$ is still true the configuration remains in $\mathcal{F}5$ . If $r$ reaches $c(R)$ , the configuration is in $\mathcal{W}$ as $\mathtt{z}_{2}$ is clearly true, and both $\mathcal{V}1_{s}$ and $\mathcal{V}2_{s}$ are false as $\mathtt{b}_{2}$ and $\mathtt{b}_{3}$ are false. If $r$ becomes faraway, then $\mathtt{z}_{1}$ becomes true and the configuration is in $\mathcal{U}$ .

$\mathit{H}^{\prime}_{5}$ :

As $m_{18}$ is safe and a single robot is moving, then when $r$ stops the configuration is stationary.

Let us consider sub-phase $\mathcal{U}$ where move $m_{19}$ is performed.

$\mathit{H}^{\prime}_{0}$ :

There is only one faraway robot $r$ moved by $m_{19}$ .

$\mathit{H}^{\prime}_{1}$ :

While $r$ is moving according to $m_{19}$ , the configuration remains asymmetric as the three robots on $C(R)$ do not form a regular triangle.

$\mathit{H}^{\prime}_{2}$ :

While $r$ is moving, predicate $\mathtt{f}_{5}$ remains true as both $\mathtt{z}_{1}$ and $\mathtt{e}$ maintain their values. Then the configuration remains in $\mathcal{F}5$ . As $\mathtt{b}_{0}$ is false and $\mathtt{z}_{1}\Rightarrow\neg\mathtt{z}_{2}$ (cf the proof of Lemma 7), the configuration cannot belong to any other sub-phase of $\mathcal{F}5$ . Finally, robot $r$ remains always recognizable during the movement.

$\mathit{H}^{\prime}_{3}$ :

There are only three robots on $C(R)$ and $r$ is moving on $C(R)$ within an arc without other robots.

$\mathit{H}^{\prime}_{4}$ :

When $r$ reaches its final position on $t$ , predicate $\mathtt{z}_{1}$ is false and so are $\mathtt{b}_{0}$ and $\mathtt{z}_{2}$ . Then the configuration is no more in $\mathcal{F}5$ as $\mathtt{f}_{5}$ is false. The configuration can verify $\mathcal{F}1_{s}$ . In fact $\mathcal{F}2_{s}$ is false as $\mathtt{s}_{2}$ is false, and $\mathcal{F}3_{s}$ is not verified as $\mathtt{g}_{2}$ is false being $\mathtt{g}_{0}$ false. Predicate $\mathtt{g}_{0}$ is false because on $C^{1}_{\uparrow}(R)$ there are at least two robots since $R\setminus\{r\}$ is symmetric. Moreover the configuration is not in $\mathcal{F}4$ as $\mathtt{q}$ is false and neither $\mathtt{i}_{1}$ or $\mathtt{i}_{2}$ are verified, as $\mathtt{g}_{1}$ is false and $\partial C^{1}_{\uparrow}(R)$ contains at least two robots.

$\mathit{H}^{\prime}_{5}$ :

As $m_{19}$ is safe and a single robot is moving, then when the robot $r$ stops the configuration is stationary.

Let us consider sub-phase $\mathcal{V}1$ where move $m_{20}$ is performed.

$\mathit{H}^{\prime}_{0}$ :

Move $m_{20}$ moves $r^{(1)}$ ; in some cases, it moves both $r^{(1)}$ and $r^{(2)}$ concurrently. Hence, at the beginning, the move involves at most two robots.

$\mathit{H}^{\prime}_{1}$ :

It is worth to note that $r^{(1)}$ cannot move only if it does not admit a rotational-free path. Such a situation can happen only if the robots on the circle $C^{i}_{\uparrow}(R)$ where $r^{(2)}$ lies form a configuration admitting a rotation. For this reason $r^{(2)}$ is moved so as to ensure that it is the only robot on the circle where it lies. This implies that no rotational symmetries are created and hence the configurations remains a leader configuration. Moreover, robots $r^{(1)}$ and $r^{(2)}$ are always recognizable as such since they move without changing their order on $\ell$ .

$\mathit{H}^{\prime}_{2}$ :

Move $m_{20}$ is safe as $\mathtt{b}_{0}$ and $\mathtt{e}$ are both true during the movement, that is, $\mathtt{f}_{5}$ holds and the configuration cannot belong to $\mathcal{F}1$ , $\mathcal{F}2$ , $\mathcal{F}3$ , $\mathcal{F}4$ . Moreover, as $\mathtt{b}_{2}$ remains true and at least one among $r^{(1)}$ and $r^{(2)}$ is not on its target, then, by Lemma 7, the configuration cannot be in the other sub-phases of $\mathcal{F}5$ as $\neg\mathtt{c}\vee\neg\mathtt{u}_{1}$ holds. Moreover, as already observed in the previous item, robots $r^{(1)}$ and $r^{(2)}$ are always recognizable.

$\mathit{H}^{\prime}_{3}$ :

No collisions are created as $r^{(1)}$ is the robot closest to $c(R)$ , its target, and $r^{(2)}$ , after starting to move, always remains the only robot between $C_{\uparrow}^{i-1}(R)$ and $C_{\uparrow}^{i+1}(R)$ .

$\mathit{H}^{\prime}_{4}$ :

Once both $r^{(1)}$ and $r^{(2)}$ reach their target, still $\mathtt{b}_{0}\wedge\mathtt{e}$ is true hence the configuration remains in $\mathcal{F}5$ , $\mathtt{z}_{2}$ becomes true but $\neg\mathtt{c}\vee\neg\mathtt{u}_{1}$ is false, that is $\mathcal{V}1_{s}$ is false. Also $\mathcal{V}2_{s}$ is false as $\mathtt{b}_{2}$ remains true, and hence $\mathcal{W}_{s}$ holds.

$\mathit{H}^{\prime}_{5}$ :

As $m_{20}$ is safe with $r^{(1)}$ and $r^{(2)}$ being the moving robots, when they both stop the configuration is stationary.

Let us consider sub-phase $\mathcal{V}2$ where move $m_{21}$ is performed.

$\mathit{H}^{\prime}_{0}$ :

As $\mathtt{b}_{3}$ holds, robots $r^{(1)}$ and $r^{(2)}$ are the only robots on the axis $\ell$ , exactly the robots moved by means of $m_{21}$ .

$\mathit{H}^{\prime}_{1}$ :

The only case in which $r^{(1)}$ does not admit a rotational-free path occurs when $r^{(2)}$ is on $t^{60}$ (cf Figure 15.(e)). In fact, this is the only case in which $C(R)$ can admit a rotation, with $r^{(2)}$ being critical by definition. Of course, the rotational configuration must be avoided as it is not a leader configuration. The only case in which $r^{(2)}$ does not move from $t^{60}$ is when $t^{x}=t^{60}$ . However, if the current configuration $R$ admits $|\partial C(R)|>4$ , then $r^{(1)}$ can freely move toward $c(R)$ whereas $r^{(2)}$ is already on target. If $|\partial C(R)|=4$ , then $r^{(1)}\in\partial C(R)$ and moves toward its intermediate target $t$ . In so doing, $t^{x}$ changes and $r^{(2)}$ can leave $t^{60}$ . From now on, $r^{(1)}$ admits a rotational-free path. Note that, while robots are moving, both their targets change. In particular, $t^{x}$ can get further from $t^{60}$ or even disappearing. $\delta C(R)$ grows and the target $c(R)$ for $r^{(1)}$ moves further from $r^{(1)}$ according to the movement of $r^{(2)}$ . Eventually, $r^{(2)}$ either reaches $t^{x}$ that does not change anymore or it reaches $t^{55}$ . Hence, also $r^{(1)}$ can eventually reach its final destination. Hence, during the movements the obtained configuration is always a leader configuration.

$\mathit{H}^{\prime}_{2}$ :

Move $m_{21}$ is safe as $\mathtt{b}_{0}$ and $\mathtt{e}$ are both true during the movement, that is, $\mathtt{f}_{5}$ holds and the configuration cannot belong to $\mathcal{F}1$ , $\mathcal{F}2$ , $\mathcal{F}3$ , $\mathcal{F}4$ . Moreover, as $\mathtt{b}_{3}$ remains true and at least one among $r^{(1)}$ and $r^{(2)}$ is not on its target, then, by Lemma 7, the configuration cannot be in the other sub-phases of $\mathcal{F}5$ as $\neg\mathtt{c}\vee\neg\mathtt{u}_{2}$ holds. Moreover, robots $r^{(1)}$ and $r^{(2)}$ are always recognizable.

$\mathit{H}^{\prime}_{3}$ :

No collisions are created as there are no further robots on $\ell$ , whereas $r^{(1)}$ and $r^{(2)}$ cannot meet.

$\mathit{H}^{\prime}_{4}$ :

Once both $r^{(1)}$ and $r^{(2)}$ reach their targets, still $\mathtt{b}_{0}\wedge\mathtt{e}$ is true hence the configuration remains in $\mathcal{F}5$ , $\mathtt{z}_{2}$ becomes true but $\neg\mathtt{c}\vee\neg\mathtt{u}_{2}$ is false, that is $\mathcal{V}2_{s}$ is false. Also $\mathcal{V}1_{s}$ is false as $\mathtt{b}_{3}$ remains true, and hence $\mathcal{W}_{s}$ holds.

$\mathit{H}^{\prime}_{5}$ :

As $m_{21}$ is safe with $r^{(1)}$ and $r^{(2)}$ being the moving robots, when they both stop the configuration is stationary.

Let us consider sub-phase $\mathcal{V}3$ where move $m_{22}$ is performed.

$\mathit{H}^{\prime}_{0}$ :

As $\mathtt{b}_{4}$ holds, only $r^{(1)}$ moves on the axis $\ell$ by means of $m_{22}$ .

$\mathit{H}^{\prime}_{1}$ :

While $r$ moves toward $c(R)$ , it remains not critical and it is always detected as the robot to move (cf Figure 15.(f)). Moreover the configuration remains a leader configuration as it cannot become rotational: in fact, the critical robots are the only robots on $C(R)$ , then the only possible rotation $\varphi$ is a $180^{\circ}$ rotation, but in this case $\varphi(r^{(1)})$ would not exists.

$\mathit{H}^{\prime}_{2}$ :

Move $m_{22}$ is safe as $\mathtt{b}_{0}$ and $\mathtt{e}$ are both true during the movement, that is, $\mathtt{f}_{5}$ holds and the configuration cannot belong to $\mathcal{F}1$ , $\mathcal{F}2$ , $\mathcal{F}3$ , $\mathcal{F}4$ . Moreover, as $\neg\mathtt{c}\wedge\mathtt{b}_{4}$ remains true, the configuration cannot be in the other sub-phases of $\mathcal{F}5$ and $r^{(1)}$ remains the only moving robot.

$\mathit{H}^{\prime}_{3}$ :

No collisions are created as $r^{(1)}$ admits a rotational-free path.

$\mathit{H}^{\prime}_{4}$ :

Once $r$ reaches its target, still $\mathtt{b}_{0}\wedge\mathtt{e}$ is true hence the configuration remains in $\mathcal{F}5$ . Once $r$ is in $c(R)$ , $\mathtt{z}_{2}$ holds. Since $\mathtt{b}_{4}$ remains true, neither $\mathcal{V}1_{s}$ nor $\mathcal{V}2_{s}$ can become true, then $\mathcal{W}_{s}$ holds.

$\mathit{H}^{\prime}_{5}$ :

As $m_{22}$ is safe and a single robot is moving, then when $r^{(1)}$ stops the configuration is stationary.

Let us consider sub-phase $\mathcal{V}4$ where move $m_{23}$ is performed.

$\mathit{H}^{\prime}_{0}$ :

As $\mathtt{b}_{5}$ holds, there is only one robot $r$ on the axis $\ell$ moved by $m_{23}$ .

$\mathit{H}^{\prime}_{1}$ :

While $r$ moves, it is always detected as the robot on $\ell$ closest to $C(R\setminus\{r^{(1)},r^{(2)}\})$ (cf Figure 15.(g)). Then, no rotational symmetry can be created and hence the configuration remains a leader configuration.

$\mathit{H}^{\prime}_{2}$ :

Move $m_{23}$ is safe as $\mathtt{b}_{0}$ and $\mathtt{e}$ are both true during the movement, that is, $\mathtt{f}_{5}$ holds and the configuration cannot belong to $\mathcal{F}1$ , $\mathcal{F}2$ , $\mathcal{F}3$ , $\mathcal{F}4$ . Moreover, as $\mathtt{b}_{5}\wedge\neg\mathtt{c}$ remains true, the configuration cannot be in the other sub-phases of $\mathcal{F}5$ and $r$ remains the only moving robot.

$\mathit{H}^{\prime}_{3}$ :

No collisions are created as $r$ moves on $\ell$ and the only other robot on $\ell$ is antipodal.

$\mathit{H}^{\prime}_{4}$ :

Once $r$ reaches its target, still $\mathtt{b}_{0}\wedge\mathtt{e}$ is true hence the configuration remains in $\mathcal{F}5$ . Now $r$ is not critical, hence $\mathtt{b}_{3}$ holds and sub-phase $\mathcal{V}2$ is reached.

$\mathit{H}^{\prime}_{5}$ :

As $m_{23}$ is safe and a single robot is moving, then when the robot $r$ stops the configuration is stationary.

Let us consider sub-phase $\mathcal{W}$ where move $m_{24}$ is performed.

$\mathit{H}^{\prime}_{0}$ :

There is only one robot $r$ moved by $m_{24}$ , the one identified as the closest to $c(R)$ .

$\mathit{H}^{\prime}_{1}$ :

While $r$ is moving according to $m_{24}$ , the configuration remains asymmetric as $R^{\prime}=R\setminus\{r\}$ is symmetric, being $\mathtt{z}_{2}$ true, and $r$ is not moving along an axis of symmetry.

$\mathit{H}^{\prime}_{2}$ :

While $r$ is moving, either $\mathtt{i}_{2}$ becomes true or $\mathtt{z}_{2}\wedge e$ holds and hence $\mathtt{f}_{5}$ remains true. In the first case, the configuration may belong to $\mathcal{F}4$ , and in particular to sub-phase $\mathcal{P}2$ . However, from $\mathcal{P}2$ , by move $m_{14}$ , only the same robot $r$ is allowed to move. In the second case, the configuration remains in $\mathcal{F}5$ . As $\mathtt{b}_{0}$ is false and $\mathtt{z}_{2}\Rightarrow\neg\mathtt{z}_{1}$ , the configuration cannot belong to any other sub-phase of $\mathcal{F}5$ .

$\mathit{H}^{\prime}_{3}$ :

By definition of $C^{g}(R)$ there are no robots between $r$ and its target.

$\mathit{H}^{\prime}_{4}$ :

When $r$ reaches its final position on $C^{g}(R)$ , predicate $\mathtt{z}_{2}$ is false and so are $\mathtt{b}_{0}$ and $\mathtt{z}_{1}$ . Then the configuration is no more in $\mathcal{F}5$ as $\mathtt{f}_{5}$ is false. The obtained configuration can verify $\mathcal{F}1_{s}$ , $\mathcal{F}2_{s}$ or $\mathcal{F}4_{s}$ . It cannot verify $\mathcal{F}3_{s}$ as $\mathtt{g}_{2}$ is false being $\mathtt{g}_{1}$ false. Predicate $\mathtt{g}_{1}$ is false since $r$ does not form the reference angle of $\alpha$ degree. Predicate $\mathtt{w}$ cannot hold as $r$ is on $C^{g}(R)$ .

$\mathit{H}^{\prime}_{5}$ :

As $m_{24}$ is safe and a single robot is moving, then when the robot $r$ stops the configuration is stationary.

∎

Theorem 7.1

Let $R$ be an initial leader configuration of Async robots without chirality, and $F$ any pattern (possibly with multiplicities) with $|F|=|R|$ . Then, there exists an algorithm able to form $F$ from $R$ .

Proof

As remarked in Section 6, the cases of $|R|\leq 2$ are either trivial or unsolvable, and hence are not required to be managed by our algorithm. The case of $F$ being a single point is delegated to CFPS12 , whereas when $|R|=3$ Theorem 6.1 holds. When $|R|>3$ , the claim simply follows by Lemmata 2, 8, 9, 10, 11, and 12. In fact, Lemma 2 shows that $R$ belongs to exactly one phase among $\mathcal{F}1$ , $\mathcal{F}2$ , $\mathcal{F}3$ , $\mathcal{F}4$ , and $\mathcal{F}5$ . Lemmata 8–11 show that from a given phase among $\mathcal{F}1,\cdots,\mathcal{F}4$ only subsequent phases can be reached, or $\mathtt{w}$ eventually holds (cf Table 2, first and last column). Lemma 12 instead shows that from $\mathcal{F}5$ any other phase but $\mathcal{F}3$ can be reached, or $\mathtt{w}$ eventually holds. Cycles among phases can occur only between $\mathcal{F}1$ and $\mathcal{F}5$ . However, the involved moves $m_{4}$ and $m_{19}$ guarantee that the transitions of such a cycle can be traversed only once.

Inside each phase among $\mathcal{F}1$ , $\cdots$ , $\mathcal{F}5$ , the only possible cycles among transitions can occur in phase $\mathcal{F}1$ among sub-phases $\mathcal{A}1$ and $\mathcal{A}2$ , or in $\mathcal{F}3$ among sub-phases $\mathcal{M}$ , $\mathcal{N}$ and $\mathcal{O}$ . However, the corresponding Lemmata 8 and 10 also show that such cycles can be performed only a finite number of times. ∎

From FPSW08 , it is possible to state the next theorem. For the sake of completeness we also remind the corresponding easy proof.

Theorem 7.2

FPSW08 * Let $R$ be an initial configuration of $n$ Async robots without chirality. If $APF$ is solvable, then also Leader Election can be solved.*

Proof

Consider the pattern $F$ with $n-1$ collinear points evenly placed such that the distance between two adjacent points is some $d$ , and one further point on the same line at distance $2d$ from its unique neighbor. If robots can form $F$ , then the unique robot with one neighbor at distance $2d$ can be elected as the leader. ∎

From Theorem 7.1 and Theorem 7.2 we obtain Theorem 1.1 that we now rephrase in a more explicit form:

Theorem 7.3

Let $R$ be an initial configuration of Async robots without chirality. There exists a deterministic transition-safe algorithm that solves $APF$ from $R$ if and only the Leader Election problem can be solved in $R$ , that is, $R$ is a leader configuration.

8 Conclusion

We considered the Arbitrary Pattern Formation problem in the well-known asynchronous Look-Compute-Move model. So far the problem has been mainly investigated with the further assumption on the capability of robots to share a common left-right orientation (chirality).

Our study removes any assumption concerning the orientation of the robots. We shown that starting from initial leader configurations, robots can deterministically form any pattern including symmetric ones and those containing multiplicities. This extends the previously known results in terms of required number of robots, orientation capabilities, multiplicities, and formalisms. In fact, our algorithm does not rely on any assumption on the number of robots, nor on any orientation of the robots, it allows the formation of multiplicities if required by the given pattern, and it is provided in terms of logical predicates that facilitate to check its correctness.

Also, the relevance of our results is shown in light of the consequences obtained with respect to FYOKY15 , BT15 ; BT16b , and DPVarx09 . Recently, errata to FYOKY15 and BT15 ; BT16b have been delivered but the level of formalism and details with respect to our approach is still something remarkable.

The main open question left asks to provide a deterministic algorithm that solves the Pattern Formation rather than the Arbitrary Pattern Formation from any initial configuration, including symmetric ones. Potentially, robots should be able to form any pattern if starting from configurations characterized by symmetries that are included in the final pattern. The main difficulty in designing an algorithm for such cases is that in symmetric configurations many robots may move simultaneously, all those that look equivalent with respect to the symmetry. The adversary can decide to move any subset of such robots, and all of them may traverse different distances as the adversary can stop them in different moments. Hence, during a Look phase, it becomes very difficult to provide a mean to guess how the current configuration has been originated.

Bibliography32

The reference list from the paper itself. Each links out to its DOI / PubMed record.

1(1) Bérard, B., Lafourcade, P., Millet, L., Potop-Butucaru, M., Thierry-Mieg, Y., Tixeuil, S.: Formal verification of mobile robot protocols. Distributed Computing 29 (6), 459–487 (2016)
2(2) Bhagat, S., Chaudhuri, S.G., Mukhopadhyaya, K.: Formation of general position by asynchronous mobile robots under one-axis agreement. In: Proc. 10th Int.’l WS on Algorithms and Computation (WALCOM), LNCS , vol. 9627, pp. 80–91. Springer (2016)
3(3) Bonnet, F., Potop-Butucaru, M., Tixeuil, S.: Asynchronous gathering in rings with 4 robots. In: Proc. 5th Int.’l Conf. on Ad-hoc, Mobile, and Wireless Networks (ADHOC-NOW), LNCS , vol. 9724, pp. 311–324. Springer (2016)
4(4) Bramas, Q., Tixeuil, S.: Brief Announcement: Probabilistic asynchronous arbitrary pattern formation. In: Proc. 35th ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computing (PODC) (2016)
5(5) Bramas, Q., Tixeuil, S.: Brief Announcement: Probabilistic asynchronous arbitrary pattern formation. In: Proc. 18th Int.’l Symp. on Stabilization, Safety, and Security of Distributed Systems (SSS), Lecture Notes in Computer Science , vol. 10083, pp. 88–93 (2016)
6(6) Bramas, Q., Tixeuil, S.: Probabilistic asynchronous arbitrary pattern formation. Co RR abs/1508.03714 (2016). URL https://arxiv.org/abs/1508.03714
7(7) Chaudhuri, S.G., Ghike, S., Jain, S., Mukhopadhyaya, K.: Pattern formation for asynchronous robots without agreement in chirality. Co RR abs/1403.2625 (2014). URL http://arxiv.org/abs/1403.2625
8(8) Cicerone, S., Di Stefano, G., Navarra, A.: Asynchronous embedded pattern formation without orientation. In: Proc. 30th Int.’l Symp. on Distributed Computing (DISC), LNCS , vol. 9888, pp. 85–98. Springer (2016)

TL;DR

Contribution

Findings

Abstract

Peer Reviews

Videos

Taxonomy

Asynchronous Arbitrary Pattern Formation: the effects of a rigorous approach††thanks: The work has been supported in part by the European project

Abstract

Keywords:

1 Introduction

1.1 Motivation and related work

1.2 Our results

Theorem 1.1

1.3 Outline

2 Robot Model

Definition 1

Definition 2

3 Notation and basic properties

Property 1

Property 2

Definition 3

Definition 4

Definition 5

3.1 View of a point and symmetries

Definition 6

4 The strategy

5 Counter-examples

5.1 A counter-example to the correctness of the algorithm presented in FYOKY15

5.2 A counter-example to the correctness of the algorithm presented in BT15 ; BT16b

5.3 A counter-example to the correctness of the algorithm presented in DPVarx09

6 The algorithm

Theorem 6.1

Proof

6.1 Phase F1\mathcal{F}1F1

6.2 Phase F2\mathcal{F}2F2

6.3 Phase F3\mathcal{F}3F3

Lemma 1

Proof

6.4 Phase F4\mathcal{F}4F4

Definition 7

6.5 Phase F5\mathcal{F}5F5

7 Correctness

Lemma 2

Proof

Lemma 3

Proof

Lemma 4

Proof

Lemma 5

Proof

Lemma 6

Proof

Lemma 7

Proof

Lemma 8

Proof

Lemma 9

Proof

Lemma 10

Proof

Lemma 11

Proof

Lemma 12

Proof

Theorem 7.1

Proof

Theorem 7.2

Proof

Theorem 7.3

8 Conclusion

6.1 Phase $\mathcal{F}1$

6.2 Phase $\mathcal{F}2$

6.3 Phase $\mathcal{F}3$

6.4 Phase $\mathcal{F}4$

6.5 Phase $\mathcal{F}5$