Automated Trajectory Synthesis for UAV Swarms Based on Resilient Data Collection Objectives

A UAV swarm is a network of UAVs that can communicate with each other (mostly following the ad-hoc wireless networking) and usually perform a common task, autonomously or with the instructions from operators. It is important to maintain appropriate trajectories for all the UAVs in a network in order to avoid mid-air-collision or restricted areas (e.g., adverse territory or restricted private locations). It is also required to maintain successful communication between the neighboring UAVs and cover the surveillance points within a time constraint. In this research, we propose a formal framework that plans for the trajectories of the UAVs in a swarm, so that all or at least a fraction of the points near the data sources are covered within a given period. The coverage requirement may ensure that at least one of the available UAVs should cover each data point once or at each operator-specified time interval within the period. The resiliency specification considered in this research states that even if a certain number ($r$ or $k$) of UAVs fail to operate due to technical failures or cyberattacks, the surveillance goal is still fulfilled. In other words, the trajectory plan for the remaining UAVs can still securely surveil the required percentage of the data points.

Fig. 1 presents two sample trajectories for two different UAVs. They collect the available data in a combined way. The figure shows the starting points for both the UAVs, as well as the positions or waypoints from where they can collect the data. In our research problem, we consider a set of points in the three-dimensional space where the UAVs can travel, as well as subsets of the points where data is available and where traveling is forbidden.

A swarm of UAVs is deployed to collect data over an area from a set of predefined sensors planted on the ground. The sensors are located on the $XY$ plane of the three-dimensional Euclidean space with $X$, $Y$, and $Z$ axes. There are multiple points with $xyz$ coordinates, of which some are directly above the data sensors or near to them from where the UAVs can collect the transmitted data. Higher $z$ value denotes points with higher altitude. A subset of the points are restricted, which must be avoided during the flight. Designing trajectories of all the UAVs so that the budget and time restrictions are met, they do not collide with one another, avoid restricted areas, and still perform the desired data collection surveillance is a multi-objective problem (NP-hard). We use satisfiability modulo theories (SMT) to solve this problem and generate the trajectories in the 3D space that satisfies all the constraints and requirements.

There are several works in the literature that provides solutions to the problems of path projection and path planning for UAVs. For example, Tisdale et al. proposed a mechanism to perform path planning while minimizing the uncertainty in sensing missions by considering a blend of online sensor models and estimation objectives [6]. Yeung et al. proposed two heuristic-based techniques to find an optimal route of aerial vehicles so that the original target and waypoints are not affected [4, 7]. They also consider the flight maneuvering constraints of the UAVs and keep the deviation from the original route to a minimum while maximizing the number of sensor tasks from the ground. They also consider the time deadlines to cover the taskpoints and maintenance of QoS. Mekala et al. proposed a similar method to generate the flight trajectory, which is a collection of predefined waypoints [8]. They also propose an algorithm to optimize the flight path. Liu et al. studied the age-optimal trajectory planning in UAV-enabled wireless sensor networks [9]. They ensure that the age of the data collected from different sensor nodes is bounded by a threshold. They proposed a dynamic programming method and a genetic algorithm-based method.

Beard et al. designed semi-autonomous UAVs and proposed their graph-based approach to path planning and trajectory generation [10]. Ceccarelli et al. developed a path planning model for micro UAVs to obtain video footage of a set of known targets [11]. In the presence of constant winds, they find the best selection of waypoints for achieving the reconnaissance goals. A pheromone model, where the movement of a group of UAVs is guided by pheromone, was proposed by Kuiper et al. [12]. This model performs well in reconnaissance.

A two-step algorithm was proposed by Bortoff to obtain a path for UAVs traveling through unauthorized sites [13]. The algorithm performed a trade-off between the shortest path for traveling and avoiding radars. A trajectory design with the aid of an iterative algorithm was proposed by Wu et al. where aerial base stations for a wireless communication system on the ground were mounted on the UAVs [14]. Bagherian proposed a genetic and particle swarm algorithm to generate the optimal three-dimensional path planning in an adverse environment [15]. They considered the terrain information and the kinematic constraints of the UAVs.

