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

Ihab Tabbara, Eliya Badr, and Hussein Sibai

Department of Computer Science & Engineering, Washington University in St. Louis

Paper Code coming soon

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.

Sound bounds and adaptive grid refinement

We compute sound lower and upper bounds on Hamilton–Jacobi reach-avoid value functions. Classical grid-based HJ methods evaluate the value function at cell centers and can misclassify cells because they ignore discretization error. Our bounds account for that error, so a cell is labeled only when the bound is enough to certify it.

A cell is green when the conservative lower bound is positive (Vcons > 0) and red when the conservative upper bound is negative (V̄cons < 0). Gray cells sit between the two bounds and stay unclassified. The refinement algorithm then splits those gray cells, recomputes the bounds, and produces a tighter value function concentrated near the reach-avoid boundary. Unsafe cells are never labeled safe at any resolution.

Sound lower and upper bounds

The two conservative value functions give a guaranteed classification: green cells belong to the reach-avoid set, red cells do not. Coarse grids stay sound because unlabeled cells remain gray instead of being guessed.

Refinement tightens the value function

Algorithm 2 splits unclassified cells along their longest side and reruns value iteration. Each iteration yields tighter bounds and a finer grid only where the boundary is still unresolved.

Dubins car conservative upper and lower reach-avoid value bounds and cell classifications after refinement iterations 1, 7, and 14
Figure 2 from the paper — Dubins car. Algorithm 2 at iterations 1, 7, and 14, shown at θ = π. The top row is the conservative upper bound V̄, the middle row is the conservative lower bound V, and the bottom row is the resulting cell classification. Green: Vcons > 0. Red: V̄cons < 0. Gray: still unclassified. After more refinement, the gray band shrinks to a thin boundary layer while the certified green and red regions expand. The solid blue circle is the failure set; the dashed yellow circle is the target set.
Three-dimensional evasion conservative upper and lower reach-avoid value bounds and cell classifications after refinement iterations 1, 7, and 10
Figure 3 from the paper — 3D evasion. Algorithm 2 at iterations 1, 7, and 10, shown at θ = π, with the same sound classification rule. The target neighborhood is already certified at iteration 1; later iterations refine the remaining gray cells and tighten the value bounds around the more complicated reach-avoid boundary. Easy regions stay coarse. The solid blue circle is the failure set; the dashed yellow circle is the target set.

Citation

@misc{tabbara2025computingsoundlowerupper,
  title={Computing Sound Lower and Upper Bounds on Hamilton-Jacobi Reach-Avoid Value Functions},
  author={Ihab Tabbara and Eliya Badr and Hussein Sibai},
  year={2025},
  eprint={2511.15238},
  archivePrefix={arXiv},
  primaryClass={eess.SY},
  url={https://arxiv.org/abs/2511.15238},
}