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.

翻译：Hamilton-Jacobi (HJ) 可达性分析是非线性控制系统安全验证和综合控制的基本工具。经典 HJ 可达性分析方法在离散化连续状态空间的网格上计算值函数。此类方法未考虑离散化误差，因此无法保证：当给定避免规范时，计算所得值函数表示的集合是后向可达集 (BRS) 的过逼近；当给定可达-避免规范时，则是可达-避免集 (RAS) 的欠逼近。我们通过提出一种算法来解决此问题，该算法计算 HJ 值函数的可靠上界和下界，从而保证 BRS 的可靠过逼近以及 RAS 的可靠欠逼近。此外，我们开发了一种细化算法，对根据计算所得界无法判定为属于或排除于 BRS 或 RAS 的网格单元进行划分，以获取更紧的界。我们通过两个案例研究验证了算法的有效性。