The Reachability Problem for Neural-Network Control Systems
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.
Code (0)
등록된 구현이 없습니다.
Methods 이 논문이 사용한 방법론
Similar Papers 제목 키워드 기반
Scalable Forward Reachability Analysis of Multi-Agent Systems with Neural Network Controllers
Neural networks (NNs) have been shown to learn complex control laws successfully, often with performance advantages or decreased computational cost compared to alternative methods. Neural network controllers (NNCs) are, …
TTT: A Temporal Refinement Heuristic for Tenuously Tractable Discrete Time Reachability Problems
Reachable set computation is an important tool for analyzing control systems. Simulating a control system can show general trends, but a formal tool like reachability analysis can provide guarantees of correctness. Reach…
A Forward Reachability Perspective on Robust Control Invariance and Discount Factors in Reachability Analysis
Control invariant sets are crucial for various methods that aim to design safe control policies for systems whose state constraints must be satisfied over an indefinite time horizon. In this article, we explore the conne…
validOn the Reachability and Controllability of Temporal Continuous-Time Linear Networks: A Generic Analysis
Temporal networks are a class of time-varying networks, which change their topology according to a given time-ordered sequence of static networks (known as subsystems). This paper investigates the reachability and contro…
Temporal SequencesPolynomial-Time Reachability for LTI Systems with Two-Level Lattice Neural Network Controllers
In this paper, we consider the computational complexity of bounding the reachable set of a Linear Time-Invariant (LTI) system controlled by a Rectified Linear Unit (ReLU) Two-Level Lattice (TLL) Neural Network (NN) contr…