The Reachability Problem for Neural-Network Control Systems
Christian Schilling, Martin Zimmermann
TL;DR
This paper studies reachability in neural-network control systems (NNCS) where the controller is a ReLU DNN $N:\mathbb{R}^d\to\mathbb{R}^c$ and the plant is $P:\mathbb{R}^{d+c}\to\mathbb{R}^d$, with the loop map $C_{P,N}=P(\cdot,N(\cdot))$ and reachability defined by the existence of $x_0\in X_0$, $k\ge0$ such that $(C_{P,N})^k(x_0)\in\varphi$, for polyhedral $X_0,\varphi$. The central result shows undecidability: the NNCS reachability problem is undecidable even for a trivial plant and fixed-depth networks with $3$ inputs and $3$ outputs, using a reduction from the halting problem of a two-counter machine. In contrast, the authors establish semi-decidability when the plant and the input/target sets are $\omega$-regular (definable by Büchi automata), by encoding DNN behavior as automata and composing with an automaton-definable plant. They further identify $\omega$-regular plants, such as multi-mode linear maps, as a practical class enabling a semi-decision procedure via automata intersections, highlighting a boundary between undecidable and semi-decidable regimes and guiding verification approaches for restricted NNCS classes.
Abstract
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.