# Safety Verification of Neural Feedback Systems Based on Constrained Zonotopes

arXiv: https://arxiv.org/abs/2204.00903 · HTML: https://mlsanity.com/paper/2204.00903/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 2 Apr 2022.

## Built on by (most cited first, 7 of 7)

- [Physics-Informed Machine Learning for Modeling and Control of Dynamical Systems](https://mlsanity.com/paper/2306.13867/) (2023)
- [Hybrid Zonotopes Exactly Represent ReLU Neural Networks](https://mlsanity.com/paper/2304.02755/) (2023)
- [Contraction-Guided Adaptive Partitioning for Reachability Analysis of Neural Network Controlled Systems](https://mlsanity.com/paper/2304.03671/) (2023)
- [Provably-Safe Neural Network Training Using Hybrid Zonotope Reachability Analysis](https://mlsanity.com/paper/2501.13023/) (2025)
- [Learning Verifiable Control Policies Using Relaxed Verification](https://mlsanity.com/paper/2504.16879/) (2025)
- [Runtime Monitoring and Fault Detection for Neural Network-Controlled Systems](https://mlsanity.com/paper/2403.16132/) (2024)
- [Efficient Reachability Analysis for Convolutional Neural Networks Using Hybrid Zonotopes](https://mlsanity.com/paper/2503.10840/) (2025)

## Abstract (arXiv)

Artificial neural networks have recently been utilized in many feedback control systems and introduced new challenges regarding the safety of such systems. This paper considers the safe verification problem for a dynamical system with a given feedforward neural network as the feedback controller by using a constrained zonotope-based approach. A novel set-based method is proposed to compute both exact and over-approximated reachable sets for neural feedback systems with linear models, and linear program-based sufficient conditions are presented to verify whether the trajectories of such a system can avoid unsafe regions represented as constrained zonotopes. The results are also extended to neural feedback systems with nonlinear models. The computational efficiency and accuracy of the proposed method are demonstrated by two numerical examples where a comparison with state-of-the-art methods is also provided.