Computing Sound Lower and Upper Bounds on Hamilton-Jacobi Reach-Avoid Value Functions
For safety verification and control synthesis of nonlinear systems, this work addresses the critical issue of discretization errors in HJ reachability, providing guaranteed bounds.
The paper presents an algorithm for computing sound upper and lower bounds on Hamilton-Jacobi reach-avoid value functions, guaranteeing over-approximation of backward reachable sets and under-approximation of reach-avoid sets, with a refinement algorithm to tighten bounds. Validation on two case studies shows effectiveness.
Hamilton-Jacobi (HJ) reachability analysis is a fundamental tool for the safety verification and control synthesis of nonlinear control systems. Classical HJ reachability analysis methods compute value functions over grids which discretize the continuous state space. Such approaches do not account for discretization errors and thus do not guarantee that the sets represented by the computed value functions over-approximate the backward reachable sets (BRS) when given avoid specifications or under-approximate the reach-avoid sets (RAS) when given reach-avoid specifications. We address this issue by presenting an algorithm for computing sound upper and lower bounds on the HJ value functions that guarantee the sound over-approximation of BRS and under-approximation of RAS. Additionally, we develop a refinement algorithm that splits the grid cells which could not be classified as within or outside the BRS or RAS given the computed bounds to obtain corresponding tighter bounds. We validate the effectiveness of our algorithm in two case studies.