77 Shades of Grey

These constraints clearly constitute a new challenge for us. Nevertheless, we accepted this mission and designed two algorithms; one operates in the dark, while the other operates in the light mode. In this paper, we describe the details of our algorithms for Batdroids, naturally with the authorization of Bruce Wayne. The design of the Batdroids themselves is confidential and protected by patents in order to preserve the intellectual property of Wayne Enterprises; consequently, we do not disclose any information regarding their conception. Our two algorithms operate in the FSync model and enable Batdroids to perpetually explore a three-dimensional grid representing the cave. As motivated above, our goal is to minimize both the size of the colony (i.e., the number of Batdroids that compose it) and the capabilities required by those Batdroids.

We first investigate the problem under visibility range one in dark mode. Under this assumption, it is already known from [5] that three Batdroids are necessary to solve the problem. We show that this number is also sufficient in our context, despite the absence of common chirality. Specifically, we present an algorithm that uses only three Batdroids with visibility range one and requires 77 shades of grey. However, this algorithm has a shortcoming: although it successfully ensures perpetual and complete patrolling of the cave, its executions are not fully deterministic. Some rules are ambiguous and rely on symmetry breaking that is arbitrarily resolved by an adversary. As a result, the patrol behavior is not fully under control – an unsatisfactory property for a highly self-disciplined individual such as Bruce Wayne. In other words, Bruce Wayne requires a well-defined algorithm (i.e., non-ambiguous) for his Batdroids.

Nevertheless, we prove that, regardless of the number of available colors, no well-defined algorithm allows three Batdroids to perpetually patrol caves under visibility range one without common chirality. Bruce Wayne is willing to accept this limitation in dark mode, acknowledging that darkness naturally restricts Batdroid perception. However, he argues that in light mode, increasing the visibility range is a reasonable way to circumvent this impossibility.

Motivated by this observation, we investigate a well-defined solution under visibility range two for light mode. This second solution also requires only three Batdroids. Moreover, the increased visibility range allows us to drastically reduce the required capabilities: in light mode, only four colors are sufficient to implement our algorithm.

In the next section, we formally define the model, the Batdroid capabilities, and the problem to solve, the so-called Perpetual Exploration Problem (PEP). In Section 3, we present a lower bound on the number of Batdroids necessary to solve the problem with a well-defined algorithm and under visibility range one. In Sections 4 and 5, we present our two algorithms. We give a detailed related work in Section 6. Finally, we conclude in Section 7. Notice also that, to help the reader, online animations illustrating the behavior of our algorithms are available for both solutions: [3] and [4].

A configuration $C$ in a 3D grid $G(V,E)$ is a set of pairs $(p,c)$, where $p\in V$ is an occupied node and $c\in \mathrm{𝐶𝑙}$ is the color of the Batdroid located at $p$. A node $p$ is empty if and only if $\forall c,(p,c)\notin C$. We sometimes just write the set of occupied nodes when the colors are clear from the context.

We denote by $G_r$ the globally oriented view centered at the Batdroid $r$, i.e., the subset of the configuration containing the states of the nodes at distance at most $\mathrm{\Phi }$ from $r$, translated so that the coordinates of $r$ are $(0,0,0)$. We use this globally oriented view in our analysis to describe the movements of the Batdroids (see, for example, Figure 1): when we say “the Batdroid moves Left”, it is according to the globally oriented view. However, since Batdroids do not agree on any axis, they have no access to the globally oriented view. When a Batdroid looks at its surroundings, it instead obtains a local view. To model this, we assume that the local view acquired by a Batdroid $r$ in the Look phase is the result of an arbitrary indistinguishable transformation on $G_r$. Here, we assume that Batdroids are self-inconsistent, meaning that different transformations may be applied at different rounds. An indistinguishable transformation consists of applying to each of the three axes ($x$-axis, $y$-axis, and $z$-axis) passing through $r$ a rotation (maybe different for each axis) picked in the set $\{0,\frac{\pi }{2},\pi ,\frac{3\pi }{2}\}$. We denote by $ℐ𝒯$ the set of all possible indistinguishable transformations. Contrary to Beedroids in [5], Batdroids do not share a common chirality. That is, they cannot distinguish a local view from its reflection and hence take different decisions in each case. For instance, in Figure 2, Batdroids cannot distinguish Above from Below as they cannot use the right-hand rule to determine the third axis knowing two other axes.

