This paper presents a method for decomposing Linear Temporal Logic (LTL) specifications into independent parts based on structures recognized in their corresponding Büchi automata representations. The goal is to obtain a decomposition that allows the execution of the global mission by identifying and formalizing segments that can be executed concurrently by a team of mobile robots. We introduce formal concurrency characterization for two and three tasks, and provide a structured framework for recognizing these patterns within the automaton. The method algorithmically analyses an accepted run of the trimmed Büchi automaton, partitions it into containers of sequential and concurrent tasks, and incrementally extends this concurrency while reducing the number of synchronization points. Although the current formal framework supports up to three concurrent tasks, it may represent a step towards generalization.

This paper proposes an extension of an algorithm that decomposes a high-level specification into sub-formulas that are called tasks. The extension consists in enabling repetitive (non-terminating) behaviors expressed in Linear Temporal Logic (LTL), rather than only terminating ones, as the previous version of our method allowed. The LTL specification has the meaning of a global mission that must be accomplished by a team of mobile agents, while the decomposition ensures that the tasks can be executed independently by the robots, thus avoiding communications or synchronizations. An example is illustrating the presented work, while future research will be conducted towards inclusion of negations in formulas.

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.