arxiv: 2604.27008 · v1 · submitted 2026-04-29 · 💻 cs.LO · cs.NE

Recognition: unknown

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)

Authors on Pith no claims yet

Pith reviewed 2026-05-07 10:58 UTC · model grok-4.3

classification 💻 cs.LO cs.NE

keywords ACAS-XuBinary Decision DiagramsLookup TablesFormal VerificationEmbedded SystemsCollision AvoidanceSymbolic Representation

0 comments

The pith

Binary decision diagrams exactly compress the ACAS-Xu lookup tables while preserving every original decision and supporting direct formal checks.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that the large certified lookup tables driving ACAS-Xu collision avoidance can be replaced by a much smaller binary decision diagram representation that remains fully equivalent to the tables. This matters because the original tables consume too much memory for many embedded platforms, while neural approximations introduce errors that are difficult to verify formally. By casting both the decision logic and safety properties as Boolean formulas over the same diagrams, verification reduces to standard emptiness checks that either confirm the property or return a precise counterexample. The result is a representation that is canonical, deterministic, and suitable for real-time execution with predictable timing.

Core claim

The authors show that the exact decision logic encoded in the ACAS-Xu lookup tables admits a compact encoding as binary decision diagrams. These diagrams are canonical and deterministic, fully equivalent to the original tables, and permit both the system behavior and domain-specific operational properties to be expressed as Boolean formulas. Verification of those properties then reduces to efficient BDD operations and emptiness checks, with counterexamples produced when a property does not hold.

What carries the argument

Binary decision diagrams that compactly encode the Boolean functions representing the full ACAS-Xu decision logic from the lookup tables.

If this is right

Memory required to store the collision avoidance logic drops substantially below that of the full lookup tables.
Execution time becomes predictable and low enough for real-time embedded hardware.
Safety and operational properties can be checked exactly by testing whether certain Boolean formulas are satisfiable in the diagrams.
Any violation of a checked property yields a concrete counterexample that identifies the violating input combination.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same compression could apply to other certified lookup-table controllers in avionics where memory and verifiability are both constraints.
Because the representation stays exact, it might simplify certification arguments that currently rely on exhaustive table inspection.
Engineers could embed the diagrams in smaller general-aviation aircraft that cannot accommodate the original table sizes.

Load-bearing premise

The decision logic in the ACAS-Xu tables admits a compact binary decision diagram encoding whose size remains practical rather than growing explosively.

What would settle it

Constructing the BDD representation for the complete ACAS-Xu tables requires more memory than the original tables or takes so long that the approach becomes unusable in practice.

Figures

Figures reproduced from arXiv: 2604.27008 by Christophe Garion (ISAE-SUPAERO), Jean-Baptiste Chaudron (ISAE-SUPAERO), Julien Brunel, Martin Boniol (ISAE-SUPAERO), Xavier Thirioux (ISAE-SUPAERO).

**Figure 1.** Figure 1: ACAS-Xu geometry (taken from [21]) 2.2 LUTs as the Core Decision Representation The ACAS-Xu decision logic relies on several structural features that characterize how the system evaluates potential collision scenarios. When an advisory must be issued, the system first acquires the current encounter state, which describes the relative geometry and kinematics of the ownship and the intruder. This continuou… view at source ↗

**Figure 2.** Figure 2: ACAS-Xu Architecture view at source ↗

**Figure 3.** Figure 3: ACAS-Xu Architecture with NN The ACAS-Xu advisory decision process is implemented through an array of 45 distinct Deep Neural Networks, each trained to operate within a specific region of the state space. These networks are obtained by discretizing two ACASXu input dimensions: τ (time to loss of vertical separation) and aprev (previous advisory). The architecture overview is shown in view at source ↗

**Figure 4.** Figure 4: Decision tree and BDD representations of view at source ↗

**Figure 5.** Figure 5: ACAS-Xu Architecture with BDDs view at source ↗

**Figure 6.** Figure 6: Final Single-Root BDDSR illustration (aprev = SR) view at source ↗

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

BDDs give an exact, verifiable encoding for ACAS-Xu tables but the paper still needs to prove the diagrams stay compact enough to beat the original LUT size on embedded hardware.

read the letter

