用于有限视界下多机器人路径规划的计数时间时序逻辑

《IEEE Transactions on Automation Science and Engineering》：Counting Time Temporal Logic for Multi-Robot Path Planning in Finite Horizons

多机器人路径规划中提出CTTL时态逻辑，通过整数线性规划编码任务计数需求，验证方法高效性与机器人实验可行性。

　　

摘要：

在本文中，我们研究了具有有限时间范围的高层次任务的多机器人路径规划问题。在许多情况下，需要统计子任务被满足的次数以达到整体任务的目标。然而，现有的时态逻辑语言（如线性时态逻辑）在描述这类需求时效率较低。为了解决这个问题，我们提出了一种新的时态逻辑语言——计数时态逻辑（Counting Time Temporal Logic，简称CTTL），它通过明确计算某些任务被满足的次数来扩展线性时态逻辑的功能。为了解决CTTL路径规划问题，我们提出了一种基于整数线性规划的高效方法来编码任务满足情况。我们证明了该方法在逻辑完备性和有效性方面都是可靠的，并且比直接编码这类需求的方法具有更高的效率。此外，我们还研究了该问题的几种变体。为了验证我们的结果，我们通过多个数值实验展示了所提出方法的可扩展性，并通过一个自主机器人团队的仿真案例研究来说明合成过程的可行性。最后，为了评估我们方法在现实世界中的可行性，我们使用两个Turtlebot3-Burger移动机器人进行了硬件实验。