The proliferation of neural networks in safety-critical applications necessitates the development of effective methods to ensure their safety. This letter presents a novel approach for computing the exact backward reachable sets of neural feedback systems based on hybrid zonotopes. It is shown that the input-output relationship imposed by a ReLU-activated neural network can be exactly described by a hybrid zonotope-represented graph set. Based on that, the one-step exact backward reachable set of a neural feedback system is computed as a hybrid zonotope in the closed form. In addition, a necessary and sufficient condition is formulated as a mixed-integer linear program to certify whether the trajectories of a neural feedback system can avoid unsafe regions in finite time. Numerical examples are provided to demonstrate the efficiency of the proposed approach.
@article{arxiv.2303.10513,
title = {Backward Reachability Analysis of Neural Feedback Systems Using Hybrid Zonotopes},
author = {Yuhao Zhang and Hang Zhang and Xiangru Xu},
journal= {arXiv preprint arXiv:2303.10513},
year = {2023}
}