Hybrid dynamical systems with non-linear 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 such hybrid systems can still prove to be 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 non-linear dynamics in the presence of bounded inputs and disturbances, to hybrid dynamical systems. Our framework can compute reachable sets for hybrid systems consisting of multiple discrete modes, each with its own set of non-linear 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 simulation on an aircraft collision avoidance problem, as well as on a real-world testbed to solve the optimal mode planning problem for a quadruped with multiple gaits.

翻译：具有非线性动力学的混合动力系统是描述机器人系统（尤其是接触丰富的系统）最通用的建模工具之一。然而，由于需要同时推理连续状态演化与离散模式切换，为此类混合系统提供安全性或性能保障仍是一个具有挑战性的问题。本研究通过将经典Hamilton-Jacobi（HJ）可达性分析——一种针对存在有界输入和扰动的连续非线性动力学的形式化验证方法——扩展到混合动力系统，来解决这一问题。我们的框架能够为包含多个离散模式的混合系统计算可达集合，每个模式拥有独立的非线性连续动力学，以及可由直接指令控制或由离散控制输入强制触发的离散转换，同时仍能考虑状态演化中的控制上界与对抗性扰动。除可达集合外，该框架还提供最优连续与离散控制器以确保系统安全性。我们通过飞行器防撞问题的仿真，以及在真实测试平台上解决多步态四足机器人的最优模式规划问题，验证了该框架的有效性。