Compressing ACAS-Xu Lookup Tables with Binary Decision Diagrams

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 violated. We demonstrate that the proposed BDD-based representation significantly reduces memory usage, achieves predictable and low-latency execution, and can be deployed on embedded platforms. These results highlight BDDs as a compelling alternative for exact, verifiable, and embedded deployment of ACAS-Xu decision logic.