On Multi-Robot Path Planning Based on Petri Net Models and LTL specifications

TL;DR

This paper presents a complete method for multi-robot path planning that ensures robots satisfy complex temporal specifications using Petri nets and automata, solved via MILP, with improved computational efficiency.

Contribution

It introduces a novel combined Petri net model for multi-robot planning that guarantees completeness and reduces computational complexity compared to previous methods.

Findings

The proposed approach guarantees finding a solution if one exists.

Simulation results show improved computational efficiency over previous methods.

The method effectively generates collision-free trajectories satisfying LTL specifications.

Abstract

This work considers the path planning problem for a team of identical robots evolving in a known environment. The robots should satisfy a global specification given as a Linear Temporal Logic (LTL) formula over a set of regions of interest. The proposed method exploits the advantages of Petri net models for the team of robots and B\"uchi automata modeling the specification. The approach in this paper consists in combining the two models into one, denoted Composed Petri net and use it to find a sequence of action movements for the mobile robots, providing collision free trajectories to fulfill the specification. The solution results from a set of Mixed Integer Linear Programming (MILP) problems. The main advantage of the proposed solution is the completeness of the algorithm, meaning that a solution is found when exists, this representing the key difference with our previous work in [1]. The simulations illustrate comparison results between current and previous approaches, focusing on the computational complexity.