It is important to note that when a Batdroid $r$ computes a destination $d$, it is relative to its local view $f(G_r)$, which is the globally oriented view transformed by some $f\in ℐ𝒯$. So, the actual movement of the Batdroid in the globally oriented view is $f^{-1}(d)$. For example, if $d=\mathrm{𝐴𝑏𝑜𝑣𝑒}$ but the Batdroid sees the 3D grid upside-down ($f$ is the $\pi$-rotation along the $y$-axis), then the Batdroid moves $\mathrm{𝐵𝑒𝑙𝑜𝑤}=f^{-1}(\mathrm{𝐴𝑏𝑜𝑣𝑒})$. In a configuration $C$, $V_C(i,j)$ denotes the globally oriented view of a Batdroid located at $(i,j)$.

A Batdroid is said to be lost when it sees no wall and no other Batdroids. Observe that in this case, if the Batdroid decides to move, the destination is entirely determined by the choice of the transformation $f$ done by the adversary.

An algorithm ${𝖠}^{}$ is a tuple $(\mathrm{𝐶𝑙},\mathrm{𝐼𝑛𝑖𝑡},T)$ where $\mathrm{𝐶𝑙}$ is the set of possible colors, $\mathrm{𝐼𝑛𝑖𝑡}$ is a mapping from any considered 3D grid to a non-empty set of initial configurations in that 3D grid, and $T$ is the transition function $Views\to \{\mathrm{𝐼𝑑𝑙𝑒},\mathrm{𝐹𝑟𝑜𝑛𝑡},\mathrm{𝐵𝑎𝑐𝑘},\mathrm{𝐿𝑒𝑓𝑡},\mathrm{𝑅𝑖𝑔ℎ𝑡},$ $\mathrm{𝐴𝑏𝑜𝑣𝑒},\mathrm{𝐵𝑒𝑙𝑜𝑤}\}\times \mathrm{𝐶𝑙}$, where $Views$ is the set of local views. When the Batdroids are in Configuration $C$, a configuration $C^{\prime }$ obtained after one round satisfies: $((i,j,k),c^{\prime })\in C^{\prime }$, if and only if there exists a color $c\in \mathrm{𝐶𝑙}$ and a transformation $f\in ℐ𝒯$ such that one of the following conditions holds:

• $\mathrm{■}$

  $((i,j,k),c)\in C$ and $f^{-1}\circ T\circ f\circ V_C(i,j,k)=(\mathrm{𝐼𝑑𝑙𝑒},c^{\prime })$,

• $\mathrm{■}$

  $((i-1,j,k),c)\in C$ and $f^{-1}\circ T\circ f\circ V_C(i-1,j,k)=(\mathrm{𝑅𝑖𝑔ℎ𝑡},c^{\prime })$,

• $\mathrm{■}$

  $((i+1,j,k),c)\in C$ and $f^{-1}\circ T\circ f\circ V_C(i+1,j,k)=(\mathrm{𝐿𝑒𝑓𝑡},c^{\prime })$,

• $\mathrm{■}$

  $((i,j-1,k),c)\in C$ and $f^{-1}\circ T\circ f\circ V_C(i,j-1,k)=(\mathrm{𝐹𝑟𝑜𝑛𝑡},c^{\prime })$,

• $\mathrm{■}$

  $((i,j+1,k),c)\in C$ and $f^{-1}\circ T\circ f\circ V_C(i,j+1,k)=(\mathrm{𝐵𝑎𝑐𝑘},c^{\prime })$,

• $\mathrm{■}$

  $((i,j,k-1),c)\in C$ and $f^{-1}\circ T\circ f\circ V_C(i,j,k-1)=(\mathrm{𝐴𝑏𝑜𝑣𝑒},c^{\prime })$, or

• $\mathrm{■}$

  $((i,j,k+1),c)\in C$ and $f^{-1}\circ T\circ f\circ V_C(i,j,k+1)=(\mathrm{𝐵𝑒𝑙𝑜𝑤},c^{\prime })$.

