# Reach-SDP: Reachability Analysis of Closed-Loop Systems with Neural Network Controllers via Semidefinite Programming

arXiv: https://arxiv.org/abs/2004.07876 · HTML: https://mlsanity.com/paper/2004.07876/

## Key facts

- Cited by 43 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 16 Apr 2020.

## Built on by (most cited first, 30 of 43)

- [The Safety Filter: A Unified View of Safety-Critical Control in Autonomous Systems](https://mlsanity.com/paper/2309.05837/) (2023)
- [Reachability Analysis of Neural Feedback Loops](https://mlsanity.com/paper/2108.04140/) (2021)
- [Imitation Learning with Stability and Safety Guarantees](https://mlsanity.com/paper/2012.09293/) (2020)
- [Provably Bounding Neural Network Preimages](https://mlsanity.com/paper/2302.01404/) (2023)
- [Backward Reachability Analysis of Neural Feedback Loops: Techniques for Linear and Nonlinear Systems](https://mlsanity.com/paper/2209.14076/) (2022)
- [Gameplay Filters: Robust Zero-Shot Safety through Adversarial Imagination](https://mlsanity.com/paper/2405.00846/) (2024)
- [Neural Network Verification in Control](https://mlsanity.com/paper/2110.01388/) (2021)
- [A Simple and Efficient Sampling-based Algorithm for General Reachability Analysis](https://mlsanity.com/paper/2112.05745/) (2021)
- [Learning Density Distribution of Reachable States for Autonomous Systems](https://mlsanity.com/paper/2109.06728/) (2021)
- [Efficient Reachability Analysis of Closed-Loop Systems with Neural Network Controllers](https://mlsanity.com/paper/2101.01815/) (2021)
- [LinSyn: Synthesizing Tight Linear Bounds for Arbitrary Neural Network Activation Functions](https://mlsanity.com/paper/2201.13351/) (2022)
- [Backward Reachability Analysis for Neural Feedback Loops](https://mlsanity.com/paper/2204.08319/) (2022)
- [Interval Reachability of Nonlinear Dynamical Systems with Neural Network Controllers](https://mlsanity.com/paper/2301.07912/) (2023)
- [Efficient Interaction-Aware Interval Analysis of Neural Network Feedback Loops](https://mlsanity.com/paper/2307.14938/) (2023)
- [Reachability Analysis of Neural Network Control Systems](https://mlsanity.com/paper/2301.12100/) (2023)
- [A Hybrid Partitioning Strategy for Backward Reachability of Neural Feedback Loops](https://mlsanity.com/paper/2210.07918/) (2022)
- [DRIP: Domain Refinement Iteration with Polytopes for Backward Reachability Analysis of Neural Feedback Loops](https://mlsanity.com/paper/2212.04646/) (2022)
- [DeepBern-Nets: Taming the Complexity of Certifying Neural Networks using Bernstein Polynomial Activations and Precise Bound Propagation](https://mlsanity.com/paper/2305.13508/) (2023)
- [System-level Safety Guard: Safe Tracking Control through Uncertain Neural Network Dynamics Models](https://mlsanity.com/paper/2312.06810/) (2023)
- [Hybrid Zonotopes Exactly Represent ReLU Neural Networks](https://mlsanity.com/paper/2304.02755/) (2023)
- [Automated Controller Calibration by Kalman Filtering](https://mlsanity.com/paper/2111.10832/) (2021)
- [Learning Neural Networks under Input-Output Specifications](https://mlsanity.com/paper/2202.11246/) (2022)
- [Contraction-Guided Adaptive Partitioning for Reachability Analysis of Neural Network Controlled Systems](https://mlsanity.com/paper/2304.03671/) (2023)
- [Verification of Neural Network Control Systems using Symbolic Zonotopes and Polynotopes](https://mlsanity.com/paper/2306.14619/) (2023)
- [Forward Invariance in Neural Network Controlled Systems](https://mlsanity.com/paper/2309.09043/) (2023)
- [Value Approximation for Two-Player General-Sum Differential Games with State Constraints](https://mlsanity.com/paper/2311.16520/) (2023)
- [State space representations of the Roesser type for convolutional layers](https://mlsanity.com/paper/2403.11938/) (2024)
- [Provable Bounds on the Hessian of Neural Networks: Derivative-Preserving Reachability Analysis](https://mlsanity.com/paper/2406.04476/) (2024)
- [Certified Robust Invariant Polytope Training in Neural Controlled ODEs](https://mlsanity.com/paper/2408.01273/) (2024)
- [Certified Training with Branch-and-Bound for Lyapunov-stable Neural Control](https://mlsanity.com/paper/2411.18235/) (2024)

## Abstract (arXiv)

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.