Path planning for robotic teams based on LTL specifications and Petri net models

This research proposes an automatic strategy for planning a team of identical robots evolving in a known environment. The robots should satisfy a global task for the whole team, given in terms of a Linear Temporal Logic (LTL) formula over predefined regions of interest. A Robot Motion Petri Net (RMPN) system is used for modeling the evolution of the robotic team in the environment, bringing the advantage of a fixed topology versus the number of robots, with respect to methods based on synchronous automaton products. The algorithmic method iterates the selection of an accepted run that satisfies the specification and the search for RMPN sequences of reachable markings that can produce desired observations. A Buchi automaton witnesses the advancement towards formula fulfillment, and at the core of our methods are three Mixed Integer Linear Programming (MILP) formulations that yield firing sequences and markings of RMPN model. The cost functions of these formulations reduce the number of robot synchronizations and induce collision avoidance. Simulation examples support the computational feasibility of the proposed method.