We write an algorithm as a set of rules, where a rule is a triplet $(V,d,c)\in Views\times \{\mathrm{𝐼𝑑𝑙𝑒},\mathrm{𝐹𝑟𝑜𝑛𝑡},\mathrm{𝐵𝑎𝑐𝑘},\mathrm{𝐿𝑒𝑓𝑡},\mathrm{𝑅𝑖𝑔ℎ𝑡},$ $\mathrm{𝐴𝑏𝑜𝑣𝑒},\mathrm{𝐵𝑒𝑙𝑜𝑤}\}\times \mathrm{𝐶𝑙}$. We say that an algorithm $(\mathrm{𝐶𝑙},\mathrm{𝐼𝑛𝑖𝑡},T)$ includes the rule $(V,d,c)$, if $T(V)=(d,c)$. By extension, the same rule applies to indistinguishable views, i.e., $\forall f\in ℐ𝒯,T(f(V))=(f(d),c)$. Consequently, we forbid an algorithm to contain two rules $(V,d,c)$ and $(V^{\prime },d^{\prime },c^{\prime })$ such that $V^{\prime }=f(V)$ for some $f\in ℐ𝒯$.

As an illustrative example, consider the rule $R_1$ given in Figure 1. This rule is defined for Batdroids having a visibility range of one. This rule means that, when a Batdroid sees three Batdroids, one with Color $B$ on its left, one with color $G$ in front of it, and the third one with Color $B$ below it, then the red Batdroid is dictated to move Above and change its color to $O$.

In the same figure, Rule $R_2$ is a rule where a black node represents a part of the outer boundary of the 3D grid, that we call a wall in the remaining of the paper. In our algorithms, we often define similar rules that apply regardless of the presence of a wall in some part of the view. Thus, to avoid defining the same rules multiple times with very similar views, we propose a notation to represent several rules in just one picture. For example, Rule $R_3$ in Figure 1 has one node hatched with vertical lines, which means that the rule applies regardless of the presence of a wall located at this node. In practice, every rule that contains such vertical (resp. horizontal) hatched lines, represents a set of rules obtained by replacing each of those lines either by walls, or by empty nodes. For example, Rule $R_3$ in Figure 1 is a concise representation of Rules $R_1$ and $R_2$.

Figure 2 shows an ambiguous rule. The Batdroid has a symmetric view so that, depending on the transformation $f$ chosen by the adversary, the Batdroid executing this rule moves either above or below. In the following, we represent in ambiguous rules all possible destinations that can be dictated by the adversary.

Recall that Batdroids are assumed to be self-inconsistent. In this context, we say that an algorithm $(\mathrm{𝐶𝑙},\mathrm{𝐼𝑛𝑖𝑡},T)$ is well-defined if the global destination computed by a Batdroid does not depend on the applied indistinguishable transformation $f$, i.e., for every globally oriented view $V$, and every transformation $f\in ℐ𝒯$, we have $T(V)=f^{-1}(T(f(V)))$. An algorithm that is not well-defined is said to be ambiguous, as it may lead to different movements depending on the choice of the transformation $f$ done by the adversary (see Figure 2 for an example). Note that a well-defined algorithm does not contain any ambiguous rule.

We denote by $C\rightsquigarrow C^{\prime }$ the fact that $C^{\prime }$ can be reached in one round from $C$ (n.b., $\rightsquigarrow$ is then a binary relation over configurations).

An execution of Algorithm ${𝖠}^{}$ in a 3D grid $G$ is then a sequence ${(C_i)}_{i\in \mathbb{N}}$ of configurations such that $C_0\in \mathrm{𝐼𝑛𝑖𝑡}(G)$ and $\forall i\ge 0$, $C_i\rightsquigarrow C_{i+1}$.

An execution ${(C_i)}_{i\in \mathbb{N}}$ in a 3D grid $G=(V,E)$ achieves the Perpetual Exploration Problem (PEP) if for every node $u\in V$ and for every time $t$, there exists a time $t^{\prime }\ge t$ such that $u$ is occupied in $C_{t^{\prime }}$.

An algorithm ${𝖠}^{}$ that uses $n$ Batdroids solves the PEP if, for every cave (i.e., any 3D grid with $S_x\ge 4$, $S_y\ge 4$, $S_z\ge 4$) and every initial configuration $C_0\in \mathrm{𝐼𝑛𝑖𝑡}(G)$, we have every execution of ${𝖠}^{}$ in $G$ starting from $C_0$ that achieves the PEP.

Assume, by the contradiction, that there exists a well-defined algorithm allowing three Batdroids under visibility one to perpetually explore caves, using an arbitrary large number of light colors. In the following, we denote by $B_1$, $B_2$, and $B_3$ the three Batdroids. Consider any cave $𝒞$ of size $S_x\times S_y\times S_z$ with $S_x=S_y=S_z\ge 13$ and $S_x$ is even. First, remark that $𝒞$ has four centers.¹¹1A center is any node of minimum eccentricity. Observe that (*) if at some time, there exists a slice $S$ of $𝒞$ containing a center and all three Batdroids, then exploration with a well-founded algorithm becomes impossible. Indeed, (1) there are nodes of $𝒞$ outside $S$, and (2) any destination allowing a Batdroid to leave $S$ is ambiguous. As a consequence, the three Batdroids remain forever trapped to $S$ making the perpetual exploration fail.

