# UAV Cluster Behavior Modeling Based on Spatial-Temporal Hybrid Petri Net
## 3 UAV Cluster Modeling and Formal Verification
### Modeling Instance
\begin{table}
\begin{tabular}{c c} \hline \hline
**Transition** & **Explanation** \\ \hline \(P_{1}\) & Initial state of attack mission \\ \(P_{2}\) & Phase of reconnaissance of attack mission \\ \(P_{3}\) & Phase of task assignment \\ \(P_{4}\) & Phase of approaching target (attack UAVs) \\ \(P_{5}\) & Phase of assistance of approaching target (reconnaissance UAVs) \\ \(P_{6}\) & Phase of acquiring targets \\ \(P_{7}\) & Phase of attacking targets \\ \(P_{8}\) & Attack mission complete \\ \(T_{r}\) & Event of reconnaissance \\ \(T_{r\_t}\) & Event of targets detected \\ \(T_{r\_f}\) & Event of targets are not detected \\ \(T_{ss}\) & Event of task assignment \\ \(T_{ap}\) & Event of keep effective firing range (attack UAVs) \\ \(T_{ap}\) & Event of keep effective firing range (reconnaissance UAVs) \\ \(T_{l\_t}\) & Event of targets acquired \\ \(T_{l\_f}\) & Event of losing targets \\ \(T_{s}\) & Event of targets are destroyed \\ \(T_{f}\) & Event of failure of the attack mission \\ \hline \hline \end{tabular}
\end{table} 
Table 1: The explanation of transitions. some targets are left undestroyed. \(T_{5}\) shows that all two targets were destroyed. The initial marking \(M_{0}=\{3,0,0,0,0,0,0,0,0\}\). Figure 2b shows the model of the coordinated reconnaissance process, \(P_{0}\) shows that the reconnaissance UAVs arrive at the specified area; \(P_{ij}\) represents the state of each UAV, \(1\leq i\leq 2,i\in\) N; \(i\) is used to identify different reconnaissance UAVs; \(j\) is used to represent the different states of reconnaissance task, \(1\ \leq\ j\ \leq\ 7\), \(j\in N\). When \(j=1\), reconnaissance UAVs carry out the reconnaissance task, \(j\in\{2,3,4,5\}\) represents the exchange of information between two reconnaissance UAVs, \(j=6\) determines whether the current reconnaissance information is fully obtained, \(j=7\) shows that the reconnaissance task is complete. The initial marking is \(M_{0}=\{2,0,0,0,0,0,0,0,0,0,0,0,0,0\}\). We used spatial-temporal hybrid Petri nets to simulate the behavior of the individual UAV, as shown in Figure 3.  
The UAV completes an attack mission through the following procedures. * Reaches the specified position through horizontal acceleration maneuver;
* Performs a dive maneuver to reach directly above the first target;
* Performs a horizontal deceleration maneuver to approach the target;
* Performs a Chandelle maneuver;
* Performs a zooming maneuver and finishes the attack mission. Figure 2: The Petri net of the attack/reconnaissance process. (**a**) Petri net of the coordinated attack process. (**b**) Petri net of the coordinated reconnaissance process. The places and transitions in the spatial-temporal hybrid Petri net include discrete and continuous attributes. Place \(P_{i}\) represents the state of different maneuvers of the attack UAVs. Transition \(T_{i}\) shows when the maneuver changes. \(M_{0}=\{(1,u_{0_{i}}),(0,u_{1}),\cdots,(0,u_{6})\}\), \(1\) represents the token in \(P_{1}\); \(u_{i}\) represents the continuous attributes of UAV shown in Formula (1). \(P_{1}\) represents the level accelerating, where the speed of the UAV rises from 200 m/s to 300 m/s, and key attributes such as velocity and tangential overload are changed. The velocity \(v_{1}\) of the UAV at time \(t_{1}\) in \(T_{8}\) represents the differential equation for the change in velocity, as defined in Equation (16). \[dV=\frac{F_{x}\cos\alpha\cos\beta+F_{y}\sin\beta+F_{z}\sin\alpha\sin\beta}{m} \tag{15}\]  
\(T_{1}\) indicates that the horizontal acceleration maneuver has been completed. \(P_{2}\) represents the dive maneuver. The differential equation for the change in the angle of attack is as defined in Equation (17). \[da=\frac{F_{z}\cos\alpha-F_{x}\sin\alpha}{mV\cos\beta}+q-\tan\beta(p\cos \alpha+r\sin\alpha) \tag{16}\]  
\(T_{2}\) indicates that the dive maneuver has been completed. \(P_{3}\) represents the horizontal deceleration maneuver, which is like the horizontal acceleration maneuver. \(T_{3}\) indicates that the horizontal deceleration maneuver has been completed.