Reach-SDP: Reachability Analysis of Closed-Loop Systems with Neural Network Controllers via Semidefinite Programming
This addresses the safety verification problem for control systems with neural networks, which is crucial for applications like autonomous vehicles, but it is incremental as it builds on existing abstraction techniques.
The paper tackles the challenge of providing safety and stability guarantees for closed-loop control systems with neural network controllers by proposing a forward reachability analysis method that uses quadratic constraints and semidefinite programming to compute outer-approximations of reachable sets, demonstrated in a quadrotor example with certification of finite-time reachability and constraint satisfaction.
There has been an increasing interest in using neural networks in closed-loop control systems to improve performance and reduce computational costs for on-line implementation. However, providing safety and stability guarantees for these systems is challenging due to the nonlinear and compositional structure of neural networks. In this paper, we propose a novel forward reachability analysis method for the safety verification of linear time-varying systems with neural networks in feedback interconnection. Our technical approach relies on abstracting the nonlinear activation functions by quadratic constraints, which leads to an outer-approximation of forward reachable sets of the closed-loop system. We show that we can compute these approximate reachable sets using semidefinite programming. We illustrate our method in a quadrotor example, in which we first approximate a nonlinear model predictive controller via a deep neural network and then apply our analysis tool to certify finite-time reachability and constraint satisfaction of the closed-loop system.