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.

翻译：控制系统由被控对象组件和控制器组成，控制器周期性地为被控对象计算控制输入。我们研究控制器由具有ReLU激活函数的前馈神经网络实现的系统。可达性问题询问：给定一组初始状态，能否到达一组目标状态。我们证明，即使对于平凡的被控对象和具有三个输入输出的固定深度神经网络，该问题也是不可判定的。我们还证明，当被控对象以及输入集和目标集由无限词上的自动机给定时，该问题变为半可判定的。