Geometric Reachability for Attitude Control Systems via Contraction Theory

TL;DR

The paper tackles safety verification for attitude control by developing a coordinate-free reachability framework on the product manifold $SO(3)\times \mathbb{R}^3$. It introduces a parametric family of left-invariant Riemannian metrics $\mathbb{G}=\mathbb{G}_{Q}\times\mathbb{G}_{P}$ and derives a contraction-based bound $d(\psi(q_1,t),\psi(q_2,t))\le e^{ct}d(q_1,q_2)$ via the matrix inequality $\hat{\omega}Q - Q\hat{\omega} - 2cQQ + A^{\top}PQ + PAB^{\top}P + PB - 2cP \preceq 0$. Using this, it proposes a simulation-based ConReach algorithm that partitions the initial set, runs nominal trajectories, and solves SDP subproblems to minimize metric-ball volumes while ensuring inclusions; the reachable set is over-approximated by metric balls $\mathcal{B}_{Q_{i+1}\times P_{i+1}}((R_{i+1},\omega_{i+1}),r_{i+1})$. It also provides equivalent representations of metric balls on $SO(3)$ via reduced geodesic dynamics and an exp atlas to enable Euclidean visualization and analysis. Numerical experiments validate the method's ability to produce tight over-approximations and demonstrate practical computation on standard hardware. The work paves the way for safe-control synthesis and extended coupling of attitude and position dynamics using geometric reachability on manifolds.

Abstract

In this paper, we present a geometric framework for the reachability analysis of attitude control systems. We model the attitude dynamics on the product manifold $\mathrm{SO}(3) \times \mathbb{R}^3$ and introduce a novel parametrized family of Riemannian metrics on this space. Using contraction theory on manifolds, we establish reliable upper bounds on the Riemannian distance between nearby trajectories of the attitude control systems. By combining these trajectory bounds with numerical simulations, we provide a simulation-based algorithm to over-approximate the reachable sets of attitude systems. We show that the search for optimal metrics for distance bounds can be efficiently performed using semidefinite programming. Additionally, we introduce a practical and effective representation of these over-approximations on manifolds, enabling their integration with existing Euclidean tools and software. Numerical experiments validate the effectiveness of the proposed approach.

Figures (1)

• Figure 1: Over-approximated reachable sets for attitude control systems with the initial set $\mathcal{I}$ over the time interval $[0,4]$. (a) Fast over-approximation of the reachable set for angular velocity $\boldsymbol{\omega} \in \mathbb{R}^{3}$ (blue region) using the Euclidean reachability algorithm LDF2. The dashed boxes represent over-approximated reachable tubes during $[t_{0}=0, t_{1}=0.1]$ and $[t_{6}=0.6, t_{7}=0.7]$, which serve as search regions in our ConReach algorithm at Step 0 and Step 6, respectively. (b) Over-approximation of reachable set of attitudes (blue region) computed using our ConReach algorithm and represented in the exp chart $(\mathcal{X}_{0}, \Psi_{0})$.