Hamilton-Jacobi Reachability for Hybrid Systems: Unified Goal-Driven Control with Safety Guarantees

Summary

Abstract Summary

Hybrid dynamical systems provide a powerful modeling framework for robotic systems, particularly in contact-rich environments. However, ensuring safety and performance in such systems remains challenging due to the intricate coupling between continuous dynamics and discrete mode transitions. In this work, we extend classical Hamilton-Jacobi (HJ) reachability analysis, a formal verification method for continuous-time nonlinear systems, to hybrid dynamical systems. Our framework characterizes safe sets for hybrid systems through a generalized value function defined over both discrete and continuous states while accounting for control constraints and model uncertainty. We additionally provide a numerical algorithm to compute this value function. Building on these safe sets, we propose two different mechanisms to integrate performance objectives. First, we introduce a hybrid least-restrictive safety filter that intervenes on both the discrete and continuous components of a nominal controller only when necessary to avoid unsafe states, thereby preserving nominal behavior whenever possible. Second, we formulate and compute hybrid backward reach-avoid tubes, enabling the simultaneous enforcement of safety and goal-reaching behavior, an extension not previously addressed within hybrid HJ reachability. This enables the synthesis of continuous and discrete control policies that guarantee both safety and task completion. We validate our framework through simulation studies and real-world experiments on a quadrupedal robot, demonstrating its effectiveness in hybrid mode planning and safety-critical applications.

Key Points

Hybrid dynamical systems provide a powerful modeling framework for robotic systems, particularly in contact-rich environments.
However, ensuring safety and performance in such systems remains challenging due to the intricate coupling between continuous dynamics and discrete mode transitions.
In this work, we extend classical Hamilton-Jacobi (HJ) reachability analysis, a formal verification method for continuous-time nonlinear systems, to hybrid dynamical systems.
Our framework characterizes safe sets for hybrid systems through a generalized value function defined over both discrete and continuous states while accounting for control constraints and model uncertainty.
We additionally provide a numerical algorithm to compute this value function

Problem Formulation

We consider a hybrid dynamical system as defined by Lygeros et al. (2008) : where $Q:=\{q_{1},q_{2},\ldots,q_{N}\}$ is a finite set of discrete modes. We also refer to $q_{i}$ as the discrete state of the system.

Let $x\in X\subset\mathbb{R}^{n_{x}}$ be the continuous state of the system, $u\in U\subset\mathbb{R}^{n_{u}}$ be the continuous control input, and $d\in D\subset\mathbb{R}^{n_{d}}$ be the continuous disturbance in the system.

Problem Formulation — Hamilton-Jacobi Reachability for Hybrid Systems: Unified Goal-Driven Control with Safety Guarantees — Figure 1: Hybrid dynamical system with controlled and forced transitions.

Safety Filtering for Hybrid Systems

In this section, we address the hybrid safety filtering problem introduced in Subsection 3.2 , where the goal is to enforce safety in a hybrid system by modifying a nominal control policy only when necessary to prevent eventual entry into the failure set.

To this end, we propose and validate a minimally intrusive hybrid safety control filter that wraps around a given nominal hybrid control policy and ensures that the system remains within the safe set throughout its operation.

Safety Filtering for Hybrid Systems — Hamilton-Jacobi Reachability for Hybrid Systems: Unified Goal-Driven Control with Safety Guarantees — Figure 3: Hybrid dynamics of the planar jumping robot with two modes: stance ($q_{1}$), where ground-actuated forces apply, and flight ($q_{2}$), with ballistic motion. Forced transitions are triggered when the vertical position reaches the leg-length boundary.

Reach-Avoid Formulation for Hybrid Systems

In previous sections, we introduced the hLRF as a mechanism to ensure safety by filtering unsafe actions in real time. While this provides strong safety guarantees, many applications also require task completion guarantees, such as reaching a goal location within specific time constraints.

In this section, we address this complementary need by introducing a reach-avoid formulation for hybrid systems that guarantees both safety and task completion.

Reach-Avoid Formulation for Hybrid Systems — Hamilton-Jacobi Reachability for Hybrid Systems: Unified Goal-Driven Control with Safety Guarantees — Figure 4: hLRF renders nominal policies safe in a jumping robot example. Top plot corresponds to $u_{nom1}$ (horizontal movement), bottom plot shows $u_{nom2}$ (hopping behavior). In light orange, we show slices of the unsafe hBRT at the states that trigger the filter by coming into contact with its boundary. Dashed lines show the unsafe unfiltered trajectories.

Full System Experiments

To illustrate feasibility of real-time online execution of the proposed hBRAT framework proposed in Section 6 , we test it on a real-world quadruped experiment in the adapted Barkour ( Caluwaerts et al., 2023 ) benchmarking environment inspired by dog agility competitions. The environment consists of a diverse set of obstacles as shown in Fig.

Sources and Demonstrations

Figures are reproduced from Borquez et al. See the full paper for experimental details and the project page, when the paper links one, for demonstrations and videos.