Neural Network Compression of ACAS Xu Early Prototype is Unsafe: Closed-Loop Verification through Quantized State Backreachability

ACAS Xu is an air-to-air collision avoidance system designed for unmanned aircraft that issues horizontal turn advisories to avoid an intruder aircraft. Analysis of this system has spurred a significant body of research in the formal methods community on neural network verification. While many powerful methods have been developed, most work focuses on open-loop properties of the networks, rather than the main point of the system—collision avoidance—which requiresclosed-loop analysis. In this work, we develop a technique to verify a closed-loop approximation of the system using state quantization and back-reachability. We use favorable assumptions for the analysis—perfect sensor information, instantfollowing of advisories, ideal aircraft maneuvers, and an intruder that only flies straight. When the method fails to prove the system is safe, we refinethe quantization parameters until generating counterexamples where the original (non-quantized) system also has collisions.