Data Structures for Finite Downsets of Natural Vectors: Theory and Practice
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866910824895873024 |
|---|---|
| author | Cadilhac, Michaël Flügel, Vanessa Pérez, Guillermo A. Rao, Shrisha |
| author_facet | Cadilhac, Michaël Flügel, Vanessa Pérez, Guillermo A. Rao, Shrisha |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2502_09189 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Data Structures for Finite Downsets of Natural Vectors: Theory and Practice Cadilhac, Michaël Flügel, Vanessa Pérez, Guillermo A. Rao, Shrisha Logic in Computer Science Data Structures and Algorithms Formal Languages and Automata Theory 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. |
| title | Data Structures for Finite Downsets of Natural Vectors: Theory and Practice |
| topic | Logic in Computer Science Data Structures and Algorithms Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2502.09189 |