# The Reachability Problem for Neural-Network Control Systems

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 8 of its 29 references that are in the map.
- First posted on arXiv 6 Jul 2024.

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

- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [On the Number of Linear Regions of Deep Neural Networks](https://mlsanity.com/paper/1402.1869/) (2014)
- [Understanding Deep Neural Networks with Rectified Linear Units](https://mlsanity.com/paper/1611.01491/) (2016)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [JuliaReach: a Toolbox for Set-Based Reachability](https://mlsanity.com/paper/1901.10736/) (2019)
- [Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopes](https://mlsanity.com/paper/2112.09197/) (2021)
- [Reachability In Simple Neural Networks](https://mlsanity.com/paper/2203.07941/) (2022)
- [Verifying And Interpreting Neural Networks using Finite Automata](https://mlsanity.com/paper/2211.01022/) (2022)

## Abstract (arXiv)

A control system consists of a plant component and a controller which periodically computes a control input for the plant. We consider systems where the controller is implemented by a feedforward neural network with ReLU activations. The reachability problem asks, given a set of initial states, whether a set of target states can be reached. We show that this problem is undecidable even for trivial plants and fixed-depth neural networks with three inputs and outputs. We also show that the problem becomes semi-decidable when the plant as well as the input and target sets are given by automata over infinite words.