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.

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