Tsourdos et al. presented a Kripke model for UAV path planning to cope with uncertainties and decision making involved in the process of collaboratively reaching the goal while covering a certain area of interest, avoiding obstacles [16]. They modeled the collision avoidance with the help of conditions such as minimum separation and non-intersection of paths at equal length. Their model can find the shortest path for each UAV. Ruz et al. proposed a Mixed Integer Linear (MILP)-based solution which modifies the A* algorithm to optimize paths in dynamic environments where pop-ups appear according to a known future probability and need to be avoided [17]. Their ILP model can choose the most suitable trajectory among different alternatives provided fuel and time constraints. The authors also presented a similar approach to trajectory optimization for UAVs in the presence of obstacles, waypoints, and risk zones in another research [18]. Jakaria et al. presented a formal model for verification of a resilient communication in a UAV swarm while maintaining safe flight trajectories for all the UAVs [1, 19]. Jameson proposed a fuel consumption algorithm for UAVs that addresses the additional fuel requirements issue in the Aviation Weather Routing Tool (AWRT) developed by the Army Research Laboratory [20]. They developed a prototype algorithm that computes the ground speeds along the different mission segments, fuel consumed, and fuel remaining while rerouting during adverse weather conditions.

Chen et al. optimized the trajectory of quad-rotor UAVs in collaborative environments [21]. They proposed a hierarchic optimization technique to solve the trajectory optimization problem of quad-rotor UAVs. Sun et al. created a trajectory-tracking controller where the autopilot is involved in the feedback control loop [22]. They proposed a generalized trajectory design model using Lyapunov based backstepping. Fadlullah et al. proposed a simple trajectory control algorithm for UAVs that manages the throughput of UAV-aided networks, where UAVs work as network nodes [23]. Kvarnstrom et al. presented a framework for UAV mission planning that combines ideas from forward-chaining planning and partial order planning [24]. They met the requirements of centralization, abstraction, and distribution of task assignments. Bethke et al. proposed a health management system for UAV teams that perform persistent surveillance [25]. Their methodology for planning missions can anticipate the negative effects of various types of anomalies on future mission states, as well as choosing actions to mitigate the effects.

However, none of these works present the path planning for resilient coverage of data points. We consider the resiliency of the planned trajectories, which ensures a certain coverage of the data sources with a certain frequency of timely visits of multiple UAVs. We solve an NP-hard problem [26], which involves trajectory synthesis while satisfying multi-objective constraints such as budget and maneuvering limitations, and operator requirements, such as resilient coverage.

To model the trajectory planning for the UAVs, we consider a set of predefined points (waypoints) in the three-dimensional space. Each point is considered to have Cartesian ($xyz$) coordinates in the Euclidean space. The UAVs start and end their flights at certain points, which are generally base stations or fueling stations. Between the starting and ending points, the UAVs may visit several other points. All these points constitute the trajectories for all the available UAVs. Our basic intention is to automatically generate these trajectories such that certain constraints and requirement goals are met. Here we formally model the route constraints, as well as the requirements of the users of the implemented tool. We make sure that the points containing the data sensors are covered with certain resiliency specifications. In other words, even if some of the UAVs fail to operate normally to visit certain data points, the points are still covered by others so that the data is collected efficiently.

If $\mathit{M}^{\hat{p},p}_{u}$ denotes whether UAV $u$ moves from $\hat{p}$ to $p$, UAV $u$ has already visited point $\hat{p}$. This is denoted by $\mathit{V}^{\hat{p}}_{u}$. Also it must be possible for the UAVs to travel from point $\hat{p}$ to $p$. In other words, there should be a link between point $\hat{p}$ and point $p$, which is denoted by $\mathit{L}^{\hat{p}}_{p}$.

We define the Boolean variable $\mathit{D}^{\hat{p}}_{p}$ as true only if the distance between point $\hat{p}$ and $p$ ($\mathit{dist}^{\hat{p}}_{p}$) is within a certain threshold, $d_{u,th}$. The threshold is specified by the properties of UAV $u$.

The UAVs have certain maneuvering constraints. We consider the restrictions on the turn angle and the climb angle in three-dimensional space [15]. The turn angle is the angle that a UAV has to turn with respect to the existing direction on the horizontal plane. We first calculate the angle for a UAV for going from $\hat{p}$ to $p$ and the existing angle which the UAV is following to reach $\hat{p}$ from $p^{\prime}$. Then we calculate the deviation which the UAV has to turn. Similarly, we calculate the climb angle on the vertical plane. Fig. 3 shows an example scenario of moving from one point to another in the three-dimensional space. $\alpha$ is the turn angle for moving from point $A$ to $B$, provided the direction of a UAV at $A$ is parallel to the $X$ axis. $\beta$ is the climb angle. Fig. 3 also provides the formulas for calculating the angles based on the horizontal and vertical movements.

