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

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 <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">count how many times</i> 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 <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">Counting Time Temporal Logic</i> (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.