Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Michaël Cadilhac, Vanessa Flügel, Guillermo A. Pérez, Shrisha Rao

TL;DR

This work analyzes antichain data structures for finite downward-closed sets of vectors in $\mathbb{N}^k$, comparing list-, sharing-tree-, and kd-tree-based approaches. It shows kd-trees can be asymptotically superior when antichains grow exponentially relative to the dimension, but real-world verification benchmarks (LTL realizability and parity games) typically do not reach those regimes. The authors implement optimized, parallelized variants and provide empirical results indicating that list-based or sharing-tree-based structures often perform best or dominate in practice, with memory considerations favoring lists. The study offers practical guidance on selecting data structures and suggests dynamic switching strategies to blend representations depending on size, dimension, and problem instance characteristics.

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é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.

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

TL;DR

This work analyzes antichain data structures for finite downward-closed sets of vectors in , comparing list-, sharing-tree-, and kd-tree-based approaches. It shows kd-trees can be asymptotically superior when antichains grow exponentially relative to the dimension, but real-world verification benchmarks (LTL realizability and parity games) typically do not reach those regimes. The authors implement optimized, parallelized variants and provide empirical results indicating that list-based or sharing-tree-based structures often perform best or dominate in practice, with memory considerations favoring lists. The study offers practical guidance on selecting data structures and suggests dynamic switching strategies to blend representations depending on size, dimension, and problem instance characteristics.

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é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.

Paper Structure

This paper contains 41 sections, 15 theorems, 7 equations, 5 figures, 5 algorithms.

Table of Contents

  1. Introduction
  2. Our contributions.
  3. Preliminaries
  4. Antichain algorithms.
  5. Algorithm analysis.
  6. List-based antichain algorithms
  7. The membership problem
  8. The union operation
  9. The intersection operation
  10. Sharing-tree-based antichain algorithms
  11. Growing sharing trees
  12. The membership problem
  13. Covering sharing trees.
  14. The union and intersection operations
  15. $k$-d -tree-based antichain algorithms
  16. ...and 26 more sections

Key Result

proposition 1

Let $k \in \mathbb{N}_{>0}$, $u \in \mathbb{N}^k$, and a finite set $V \subset \mathbb{N}^k$. Then, $\vec{u} \in V \mathrm{\downarrow}$ if and only if $\vec{u} \leq \vec{v}$ for some $\vec{v} \in \lceil V \rceil$.

Figures (5)

  • Figure 1: Survival plots of downset-based LTL-realizability.
  • Figure 2: Survival plots of downset-based parity-game solving.
  • Figure 3: Survival plots of downset-based LTL-realizability focusing on the test cases that have at least one set that is in the top 5% in terms of ratio size vs. dimension.
  • Figure 4: Survival plot of $k$-d -tree-based parity-game solving.
  • Figure 5: Memory usage of data structures on parity games

Theorems & Definitions (20)

  • definition 1: Downset
  • definition 2: Antichain
  • proposition 1
  • proposition 2
  • proposition 3
  • lemma 1: DBLP:journals/fmsd/FiliotJR11
  • proposition 4
  • lemma 2: DBLP:journals/fmsd/FiliotJR11
  • proposition 5
  • definition 3: Sharing tree
  • ...and 10 more