The deviation of turn angle to reach $p$ from $\hat{p}$, given a UAV reached $\hat{p}$ from $p^{\prime}$ is represented by $\delta^{p^{\prime},\hat{p},p}_{\alpha}$, while the deviation of climb angle to reach $p$ from $\hat{p}$, given it reached $\hat{p}$ from $p^{\prime}$, is denoted by $\delta^{p^{\prime},\hat{p},p}_{\beta}$. The deviations must be within certain thresholds ($\theta^{t}_{th}$ and $\theta^{c}_{th}$). If this is satisfied, then we can say that there is a link that a UAV can move.

Similarly, if a UAV $u$ moves from $p^{\prime}$ to $\hat{p}$ followed by $p$, then the deviation of the turn angle and climb angle to move from the path $p^{\prime}$ to $\hat{p}$ and the path $\hat{p}$ to $p$ should be within user-defined thresholds.

A UAV visits a particular point from one of its neighboring points. If UAV $u$ has visited the point $p$, that means it has traveled from one of the neighboring points, $\hat{p}$.

The starting point $S$ is the first point on the trajectory of any UAV. If the current point that a UAV $u$ is visiting is the starting point, then it has not come from any other point $\hat{p}$. This can be presented by the following equation:

If a UAV $u$ has reached the destination point $D$, it should not move to anywhere from there. This is represented by the following equation:

A UAV can travel to a certain point only from another point (not from multiple points). If a UAV $u$ has moved from $\hat{p}$ to $p$, then it should not have come from any other point $\hat{p}^{\prime}$.

Similarly, from any particular point, a UAV can only travel to one point and not multiple points. If UAV $u$ goes from $\hat{p}$ to $p$, then it must not have gone to any other point $p^{\prime}$ from $\hat{p}$. This is formally represented as the following:

A UAV $u$ must visit the starting point $S$ and the destination point $D$. This is true for all the collaborating UAVs in the network and is presented by the following:

Some of the points where the UAVs can go are in close proximity to the data collecting sensors. These points need to be visited by the UAVs so that they can collect the data. If $\mathbb{S}$ is the set of all the points that have data-points, then at least a threshold ($\mathit{v}_{th}$) fraction of all the data-points must be visited by the UAVs during their journeys towards the destination.

Some of the points in the three-dimensional space may have to be avoided by the UAVs while making their journeys, for these points may currently reside in restricted zones. If $\mathbb{F}$ denotes the set of all the forbidden points that should be avoided, then no UAV should visit them.

While calculating the fuel consumption, we not only consider the distance but also consider the turn and climb angles for going from a certain point to another. The direction of the turn angle has no effect on fuel consumption, but the direction of the climb angle does affect the amount of fuel consumption. If a UAV is going up against gravity, then it has to burn more fuel. On the other hand, if it is going down, then less fuel is required. We provision a positive climb angle if the UAV is going up with respect to its current direction, while it is counted as negative if it is doing downwards. If $\mathit{d}^{\hat{p}}_{p}$ is the distance between point $\hat{p}$ and $p$, $\alpha^{\hat{p},p}_{u}$ denotes the turn angle of UAV $u$ for going to $p$ from $\hat{p}$, $\beta^{\hat{p},p}_{u}$ is the climb angle to move, and $\mathit{r}_{u}$ is the fuel consumption rate (e.g., mpg) of a UAV $u$, then the required fuel, $\mathit{f}^{\hat{p},p}_{u}$, is calculated as follows:

Here, $k_{1}$ and $k_{2}$ are simple constants that regulate the impact of turn and climb angles, respectively, of the UAV. The fuel usage does not depend on the direction of the turn angle $\alpha^{\hat{p},p}_{u}$, while it directly depends on the direction of the climb angle $\beta^{\hat{p},p}_{u}$. If the UAV is moving to a point located at a lower altitude than the source point, then it is traveling with gravity. As a result, there is less usage of fuel. On the other hand, if it has to travel against gravity, then fuel usage increases.

If $\mathit{c}_{e}$ is the cost of per unit fuel, then the cost, $\mathit{c}^{\hat{p},p}_{u}$, for a UAV for moving from $\hat{p}$ to $p$ is calculated as follows:

