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.

翻译：在本文中，我们提出了一种新颖的框架，采用形式化方法来合成多机器人群组中具有自动形成的导航控制策略。问题的主要目标是在通过一系列航点时将机器人群组导航到目标位置。机器人群组的形成应根据相应的航点周围的地形限制而改变。此外，机器人的运动应始终满足某些运行时安全要求，例如避免与其他机器人和障碍物碰撞。我们使用时间逻辑（TL）规范指定所需的航点和机器人群组形成。然后，我们将航点和形式的转换形式化为确定性有限转换系统（DFTS），并根据TL规范合成控制策略。同时，使用控制屏障函数对运行时安全要求进行编码，而固定时间控制李亚普诺夫函数确保固定时间收敛。解决了一个二次规划（QP）问题，以细化DFTS控制策略，生成机器人的控制输入，从而同时满足TL规范和运行时安全要求。这项工作为具有复杂任务规范的多机器人系统提供了一种新颖的解决方案。所提出的框架的有效性通过仿真研究得到验证。