Next, as there are three Batdroids and four centers in the cave, at least one of them, say $c$, is initially empty. So, at least one Batdroid, say $B_1$, should eventually visit $c$, say at time $t>0$. Remark then that at time $t-1$, $B_1$ was on a neighboring node of $c$. Moreover, $B_1$ was not lost since otherwise the move would have been ambiguous. Hence, (**) at least one Batdroid was neighbor of $B_1$ at time $t-1$. At time $t$, four cases are possible:

1. 1.

   A Batdroid is neighbors of the two others.

   Then, the three Batdroids are on the same slice of $𝒞$ containing $c$, and we obtain a contradiction from (*).

2. 2.

   One Batdroid, say $B_2$, is neighbor of $B_1$ and the other $B_3$ is isolated.

   In this case, during the next round, either $B_3$ is idle, or it is neighbor of a wall and move away from the wall. In this latter case, $B_3$ become lost: due to the size of $𝒞$, it is still not neighbor $B_1$ or $B_2$ after the round, whatever be the behavior of $B_1$ and $B_2$. Thus, at time $t+1$, $B_3$ is necessarily idle. Then, let $L$ be the line passing through $B_1$ and $B_2$ at time $t$. For each of the two Batdroids $B_1$ and $B_2$, the only unambiguous destinations are located on $L$. So, they can only move along $L$. If, a time $t+1$, $B_3$ is neither on $L$, nor located on a node neighbor to a node of $L$, then $B_1$ and $B_2$ remain forever on $L$ and $B_3$ is idle forever. Now, as there exist nodes of the cave different from the final location of $B_3$ and outside $L$, the perpetual exploration fails, a contradiction. Otherwise, to eventually leave $L$, $B_1$ and $B_2$ must move so that eventually at least one of them becomes neighbor of $B_3$. But, if this happens, the three Batdroids are on a slice $S$ of $𝒞$ containing $L$: $S$ contains a center of $𝒞$ (namely, $c$) and we obtain a contradiction by (*).

3. 3.

   $B_1$ is isolated, yet $B_2$ and $B_3$ are neighbors.

   In this case, while $B_1$ is isolated, it stays idle at $c$ since all its possible destinations are ambiguous. Then, let $L$ be the line passing through $B_2$ and $B_3$ at time $t$. At time $t-1$, before arriving at $c$, $B_1$ was on a neighboring node of $c$. Thus, another Batdroid, say $B_2$, was at distance at most 2 from $c$ at time $t-1$ by (**) and so is at distance at most 3 from $c$ at time $t$. $B_3$ being neighbor of $B_2$ at time $t$, $B_3$ is then at distance at most 4 from $c$ at time $t$. Consequently, for each of the two Batdroids $B_2$ and $B_3$, the only unambiguous destinations are located on $L$: they can only move along $L$. If $B_1$ is neither on $L$, nor located on a node neighbor to a node of $L$, then $B_2$ and $B_3$ remain forever on $L$, and as there are nodes of $𝒞$ different from $c$ and outside $L$, the perpetual exploration fails, a contradiction. Otherwise, to eventually leave $L$, they must move so that at least one of them eventually becomes neighbor of $B_1$, but in this case, we retrieve the first or second case, a contradiction.

4. 4.

   The three Batdroids are isolated.

   In this case, $B_1$ is necessarily idle since lost. Another Batdroid, say $B_2$, is at distance at most 3 from $c$ by (**). So, due to the size of $𝒞$, $B_2$ is lost too and so idle. If $B_3$ is also idle, then the exploration fails, a contradiction. Otherwise, $B_3$ is neighbor of a wall at time $t$ and so at distance at least four (resp. three) from $B_1$ (resp. $B_2$), it necessarily moves away from the wall, and it is lost at time $t+1$. Hence, all three Batdroids are idle at time $t+1$, a contradiction.

Hence, in all cases we obtain a contradiction and so the theorem holds. $◀$

Without loss of generality, let assume that $S_x$, $S_y$, and $S_z$ are respectively the width, the length, and the height of the 3D grid, and that the Batdroids start exploring the grid floor by floor in a bottom-up direction.