The cumulative cost for traveling to point $p$ for UAV $u$ is the cost up to the previous point $\hat{p}$, plus the cost to move from $\hat{p}$ to $p$, $\mathit{c}^{\hat{p},p}_{u}$.

If $S$ is the starting point, the cost at the starting point for any UAV $u$ should be zero.

We assume a constant speed for each UAV while it is making its flight from a point to another particular point. $\mathit{t}^{\hat{p},p}_{u}$ is the time taken by UAV $u$ to move from $\hat{p}$ to $p$ if $\mathit{s}_{u}$ is the speed of the UAV. This is calculated as follows:

$\mathit{T}^{p}_{u}$ is the time taken by UAV $u$ to reach up to $p$ from the starting point. $\mathit{H}^{\hat{p}}_{u}$ is the time of hovering of UAV $u$ at a previous point $\hat{p}$. We consider this hovering time to be either $0$ or $1$, for simplicity. A UAV may or may not hover over a point depending on the requirement of avoiding collision.

If $\mathit{t}_{st}$ is the start time, then it is the time for all the UAVs at the starting point $S$.

The following constraint ensures that no two UAVs visit the same point at the same time. This restriction is required to avoid collision between any two UAVs.

In fact, there should be a threshold time difference between the times of visit of any two UAVs to a certain point. If both UAVs $u$ and $u^{\prime}$ visit the same point $p$, then there must be some time difference between their visits to avoid mid-air collision.

One of the objectives of the trajectory planning model is to keep the budget within a limit. We consider the budget or cost limit for each UAV to be $\mathit{b}_{c}$, while $\mathit{b}_{t}$ is the budgeted time or time boundary within which the flights need to be performed. The cost of the fuel by UAV $u$ should be less than a user-specified budget, $\mathit{b}_{c}$.

Each UAV should reach the destination point from the starting point within a certain time limit, $\mathit{b}_{t}$.

Again, a point cannot be reached by the UAVs by taking more cost than the budget or the time allows. If a UAV visits point $p$, then the cost for reaching up to that point should be less than the budget.

The time taken in reaching any point $p$ should be within the time limit.

Our trajectory modeling considers resiliency with respect to attack/contingency scenarios. The satisfaction of the resiliency specification provides resilient trajectory plans. The resiliency specification is stated such that at least a certain percentage ($r_{th}$%) of the surveillance points are (securely) covered by a set of UAVs (Equation 27), even if a certain number ($r$) of UAVs among them fail to operate or are compromised.

We abstract the resiliency requirement by introducing constraints on surveillance requirements. If $p$ is a data point ($p\in\mathbb{S}$) and it satisfies the $r-$resiliency data collection, then at least $r+1$ number of UAVs must visit (collect data at) this point during their travel to the destination. That is, to provide a single ($r=1$) UAV failure resiliency to a surveillance point, two ($r+1$) UAVs will need to visit the point. If $R^{p}_{c}$ specifies that if point $p$ is under $r-$resilient surveillance, we can formalize the above resiliency requirement as follows:

The resilient trajectory design often needs to satisfy further requirements. A requirement can be data freshness or closeness constraint that ensures that the times at which data is collected by $k+1$ UAVs at a data point should not be apart from one another more than a threshold value (say $t_{\mathit{th}}$), so that the collected data records can be verified for any discrepancy. We call such a data point to be under $k-$resilient surveillance. Such a constraint may differ for different data points based on the data change frequency (which may depend on the data type, location, etc.) and/or the criticality of the data. This constraint ensures that even if $k$ UAVs fail to visit a point $p$, there is at least a UAV $u$, which along with another UAV $u^{\prime}$ will cover this point. This constraint is formalized below:

Here, $\hat{V}^{p}_{u,u^{\prime}}$ specifies that if UAVs $u$ and $u^{\prime}$ visit point $p$, then the visiting times ($u$ earlier than $u^{\prime}$, required for ordering with respect to the visiting time) are no more than the threshold time apart. This is defined as follows:

We need to make sure that at least a certain percentage ($\mathit{k_{th}}$%) of the data points are covered by the UAVs such that the points follow the $k-$resiliency property.

