Scalable Synthesis of Formally Verified Neural Value Function for Hamilton-Jacobi Reachability Analysis

Yujie Yang, Hanjiang Hu, Tianhao Wei +2

Hamilton-Jacobi (HJ) reachability analysis provides a formal method for guaranteeing safety in constrained control problems. It synthesizes a value function to represent a long-ter…