Counting Time Temporal Logic for Multi-Robot Path Planning in Finite Horizons

Lv, Peng ; Li, Shaoyuan ; Mahulea, Cristian (Universidad de Zaragoza) ; Denis, Bruno ; Faraut, Gregory ; Yin, Xiang

Resumen: In this paper, we consider multi-robot path planning problems for high-level tasks with a finite horizon. In many situations, there is a need to count how many times a sub-task is satisfied in order to achieve the overall task. However, existing temporal logic languages, such as linear temporal logic, is not efficient in describing such requirements. To address this issue, we propose a new temporal logic language called Counting Time Temporal Logic (CTTL) that extends linear temporal logic by explicitly counting the number of times that some tasks are satisfied. To solve the CTTL path planning problem, we propose an efficient integer linear programming-based method to encode task satisfaction. We show that our approach is both sound and complete, while achieving higher efficiency than direct encodings of such requirements. Moreover, we study several variants of the problem. To validate our results, we present several numerical experiments to show the scalability of the proposed approach and a simulation case study of a team of autonomous robots to illustrate the feasibility of the synthesis procedure. Finally, to evaluate the real-world feasibility of our method, we conduct a hardware experiment with two Turtlebot3-Burger mobile robots.

Idioma: Inglés

DOI: 10.1109/TASE.2025.3636053

Año: 2025

Publicado en: IEEE Transactions on Automation Science and Engineering (2025), [11 pp.]
ISSN: 1545-5955

Financiación: info:eu-repo/grantAgreement/ES/DGA/T64-23R
Financiación: info:eu-repo/grantAgreement/ES/MCIU/PID2024-159284NB-I00

Tipo y forma: Artículo (PostPrint)

Área (Departamento): Área Ingen.Sistemas y Automát. (Dpto. Informát.Ingenie.Sistms.)