2025/02/13 by Michaël Cadilhac, Cadilhac, Michaël, Vanessa Flügel +5 · 1 citation
Computer Science · Decision Sciences · #Advanced Database Systems and Queries #Data Structures and Algorithms (cs.DS) #Distributed and Parallel Computing Systems #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Logic in Computer Science (cs.LO) #Simulation Techniques and Applications
paper · pdf · doi:10.48550/arxiv.2502.09189
openalex publication_date 2025/02/13 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Manipulating downward-closed sets of vectors forms the basis of so-called antichain-based algorithms in verification. In that context, the dimension of the vectors is intimately tied to the size of the input structure to be verified. In this work, we formally analyze the complexity of classical list-based algorithms to manipulate antichains as well as that of Zampuniéris's sharing trees and traditional and novel kdtree-based antichain algorithms. In contrast to the existing literature, and to better address the needs of formal verification, our analysis of \kdtree algorithms does not assume that the dimension of the vectors is fixed. Our theoretical results show that kdtrees are asymptotically better than both list- and sharing-tree-based algorithms, as an antichain data structure, when the antichains become exponentially larger than the dimension of the vectors. We evaluate this on applications in the synthesis of reactive systems from linear-temporal logic and parity-objective specifications, and establish empirically that current benchmarks for these computational tasks do not lead to a favorable situation for current implementations of kdtrees.