First, remark that ${𝖠}_{\mathrm{𝗅𝗂𝗀𝗁𝗍}}$ proceeds in repetitive phases that are independent from the grid size. Let $𝒞$ be the initial configuration. This configuration is periodically reached and, in between two occurrences of $𝒞$, every node of the grid must have been visited at least once. The finite exploration that happens in between two occurrences of $𝒞$ is composed of the following phases: The grid is explored floor by floor, until reaching the last one (i.e., the $S_z^{\text{th}}$), from where it changes its exploration direction (from bottom-up to top-down, or conversely). Each floor is explored line by line. The size of the floor, i.e., the length of a line and the number of lines, does not impact the way the exploration is performed. It only impacts the exploration time since Batdroids must repeat the same patterns for an additional number of times. However, the Batdroids do a $\frac{\pi }{2}$-turn when changing of floor. Thus, the exploration of two consecutive floors is analogous up to a $\frac{\pi }{2}$ rotation, meaning that the exploration of the $i^{\text{th}}$ and $j^{\text{th}}$ floors is analogous if $i(mod4)=j(mod4)$.

Hence, we proceed by induction on $S_x\times S_y\times S_z$.

• $\mathrm{■}$

  Base cases: We have validated several base cases by simulation, namely every grid of size $S_x\times S_y\times S_z$ with $4\le S_x\le 7$, $4\le S_y\le 7$, and $4\le S_z\le 7$. Since no rule is ambiguous and we consider a synchronous scheduler, this check is quite easy: We only have to perform one execution for each grid and each initial configuration $𝒞$. Once the Batdroids reach $𝒞$ again, we just have to check that every node of the grid has been visited.

• $\mathrm{■}$

  Induction hypothesis: Assume that $\exists X\ge 7,Y\ge 7,Z\ge 7$, such that ${𝖠}_{\mathrm{𝗅𝗂𝗀𝗁𝗍}}$ solves the perpetual exploration in every 3D grid of size $S_x\times S_y\times S_z$ where $4\le S_x\le X$, $4\le S_y\le Y$, and $4\le S_z\le Z$.

• $\mathrm{■}$

  Induction step: Using the previous arguments, we can easily show that the exploration of a grid $G$ of size $(X+1)\times Y\times Z$ or $X\times (Y+1)\times Z$ is analogous to the exploration of a smaller grid $G^{\prime }$ of size $X\times Y\times Z$. Similarly the exploration of a grid $G$ of size $X\times Y\times (Z+1)$ is analogous to the exploration of a smaller grid $G^{\prime }$ of size $X\times Y\times (Z-3)$. In both cases, the induction hypothesis holds on the smaller grid $G^{\prime }$ so ${𝖠}_{\mathrm{𝗅𝗂𝗀𝗁𝗍}}$ also performs the perpetual exploration on $G$.

$◀$

We now describe the main idea of the algorithm in more detail. This technique takes place in a slice of the grid at the border of the 3D grid, which we represent as a 2D grid in Figure 10. In this grid, a number represents the shade of grey of the Batdroid (for simplicity we used numbers that differ slightly from the full algorithm). The beacon Batdroid has shade 10 and is initially placed diagonally at distance 2 in one direction and distance 1 orthogonally from the line explored by the traveling group (this line is orthogonal from the slice we are seeing).

In the first grid (Step 1 of Figure 10), we see the first Batdroid of the travelling group with shade 1, denoted ① (the other is not visible in this slice but is adjacent to it, in the opposite direction from the wall). When the Batdroid ① reaches the wall and has to move, it cannot distinguish any direction in the slice, so this ambiguous move is resolved by the adversary.

The key idea is that, regardless of the direction, the travelling group will search for the beacon Batdroid ⑩ in all four directions. Interestingly, we eventually and deterministically reach a configuration where the traveling group is adjacent to the beacon as in the last step of Figure 10, regardless of the choices made by the adversary during the search process.

For the sake of this example, consider that Batdroid ① first moves up, followed by Batdroid ⑪ (Step 2 in Figure 10). After two steps, counted by Batdroid ① that becomes ②, and since the beacon is not found, Batdroid ② becomes ③ to signal the follower that they have to search in the opposite direction. Batdroids exchange their roles: former leader is now follower with color ⑪, and former follower becomes leader taking color ④. After three steps in the opposite direction (counted by the Batdroid ④ that becomes ⑤ and then ⑥), since the beacon is still not found, Batdroid ⑥ signals the follower that they have to search in the orthogonal direction by taking color ⑦.

