Controller synthesis of multi-UAV systems for concurrent satisfaction of temporal logic tasks through parallel decomposition

Synthesis of local control strategies for multiple Unmanned Aerial Vehicles (multi-UAV) systems that enable concurrent satisfaction of complex tasks has attracted extensive attention. However, the formal guarantee that the composed behavior satisfies the specified global tasks still remains unclear. In this paper, a top-down local controller synthesis method for multi-UAV systems to concurrently satisfy team-wise tasks specified as linear temporal logic formulas is proposed. First, the local event set for each UAV is generated according to its capability and the temporal constraints between the events. Then, based on these local event sets, the global task specification is decomposed into local task specifications for each UAV with the minimal completion time through natural projection. It is formally proven that the resulting global behavior along with the local synchronizations satisfies the specified global tasks. Finally, the local controllers for UAVs are synthesized in a distributed way according to their local task specifications, which are reactive to environmental changes and mechanical failures of the UAVs during task execution, without the need for task replanning. Extensive hardware-in-the-loop simulations and flight experiments are performed to evaluate the proposed method and show its advantages against several established baselines.