The paper encodes the ACAS-Xu collision-avoidance lookup tables as binary decision diagrams rather than training neural approximations. This keeps every decision identical to the certified tables and reduces verification to standard BDD emptiness checks plus counterexample generation. That is the main concrete advance: a domain-specific demonstration that the decision logic can sit inside a Boolean framework where operational properties become ordinary formula checks. The write-up is clear on why this matters for certification—neural nets introduce approximation that then has to be bounded, while the BDD version stays exact by construction. The authors also note that BDDs are deterministic and canonical, which simplifies deployment arguments. The central practical question is whether the resulting diagrams are small. ACAS-Xu is a five-dimensional function over discretized inputs, so each real-valued coordinate must be bit-blasted into several Boolean variables. BDD size is sensitive to ordering and can grow exponentially; the paper therefore needs to report final node counts, peak construction memory, and direct byte-size comparisons against the original tables. If those numbers are present and show consistent compression across the full set of tables, the embeddability claim holds. If they are only sketched or rely on a single lucky ordering, the memory and latency advantages remain unproven. The work is aimed at formal-methods groups working on avionics or other safety-critical lookup-table controllers. It is worth sending to peer review because the idea is technically sound and the application is timely, provided the experimental section supplies the missing size and timing data.

Referee Report

2 major / 0 minor

Summary. The paper proposes a BDD-based symbolic compression method for the ACAS-Xu lookup tables that preserves exact semantics, yields a canonical and deterministic representation, reduces memory footprint, supports low-latency embedded execution, and reduces verification of operational properties to standard BDD emptiness checks with counterexample generation.

Significance. If the claimed compactness and performance hold, the work supplies an exact, machine-checkable alternative to neural approximations for a certified safety-critical system, strengthening both memory efficiency and formal verifiability in avionics.

major comments (2)

[Abstract] Abstract: the central claims of 'significantly reduces memory usage' and 'achieves predictable and low-latency execution' are asserted without any supporting measurements (BDD node counts, peak construction memory, byte-size comparison to the original LUTs, or timing data on target hardware).
The manuscript provides no empirical evidence that the 5-dimensional ACAS-Xu decision logic admits a compact BDD encoding; the risk of exponential blow-up under bit-blasting and variable ordering is not addressed by any reported node counts or ordering experiments.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful review and constructive feedback. The points raised correctly identify the need for quantitative empirical support for our claims regarding memory reduction and performance. We will revise the manuscript to include the requested measurements and experiments. Point-by-point responses to the major comments are provided below.

read point-by-point responses

Referee: [Abstract] Abstract: the central claims of 'significantly reduces memory usage' and 'achieves predictable and low-latency execution' are asserted without any supporting measurements (BDD node counts, peak construction memory, byte-size comparison to the original LUTs, or timing data on target hardware).

Authors: We accept the observation. The manuscript describes the BDD construction and its theoretical benefits for exact representation, memory efficiency, and deterministic execution, but does not include quantitative benchmarks. In the revised version we will add a dedicated experimental section reporting BDD node counts for each ACAS-Xu output, peak memory during construction, byte-size comparisons against the original LUTs, and latency measurements on embedded target hardware. These data will be used to revise the abstract claims accordingly. revision: yes
Referee: The manuscript provides no empirical evidence that the 5-dimensional ACAS-Xu decision logic admits a compact BDD encoding; the risk of exponential blow-up under bit-blasting and variable ordering is not addressed by any reported node counts or ordering experiments.

Authors: The referee correctly notes the absence of node counts and ordering experiments. While the manuscript emphasizes the canonical and exact nature of BDDs, it does not empirically demonstrate compactness for the 5D tables or address potential blow-up. We will add results from variable-ordering experiments (using standard heuristics such as sifting) together with the achieved BDD sizes, and include a brief discussion of why the decision logic structure permits compact representations without exponential growth. These additions will appear in the revised manuscript. revision: yes

Circularity Check

0 steps flagged

No significant circularity; standard BDD application with empirical claims

full rationale

The paper applies canonical BDD properties to exactly encode ACAS-Xu LUT decision logic as Boolean functions, then reports memory and latency outcomes from that encoding. No equations, parameters, or derivations are defined in terms of their own outputs; no self-citations are load-bearing for the central claims; and no ansatzes or uniqueness theorems are smuggled in. The compactness and embeddability results are presented as direct consequences of the representation applied to the given tables, remaining falsifiable against external BDD size measurements and the original LUT sizes.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

