Computing Sound Lower and Upper Bounds on Hamilton-Jacobi Reach-Avoid Value Functions

TL;DR

This paper introduces an algorithm for computing guaranteed sound bounds on Hamilton-Jacobi reach-avoid value functions, improving safety verification accuracy for nonlinear control systems.

Contribution

It presents a novel method for calculating sound upper and lower bounds on HJ value functions, ensuring correct over- and under-approximations of reachable sets.

Findings

The algorithm guarantees sound over-approximation of backward reachable sets.

It provides sound under-approximation of reach-avoid sets.

Refinement improves bounds' tightness in case of classification uncertainty.

Abstract

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.