LTL Task Decomposition for 3D High-Level Path Planning

Abstract

The paper addresses the problem of planning the motion of a team of drones such that a co-safe Linear Temporal Logic (LTL) formula is accomplished. The high-level formula can include visits or avoidance of some known regions of interest from the 3D environment. The team mission is decomposed into independent tasks that can be accomplished by each drone, while the workspace is abstracted by a cell decomposition algorithm based on rectangular cuboid partitions. An optimization problem for the task assignment yields the tasks to be fulfilled by each drone, and independent trajectories are automatically obtained. The contributions include an algorithm for decomposing the co-safe LTL specification into independent tasks, a recursive cell decomposition method for 3D environments with regions of interest rather than obstacles, and an overall planning procedure that returns a trajectory for each drone. The independent tasks imply that the drones fulfilling them do not need to constantly communicate, the flight of each agent relying on positioning sensors for following the predefined path. Simulations and comparative studies based on different partitions and scenarios are included.