No free parameters, axioms, or invented entities are introduced or required by the abstract description; the method relies on standard properties of BDDs and Boolean logic.

pith-pipeline@v0.9.0 · 5517 in / 1066 out tokens · 53410 ms · 2026-05-07T10:58:41.166792+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

29 extracted references · 7 canonical work pages

[1]

AMD / Xilinx: Kria KR260 Robotics Starter Kit Product Brief (2026),https:// www.amd.com/en/products/system-on-modules/kria/k26/robotics.html, spec- ifications of the KR260 Robotics Starter Kit based on Zynq UltraScale+ MPSoC XCK26 Compressing ACAS-Xu Lookup Tables with Binary Decision Diagrams 19

2026
[2]

Advanced Mi- cro Devices, Inc., 2025.2 english edn

AMD Xilinx: Vitis High-Level Synthesis User Guide (UG1399). Advanced Mi- cro Devices, Inc., 2025.2 english edn. (2025), https://docs.amd.com/r/en-US/ ug1399-vitis-hls, accessed: 2025-11-20

2025
[3]

In: NASA Formal Methods Symposium

Bak, S., Tran, H.D.: Neural network compression of ACAS-Xu early prototype is unsafe. In: NASA Formal Methods Symposium. Springer (2022). https://doi. org/10.1007/978-3-031-06773-0_3

work page doi:10.1007/978-3-031-06773-0_3 2022
[4]

BeagleBoard.org Foundation: BeagleBone Green System Reference Manual (2026), https://www.beagleboard.org/boards/seeedstudio-beaglebone-green, speci- fications of the ARM Cortex-A8 based BeagleBone Green board

2026
[5]

BeagleBoard.org Foundation: BeagleBone X15 System Reference Manual (2026), https://git.beagleboard.org/beagleboard/beagleboard-x15/-/blob/ master/BeagleBoard-X15_SRM.pdf, specifications of the dual-core ARM Cortex- A15 based BeagleBone X15 board

2026
[6]

IEEE Transactions on ComputersC-35(8), 677–691 (1986).https://doi.org/10.1109/ TC.1986.1676819

Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on ComputersC-35(8), 677–691 (1986).https://doi.org/10.1109/ TC.1986.1676819

work page arXiv 1986
[7]

In: International Conference on Learning Representations (ICLR) (2014)

Christian Szegedy, Wojciech Zaremba, I.S., et al.: Intriguing properties of neural networks. In: International Conference on Learning Representations (ICLR) (2014)

2014
[8]

MIT Press (1999)

Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)

1999
[9]

Clavière, A.: Safety Verification of Neural Network Based Systems Using For- mal Methods. Ph.D. thesis, ISAE-SUPAERO (2023), http://www.theses.fr/ 2023ESAE0041/document, thèse de doctorat, Toulouse. Réf. 2023ESAE0041

2023
[10]

In: Proceedings of the ACM/IEEE Design Automation Conference (DAC)

Coudert, O., Madre, J.C.: Implicit and incremental computation of primes and essential primes of boolean functions. In: Proceedings of the ACM/IEEE Design Automation Conference (DAC). pp. 36–39 (1991)

1991
[11]

IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 11(10), 1265–1278 (1992)

Coudert,O.,Madre,J.C.:Aunifiedframeworkfortheformalverificationofsequen- tial circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 11(10), 1265–1278 (1992)

1992
[12]

In: Computer Safety, Reliability and Security

Damour, M., de Grancey, F., Gabreau, C., Gauffriau, A., Ginestet, J.B., Hervieu, A., Huraux, T., Pagetti, C., Ponsolle, L., Clavière, A.: Towards certification of a reduced footprint ACAS-Xu system: A hybrid ML-based solution. In: Computer Safety, Reliability and Security. LNCS, vol. 12852, pp. 31–43. Springer (2021). https://doi.org/10.1007/978-3-030-83903-1_3

work page doi:10.1007/978-3-030-83903-1_3 2021
[13]

Journal of Universal Computer Science13(11), 1573– 1597 (2007)

Doran, R.W.: The gray code. Journal of Universal Computer Science13(11), 1573– 1597 (2007). https://doi.org/10.3217/jucs-013-11-1573

work page doi:10.3217/jucs-013-11-1573 2007
[14]

Springer (1998)

Drechsler, R., Becker, B.: Binary Decision Diagrams: Theory and Implementation. Springer (1998)

