In this paper, we propose a novel framework using formal methods to synthesize a navigation control strategy for a multi-robot swarm system with automated formation. The main objective of the problem is to navigate the robot swarm toward a goal position while passing a series of waypoints. The formation of the robot swarm should be changed according to the terrain restrictions around the corresponding waypoint. Also, the motion of the robots should always satisfy certain runtime safety requirements, such as avoiding collision with other robots and obstacles. We prescribe the desired waypoints and formation for the robot swarm using a temporal logic (TL) specification. Then, we formulate the transition of the waypoints and the formation as a deterministic finite transition system (DFTS) and synthesize a control strategy subject to the TL specification. Meanwhile, the runtime safety requirements are encoded using control barrier functions, and fixed-time control Lyapunov functions ensure fixed-time convergence. A quadratic program (QP) problem is solved to refine the DFTS control strategy to generate the control inputs for the robots, such that both TL specifications and runtime safety requirements are satisfied simultaneously. This work enlights a novel solution for multi-robot systems with complicated task specifications. The efficacy of the proposed framework is validated with a simulation study.

翻译：本文提出一种新颖的框架，利用形式化方法为具备自动编队功能的多机器人集群系统综合导航控制策略。该问题的主要目标是引导机器人集群通过一系列航点到达目标位置，同时根据对应航点周围的地形限制调整集群编队形态。此外，机器人运动必须始终满足运行时安全约束（如避免与其他机器人和障碍物碰撞）。我们采用时序逻辑规范描述期望的航点序列与编队形态，将航点与编队转移过程建模为确定性有限转移系统，并综合满足时序逻辑规范的控制策略。同时，利用控制屏障函数编码运行时安全约束，通过固定时间控制李雅普诺夫函数确保固定时间收敛。通过求解二次规划问题优化确定性有限转移系统控制策略以生成机器人控制输入，使时序逻辑规范与运行时安全约束同时得到满足。该工作为具有复杂任务规范的多机器人系统提供了新颖的解决方案，并通过仿真研究验证了所提框架的有效性。