The Reachability Problem for Neural-Network Control Systems

TL;DR

This paper investigates the computational limits of determining whether neural-network controlled systems can reach certain states, proving undecidability in general and semi-decidability under specific automata-based conditions.

Contribution

It establishes the undecidability of the reachability problem for neural-network control systems and identifies conditions under which the problem becomes semi-decidable.

Findings

Reachability is undecidable for trivial plants with fixed-depth neural networks.

The problem is semi-decidable when plant and sets are represented by automata.

Provides theoretical limits on verifying neural-network controlled systems.

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.