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.

翻译：这项工作考虑了在已知环境中演进的相同机器人团队的路径规划问题。 机器人应该满足全球规格, 以线性时空逻辑( LTL) 公式为一组感兴趣的区域提供。 推荐的方法利用了机器人团队的Petri 网模型的优势, 以及 B\\\ uchi 自动模型的优势。 本文中的方法包括将两个模型合并为一个模型, 标记为混集的 Petri 网, 并用它为移动机器人寻找一系列动作动作, 提供不碰撞的轨迹来达到规格。 一组混合整形线性编程( MILP) 问题的解决方案是算法的完整性, 这意味着当存在一个解决方案时, 这代表了我们先前在 [ 1] 中的工作的关键差异。 模拟显示了当前和以往方法之间的对比结果, 重点是计算的复杂性 。