# UAV Cluster Behavior Modeling Based on Spatial-Temporal Hybrid Petri Net
## 3 UAV Cluster Modeling and Formal Verification
### Modeling Instance  
We used a heterogeneous UAV cluster combat scenario to verify the modeling method. Suppose that the red side is a heterogeneous UAV cluster system consisting of two reconnaissance UAVS, three attack UAVs and a control center, and the blue side consists of two UAVs. The red side conducts reconnaissance and attack missions against the blue side. The scenario of the attack mission is complex. There will be many situations in the actual attack mission such as weather, equipment, and surrounding environment. This paper assumes that all external factors are ideal, and the whole process of the attack mission can be regarded as a sequence of events. We will show a modeling instance for an attack mission of a heterogeneous UAV cluster. The attack mission has the following primitive behaviors:* Search target The UAV cluster searches the blue side through the event of reconnaissance carried out by reconnaissance UAVs. * Assign tasks The control center assigns specific tasks to each UAV. * Approach target With the assistance of reconnaissance UAVs, attack UAVs approach the target. * Target acquired With the assistance of reconnaissance UAVs, the targets are acquired by attack UAVs. * Mission complete UAV cluster complete attack mission. The heterogeneous UAV cluster system includes reconnaissance UAVs, attack UAVs, and reconnaissance/attack UAVs as well as sensors. The formal expression is shown in Formulas (9) and (10):  
\[U=(U_{id},\ U_{P}(D,K,M,R),\ U_{b}(S,A),U_{st}(Z,T)) \tag{9}\]  
\[S_{n}=(S_{id},S_{P}(u,v,w,p,q,r,a),S_{b}(C_{1},C_{2}),S_{st}(Z,T)) \tag{10}\]  
where \(D\) is the dynamic attributes; \(K\) is the kinematic attributes; \(S\) is the reconnaissance behavior; \(A\) is the attack behavior; \(Z\) is the coordinate of UAV; \(T\) is a point or an interval; \(C_{1}\) indicates the change of sensor data; \(C_{2}\) indicates that the sensor data remain unchanged. * Acceleration sensor \[\left(S_{ai},S,S_{ap}(v,u,w,a),S_{ab}(C_{1},C_{2}),S_{ast}(Z,T),STHP\right)\] (11)
* Gyroscope sensor \[\left(S_{gi},S,S_{gp}(p,q,r),S_{gb}(C_{1},C_{2}),S_{gst}(Z,T),STHP\right)\] (12)
* Reconnaissance UAV \[\left(U_{si},U,U_{P}\left(p_{f},p_{h}\right),U_{b}(S),U_{st}(Z,T)\right)\] (13)
* Attack UAV \[\left(U_{ki},U,U_{P}(p_{d},p_{P}),U_{b}(A),U_{st}(Z,T)\right)\] (14)  
where \(STHP\) represents the spatial-temporal hybrid Petri net; \(p_{f}\) and \(p_{h}\) represent linear flight and steady hover; \(p_{d}\) and \(p_{P}\) are the accelerated dive and sharp rise turn; \(Z\) represents the area of reconnaissance/attack or the area where the decision center is located. Modeling high level behaviors for a UAV cluster executing complex attack mission in dynamic, partially observable, and environments requires a powerful modeling method. The attack mission of a heterogeneous UAV cluster can be described as a Petri net, as shown in Figure 1. The process of the attack mission begins with a reconnaissance event. When the targets are detected, the control center will carry out task assignment. Then, with the assistance of reconnaissance UAVs, the attack UAVs approach the targets. When the targets are acquired by the attack UAVs, an attack action will be carried out. Finally, the process of the attack mission is ended whether the targets are destroyed or not. The formal model of the attack mission of a heterogeneous UAV cluster can be expressed as Formula (14). \(P=\left\{p_{1},p_{2},\cdots,p_{8}\right\}\), places \(p_{i}\) represent the execution phases of the attack mission. \(T=\left\{t_{r},t_{r},t_{r},\cdots,t_{s},t_{f}\right\}\), transitions \(t\) represent events (i.e., \(t_{r}\) is the reconnaissance event; \(t_{e}\) is the mission complete event. Here, we introduced a labeling mechanism for transitions in the Petri net to specify external events. All transitions may be labeled with conditions that must be verified in order to be fired when enabled. A condition \(e\) on the transition \(t\) is denoted with \(t.e\).