Verifying Nonlinear Neural Feedback Systems using Polyhedral Enclosures
As dynamical systems equipped with neural network controllers (neural feedback systems) become increasingly prevalent, it is critical to develop methods to ensure their safe operation. Verifying safety requires extending control theoretic analysis methods to these systems. Although existing techniques can efficiently handle linear neural feedback systems, relatively few scalable methods address the nonlinear case. We propose a novel algorithm for forward reachability analysis of nonlinear neural feedback systems. The approach leverages the structure of the nonlinear transition functions of the systems to compute tight polyhedral enclosures (i.e., abstractions). These enclosures, combined with the neural controller, are then encoded as a mixed-integer linear program (MILP). Optimizing this MILP yields a sound over-approximation of the forward-reachable set. We evaluate our algorithm on representative benchmarks and demonstrate an order of magnitude improvement over the current state of the art.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Set-based state estimation of nonlinear discrete-time systems using constrained zonotopes and polyhedral relaxations
This paper presents a new algorithm for set-based state estimation of nonlinear discrete-time systems with bounded uncertainties. The novel method builds upon essential properties and computational advantages of constrai…
State EstimationAbstraction-based Probabilistic Stability Analysis of Polyhedral Probabilistic Hybrid Systems
In this paper, we consider the problem of probabilistic stability analysis of a subclass of Stochastic Hybrid Systems, namely, Polyhedral Probabilistic Hybrid Systems (PPHS), where the flow dynamics is given by a polyhed…
Certification of Linear Inclusions for Nonlinear Systems
In this work, we propose novel method for certifying if a given set of vertex linear systems constitute a linear difference inclusion for a nonlinear system. The method relies on formulating the verification of the inclu…
The FABRIC Strategy for Verifying Neural Feedback Systems
Forward reachability analysis is a dominant approach for verifying reach-avoid specifications in neural feedback systems, i.e., dynamical systems controlled by neural networks, and a number of directions have been propos…
Reachability Analysis of Nonlinear Discrete-Time Systems Using Polyhedral Relaxations and Constrained Zonotopes
This paper presents a novel algorithm for reachability analysis of nonlinear discrete-time systems. The proposed method combines constrained zonotopes (CZs) with polyhedral relaxations of factorable representations of no…