# Reachability Analysis of Neural Network Control Systems

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

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- Builds on 17 of its 48 references that are in the map.
- First posted on arXiv 28 Jan 2023.

## Builds on (most cited first, 17 of 17)

- [End to End Learning for Self-Driving Cars](https://mlsanity.com/paper/1604.07316/) (2016)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [A Survey of Deep Learning Applications to Autonomous Vehicle Control](https://mlsanity.com/paper/1912.10773/) (2019)
- [Reachability Analysis of Deep Neural Networks with Provable Guarantees](https://mlsanity.com/paper/1805.02242/) (2018)
- [Verisig: verifying safety properties of hybrid systems with neural network controllers](https://mlsanity.com/paper/1811.01828/) (2018)
- [Reach-SDP: Reachability Analysis of Closed-Loop Systems with Neural Network Controllers via Semidefinite Programming](https://mlsanity.com/paper/2004.07876/) (2020)
- [Formal Verification of Neural Network Controlled Autonomous Systems](https://mlsanity.com/paper/1810.13072/) (2018)
- [Reachability Analysis of Neural Feedback Loops](https://mlsanity.com/paper/2108.04140/) (2021)
- [A Game-Based Approximate Verification of Deep Neural Networks with Provable Guarantees](https://mlsanity.com/paper/1807.03571/) (2018)
- [Scalable Polyhedral Verification of Recurrent Neural Networks](https://mlsanity.com/paper/2005.13300/) (2020)
- [PRoA: A Probabilistic Robustness Assessment against Functional Perturbations](https://mlsanity.com/paper/2207.02036/) (2022)
- [DIMBA: Discretely Masked Black-Box Attack in Single Object Tracking](https://mlsanity.com/paper/2207.08044/) (2022)
- [Adversarial Robustness of Deep Learning: Theory, Algorithms, and Applications](https://mlsanity.com/paper/2108.10451/) (2021)
- [3DVerifier: Efficient Robustness Verification for 3D Point Cloud Models](https://mlsanity.com/paper/2207.07539/) (2022)
- [Understanding Adversarial Robustness of Vision Transformers via Cauchy Problem](https://mlsanity.com/paper/2208.00906/) (2022)
- [Deterministic global optimization using space-filling curves and multiple estimates of Lipschitz and Holder constants](https://mlsanity.com/paper/1509.03590/) (2015)

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

- [A Survey of Safety and Trustworthiness of Large Language Models through the Lens of Verification and Validation](https://mlsanity.com/paper/2305.11391/) (2023)
- [Towards Verifying the Geometric Robustness of Large-scale Neural Networks](https://mlsanity.com/paper/2301.12456/) (2023)
- [Reward Certification for Policy Smoothed Reinforcement Learning](https://mlsanity.com/paper/2312.06436/) (2023)
- [Boosting Adversarial Training via Fisher-Rao Norm-based Regularization](https://mlsanity.com/paper/2403.17520/) (2024)
- [ReRoGCRL: Representation-based Robustness in Goal-Conditioned Reinforcement Learning](https://mlsanity.com/paper/2312.07392/) (2023)
- [Bridging Control with Neural Network Verifier alpha-beta-CROWN: A Tutorial](https://mlsanity.com/paper/2605.26577/) (2026)
- [Predicting AI Agent Behavior through Approximation of the Perron-Frobenius Operator](https://mlsanity.com/paper/2406.02723/) (2024)
- [Robust Verification of Controllers under State Uncertainty via Hamilton-Jacobi Reachability Analysis](https://mlsanity.com/paper/2511.14755/) (2025)

## Abstract (arXiv)

Neural network controllers (NNCs) have shown great promise in autonomous and cyber-physical systems. Despite the various verification approaches for neural networks, the safety analysis of NNCs remains an open problem. Existing verification approaches for neural network control systems (NNCSs) either can only work on a limited type of activation functions, or result in non-trivial over-approximation errors with time evolving. This paper proposes a verification framework for NNCS based on Lipschitzian optimisation, called DeepNNC. We first prove the Lipschitz continuity of closed-loop NNCSs by unrolling and eliminating the loops. We then reveal the working principles of applying Lipschitzian optimisation on NNCS verification and illustrate it by verifying an adaptive cruise control model. Compared to state-of-the-art verification approaches, DeepNNC shows superior performance in terms of efficiency and accuracy over a wide range of NNCs. We also provide a case study to demonstrate the capability of DeepNNC to handle a real-world, practical, and complex system. Our tool DeepNNC is available at urlhttps://github.com/TrustAI/DeepNNC.