Software Tool for Distribution of Linear Temporal Logic Specifications

Abstract

This work presents the implementation of a software tool that ensures the execution of a global Linear Temporal Logic (LTL) specification for a team of mobile agents that are evolving in a static and known environment cluttered with regions of interest. The software is build on formalisms that extend our previous work, with the main contribution of handling strictly more expressive missions that also allow negations (or temporal avoidance) of some regions of interest. An algorithm is provided for decomposing the global LTL mission into independent robots’ tasks, together with a flow diagram of the entire method that solves the path planning problem. Simulations and comparative results are discussed for a case study, in order to support the usefulness of the software tool.