# A Reachability Method for Verifying Dynamical Systems with Deep Neural Network Controllers

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

## Key facts

- Cited by 11 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 1 Mar 2019.

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

- [Provable Preimage Under-Approximation for Neural Networks (Full Version)](https://mlsanity.com/paper/2305.03686/) (2023)
- [PREMAP: A Unifying PREiMage APproximation Framework for Neural Networks](https://mlsanity.com/paper/2408.09262/) (2024)
- [Reachable Polyhedral Marching (RPM): An Exact Analysis Tool for Deep-Learned Control Systems](https://mlsanity.com/paper/2210.08339/) (2022)
- [Strategy Synthesis for Zero-Sum Neuro-Symbolic Concurrent Stochastic Games](https://mlsanity.com/paper/2202.06255/) (2022)
- [Generating Probabilistic Safety Guarantees for Neural Network Controllers](https://mlsanity.com/paper/2103.01203/) (2021)
- [Safe and Reliable Training of Learning-Based Aerospace Controllers](https://mlsanity.com/paper/2407.07088/) (2024)
- [On the Probabilistic Learnability of Compact Neural Network Preimage Bounds](https://mlsanity.com/paper/2511.11656/) (2025)
- [Efficient Preimage Approximation for Neural Network Certification](https://mlsanity.com/paper/2505.22798/) (2025)
- [Automated Repair of Neural Networks](https://mlsanity.com/paper/2207.08157/) (2022)
- [Learning Verifiable Control Policies Using Relaxed Verification](https://mlsanity.com/paper/2504.16879/) (2025)
- [Verification of Visual Controllers via Compositional Geometric Transformations](https://mlsanity.com/paper/2507.04523/) (2025)

## Abstract (arXiv)

Deep neural networks can be trained to be efficient and effective controllers for dynamical systems; however, the mechanics of deep neural networks are complex and difficult to guarantee. This work presents a general approach for providing guarantees for deep neural network controllers over multiple time steps using a combination of reachability methods and open source neural network verification tools. By bounding the system dynamics and neural network outputs, the set of reachable states can be over-approximated to provide a guarantee that the system will never reach states outside the set. The method is demonstrated on the mountain car problem as well as an aircraft collision avoidance problem. Results show that this approach can provide neural network guarantees given a bounded dynamic model.