# Automated Formation Control Synthesis from Temporal Logic Specifications

arXiv: https://arxiv.org/abs/2304.00275 · HTML: https://mlsanity.com/paper/2304.00275/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 1 Apr 2023.

## Built on by (most cited first, 1 of 1)

- [VernaCopter: Disambiguated Natural-Language-Driven Robot via Formal Specifications](https://mlsanity.com/paper/2409.09536/) (2024)

## Abstract (arXiv)

In many practical scenarios, multi-robot systems are envisioned to support humans in executing complicated tasks within structured environments, such as search-and-rescue tasks. We propose a framework for a multi-robot swarm to fulfill complex tasks represented by temporal logic specifications. Given temporal logic specifications on the swarm formation and navigation, we develop a controller with runtime safety and convergence guarantees that drive the swarm to formally satisfy the specification. In addition, the synthesized controller will autonomously switch formations as necessary and react to uncontrollable events from the environment. The efficacy of the proposed framework is validated with a simulation study on the navigation of multiple quadrotor robots.