Compressing ACAS-Xu Lookup Tables with Binary Decision Diagrams

• URL: http://arxiv.org/abs/2604.27008v1
• Date: Wed, 29 Apr 2026 09:14:53 GMT
• Title: Compressing ACAS-Xu Lookup Tables with Binary Decision Diagrams
• Abstract summary: This paper presents a symbolic compression approach based on Binary Decision Diagrams (BDDs) that preserves the exact semantics of the ACAS-Xu LUTs.<n>The resulting representation is canonical, deterministic, and fully equivalent to the original tables.<n>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.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Neural Information Causality [0.0]
  We develop a framework called neural information causality (Neural-IC)<n>We show that Neural-IC is an operational diagnostic for query leakage, precision leakage, and episode-specific memory.<n>We also provide an exact one-bit classical RAC benchmark, showing explicitly that the relevant quantum enhancement is not total information beyond the bottleneck.
  arXiv  Detail & Related papers  (2026-05-10T04:25:11Z)
• Calibrated Speculative Decoding: Frequency-Guided Candidate Selection for Efficient Inference [27.59556627479635]
  Calibrated Speculative Decoding recovers valid tokens discarded by standard verification.<n>Online Correction Memory aggregates historical rejections to propose recurring divergence patterns as rescue candidates.<n>Semantic Consistency Gating verifies candidate admissibility using probability ratios instead of exact token matching.
  arXiv  Detail & Related papers  (2026-04-15T09:01:54Z)
• Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification [49.506412445511934]
  Large Language Models (LLMs) show remarkable capabilities, yet their next-token prediction creates logical inconsistencies and reward hacking.<n>We introduce a formal logic verification-guided framework that dynamically interleaves formal symbolic verification with the natural language generation process.<n>We operationalize this framework via a novel two-stage training pipeline that synergizes formal logic verification-guided supervised fine-tuning and policy optimization.
  arXiv  Detail & Related papers  (2026-01-30T07:01:25Z)
• Accelerate Speculative Decoding with Sparse Computation in Verification [49.74839681322316]
  Speculative decoding accelerates autoregressive language model inference by verifying multiple draft tokens in parallel.<n>Existing sparsification methods are designed primarily for standard token-by-token autoregressive decoding.<n>We propose a sparse verification framework that jointly sparsifies attention, FFN, and MoE components during the verification stage to reduce the dominant computation cost.
  arXiv  Detail & Related papers  (2025-12-26T07:53:41Z)
• Randomized Smoothing Meets Vision-Language Models [6.224335082856828]
  Randomized smoothing (RS) is used to ensure correctness of machine learning models.<n>We show that RS can still be enabled for generative models.<n>We derive improved scaling laws analytically relating the certified radius and accuracy to the number of samples.<n>These advances make robustness certification both well-defined and computationally feasible for state-of-the-art VLMs.
  arXiv  Detail & Related papers  (2025-09-19T15:33:22Z)
• AutoLayout: Closed-Loop Layout Synthesis via Slow-Fast Collaborative Reasoning [102.71841660031065]
  Auto is a fully automated method that integrates a closed-loop self-validation process within a dual-system framework.<n>The effectiveness of Auto was validated across 8 distinct scenarios, where it demonstrated a significant 10.1% improvement over SOTA methods.
  arXiv  Detail & Related papers  (2025-07-06T08:35:22Z)
• Pseudo-Boolean Proof Logging for Optimal Classical Planning [9.688823478031852]
  We describe a general framework for generating lower-bound certificates based on pseudo-Boolean constraints.<n>We show how to modify the $A*$ algorithm to produce proofs of optimality with modest overhead.
  arXiv  Detail & Related papers  (2025-04-25T15:54:09Z)
• Bisimulation Learning [55.859538562698496]
  We compute finite bisimulations of state transition systems with large, possibly infinite state space. Our technique yields faster verification results than alternative state-of-the-art tools in practice.
  arXiv  Detail & Related papers  (2024-05-24T17:11:27Z)
• Mitigating Algorithmic Bias with Limited Annotations [65.060639928772]
  When sensitive attributes are not disclosed or available, it is needed to manually annotate a small part of the training data to mitigate bias. We propose Active Penalization Of Discrimination (APOD), an interactive framework to guide the limited annotations towards maximally eliminating the effect of algorithmic bias. APOD shows comparable performance to fully annotated bias mitigation, which demonstrates that APOD could benefit real-world applications when sensitive information is limited.
  arXiv  Detail & Related papers  (2022-07-20T16:31:19Z)
• Optimizing Binary Decision Diagrams with MaxSAT for classification [3.2894524838755608]
  A growing interest in explainable artificial intelligence motivates the need for interpretable machine learning (ML) models. Recently, several exact methods for computing such models are proposed to overcome weaknesses of traditional methods. In this paper, we first propose SAT-based models for learning optimal Binary decision diagrams (BDDs) Then, we lift the encoding to a MaxSAT model to learn optimal BDDs in limited depths. Finally, we tackle the fragmentation problem by introducing a method to merge compatible subtrees for the BDDs found via the MaxSAT model.
  arXiv  Detail & Related papers  (2022-03-21T23:17:37Z)
• Probabilistic Case-based Reasoning for Open-World Knowledge Graph Completion [59.549664231655726]
  A case-based reasoning (CBR) system solves a new problem by retrieving cases' that are similar to the given problem. In this paper, we demonstrate that such a system is achievable for reasoning in knowledge-bases (KBs) Our approach predicts attributes for an entity by gathering reasoning paths from similar entities in the KB.
  arXiv  Detail & Related papers  (2020-10-07T17:48:12Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.