Verification of Neural Network Control Systems using Symbolic Zonotopes and Polynotopes
Verification and safety assessment of neural network controlled systems (NNCSs) is an emerging challenge. To provide guarantees, verification tools must efficiently capture the interplay between the neural network and the physical system within the control loop. In this paper, a compositional approach focused on inclusion preserving long term symbolic dependency modeling is proposed for the analysis of NNCSs. First of all, the matrix structure of symbolic zonotopes is exploited to efficiently abstract the input/output mapping of the loop elements through (inclusion preserving) affine symbolic expressions, thus maintaining linear dependencies between interacting blocks. Then, two further extensions are studied. Firstly, symbolic polynotopes are used to abstract the loop elements behaviour by means of polynomial symbolic expressions and dependencies. Secondly, an original input partitioning algorithm takes advantage of symbol preservation to assess the sensitivity of the computed approximation to some input directions. The approach is evaluated via different numerical examples and benchmarks. A good trade-off between low conservatism and computational efficiency is obtained.
Code (0)
등록된 구현이 없습니다.
Tasks
Computational EfficiencySimilar Papers 제목 키워드 기반
Functional sets with typed symbols : Mixed zonotopes and Polynotopes for hybrid nonlinear reachability and filtering
Verification and synthesis of Cyber-Physical Systems (CPS) are challenging and still raise numerous issues so far. In this paper, based on a new concept of mixed sets defined as function images of symbol type domains, a …
Zonotope-based Symbolic Controller Synthesis for Linear Temporal Logic Specifications
This paper studies the controller synthesis problem for nonlinear control systems under linear temporal logic (LTL) specifications using zonotope techniques. A local-to-global control strategy is proposed for the desired…
Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopes
We study the verification problem for closed-loop dynamical systems with neural-network controllers (NNCS). This problem is commonly reduced to computing the set of reachable states. When considering dynamical systems an…
Open- and Closed-Loop Neural Network Verification using Polynomial Zonotopes
We present a novel approach to efficiently compute tight non-convex enclosures of the image through neural networks with ReLU, sigmoid, or hyperbolic tangent activation functions. In particular, we abstract the input-out…
Logical Zonotopes: A Set Representation for the Formal Verification of Boolean Functions
A logical zonotope, which is a new set representation for binary vectors, is introduced in this paper. A logical zonotope is constructed by XOR-ing a binary vector with a combination of other binary vectors called genera…