Safety Verification of Neural Network Control Systems Using Guaranteed Neural Network Model Reduction
This paper aims to enhance the computational efficiency of safety verification of neural network control systems by developing a guaranteed neural network model reduction method. First, a concept of model reduction precision is proposed to describe the guaranteed distance between the outputs of a neural network and its reduced-size version. A reachability-based algorithm is proposed to accurately compute the model reduction precision. Then, by substituting a reduced-size neural network controller into the closed-loop system, an algorithm to compute the reachable set of the original system is developed, which is able to support much more computationally efficient safety verification processes. Finally, the developed methods are applied to a case study of the Adaptive Cruise Control system with a neural network controller, which is shown to significantly reduce the computational time of safety verification and thus validate the effectiveness of the method.
Code (0)
등록된 구현이 없습니다.
Tasks
Computational EfficiencySimilar Papers 제목 키워드 기반
Distributed Safe Control Design and Probabilistic Safety Verification for Multi-Agent Systems
We propose distributed iterative algorithms for safe control design and safety verification for networked multi-agent systems. These algorithms rely on distributing a control barrier function (CBF) related quadratic prog…
Collision AvoidanceContinuous ControlBDD for Complete Characterization of a Safety Violation in Linear Systems with Inputs
The control design tools for linear systems typically involves pole placement and computing Lyapunov functions which are useful for ensuring stability. But given higher requirements on control design, a designer is expec…
Verification and Synthesis Methods for High-Order Control Barrier Functions
High-order control barrier functions (HOCBFs) can be used to provide autonomous systems with safety, though computational methods to verify and synthesize these functions remain lacking. In this work, we address this nee…
Verification in the Loop: Correct-by-Construction Control Learning with Reach-avoid Guarantees
In the current control design of safety-critical autonomous systems, formal verification techniques are typically applied after the controller is designed to evaluate whether the required properties (e.g., safety) are sa…
Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems
The integration of neural networks into safety-critical systems has shown great potential in recent years. However, the challenge of effectively verifying the safety of Neural Network Controlled Systems (NNCS) persists. …