## 3 Coverage Methods Utilizing Multiple Heterogeneous Robots
### Analysis  
Algorithm 1 ends when \(i==N^{s}\) or \(I^{s}\) finds no frontierPoint. If \(i==N^{s}\), then there is no remaining robot in the ship \(p^{s}\). Acknowledge that all sensing holes disappear only when \(\sum_{s=1}^{S}N^{s}\) is sufficiently large. Based on simulations, Section 4.1 presents how to estimate the number of robots required for covering a 3D workspace, considering the case where an obstacle inside the workspace is not known a priori. In Algorithm 1, a robot \(n_{i}^{s}\) travels along a directed path in \(I^{s}\) until arriving at \(f_{n^{s}}\). The next theorem proves that \(n_{i}^{s}\) can find at least one directed path from \(n_{1}^{s}\) to \(f_{n_{i}^{s}}\). Recall that \(n_{1}^{s}\) is the first robot dropped by the ship \(p^{s}\). Figure 1: \(n_{i}^{s}\) heads towards \(f_{n_{i}^{s}}\). Red curves indicate obstacle boundaries, and the path of \(n_{i}^{s}\) is illustrated with yellow line segments. The large dots indicate the robots which are already at their target positions. FrontierPoints are depicted as points on one robot’s \(Boundary^{dc}\). **Theorem 1**. : _Consider the situation where all robots move under Algorithm 1. A robot \(n_{i}^{s}\) can find at least one directed path from \(n_{1}^{s}\) to \(f_{n_{i}^{s}}\)._  
Proof. : In Algorithm 1, \(n_{i}^{s}\) finds the nearest robot, say \(m\), with a frontierPoint by applying the directed breadth-first search on \(I^{s}\). Then, one frontierPoint on \(m\) is chosen as the target position, say \(f_{n_{i}^{s}}\), of \(n_{i}^{s}\). Since \(f_{n_{i}^{s}}\) is a frontierPoint, it exists on \(Boundary^{dc}\) of \(m\). Since \(m\) is found by applying the directed breadth-first search, there exists a directed path from \(n_{1}^{s}\) to \(m\). We next prove that there exists a directed path from \(m\) to \(f_{n_{i}^{s}}\). Since a frontierPoint is a freePoint, the straight line segment connecting \(m\) and \(f_{n_{i}^{s}}\) is safe. \(f_{n_{i}^{s}}\) exists on \(Boundary^{dc}\) of \(m\). Hence, there exists a directed edge from \(n_{j}^{s}\) to \(f_{n_{j}^{s}}\). We proved that there exists a directed path from \(n_{1}^{s}\) to \(n_{j}^{s}\). Also, we proved that there exists a directed path from \(n_{j}^{s}\) to \(f_{n_{j}^{s}}\). Thus, there exists a directed path from \(n_{1}^{s}\) to \(f_{n_{i}^{s}}\), such that the path contains \(n_{j}^{s}\). We proved that there exists a directed path from \(n_{1}^{s}\) to \(f_{n_{1}^{s}}\). The next theorem proves that \(f_{n_{i}^{s}}\) and all robots along the directed path are localized. While \(n_{i}^{s}\) travels along the path, it is connected to \(n_{1}^{s}\). In addition, \(n_{i}^{s}\) avoids collision during the maneuver. **Theorem 2**. : _Consider the situation where all robots move under Algorithm 1. While a robot \(n_{i}^{s}\) moves along the directed path in \(I^{s}\) until meeting \(f_{n_{i}^{s}}\), \(n_{i}^{s}\) is connected to \(n_{1}^{s}\). During the maneuver, \(n_{i}^{s}\) avoids collision with obstacles. Also, \(f_{n_{i}^{s}}\) and all robots along the directed path are localized._  
Proof. : \(n_{i}^{s}\) travels along the directed path in \(I^{s}\) until arriving at \(f_{n_{i}^{s}}\). Let \(\{m_{1}\to m_{2}\to\cdots\to m_{end}\}\) define the order of robots along the path until arriving at \(f_{n_{i}^{s}}\). Here, \(m_{1}\) is \(n_{1}^{s}\), since \(n_{1}^{s}\) is the first robot dropped by the ship \(p^{s}\). After \(n_{i}^{s}\) arrives at \(m_{j}\) (\(j\leq end-1\)), \(n_{i}^{s}\) moves toward \(m_{j+1}\). In addition, after \(n_{i}^{s}\) arrives at \(m_{end}\), \(n_{i}^{s}\) moves toward \(f_{n_{i}^{s}}\). While \(n_{i}^{s}\) travels along an edge from \(m_{k}\) to \(m_{k+1}\), \(n_{i}^{s}\) avoids collision, since \(I^{s}\) is safe for a robot. In addition, \(n_{i}^{s}\) is connected to \(m_{k}\) utilizing the notation of \(I^{s}\). Furthermore, \(m_{k}\) is connected to \(m_{1}=n_{1}^{s}\), since the directed path is found using the directed breadth-first method. Hence, \(n_{i}^{s}\) is connected to \(n_{1}^{s}\) during the maneuver.