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.

翻译：具有非线性动力学的混合动态系统是表示机器人系统（特别是涉及丰富接触的系统）最通用的建模工具之一。然而，为非线性混合系统的安全性或性能提供保证仍然是一个具有挑战性的问题，因为这需要同时对连续状态演化与离散模式切换进行推理。在本工作中，我们通过将经典的Hamilton-Jacobi（HJ）可达性分析（一种针对连续时间非线性动态系统的形式化验证方法）扩展至混合动态系统来解决该问题。我们通过定义在混合系统离散与连续状态上的广义值函数来刻画混合系统的可达集。我们还提供了一种数值算法来计算该值函数并获取可达集。我们的框架能够计算包含多个离散模式的混合系统的可达集，其中每个模式均具有各自的非线性连续动力学，离散切换可由离散控制输入直接指令触发或强制引发，同时仍能考虑状态演化中的控制约束与对抗性扰动。除可达集外，所提出的框架还提供了确保系统安全性的最优连续与离散控制器。我们在多个仿真案例研究以及真实世界测试平台上验证了我们的框架，以解决具有多种步态的四足机器人的最优模式规划问题。