Compressing ACAS-Xu Lookup Tables with Binary Decision Diagrams

The Airborne Collision Avoidance System Xu (ACAS-Xu) uses large certified lookup tables (LUTs) encoding exact decision logic for avoiding mid-air collisions. Prior attempts to compress these tables with neural networks introduced approximation errors and complicated formal verification—a critical issue for safety-critical aviation software. Researchers from ISAE-SUPAERO (Boniol, Brunel, Chaudron, Garion, Thirioux) now propose a symbolic compression approach based on Binary Decision Diagrams (BDDs) that preserves the exact semantics of the original LUTs.

The resulting BDD representation is canonical, deterministic, and fully equivalent to the original tables, enabling sound and exact reasoning over the complete decision logic. By expressing both 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 violated. The authors demonstrate that the BDD-based representation significantly reduces memory usage, achieves predictable low-latency execution, and can be deployed on embedded platforms. Their paper, presented at NASA Formal Methods 2026, highlights BDDs as a compelling alternative for exact, verifiable, and embedded deployment of ACAS-Xu decision logic.