## 3 Coverage Methods Utilizing Multiple Heterogeneous Robots
### Analysis
Recall that every frontierPoint is a freePoint. Thus, while \(n_{i}^{s}\) travels along an edge from \(m_{end}\) to \(f_{n_{i}^{s}}\), \(n_{i}^{s}\) avoids collision. Furthermore, \(n_{i}^{s}\) is connected to \(m_{end}\). Utilizing the similar argument as in the previous paragraph, \(n_{i}^{s}\) is connected to \(n_{1}^{s}\) during the maneuver. We discuss how to localize all robots \(\{m_{1}\to m_{2}\to\cdots\to m_{end}\}\) using Assumption (A1). \(m_{1}\) is \(n_{1}^{s}\), since \(n_{1}^{s}\) is the first robot dropped by the ship \(p^{s}\). Thus, we localize \(m_{1}\) using \(\mathbf{n}_{1}^{s}\). Also, the 3D coordinates of \(m_{j+1}\) are the sum of the following two coordinates:  
1. the 3D coordinates of \(m_{j}\). 2. the relative position of \(m_{j+1}\) with respect to \(m_{j}\). Here, the relative position of \(m_{j+1}\) with respect to \(m_{j}\) is available using Assumption (A1). Using deduction, we localize \(m_{j}\) for all \(j\leq end\). We next address how to localize \(f_{n_{i}^{s}}\). The 3D coordinates of \(f_{n_{i}^{s}}\) are the sum of the following two coordinates:  
1. the 3D coordinates of \(m_{end}\). 2. the relative position of \(f_{n_{i}^{s}}\), with respect to \(m_{end}\). Here, the relative position of \(f_{n_{i}^{s}}\) with respect to \(m_{end}\) is available using Assumption (A3). This theorem is proved. In Theorem 3, it is proved that after Algorithm 1 is done, \(I^{s}\) contains all robots dropped by the ship \(p^{s}\). Also, all robots in \(I^{s}\) are localized. **Theorem 3**. : _Consider the situation where all robots move under Algorithm 1. After Algorithm 1 is done, \(I^{s}\) contains all robots dropped by \(p^{s}\). Also, all robots in \(I^{s}\) are localized._Proof. : Utilizing Theorem 2, \(n_{i}^{s}\) is connected to \(n_{1}^{s}\), while \(n_{i}^{s}\) travels along the directed path to \(f_{n_{i}^{s}}\). As \(n_{i}^{s}\) arrives at \(f_{n_{i}^{s}}\), \(n_{i}^{s}\) is connected to \(n_{1}^{s}\). Note that \(n_{1}^{s}\) doesn't move at all under Algorithm 1. Utilizing deduction, all robots \(n_{2}^{s},n_{3}^{s},\ldots n_{i-1}^{s}\) are connected to \(n_{1}^{s}\). As \(i\) varies from \(1\) to \(N^{s}\) under Algorithm 1, all robots dropped by \(p^{s}\) are located at their target positions and \(I^{s}\) contains all these robots. We next prove that all robots in \(I^{s}\) are localized. On contrary, suppose that a robot, say \(n_{c}^{s}\), is not localized. Since \(I^{s}\) contains all robots dropped by \(p^{s}\), there exists a directed path from \(n_{1}^{s}\) to \(n_{c}^{s}\) using Theorem 1. Using the similar arguments as in the last two paragraphs of proof for Theorem 2, all robots along the path are localized. Thus, \(n_{c}^{s}\) is localized. We proved that all robots in \(I^{s}\) are localized. Theorem 4 proves that if one can't find a frontierSurface, then the obstacle-free space is covered by all \(Sphere^{dc}\)s completely, such that no coverage hole exists. Theorem 4: _If we can't find a frontierSurface, then all \(Sphere^{dc}\) cover the obstacle-free space completely, such that no coverage hole exists._  
Proof. : Using the transposition rule, the below statement is proved: if an obstacle-free space, which is outside a \(Sphere^{dc}\), exists, then we can find a frontierSurface. Suppose that an obstacle-free space, which is outside a \(Sphere^{dc}\), exists. Let \(O\) indicate this uncovered obstacle-free space. Then, at least one robot, say \(n_{i}^{s}\), has a frontierSurface intersecting \(O\). Using Theorem 3, \(I^{s}\) contains \(n_{i}^{s}\) under Algorithm 1. Hence, we can find this frontierSurface using \(I^{s}\). Theorem 4 proved that once the 3D network is completely generated using Algorithm 1, then no sensing hole remains. In Algorithm 1, \(n_{i}^{s}\) moves along the directed path in \(I^{s}\) until meeting \(f_{n_{i}^{s}}\). Let \(\{m_{1}\to m_{2}\to\cdots\to m_{end}\}\) represent the robots on the path. Here, \(m_{1}\) is \(n_{1}^{s}\). After \(n_{i}^{s}\) arrives at \(m_{j}\) (\(j\leq end-1\)), \(n_{i}^{s}\) heads towards \(m_{j+1}\).