1998
[15]

EUROCAE: ED-275: Minimum operational performance standards for airborne collision avoidance system ACAS-Xu. Tech. rep., EUROCAE (Dec 2020),https: //www.eurocae.net/documents-and-projects/documents/ed-275/, licensed to ONERA

2020
[16]

EUROCONTROL: ACAS guide (2022),https://www.eurocontrol.int/system/ acas

2022
[17]

com/johnyf/dd (2015)

JohnyF, contributors: dd: Decision diagram package for python.https://github. com/johnyf/dd (2015)

2015
[18]

Journal of Guidance, Control, and Dynamics 42(9), 1969–1982 (2019)

Julian, K.D., Kochenderfer, M.J.: Policy compression for aircraft collision avoid- ance systems. Journal of Guidance, Control, and Dynamics 42(9), 1969–1982 (2019)

1969
[19]

Deep Neural Network Compression for Aircraft Collision Avoidance Systems

Julian, K.D., Kochenderfer, M.J., Owen, M.P.: Deep neural network compression for aircraft collision avoidance systems. Journal of Guidance, Control, and Dynam- ics 42(3), 598–608 (2019).https://doi.org/10.2514/1.G003724 20 F. Author et al

work page doi:10.2514/1.g003724 2019
[20]

In: International Con- ference on Computer Aided Verification (CAV)

Julian, K.D., Lopez, J., Brush, J.S., Owen, M.P., Kochenderfer, M.J.: A scalable approach to verifying safety properties of neural networks. In: International Con- ference on Computer Aided Verification (CAV). Springer (2016)

2016
[21]

and Julian, Kyle and Kochenderfer, Mykel J

Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: An efficient SMT solver for verifying deep neural networks. In: Majumdar, R., Kunčak, V. (eds.) Computer Aided Verification. pp. 97–117. Springer (2017).https://doi. org/10.1007/978-3-319-63387-9_5

work page doi:10.1007/978-3-319-63387-9_5 2017
[22]

Kochenderfer, M.J., Chryssanthacopoulos, J.P.: Robust airborne collision avoid- ance through dynamic programming. Tech. Rep. ATC-371, MIT Lincoln Labora- tory, Lexington, MA (Jan 2011),https://apps.dtic.mil/sti/pdfs/ADA537522. pdf, prepared for the Federal Aviation Administration

2011
[23]

In: 2019 IEEE/AIAA 38th Digital Avionics Systems Conference (DASC)

Lopez, J.G., Ren, L., Meng, B., Fisher, R., Markham, J., Figard, M., Evans, R., Spoelhof, R., Rubenstahl, M., Edwards, S., Pedan, I., Barrett, C.: Integration and flight test of small uas detect and avoid on a miniaturized avionics platform. In: 2019 IEEE/AIAA 38th Digital Avionics Systems Conference (DASC). pp. 1–5 (2019). https://doi.org/10.1109/DASC435...

work page doi:10.1109/dasc43569.2019.9081780 2019
[24]

McMillan, K.L.: Symbolic Model Checking. Ph.D. thesis, Carnegie Mellon Univer- sity (1993)

1993
[25]

In: Proceedings of the IEEE/ACM International Conference on Computer-Aided Design (ICCAD)

Rudell, R.E.: Dynamic variable ordering for ordered binary decision diagrams. In: Proceedings of the IEEE/ACM International Conference on Computer-Aided Design (ICCAD). pp. 42–47 (1993)

1993
[26]

Somenzi,F.:Cudd:Cudecisiondiagrampackage.Tech.rep.,UniversityofColorado at Boulder (1998)

1998
[27]

Stanford Intelligent Systems Laboratory: NNet: Documentation and scripts related to the .nnet file format (2025),https://github.com/sisl/NNet

2025
[28]

StarFive Technology Co., Ltd.: StarFive JH7110 SoC Datasheet (2026),https:// sizeof.cat/post/starfive-visionfive-2/files/docs/JH7110_Datasheet.pdf, hardware overview and technical specifications of the JH7110 RISC-V processor

2026
[29]

Xilinx, Inc.: Zynq ultrascale+ mpsoc data sheet: Overview. Tech. Rep. DS891, Xilinx, Inc. (Feb 2022), https://docs.xilinx.com/r/en-US/ ds891-zynq-ultrascale-plus-overview

2022