Verify and Deploy Airborne Collision Avoidance System (ACAS) Xu Neural Networks

Since R2026a

This example uses:

Open Live Script

This example shows how to verify the behavior of the 45 ACAS Xu neural networks using formal verification methods. Formally verify the global robustness of the networks as well as more general Verification of Neural Networks Library (VNN-LIB) [6] properties. Then, integrate the networks into a Simulink® model and test the entire system using scenario-based closed-loop testing.

ACAS Xu is a system developed by the Federal Aviation Authority (FAA) in the United States, designed to prevent collisions of unmanned aerial systems (UAS) such as delivery drones. ACAS Xu issues steering advisory to the ownship, based on these parameters:

  • Previous advisory

  • Vertical separation of the ownship and intruder ship

  • Horizontal distance between the two aircraft

  • Heading direction of both aircraft

  • Speed of both aircraft

ACAS Xu issues one of five advisories: Clear-of-conflict (do nothing), weak left, strong left, weak right, or strong right.

Originally, ACAS Xu consisted of a set of lookup tables. However, the lookup tables require a large amount of memory, about 2 GB. Furthermore, you must interpolate between states in the lookup tables. Choosing the wrong interpolation scheme can result in collisions.

To reduce the memory requirement and optimize the interpolation scheme, you can replace the lookup tables with a set of 45 small neural networks, one for each combination of previous advisory and discrete values of vertical separation, requiring about 3 MB of memory.

This example shows how to verify that the ACAS Xu neural networks correctly and reliably reproduce the predictions of the lookup tables, using formal verification methods provided by AI Verification Library for Deep Learning Toolbox™.

The workflow is organized into several live scripts. You can run the scripts in order or run each one independently.

  1. Explore ACAS Xu Neural Networks

  2. Verify Local Robustness of ACAS Xu Neural Networks

  3. Verify Global Stability of ACAS Xu Neural Networks

  4. Verify Global Stability of ACAS Xu Neural Network Using Adaptive Mesh

  5. Verify VNN-COMP Benchmark for ACAS Xu Neural Networks

  6. Verify VNN-COMP Benchmark for ACAS Xu Neural Networks Using α,β-CROWN

  7. Define and Verify AI Constituent Requirements for ACAS Xu Neural Networks

  8. Integrate ACAS Xu Neural Networks into Simulink

  9. Define and Verify AI System Requirements for ACAS Xu Neural Networks Integrated Into Simulink

References

[1] Julian, Kyle D., et al. “Policy Compression for Aircraft Collision Avoidance Systems.” 2016 IEEE/AIAA 35th Digital Avionics Systems Conference (DASC), 2016, pp. 1–10. IEEE Xplore, https://doi.org/10.1109/DASC.2016.7778091.

[2] Katz, Guy. Guykatzz/ReluplexCav2017. 3 May 2017, C. 15 Jun. 2025. GitHub, https://github.com/guykatzz/ReluplexCav2017.

[3] Manzanas Lopez, Diego, et al. “Evaluation of Neural Network Verification Methods for Air-to-Air Collision Avoidance.” Journal of Air Transportation, vol. 31, no. 1, Jan. 2023, pp. 1–17. DOI.org (Crossref), https://doi.org/10.2514/1.D0255.

[4] Katz, Guy, et al. “Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks.” arXiv:1702.01135, arXiv, 19 May 2017. arXiv.org, https://doi.org/10.48550/arXiv.1702.01135.

[5] “ReluplexCav2017/Nnet/ACASXU_run2a_5_9_batch_2000.Nnet at Master · Guykatzz/ReluplexCav2017.” GitHub, https://github.com/guykatzz/ReluplexCav2017/blob/master/nnet/ACASXU_run2a_5_9_batch_2000.nnet.

[6] VNN-COMP. VNN-COMP/Vnncomp2025_benchmarks. 7 May 2025, Shell. 16 Jul. 2025. GitHub, https://github.com/VNN-COMP/vnncomp2025_benchmarks.

[7] Goodfellow, Ian J., Jonathon Shlens, and Christian Szegedy. “Explaining and Harnessing Adversarial Examples.” Preprint, submitted March 20, 2015. https://doi.org/10.48550/arXiv.1412.6572.

[8] Zhang, Huan, et al. “Efficient Neural Network Robustness Certification with General Activation Functions.” arXiv:1811.00866, arXiv, 2 Nov. 2018. arXiv.org, https://doi.org/10.48550/arXiv.1811.00866.

[9] Singh, Gagandeep, Timon Gehr, Markus Püschel, and Martin Vechev. “An Abstract Domain for Certifying Neural Networks”. Proceedings of the ACM on Programming Languages 3, no. POPL (January 2, 2019): 1–30. https://doi.org/10.1145/3290354.

[10] Xu, Kaidi, et al. “Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers.” arXiv:2011.13824, arXiv, 16 Mar. 2021. arXiv.org, https://doi.org/10.48550/arXiv.2011.13824.

[11] VNN-LIB. https://www.vnnlib.org/. Accessed 4 Sep. 2025.

[12] Verified Intelligence. Verified-Intelligence/Alpha-Beta-CROWN. 29 Jun. 2021, Python. 3 Sep. 2025. GitHub, https://github.com/Verified-Intelligence/alpha-beta-CROWN.

[13] “Alpha-Beta-CROWN/Complete_verifier/Exp_configs/Vnncomp23/Acasxu.Yaml at 1a3533a02cddfc971213a9ef28002c8e131f7c96 · Verified-Intelligence/Alpha-Beta-CROWN.” GitHub, https://github.com/Verified-Intelligence/alpha-beta-CROWN/blob/1a3533a02cddfc971213a9ef28002c8e131f7c96/complete_verifier/exp_configs/vnncomp23/acasxu.yaml. Accessed 5 Sep. 2025.

See Also

| |

Topics