Verification-Guided Nonlinear Model Predictive Control Using Hamilton-Jacobi Reachability

Sammanfattning

Ensuring safety in real-time control remains a central challenge for nonlinear model predictive control (NMPC), particularly in safety-critical systems where constraint-based formulations can become overly conservative or computationally infeasible. This thesis investigates how Hamilton–Jacobi reachability analysis can be integrated into NMPC so that formally verified safety information directly guides decision making during execution. Two formulations are proposed. The first embeds the reachability value function V (x, t) as an additional cost term, linking the optimization directly to the verified safe set. The second constructs a control-affine form α + βu from the gradient of V (x, t), allowing safety information to be evaluated efficiently in the lower-dimensional input space. The methods are tested on a five-dimensional vehicle navigation task that requires safe and feasible merging from a parking lot onto a highway. The direct formulation demonstrates how reachability guarantees can be preserved within NMPC, while the second approach achieves an order-of-magnitude improvement in computation speed and consistent real-time performance. The results show that verification-guided NMPC can reconcile safety and responsiveness by introducing a formally derived safety potential within the controller’s cost structure. This establishes a practical path toward deploying reachability- based safety mechanisms in embedded, safety-critical control systems