In Step 9 of Figure 10, Batdroid ⑧ moves orthogonally with an ambiguous move. Its next color is ① and we reach exactly the configuration that we would have reached if the first move of the search had been in this orthogonal direction. Thus, by repeating the same sequence of moves, we eventually reach the configuration where the travelling group is adjacent to the beacon Batdroid ⑩ (Step 11 of Figure 10). When this happens, Batdroid ② becomes ⑨ to signal the follower that they can start the next phase of the exploration. This last configuration is reached regardless of the choices made by the adversary during the search process (in step 1 and 9), which is crucial for the correctness of the algorithm.

Once the traveling group is adjacent to the beacon Batdroid, they can determine the three necessary directions to continue their exploration: order of exploration of nodes in each line (away from the adjacent wall), the order in which lines are explored (from left to right in the figure), and the order in which floors are explored (from bottom to top in the figure). From step 11, the next line to be explored is the line that is orthogonal to the slice we are seeing and passing through batdroid ⑪, which is in fact the line that is parallele and at distance one from the line the travelling group just explored in step 1.

After a sequence of moves, the three Batdroids reach the same configuration as when they started exploring the previous line, but translated to the next line. So the exact same sequence of moves can be repeated to explore this new line. This process is repeated until the entire floor is explored.

After exploring the penultimate line of the floor, the traveling group detects it as the beacon is now adjacent to a wall. After exploring the last line of the floor, a sequence of moves (again containing some ambiguous moves) is performed to move the three Batdroids to the next floor and start exploring the first line of this new floor. Here the Batdroids reach one of two possible configurations that are mirrored, but both are similar to the configuration formed when they started exploring the previous floor (but translated to the next floor and rotated by $\frac{\pi }{2}$), the exact same sequence of moves can be repeated to explore this new floor. This process is repeated until the entire 3D grid is explored.

The Batdroids detect when they are exploring the last floor. At this point, each sequence we described previously is slightly modified (actually simplified since we have the wall located above to help), eventually the beacon Batdroid reaches the last corner of the last floor. After exploring the last line of the last floor, a final sequence of moves is performed to turn the Batdroids around and start exploring the 3D grid in the opposite direction, repeating the same process as before.

When putting all the steps together, we obtain the full algorithm ${𝖠}_{\mathrm{𝖽𝖺𝗋𝗄}}$ that can be executed in the online simulator [4], where one can see the exploration and check what rule is executed by which Batdroid.

The proof of this theorem follows the same structure as the proof of Theorem 2 in Section 4. The main difference is that the execution is not deterministic due to the ambiguous moves. It may seem intractable to check all the possible execution, however, as explained in the description of the algorithm, the key property that ensures the correctness of the algorithm is that, whenever an ambiguous move is performed at a time $t$, there exists a time $t^{\prime }>t$ when we reach a set of configurations regardless of the choice of the adversary. Informally, if we reach a single configuration, we can ignore the configurations between $t$ and $t^{\prime }$ every time an ambiguous move occurs. In some cases, for instance when we change floor, we may reach two configurations that differ by a rotation or a mirroring, but both configurations are equivalent for the exploration purpose.

The induction step of the proof, similar to the one of Theorem 2, can then be applied similarly since the exploration of a line does not depend on its length, nor does the exploration of a floor depend on its size, nor does the exploration of the 3D grid depend on its height.

So the correctness of the algorithm relies on the fact that an ambiguous move is followed by a sequence of moves that eventually leads to a configuration or a set of configurations that does not depend on the choice of the adversary. This property can be proved by simply checking that the configuration graph starting from a configuration $C$ (where a Batdroid has an ambiguous move), is a Directed Acyclic Graph (DAG) with a sink $C^{\prime }$.

For instance, there is a configuration in the execution of our algorithm where the three Batdroids form an L-shape (all adjacent to a wall) and we want to reach a configuration where one Batdroid is at distance two and three from the two other Batdroids respectively (to be adjacent to the beacon), as shown in Figure 11. The graph of configuration from this configuration is shown in Figure 12.

A similar graph can be built for the ambiguous moves shown in Figures 10. In all these cases, we can check that the configuration graph is a DAG with a unique sink, which proves the desired property.

Therefore, by checking all the ambiguous moves of the algorithm, we can conclude that the algorithm eventually reaches configurations that do not depend on the choices of the adversary after each ambiguous move.

Thus, the exploration proceeds as in a deterministic execution, which concludes the proof.

$◀$