Abstraction-based Safety Analysis of Linear Dynamical Systems with Neural Network Controllers

We consider the safety verification problem of a closed-loop discrete-time linear dynamical system with a neural network controller. The crux of safety verification relies on computing output reachable sets of the dynamical system and the neural network. Reachable set computation time of the neural network grows with the network size. To address the scalability issue, our main approach consists of abstracting the neural network controller into a smaller annotated interval neural network (AINN), and using this to compute an over- approximation of the reachable set of the closed-loop system. We present a novel approach for output reachable set computation of an AINN by decomposing it into two reachable set computation problems on neural networks, which we then compute using star-sets. Our experimental analysis on two benchmarks demonstrate the trade-off in the precision and time for reachable set computation.