Reachability Analysis and Safety Verification for Neural Network Control Systems

Abstract

Autonomous cyber-physical systems (CPS) rely on the correct operation of numerous components, with state-of-the-art methods relying on machine learning (ML) and artificial intelligence (AI) components in various stages of sensing and control. This paper develops methods for estimating the reachable set and verifying safety properties of dynamical systems under control of neural network-based controllers that may be implemented in embedded software. The neural network controllers we consider are feedforward neural networks called multilayer perceptrons (MLP) with general activation functions. As such feedforward networks are memoryless, they may be abstractly represented as mathematical functions, and the reachability analysis of the network amounts to range (image) estimation of this function provided a set of inputs. By discretizing the input set of the MLP into a finite number of hyper-rectangular cells, our approach develops a linear programming (LP) based algorithm for over-approximating the output set of the MLP with its input set as a union of hyper-rectangular cells. Combining the over-approximation for the output set of an MLP based controller and reachable set computation routines for ordinary difference/differential equation (ODE) models, an algorithm is developed to estimate the reachable set of the closed-loop system. Finally, safety verification for neural network control systems can be performed by checking the existence of intersections between the estimated reachable set and unsafe regions. The approach is implemented in a computational software prototype and evaluated on numerical examples.

21 pages, 6 figures

References in corpus (4)

• End to End Learning for Self-Driving Cars
• An approach to reachability analysis for feed-forward ReLU neural networks
• Output Range Analysis for Deep Neural Networks
• Reachable Set Estimation and Safety Verification for Piecewise Linear Systems with Neural Network Controllers

Cited by in corpus (9)

• A Roadmap Towards Resilient Internet of Things for Cyber-Physical Systems
• Guaranteeing Safety for Neural Network-Based Aircraft Collision Avoidance Systems
• ReachNN: Reachability Analysis of Neural-Network Controlled Systems
• Energy-Efficient Control Adaptation with Safety Guarantees for Learning-Enabled Cyber-Physical Systems
• Verification of Neural Network Control Policy Under Persistent Adversarial Perturbation
• Generating Probabilistic Safety Guarantees for Neural Network Controllers
• Verification in the Loop: Correct-by-Construction Control Learning with Reach-avoid Guarantees
• Gray-box Adversarial Testing for Control Systems with Machine Learning Component
• Reachable Set Estimation for Neural Network Control Systems: A Simulation-Guided Approach