Compressing ACAS-Xu Lookup Tables with Binary Decision Diagrams
Martin Boniol (ISAE-SUPAERO), Julien Brunel, Jean-Baptiste Chaudron (ISAE-SUPAERO), Christophe Garion (ISAE-SUPAERO), Xavier Thirioux (ISAE-SUPAERO)

TL;DR
This paper introduces a BDD-based method to compress ACAS-Xu lookup tables, enabling exact, memory-efficient, and verifiable decision logic deployment in embedded systems.
Contribution
It presents a symbolic compression technique using Binary Decision Diagrams that preserves the exact semantics of ACAS-Xu LUTs, improving verification and deployment.
Findings
Significant reduction in memory usage for ACAS-Xu LUTs.
Enables sound, exact reasoning and verification of decision logic.
Achieves predictable, low-latency execution suitable for embedded platforms.
Abstract
The Airborne Collision Avoidance System Xu (ACAS-Xu) relies on large certified Look-Up Tables (LUTs) that encode the exact decision logic used in operation. Neural-network-based approximations have been proposed to reduce memory requirements, but they inherently introduce approximation errors and complicate formal verification. This paper presents a symbolic compression approach based on Binary Decision Diagrams (BDDs) that preserves the exact semantics of the ACAS-Xu LUTs. The resulting representation is canonical, deterministic, and fully equivalent to the original tables, enabling sound and exact reasoning over the complete decision logic. By expressing both the system behavior and domain-specific operational properties within a common Boolean framework, verification reduces to efficient BDD operations and emptiness checks, with precise counterexamples generated when properties are…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
