A Study On The Strategy Synthesis Method Of UAV Swarms Under Temporal Logic Tasks

Unmanned Aerial Vehicle(UAV)swarms are usually composed of a certain number of UAVs with relatively low cost and simple individual intelligence,which generate complex group behaviors through individual behaviors and local interactions.How to automatically generate these action strategies(controlling individual behaviors)and coordination strategies(realizing local interactions)of each UAV to meet the requirements of a given global mission is a key problem in the complex mission planning of UAV swarms.With the theoretical support of formal methods and model checking methods,this paper focuses on the mission planning problem of UAV swarms,studies the method of synthesizing distributed UAV swarm strategies based on task temporal logic,realizes automatic swarm mission planning at the semantic level,and lays a foundation for the low man-machine ratio swarm accusation.The main research contents and contributions of this paper are as follows:(1)Taking UAV swarms as the research objects,the discrete behavior model of a UAV swarm is established by hierarchical abstract methods,and a top-down mission planning method is proposed turning the temporal logical description of missions into the cooperative behaviors among individual UAVs,which lays a foundation for the subsequent research on synthesis method of distributed strategies.Firstly,the behaviors of each UAV are abstracted,and the system attributes are described by atomic propositions,thus the transition system model of each individual UAV is obtained.Secondly,according to the abstract models of the UAV swarm,the finite horizon mission is described by linear temporal logic languages which are defined over the system atomic propositions.Thirdly,a suitable cooperative behavior formulation method is selected to obtain the transition system model of swarm behaviors,and a feasible action plan satisfying the mission description is obtained by the proposed model-checking-based finite horizon planning algorithm.Finally,the feasible action plan is transformed into the action strategies of the swarm according to the cooperative behavior formulation of the system to complete the task execution.(2)Aiming at the disadvantages of swarm synchronously concurrent execution mechanism,such as low task efficiency and large communication demand,a type of cooperative distributed strategy is established based on the transition system model,the mission satisfaction criterion of strategy synthesis problem is proposed,and the corresponding multi-UAV distributed synthesis method of single strategy is designed,realizing the synthesis of cooperative distributed strategy under an asynchronously concurrent execution mechanism.Firstly,a cooperative distributed strategy model under an asynchronously concurrent execution mechanism is established,expanding the strategy form of temporal logical strategy synthesis from a single action sequence to a transition system,achieving local autonomous task coordination through the action handshake between UAVs.Secondly,the synthesis problem of UAV swarm cooperative distributed strategies under an asynchronously concurrent execution mechanism is formulated,and the mission satisfaction criterion of both equivalent global strategy and distributed strategies are derived respectively.Thirdly,a synthesis method of multi-UAV distributed single strategy is proposed,of which the global permissive plan set satisfying the mission description is obtained from the product automaton,and among the set,a permissive plan satisfying trace closure criterion was found and mapped to the distributed single strategy.Finally,the simulation experiments demonstrate that the proposed method can realize the synthesis of distributed strategy under an asynchronously concurrent execution mechanism,and the resulted strategies outperform the traditional strategies under the same condition,which short the mission execution time by an average of 42% and reduce communications required for task coordination by an average of 72%.(3)In view of the limitations and inflexibility in the synthesis of single strategy,by introducing the decomposability of concurrent systems,the satisfiability criterion for the synthesis of distributed multiple strategy is given and proved,and a heuristic synthesis method of multi-UAV distributed multiple strategy is proposed by using the monotonicity rule of decomposability criterion,realizing the synthesis of distributed multiple strategy for UAV swarms.Firstly,by introducing the decomposability of concurrent systems,the satisfiability criterion for the synthesis of distributed multiple strategy is proposed.Secondly,based on the decomposability theorem,the upper bound of the decomposability of global strategies is found,and a synthesis method of distributed multiple strategy is proposed,which finds the decomposable global strategies by tree search and projects them to distributed multiple strategies.Thirdly,by the monotonicity rule of the decomposability criterion,a branch clipping operation is designed and the heuristic information of node expansion is given in the tree search process,which speeds up the searching for decomposable global strategy.Finally,simulation experiments under different mission complexity and scale of cooperative UAVs are carried out to verify the applicability of the proposed method and the correctness of the results.The proposed branch clipping and heuristic search method can significantly improve the speed and the scalability of decomposable global strategy search.(4)To solve the problem of dimension explosion in strategy synthesis of UAV swarms,a discrete sampling strategy was introduced,and a biased-sampling-based global strategy synthesis method is proposed,which is applied to the synthesis method of the distributed single strategies and multiple strategies,respectively,realizing the synthesis of distributed strategies for UAV swarms with a certain scale.Firstly,based on the advantages of the discrete sampling methods in dealing with large-scale problems,according to the permissive global behavior characteristics under an asynchronously concurrent execution mechanism,a sampling-based global strategy synthesis method is proposed.Secondly,by analyzing the mission progress information in the sampling process,the sampling bias strategy is designed to improve the construction speed of the permissive action plans.Thirdly,this method is applied to the synthesis method of the distributed single strategies and multiple strategies,respectively,to realize the synthesis of distributed strategy for UAV swarms.Finally,the simulation results show that the proposed method is capable of the strategy synthesis for UAV swarms with size of 10-20 under complex missions,isomorphism verification and model check prove the correctness.