Symmetry-based Abstraction Algorithm for Accelerating Symbolic Control Synthesis

TL;DR

The paper addresses scalable symbolic control synthesis for reach-avoid specifications in systems with dynamical symmetries. It introduces a two-layer abstraction, combining a grid-based abstraction (GA) with a symmetry-based abstraction (SA) that groups concrete states by symmetric relative positions and guides control exploration, leveraging moving frames to transform and reuse precomputed reachable sets. The authors formalize an equivariant framework with a Lie group $\mathcal{G}$, use cross-sections and a moving frame to decompose reachability computations, and prove that the SA approach preserves the guarantees of GA. Empirical results on a 3D ship model with $SE(2)$ symmetry show substantial computational speedups, demonstrating the practical impact for reach-avoid controller synthesis in symmetric environments.

Abstract

We propose an efficient symbolic control synthesis algorithm for equivariant continuous-time dynamical systems to satisfy reach-avoid specifications. The algorithm exploits dynamical symmetries to construct lean abstractions to avoid redundant computations during synthesis. Our proposed algorithm adds another layer of abstraction over the common grid-based discrete abstraction before solving the synthesis problem. It combines each set of grid cells that are at a similar relative position from the targets and nearby obstacles, defined by the symmetries, into a single abstract state. It uses this layer of abstraction to guide the order by which actions are explored during synthesis over the grid-based abstraction. We demonstrate the potential of our algorithm by synthesizing a reach-avoid controller for a 3-dimensional ship model with translation and rotation symmetries in the special Euclidean group SE(2).