有限向量下downset的数据结构：理论与实践
计算机科学中的逻辑
2025-02-14 v1 数据结构与算法
形式语言与自动机理论
摘要
操作向下封闭的向量集合是所谓基于反链的算法的基础，这些算法在验证领域得到广泛应用。在该语境下，向量的维数与要验证的输入结构的规模密切相关。本文正式分析了经典基于列表的算法以及Zampunieri的共享树以及传统和新颖的kdtree-based反链算法的复杂度。与现有文献不同，为了更好地满足形式化验证的需求，我们的kdtree算法分析不假设向量的维数是固定的。我们的理论结果表明，当反链的数据结构在向量维数指数级增大时，kdtree在数据结构层面上均 asymptotically 优于基于列表和共享树的算法。我们在从线性时序逻辑和奇偶目标规范合成响应系统的应用中进行了评估，并在实证上确立了当前基准对于kdtree实现的当前情况并不利。
引用
@article{arxiv.2502.09189,
title = {Data Structures for Finite Downsets of Natural Vectors: Theory and Practice},
author = {Michaël Cadilhac and Vanessa Flügel and Guillermo A. Pérez and Shrisha Rao},
journal= {arXiv preprint arXiv:2502.09189},
year = {2025}
}