We implement Synth4UAV by encoding the above formal model into SMT formulas [27]. In this encoding purpose, we use Z3, an efficient SMT solver [28]. The solver checks the verification constraints and provides a satisfiable (SAT) result if all the constraints are satisfied. The SAT result provides a SAT instance, which represents the value assignments to the parameters of the model. According to our objective, we are mainly interested in the assignments to the following variables: (i) the decision variable referring to whether a UAV $u$ has visited a particular point $p$, $\mathit{V}^{p}_{u}$ and (ii) the variable denoting whether a UAV $u$ travels from a point $\hat{p}$ to $p$, $\mathit{M}^{\hat{p},p}_{u}$. We can retrieve the trajectories for all the UAVs with the values of these two variables. The assignments of the variables are printed in an output text file. The values of other variables such as $\mathit{T}^{p}_{u}$ can provide information on which point was traveled at what time, while $\mathit{C}^{p}_{u}$ can tell about the fuel cost associated with traveling up to certain points. Appendix B presents an excerpt from the generated z3 code. It shows a few of the expressions that assert the constraints according to our trajectory synthesis model.

Throughout the model of the network synthesis, for simplicity, we have used the sum of Boolean variables several times for formally modeling the constraints. While encoding the summation of Boolean variables, we have created corresponding integer variables ($0$ or $1$) and used their sum for calculation.

The synthesis result represents a comprehensive trajectory plan for the UAVs to perform the intended tasks. There is usually more than one satisfiable model that can satisfy the constraints. These models will provide different costs and times for the overall process, although all of them will be less than the budgeted cost ($\mathit{b}_{c}$) and time ($\mathit{b}_{t}$). We can choose the most cost- and time-efficient trajectory plans among all alternative satisfiable models for the same set of constraints. We use Algorithm 1 which updates the minimum ($\mathit{b}_{c}^{min}$) and maximum ($\mathit{b}_{c}^{max}$) values of the budget, and finds the optimal trajectory plan. Their values are used to update $\mathit{b}_{c}$, which is used to try for a more optimal solution. Initially, $\mathit{b}_{c}^{max}$ is set to the initial user-defined budget ($\mathit{b}_{c}$) and $\mathit{b}_{c}^{min}$ is set to zero. We use a binary search-based method to find the optimal budget.

However, finding the optimal solution using the algorithm usually requires more time than a single satisfiable model. The algorithm requires several invocations of the model solver and often confronts UNSAT results, which usually take a longer time. The time complexity of this algorithm becomes $\mathcal{O}(T\times\log_{2}D)$, where $T$ is the time for one model solution and $D$ is the difference between $\mathit{b}_{c}^{min}$ and $\mathit{b}_{c}^{max}$. The user can control the number of iterations of the model ($\mathit{C}^{max}$) and generate a sub-optimal solution if required.

The synthesized trajectories can be smoothed by applying a 3D Bezier curve interpolation [26]. Careful studies need to be done to make sure that the smooth trajectories remain adequately close to the data sources so that the UAVs and the sources are within range of each other. While this is out of the scope of this research, we leave it for our future works.

UAVs can be used to collect data from sensors deployed in remote points, which is essentially an alternative to the use of UAVs in a surveillance purpose. This is efficient technology when it is not feasible (either technically or economically) to deploy necessary communication infrastructures. If sensors cannot transmit data by themselves to the data center due to the lack of proper infrastructure or energy-saving purposes, UAVs are convenient options to collect data from them. We need to make sure that a certain percentage of the points with sensors are covered by the set of UAVs, even if a certain number of UAVs fail while in flight.

In this case study, we consider 30 waypoints in the three-dimensional coordinate space, of which 15 contain data sources. The coordinates are depicted in the input file presented in Appendix A. For example, (100, 100, 0), (500, 1000, 100), (500, 2000, 100), etc. are some of the points that the UAVs can travel to. In other words, these points may or may not be parts of the trajectories of the UAVs. The indices of the data points are provided from the input file. The start point and end point of the UAV trajectories are specified, which can be the coordinates of base stations. In this case, point 1 is the starting point and point 18 is the ending point for all the UAVs. There are four forbidden points, 6, 14, 19, and 30, which should be avoided by the UAVs while flying from the starting point to the ending point.

We consider 5 UAVs. The average velocity, mileage, and angle with $X$ axis (at the beginning) of the UAVs are also provided. The restrictions of turn and climb angles (in degrees) of the UAVs while moving from one point to another are given in the input file. We consider the deviation of the moving direction of the UAVs. That is, after a UAV reaches a particular point, how much it can deviate from its current trajectory both vertically and horizontally in order to move to the next point.

