Data Structures for Finite Downsets of Natural Vectors: Theory and Practice

TL;DR

This paper analyzes and compares data structures for manipulating downward-closed sets of vectors, showing kdtrees' asymptotic advantages in certain conditions, with empirical evaluation in reactive system synthesis.

Contribution

It provides a formal complexity analysis of various antichain algorithms, including novel kd-tree approaches, without fixing vector dimension, and evaluates their practical performance.

Findings

kdtrees outperform list- and sharing-tree algorithms asymptotically

Current benchmarks do not favor kd-tree implementations in practice

Analysis extends to variable vector dimensions in verification contexts

Abstract

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\'eris'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.