# Synthesising Robust Controllers for Robot Collectives with Recurrent Tasks: A Case Study

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 4 of its 17 references that are in the map.
- First posted on arXiv 21 Nov 2024.

## Builds on (most cited first, 4 of 4)

- [Verified Synthesis of Optimal Safety Controllers for Human-Robot Collaboration](https://mlsanity.com/paper/2106.06604/) (2021)
- [An Abstraction-based Method to Check Multi-Agent Deep Reinforcement-Learning Behaviors](https://mlsanity.com/paper/2102.01434/) (2021)
- [A Manifesto for Applicable Formal Methods](https://mlsanity.com/paper/2112.12758/) (2021)
- [Scheduling of Missions with Constrained Tasks for Heterogeneous Robot Systems](https://mlsanity.com/paper/2209.14040/) (2022)

## Abstract (arXiv)

When designing correct-by-construction controllers for autonomous collectives, three key challenges are the task specification, the modelling, and its use at practical scale. In this paper, we focus on a simple yet useful abstraction for high-level controller synthesis for robot collectives with optimisation goals (e.g., maximum cleanliness, minimum energy consumption) and recurrence (e.g., re-establish contamination and charge thresholds) and safety (e.g., avoid full discharge, mutually exclusive room occupation) constraints. Due to technical limitations (related to scalability and using constraints in the synthesis), we simplify our graph-based setting from a stochastic two-player game into a single-player game on a partially observable Markov decision process (POMDP). Robustness against environmental uncertainty is encoded via partial observability. Linear-time correctness properties are verified separately after synthesising the POMDP strategy. We contribute at-scale guidance on POMDP modelling and controller synthesis for tasked robot collectives exemplified by the scenario of battery-driven robots responsible for cleaning public buildings with utilisation constraints.
