Optimal task allocation for distributed co-safe LTL specifications

Abstract

We consider the problem of obtaining independent trajectories for robots from a team, such that their movement satisfies a global co-safe Linear Temporal Logic (LTL) mission over some regions of interest from the environment. For this, the environment is abstracted into a discrete event system using an underlying partition and an available method is used for decomposing the LTL formula into more parts that can be independently satisfied by a robot. Then, we translate these parts into a conjunction of Boolean formulas and use another approach for planning a team based on Boolean specifications and Petri net models. The proposed combination among the two methods yields independent robot trajectories that are optimal with respect to the number of traversed cells from the partition. The advantages are also illustrated through simulation examples.