A Satisfiable Case: The data coverage threshold is selected to be 80% in this case study. That means, at least 80% of the data points must be covered by the UAVs while they are making their journeys. The data freshness threshold specifies the time (in seconds) within which a certain number of UAVs must visit a data point to ensure the freshness of the data. At the beginning of this case study, we consider this to be 20 sec. At this point, we consider the value of $k$ to be 2, while the resilient data coverage is chosen to be 70%. This means there should be at least 70% of the data points, such that they are covered by at least $k=2$ UAVs every 20 seconds. We also need to make sure that at least 70% of the data points are covered by a minimum of $k$ UAVs.

The price of fuel is provided in the input file. The available budget and the total available time within which the UAVs need to finish their task by traveling from the start point to the end point are also provided. For the first run of the tool in this case study, we consider a budget of $6000, and the total allowed time is chosen to be 2000 sec.

Now we try to solve this multi-objective problem in order to find the trajectories of the UAVs. The solution should provide the paths for each of the UAVs that satisfy all the conditions mentioned in Section 4. In this case, the solver gives a SAT result. The result is printed in an output file, which is presented in Appendix A. The output file provides the times at which the UAVs visit each of the points on their trajectories. For example, UAV 1 is at point 1 at the beginning (0 sec), it is at point 2 at 20.79 sec, at point 3 at 41.79 sec, and so on. If a UAV needs to hover over any point to avoid a mid-air crash, the time of hovering is also presented in the output file. The output also provides the trajectories. For example, UAV 1 visits the following points during its journey in sequence: 1, 2, 3, 27, 29, 21, 20, 12, 11, 13, 16, 17, and 18. Similarly, the trajectories of all other UAVs are printed. Fig. 4 presents a top view of the overall trajectory plan for 3 of the 5 UAVs on the $XY$ plane. The data points are colored green, while the forbidden ones are red. All other points are colored blue. All of the UAVs start from waypoint 1 and end their flight at waypoint 18. During their flights, they cover the points that have the data sources with the required resiliency.

An Unsatisfiable Case: For the next run, we increase the value of $k$ to 3. In this scenario, the solver provides an UNSAT result, which means there is no satisfiable solution to the problem, and there cannot be any trajectory for the UAVs unless some conditions are modified. Increasing the budget, number of UAVs, etc. may provide us with a SAT result.

We create synthetic problem sets in a three-dimensional Cartesian space, where there are different points indicating the probable points for UAVs to fly. We randomly specify some data points (50-80% of all the points), which must be covered by the UAVs while performing their flights from a pre-specified starting point to an end point. There are several forbidden points in the space as well, indicating the areas of geographical obstacles or unauthorized zones.

We run the tool that implements the formal model on a Windows 10 machine equipped with an Intel Core i5 processor and 12 GB of memory. We change different parameters of the model from the input file and observe the scalability of the tool, as well as the relationships between the parameters. The evaluation heavily depends on the placement of the available points in the 3D space and the allowed ranges of the UAVs. The maximum allowed turn angle and climb angle are chosen according to the placements of the points.

We present the relationship among different parameters in Fig. 6 and 7. We observe the maximum coverage produced by a SAT result while varying the budget for each UAV in Fig. 5. We present the analysis for two cases: one with 2 UAVs and the other with 4 UAVs while allowing adequate time for coverage. It is obvious that more points can be covered by the UAVs if there is more budget for fuel. If we use more UAVs, then we can cover 100% of the data points with less budget per UAV. For example, if we use 2 UAVs, then we can cover 77% of the data points with a budget of $700 per UAV. On the other hand, using 4 UAVs with the same budget allows us to cover all the data points.

In Fig. 5, we present the coverage time of the data points for the different numbers of UAVs. We show results for the requirement of 40% coverage and 60% coverage. If there are more than 1 UAVs, they reach the destination point at different times, as they may have different speeds and are not allowed to visit the same point at the same time. We take the time required by the last UAV to reach the destination. We can observe that the required time decreases slowly if we have more UAVs to cover our intended percentage of data points.

We present the minimum number of required UAVs to cover different percentages of the data points in Fig. 6. As we increase our requirement of coverage, the minimum number of required UAVs also increases if we keep the budget cost per UAV, and the total budgeted time constant. We show the results for two problem sets: one with 50 points and another with 90 points.

