# Ground Control System Based Routing for Reliable and Efficient Multi-Drone Control System
## 3 GCS-Routing Design
### Routing Loops in GCS-Routing
#### 3.4.2 Loop-Free GCS-Routing Proof  
We formally prove that GCS-routing is loop-free. Let \(G=(V,E,g)\) be a weighted directed graph, with \(g\): \(E(G)\rightarrow\mathbb{R}\) representing a flying ad-hoc network where each vertex represents a drone or GCS, and an edge is incident to two vertices when both vertices are in transmission range of each other. We assume that membership in the vertex set, \(V(G)\), is quasi-static and \(G\) is always connected. (This assumption is reasonable since GCS controls and manages one or more drones to accomplish a given mission.) The edge set, \(E(G)\), can be changed depending on drone mobility and link state. Since GCS-routing uses distance (based on GPS information) as the routing metric, \(G\) cannot have negative weight cycles. Let \(\left\langle T_{i}\right\rangle\) (\(T_{i}>0\), \(i=1,2,3,\cdots\)) be a sequence of distinct time instants, \(T_{1}\), \(T_{2},\cdots\), when the network topology changes due to mobility and link state. Lemma 1: _GCS-routing generates a shortest paths tree rooted at each vertex \(s\) in \(V(G)\). (\"Shortest paths tree rooted at vertex \(s\)\" means that the GCS-routing algorithm returns a directed tree rooted at \(s\), such that it contains all vertices and every tree path to each vertex is the shortest path in the given graph. )_  
Proof: GCS-routing used edge relaxation such as [PERSON]'s or Bellman-Ford's algorithm to generate shortest paths to all the vertices in \(V(G)\) for a given source vertex, \(s\). Thus, from many well-known theorems [34], GCS-routing generates a shortest paths tree rooted at \(s\) in \(V(G)\). Then, let a shortest paths tree rooted at \(s\) be \(G_{s}^{t}\) at an arbitrary time instant \(t\). Figure 7: Example scenario where a transient loop is formed in GCS-routing. **Lemma 2**: _For any time interval \([T_{i},T_{i+1}]\), \(i\geq 1\), \(G_{s}^{T_{i}}\) is not changed._  
Suppose \(G_{s}^{T_{i}}\) is changed within the interval. Let \(T_{i+a}\) be the time instant when the topology is changed. Then, \(T_{i+a}=T_{i+1}\) since \(T_{i+a}\) should be in \(\left\langle T_{i}\right\rangle\). This contradicts the assumption. Once a shortest paths tree, \(G_{s}^{T_{i}}\), rooted at \(s\), is constructed by GCS-routing after time instant \(T_{i}\), it is continuously used to route all the packets from node \(s\) to the other vertices until \(T_{i+1}\). \(T_{i+1}\) is when GCS initiates GCS-routing after perceiving a change in the network topology. Then GCS-routing generates a new shortest paths tree, \(G_{s}^{T_{i+1}}\), rooted at each \(s\). **Lemma 3**: _There exists a short interval \(\delta(T_{i},T_{i+1})\), \(i\geq 1\), when the subgraph that GCS-routing generates for vertex \(s\) is not a tree after GCS-routing is initiated, i.e., the topology is changed._  
When GCS-routing notices one or more topology changes at time instant \(T_{i+1}\), it takes finite time to make \(G_{s}^{T_{i+1}}\) different from \(G_{s}^{T_{i}}\). Therefore, any subgraph \(G_{s}^{T_{i}(T_{i},T_{i+1})}\) of \(G_{s}^{T_{i}}\cup G_{s}^{T_{i+1}}\) can be possible until \(G_{s}^{T_{i+1}}\) is completely constructed. Hence, there could be a cycle between two nodes \(v_{i}\) and \(v_{j}\). The cycle is constructed in the way that one part of the cycle comes from \(G_{s}^{T_{i}}\) and the other part is from \(G_{s}^{T_{i+1}}\), and hence \(G_{s}^{T_{i}(T_{i},T_{i+1})}\) is not a tree. **Lemma 4**: _Any short interval \(\delta(T_{i},T_{i+1})\), \(i\geq 1\), when the subgraph that GCS-routing generates for vertex \(s\) is not a tree is eventually terminated if all the routing messages from GCS are eventually delivered to all the participating nodes._  
Since we assume membership of \(V(G)\) is not changed and any vertex is connected to at least one other vertex, all routing control messages generated by GCS-routing are eventually delivered to every vertex. Therefore, vertex \(s\) comes to have a new shortest paths tree based on newly delivered routing messages.