Hamilton-Jacobi Reachability Analysis for Hybrid Systems with Controlled and Forced Transitions

TL;DR

This paper extends Hamilton-Jacobi reachability analysis to hybrid systems with multiple modes and transitions, enabling safety verification and optimal control synthesis for complex robotic systems.

Contribution

It introduces a generalized value function for hybrid systems, along with a numerical algorithm to compute reachable sets and controllers, handling nonlinear dynamics and mode transitions.

Findings

Successfully computed reachable sets for hybrid systems with multiple modes

Provided optimal controllers ensuring system safety

Validated framework on simulations and real quadruped robot

Abstract

Hybrid dynamical systems with nonlinear dynamics are one of the most general modeling tools for representing robotic systems, especially contact-rich systems. However, providing guarantees regarding the safety or performance of nonlinear hybrid systems remains a challenging problem because it requires simultaneous reasoning about continuous state evolution and discrete mode switching. In this work, we address this problem by extending classical Hamilton-Jacobi (HJ) reachability analysis, a formal verification method for continuous-time nonlinear dynamical systems, to hybrid dynamical systems. We characterize the reachable sets for hybrid systems through a generalized value function defined over discrete and continuous states of the hybrid system. We also provide a numerical algorithm to compute this value function and obtain the reachable set. Our framework can compute reachable sets for hybrid systems consisting of multiple discrete modes, each with its own set of nonlinear continuous dynamics, discrete transitions that can be directly commanded or forced by a discrete control input, while still accounting for control bounds and adversarial disturbances in the state evolution. Along with the reachable set, the proposed framework also provides an optimal continuous and discrete controller to ensure system safety. We demonstrate our framework in several simulation case studies, as well as on a real-world testbed to solve the optimal mode planning problem for a quadruped with multiple gaits.