The Reachability Problem for Neural-Network Control Systems
This addresses a fundamental verification challenge for neural-network-based control systems, with implications for safety-critical applications, though it is incremental in extending undecidability results to neural networks.
The paper tackles the reachability problem for control systems where the controller is a feedforward neural network with ReLU activations, showing that this problem is undecidable even for simple cases with trivial plants and small networks, but becomes semi-decidable under certain conditions involving automata over infinite words.
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.