paper-with-me

홈 › Papers

Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopes

2021-12-16 · Christian Schilling, Marcelo Forets, Sebastian Guadalupe

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 and neural networks in isolation, there exist precise approaches for that task based on set representations respectively called Taylor models and zonotopes. However, the combination of these approaches to NNCS is non-trivial because, when converting between the set representations, dependency information gets lost in each control cycle and the accumulated approximation error quickly renders the result useless. We present an algorithm to chain approaches based on Taylor models and zonotopes, yielding a precise reachability algorithm for NNCS. Because the algorithm only acts at the interface of the isolated approaches, it is applicable to general dynamical systems and neural networks and can benefit from future advances in these areas. Our implementation delivers state-of-the-art performance and is the first to successfully analyze all benchmark problems of an annual reachability competition for NNCS.

📄 PDF Abstract BibTeX arXiv:2112.09197

Code (1)

juliareach/aaai22_re 공식 구현

Similar Papers 제목 키워드 기반

Open- and Closed-Loop Neural Network Verification using Polynomial Zonotopes

2022-07-06 · Niklas Kochdumper, Christian Schilling, Matthias Althoff, Stanley Bak

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…

Data-Driven Safety Verification using Barrier Certificates and Matrix Zonotopes

2025-04-01 · Mohammed Adib Oumer, Amr Alanwar, Majid Zamani

Ensuring safety in cyber-physical systems (CPSs) is a critical challenge, especially when system models are difficult to obtain or cannot be fully trusted due to uncertainty, modeling errors, or environmental disturbance…

Zonotope-based Symbolic Controller Synthesis for Linear Temporal Logic Specifications

2024-05-02 · Wei Ren, Raphael M. Jungers, Dimos V. Dimarogonas

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…

Logical Zonotopes: A Set Representation for the Formal Verification of Boolean Functions

2022-10-16 · Amr Alanwar, Frank J. Jiang, Samy Amin, Karl H. Johansson

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…

Scalable Zonotopic Under-approximation of Backward Reachable Sets for Uncertain Linear Systems

2021-07-04 · Liren Yang, Necmiye Ozay

Zonotopes are widely used for over-approximating forward reachable sets of uncertain linear systems for verification purposes. In this paper, we use zonotopes to achieve more scalable algorithms that under-approximate ba…