The change in the percentage of coverage with respect to the budgeted time is presented in Fig. 6. This is the maximum total time allowed for all the UAVs to reach the end point of their trajectories. We show two cases for 2 UAVs and 5 UAVs for a total of 100 points and 40 data points. We keep the values of $k$ and $r$ as 2 and 3, respectively. We can observe that as the allowed time increases, more of the data points can be covered. The higher number of UAVs means that more of the data points can be covered. For a budgeted time of 1800 sec, 5 UAVs can visit all the data points and reach the final point on their trajectories.

Next, we present the minimum required budget per UAV while varying the number of data points in Fig. 7. We keep the total number of points, required coverage, the values of $k$ and $r$, etc. unchanged for this evaluation. The minimum required budget is the budget for which the solver returns a SAT answer, which means that trajectories are possible. As expected, the required budget increases with the increment of the number of data points.

The minimum required budget per UAV with the change of the value of $k$ is presented in Fig. 7. We can observe that with the increment of $k$, the required budget increases quickly. As the value of $k$ increases, higher numbers of UAVs need to cover more data points, which results in the complex trajectories of the UAVs. Hence, a bigger budget is required to cover the fuel cost of the UAVs.

We present the scalability of our developed tool based on the formal model discussed earlier in Fig. 8 and 10. Fig. 8 shows the trajectory synthesis time for different sizes of the problem space. We vary the number of points in 3D space and observe the time required to obtain the trajectory plan. We can observe that the required time increases with the increment of the number of points. As we have more points in the problem space, the solver requires to solve more constraints, which leads to the almost linear increment of synthesis time. We can also observe that the UNSAT cases require more synthesis time than the SAT cases.

In Fig. 8, we show the required synthesis time by varying the number of UAVs. We show two cases for two problem sizes: 60 points and 90 points. In these cases, we keep the required percentage of coverage and other parameters constant. We observe that as the number of UAVs increases, the required synthesis time also increases. In the case of 90 points, the number of clauses to satisfy the problem increases quickly with the increment of UAVs. As a result, the time also increases quickly.

We present the trajectory synthesis time by varying the required coverage of the data points in Fig. 9. As the requirement to cover more points grows, the synthesis time also increases. For larger problem sets, the time grows quickly, as more constraints are needed to be satisfied.

The required verification time with respect to the number of data points is observed in Fig. 9. We show the time for two cases: one which is for a total of 50 points, and another is for 80 total points where the UAVs can go. We keep all other parameters constant. For example, the required coverage is kept constant at 80%, the value for $k$ is 2, while $r$ is kept at 3. We can observe that the verification time increases slowly with the increment of the number of data points for a certain problem size (number of total points). This is because, with the increment of data points, the UAVs need to make sure to visit more points, and the solver needs to solve a more strict set of constraints; however, the number of clauses does not increase drastically.

Next, we present the verification time by varying the value of $r$, which is the minimum number of UAVs that need to visit at least a certain percentage of data points. We can observe that the required time increases quickly as $r$ increases. However, the increment rate is less than the case of increasing $k$. This is because the solver needs to verify less strict conditions when $r$ increases than when $k$ increases.

Fig. 10 presents the change in verification time with the change of the value of $k$, which is the minimum number of UAVs visiting a certain percentage of the data points while visiting them at a certain time difference. We keep other parameters, such as the number of UAVs and total points, required coverage, etc., constant and show the results for 30 data points and 50 data points. As the value of $k$ increases, the verification time increases rapidly. With the increment of $k$, the constraints become strict very quickly, as the solver needs to find more complex trajectories for the UAVs so that they can visit more points.

We developed a simulator program to verify the effectiveness of the trajectory generation tool. The simulator is developed in Unity 3D [29]. A user of the simulator can specify the coordinates of the possible waypoints in a three-dimensional space. The simulator reads the number of UAVs and their properties, such as speed, mileage, turning angle constraints, etc., from a user-provided input file. The trajectories are provided based on the output of the trajectory generator. The times of reaching each waypoint on their trajectories, hovering times, etc. are also provided to the simulator. When started, the simulator shows the movement of the UAVs according to its input and proves the effectiveness of the trajectory generator by showing that the UAVs do not collide, but collectively collect the required data and complete the job before the deadline in order to prevent fuel outage, as well as satisfy the resiliency requirements. Appendix C provides further information on this simulator, including a screenshot of the interface.