# Reachability Analysis and Safety Verification for Neural Network Control Systems

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

## Key facts

- Cited by 12 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 25 May 2018.

## Built on by (most cited first, 12 of 12)

- [Robust Machine Learning Systems: Challenges, Current Trends, Perspectives, and the Road Ahead](https://mlsanity.com/paper/2101.02559/) (2021)
- [Joint Differentiable Optimization and Verification for Certified Reinforcement Learning](https://mlsanity.com/paper/2201.12243/) (2022)
- [Scalable Surrogate Verification of Image-based Neural Network Control Systems using Composition and Unrolling](https://mlsanity.com/paper/2405.18554/) (2024)
- [ModelVerification.jl: a Comprehensive Toolbox for Formally Verifying Deep Neural Networks](https://mlsanity.com/paper/2407.01639/) (2024)
- [Safety Verification for Neural Networks Based on Set-boundary Analysis](https://mlsanity.com/paper/2210.04175/) (2022)
- [Generating Probabilistic Safety Guarantees for Neural Network Controllers](https://mlsanity.com/paper/2103.01203/) (2021)
- [Towards Optimal Branching of Linear and Semidefinite Relaxations for Neural Network Robustness Certification](https://mlsanity.com/paper/2101.09306/) (2021)
- [Robust Optimization Framework for Training Shallow Neural Networks Using Reachability Method](https://mlsanity.com/paper/2107.12801/) (2021)
- [An Overview and Prospective Outlook on Robust Training and Certification of Machine Learning Models](https://mlsanity.com/paper/2208.07464/) (2022)
- [Verifying Safety of Neural Networks from Topological Perspectives](https://mlsanity.com/paper/2306.15403/) (2023)
- [Architectural Transformations and Emerging Verification Demands in AI-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2510.00519/) (2025)
- [Robust Verification of Controllers under State Uncertainty via Hamilton-Jacobi Reachability Analysis](https://mlsanity.com/paper/2511.14755/) (2025)

## Abstract (arXiv)

Autonomous cyber-physical systems (CPS) rely on the correct operation of numerous components, with state-of-the-art methods relying on machine learning (ML) and artificial intelligence (AI) components in various stages of sensing and control. This paper develops methods for estimating the reachable set and verifying safety properties of dynamical systems under control of neural network-based controllers that may be implemented in embedded software. The neural network controllers we consider are feedforward neural networks called multilayer perceptrons (MLP) with general activation functions. As such feedforward networks are memoryless, they may be abstractly represented as mathematical functions, and the reachability analysis of the network amounts to range (image) estimation of this function provided a set of inputs. By discretizing the input set of the MLP into a finite number of hyper-rectangular cells, our approach develops a linear programming (LP) based algorithm for over-approximating the output set of the MLP with its input set as a union of hyper-rectangular cells. Combining the over-approximation for the output set of an MLP based controller and reachable set computation routines for ordinary difference/differential equation (ODE) models, an algorithm is developed to estimate the reachable set of the closed-loop system. Finally, safety verification for neural network control systems can be performed by checking the existence of intersections between the estimated reachable set and unsafe regions. The approach is implemented in a computational software prototype and evaluated on numerical examples.