A New Strategy for Verifying Reach-Avoid Specifications in Neural Feedback Systems

TL;DR

This paper introduces novel algorithms for verifying reach-avoid properties in neural feedback systems by computing backward reachable sets and integrating them with forward analysis, enhancing scalability and robustness.

Contribution

It presents new algorithms for backward reachability analysis and combines them with forward methods to improve verification of neural feedback systems.

Findings

Algorithms effectively compute over- and under-approximations of backward reachable sets.

Unified framework improves verification accuracy and scalability.

Applicable to complex neural feedback control systems.

Abstract

Forward reachability analysis is the predominant approach for verifying reach-avoid properties in neural feedback systems (dynamical systems controlled by neural networks). This dominance stems from the limited scalability of existing backward reachability methods. In this work, we introduce new algorithms that compute both over- and under-approximations of backward reachable sets for such systems. We further integrate these backward algorithms with established forward analysis techniques to yield a unified verification framework for neural feedback systems.