Research Analyzer
← Back ICRA 2026

Online Modifications of High-Level Swarm Behaviors

Bo-Ruei Huang, Hadas Kress-Gazit

PDF

AI summary

Key figure (auto-extracted from paper)
We introduce a localized patching method that enables real-time modification of high-level swarm specifications while preserving formal correctness guarantees.
Swarm robotics online specification modification formal methods constraint programming temporal logic swarm control synthesis

Problem

Current swarm control synthesis relies on fixed, a priori specifications and cannot adapt to mid-execution changes like unexpected obstacles or shifting mission goals. This work addresses how to modify swarm behavior specifications during execution while maintaining formal safety and liveness guarantees.

Approach

The authors define three types of online specification modifications and synthesize localized control patches by combining symbolic GR(1) strategy generation with constraint programming to replace violating sub-sequences in the original plan.

Key results

  • Formal definition of three online specification modification types
  • Localized patching algorithm that repairs violations without full re-synthesis
  • Constraint programming integration ensuring valid robot assignments and safe intermediate states
  • Simulation validation of dynamic swarm plan adaptation

Why it matters

Enables robust, real-time adaptation of swarm robotics systems to dynamic environments and changing mission requirements while preserving formal correctness guarantees.

Abstract

Recent work has demonstrated how one can write high-level specifications for swarm behaviors and automatically create controllers for the individual robots to achieve the overall swarm task. In this letter, we address the question of how to modify, during execution, the desired behavior while maintaining guarantees on the behavior, if possible; we define three types of modification: changing the maximum number of robots in a region of the workspace, changing the connectivity of the workspace, and redistributing robots. During execution, if the specification is modified, we update the controller by creating local patches. Given the starting and ending state of the patch, we jointly use a symbolic synthesis tool and a constraint programming solver to synthesize robot control. We demonstrate our approach in simulation.

Index terms

Swarm Robotics Formal Methods in Robotics and Automation

Related papers