REVIEW 2 major objections 4 minor 35 references
Data Structures for Finite Downsets of Natural Vectors: Theory and Practice
T0 review · 2 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash
Pith's one-line read This paper proves k-d trees outperform lists and sharing trees for antichains exactly when set size is exponential in dimension, and shows real verification benchmarks rarely hit that regime.
desk verdict Solid theoretical contribution with a real threshold bug in the simplification and a deferred-code caveat; worth refereeing but not in current form. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The central object is the k-d tree built by median splitting on cyclically rotating coordinates, searched with a region-based pruning algorithm that skips a subtree when the subtree's region lies entirely above the query vector. The argument's engine is the counting of ``$i$-interesting'' regions: for each dimension $i$, at most one child of any node can be interesting with respect to the query, and this dichotomy fails to double the node count at every $k$-th level, producing $O(m^{1-1/k})$ interesting nodes per dimension and hence the $O(k^2 m^{1-1/k})$ bound after accounting for per-leaf comparisons. The complementary object is the size-to-dimension ratio $m/k$, which the paper uses as the practical predictor of when the k-d tree's asymptotic advantage materializes.
What would settle it
Identify any antichain-based verification task, such as a Petri-net coverability check or an automaton inclusion check, whose measured antichains satisfy $m \geq 2^k$, and benchmark the three data structures on it: if k-d trees do not outperform lists there, the central complexity comparison fails in practice, while such a workload would directly contradict the paper's empirical generalization.
Extended reading notes
Core claim
The paper's central claim is that a k-d tree storing the $m$ maximal vectors of a downset in $\mathbb{N}^k$ supports membership queries in $O(\min(km, k^2 m^{1-1/k}))$ time, and that the same dimension-sensitive analysis carries over to union and intersection. The proof counts ``$i$-interesting'' regions to bound the number of visited tree nodes by $O(m^{1-1/k})$ per dimension, without assuming $k$ is fixed. Because of this, the k-d tree bounds beat the list-based $O(km)$ membership, $O(kmn)$ union, and $O(km^2n^2)$ intersection bounds precisely when $m$ is exponentially larger than $k$; when $m$ is only a constant multiple of $k$, the bounds coincide with or exceed the list bounds. The paper uses the threshold $m \geq 2k \log k$ to design a dynamic list/k-d-tree switching strategy and evaluates it on LTL synthesis and parity-game benchmarks, finding that the threshold is rarely crossed in those workloads.
Load-bearing premise
The empirical conclusion that current verification workloads do not favor k-d trees rests on the benchmarks used (the LTL synthesis and parity-game competition suites) being representative of antichain-heavy applications; if other applications produce antichains exponentially larger than their dimension, the practical verdict could reverse.
Editorial extensions
If this is right
- Membership in a downset stored as a k-d tree costs $O(\min(km, k^2 m^{1-1/k}))$, which improves on the $O(km)$ needed by lists and sharing trees when $m$ is exponentially larger than $k$.
- Union of antichains of sizes $m \leq n$ runs in $O(kn \min(m, k m^{1-1/k}) + n \log n)$, beating the list-based $O(kmn)$ in the same exponential regime when $n \leq 2m$.
- Intersection runs in $O(kmn \min(mn, k(mn)^{1-1/k}))$, improving over the list-based $O(km^2n^2)$ under the same size-dimension condition.
- A dynamic switch from lists to k-d trees at the threshold $m \geq 2k \log k$ is theoretically sound, but on the tested LTL synthesis and parity-game benchmarks the threshold is crossed rarely, so the switch tracks list performance.
- Sharing trees and covering sharing trees trail both lists and k-d trees on the experimental workloads, both in solved instances and in memory usage.
Reading between the lines
- A natural next step is to benchmark the same three data structures on antichain-heavy workloads whose size-to-dimension ratio is deliberately varied, which would measure the constant factors behind the $m \geq 2k \log k$ crossover and produce a practical decision rule for when to switch.
- The same interesting-region counting technique likely transfers to other orthogonal range-searching structures, so data structure libraries for verification might be designed around dimension-parameterized bounds rather than fixed-dimension heuristics.
- If future antichain benchmarks from Petri-net coverability or automata inclusion turn out to have exponentially larger antichains, the paper's theoretical results predict k-d trees would win there; this is a testable prediction, not something the paper measured.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper studies data structures for representing finite downsets of natural vectors through their antichains of maximal elements. It analyzes worst-case running times, in the RAM model with k part of the input, for membership, union, and intersection, comparing list-based algorithms, sharing-tree-based algorithms using Zampuniéris's sharing trees, and k-d-tree-based algorithms. The main theoretical result is Theorem 3, an O(min(km, k^2 m^{1-1/k})) membership bound for k-d trees, from which the paper derives union and intersection bounds and concludes that k-d trees are asymptotically better than lists and sharing trees when antichains are exponentially larger than the dimension. The paper also implements the algorithms in C++ and evaluates them on LTL-realizability benchmarks from SYNTCOMP and on parity-game benchmarks, reporting that current benchmarks do not favor k-d trees and that list-based implementations remain competitive or better.
Significance. If the theoretical analysis is correct, this is a useful contribution: it is one of the few systematic, dimension-sensitive complexity studies of antichain data structures, and it gives clean worst-case bounds without treating the dimension as a constant. The paper also makes a valuable empirical point by measuring, on real verification workloads, the size-versus-dimension ratios of the antichains that actually arise, and by honestly reporting a negative result for k-d trees instead of overclaiming. The proofs are coherent and the complexity bounds are derived from first principles with no fitted parameters. However, one load-bearing threshold claim in the simplification of Theorem 3 is wrong, and because that threshold is reused for the dynamic-switching recommendation and for the claimed superiority of the union and intersection algorithms, the paper needs a substantive correction before the theoretical conclusions can be accepted in their current form.
major comments (2)
- [Section 5.2, Theorem 3] The statement that the bound O(min(km, k^2 m^{1-1/k})) 'simplifies to O(k^2 m^{1-1/k}) if m ≥ 2k log k' is incorrect. The second term is at most the first exactly when k^2 m^{1-1/k} ≤ km, which is equivalent to k ≤ m^{1/k}, i.e. m ≥ k^k = 2^{k log k}. For example, for k=10 the paper's threshold is about 46, while k^k = 10^10; at m=10^6 the list bound km = 10^7 is smaller than k^2 m^{1-1/k} ≈ 2.5×10^7, so the paper's criterion would treat the k-d tree term as active when it is not. This invalidates the simplification and the 'Henceforth, to simplify our analysis, we will assume this inequality holds' remark in Section 5.2.
- [Sections 5.4 and 5.5] The same incorrect threshold is load-bearing for the comparative claims and for the implementation advice. The statement after Theorem 4 that the dynamic switch from lists to k-d trees is supported when 2k log k ≤ m ≤ n ≤ 2m, and the statement after Theorem 5 that the intersection bound is better than the list bound assuming 2k log k ≤ m, n, both rely on the false simplification. The k-d term in the union bound is better than the list term only when m ≥ k^k, and the k-d term in the intersection bound is better only when mn ≥ k^k. The full min-form statements of Theorems 3–5 may still be correct, but the threshold-based conclusions in Section 5.5 and the interpretation of the experiments as showing that 'the threshold provided by the theory is rarely crossed' must be re-derived with the corrected threshold. The negative empirical conclusion may survive, but it is not currently supported by the theory as stated.
minor comments (4)
- [Definition 2] The definition of incomparability says 'neither u ≤ v nor u ≤ v'; the second inequality should be 'v ≤ u'.
- [Section 4, opening] The phrase 'A is a (finite) regular language' is informal: a set of fixed-length vectors is a finite set of words, and the sharing tree is its minimal acyclic DFA. This is understandable but could be phrased more precisely.
- [Section 6.1] The text says experiments 'were carried on' a CPU; this should be 'carried out on'. There are also a few grammatical slips in Section 7, e.g. 'We provided a theoretical analysis of two data structures' immediately before three structures are listed.
- [Figures 1 and 2] The survival plots are informative, but the captions do not state the timeout or the number of instances omitted from the displayed range. Adding these details in the captions would make the figures self-contained.
Circularity Check
No circularity: complexity bounds derived from first principles; self-citation is comparative and self-corrective.
full rationale
The paper's central theoretical claims, especially Theorem 3's k-d-tree membership bound, are derived from first principles in the RAM model using standard external k-d tree analyses (de Berg et al. [2] and Brass [6]). The bound is obtained by counting nodes with 'i-interesting' regions and is not obtained from the empirical data. The empirical benchmarks in Section 6 are used only for evaluation and comparison, not to fit any parameter of the algorithms; the dynamic-switching threshold in Section 5.5 is derived from the theoretical bound rather than calibrated to measurements. The paper's use of the authors' prior work [7] is comparative: it reports that the new optimized implementation improves on the older Acacia-Bonsai k-d tree implementation and that k-d trees still do not beat list-based antichains. This is a self-corrective check, not a load-bearing self-citation. No prediction is equivalent by construction to a fitted input, no uniqueness theorem is imported from the authors' own work, and the sharing-tree analysis is grounded in the independently known minimal-DFA/sharing-tree literature [31,12]. The only notable concern is a mathematical error in the simplification threshold: Section 5.2 states the O(k^2 m^{1-1/k}) bound applies when m >= 2k log k, but comparing with the O(km) list bound shows the crossover actually occurs around m >= k^k. This is an error in applying the derived bound, not a circularity; the full min bound in Theorem 3 remains a first-principles result. Accordingly, no circular step is exhibited.
Assumptions & free parameters
assumptions (4)
- domain assumption RAM model with constant-time comparisons of natural numbers and constant-time indirect addressing (Section 'Algorithm analysis').
- standard math Dickson's lemma: every antichain of natural vectors is finite (used in Definition 2).
- standard math A k-d tree built by ≺-median splits has depth O(log m) [2, Lemma 5.3] (used in Lemma 4 and Theorem 3).
- domain assumption SYNTCOMP and Keiren benchmarks are representative of antichain workloads in formal verification (assumed in the empirical conclusions of Section 6).
Cite this review
Pith. "Pith review of Data Structures for Finite Downsets of Natural Vectors: Theory and Practice." pith.science (2026). https://pith.science/paper/PHZK7XSO
@misc{pith2026250209189,
author = {Pith},
title = {Pith review of: Data Structures for Finite Downsets of Natural Vectors: Theory and Practice},
year = {2026},
howpublished = {\url{https://pith.science/paper/PHZK7XSO}},
note = {Machine review of arXiv:2502.09189}
}
read the original 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.
Figures
Reference graph
Works this paper leans on
-
[1]
MIT Press (2008)
Baier, C., Katoen, J.: Principles of model checking. MIT Press (2008)
2008
-
[2]
Springer (2008), https:// www.worldcat.org/oclc/227584184
de Berg, M., Cheong, O., van Kreveld, M.J., Overmars, M.H.: Computational geometry: algorithms and applications, 3rd Edition. Springer (2008), https:// www.worldcat.org/oclc/227584184
arXiv 2008
-
[3]
Bernet, J., Janin, D., Walukiewicz, I.: Permissive strategies: from parity games to safety games. RAIRO Theor. Informatics Appl.36(3), 261–275 (2002).https: //doi.org/10.1051/ITA:2002013, https://doi.org/10.1051/ita:2002013
-
[4]
Berwanger, D., Chatterjee, K., Wulf, M.D., Doyen, L., Henzinger, T.A.: Strategy construction for parity games with imperfect information. Inf. Comput.208(10), 1206–1220 (2010)
work page 2010
-
[5]
Blumer, A., Blumer, J., Ehrenfeucht, A., Haussler, D., McConnell, R.M.: Linear size finite automata for the set of all subwords of a word - an outline of results. Bull. EATCS21, 12–20 (1983)
work page 1983
-
[6]
Cambridge University Press (2008).https: //doi.org/10.1017/CBO9780511800191
Brass, P.: Advanced Data Structures. Cambridge University Press (2008).https: //doi.org/10.1017/CBO9780511800191
-
[7]
Cadilhac, M., Pérez, G.A.: Acacia-bonsai: A modern implementation of downset- based LTL realizability. In: TACAS (2). Lecture Notes in Computer Science, vol. 13994, pp. 192–207. Springer (2023)
work page 2023
-
[8]
Chan, T.M.: Orthogonal range searching in moderate dimensions: k-d trees and range trees strike back. Discret. Comput. Geom. 61(4), 899–922 (2019). https://doi.org/10.1007/S00454-019-00062-5, https://doi.org/10. 1007/s00454-019-00062-5
Show all 35 references
-
[9]
(eds.): Handbook of Model Checking
Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer (2018). https://doi.org/10.1007/978-3-319-10575-8 , https://doi.org/10.1007/978-3-319-10575-8
2018 doi
-
[10]
Daciuk, J., Mihov, S., Watson, B.W., Watson, R.E.: Incremental construc- tion of minimal acyclic finite state automata. Comput. Linguistics 26(1), 3– 16 (2000). https://doi.org/10.1162/089120100561601, https://doi.org/10. 1162/089120100561601
2000 doi
-
[11]
Daskalakis, C., Karp, R.M., Mossel, E., Riesenfeld, S.J., Verbin, E.: Sorting and selection in posets. SIAM J. Comput.40(3), 597–622 (2011). https://doi.org/ 10.1137/070697720, https://doi.org/10.1137/070697720
2011 doi
-
[12]
Delzanno, G., Raskin, J., Begin, L.V.: Covering sharing trees: a compact data structure for parameterized verification. Int. J. Softw. Tools Technol. Transf. 5(2-3), 268–297 (2004). https://doi.org/10.1007/S10009-003-0110-0, https: //doi.org/10.1007/s10009-003-0110-0
2004 doi
-
[13]
In: TACAS
van Dijk, T.: Oink: An implementation and evaluation of modern parity game solvers. In: TACAS. Lecture Notes in Computer Science, vol. 10805, pp. 291–
-
[14]
In: Finkbeiner, B., Kovács, L
van Dijk, T., van Abbema, F., Tomov, N.: Knor: reactive synthesis using oink. In: Finkbeiner, B., Kovács, L. (eds.) Tools and Algorithms for the Construc- tion and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences o...
2024 doi
-
[15]
In: TACAS (1)
Doveri, K., Ganty, P., Hadzi-Dokic, L.: Antichains algorithms for the inclusion problem between omega-VPL. In: TACAS (1). Lecture Notes in Computer Science, vol. 13993, pp. 290–307. Springer (2023)
2023
-
[16]
Doyen, L., Raskin, J.: Antichains for the automata-based approach to model- checking. Log. Methods Comput. Sci.5(1) (2009)
2009
-
[17]
In: Lectures in Game Theory for Computer Scientists, pp
Doyen, L., Raskin, J.: Games with imperfect information: theory and algorithms. In: Lectures in Game Theory for Computer Scientists, pp. 185–212. Cambridge University Press (2011)
2011
-
[18]
Falgas-Ravry, V., Räty, E., Tomon, I.: Dedekind’s problem in the hypergrid (2023), https://arxiv.org/abs/2310.12946
2023 arXiv
-
[19]
Formal Methods Syst
Filiot, E., Jin, N., Raskin, J.: Antichains and compositional algorithms for LTL synthesis. Formal Methods Syst. Des.39(3), 261–296 (2011)
2011
-
[20]
Master’s thesis, Université Libre de Bruxelles, Belgium (2002)
Ganty, P.: Algorithmes et Structures de Données Efficaces Pour La Manipulation de Contraintes Sur Les Intervalles (in French). Master’s thesis, Université Libre de Bruxelles, Belgium (2002)
2002
-
[21]
Ganty, P., Meuter, C., Delzanno, G., Kalyon, G., Raskin, J., Van Begin, L.: Sym- bolic Data Structure for sets of k-uples. Tech. Rep. 570, Université Libre de Brux- elles, Belgium (2007)
2007
-
[22]
Formal Methods Syst
Holík, L., Iosif, R., Rogalewicz, A., Vojnar, T.: Abstraction refinement and an- tichains for trace inclusion of infinite state systems. Formal Methods Syst. Des. 55(3), 137–170 (2020)
2020
-
[23]
In: Champarnaud, J., Maurel, D
Holub, J., Crochemore, M.: On the implementation of compact dawg’s. In: Champarnaud, J., Maurel, D. (eds.) Implementation and Application of Au- tomata, 7th International Conference, CIAA 2002, Tours, France, July 3-5, 2002, Revised Papers. Lecture Notes in Computer Science, v...
2002
-
[24]
Acta Informatica 55(8), 627–647 (2018)
Hunter,P.,Pérez,G.A.,Raskin,J.:Lookingatmeanpayoffthroughfoggywindows. Acta Informatica 55(8), 627–647 (2018)
2018
-
[25]
Jacobs, S., Pérez, G.A., Abraham, R., Bruyère, V., Cadilhac, M., Colange, M., Delfosse, C., van Dijk, T., Duret-Lutz, A., Faymonville, P., Finkbeiner, B., Khalimov, A., Klein, F., Luttenberger, M., Meyer, K.J., Michaud, T., Pom- mellet, A., Renkin, F., Schlehuber-Caissier, P.,...
2024 doi
-
[26]
In: Reichel, H., Tison, S
Jurdzinski, M.: Small progress measures for solving parity games. In: Reichel, H., Tison, S. (eds.) STACS 2000, 17th Annual Symposium on Theoretical Aspects of Computer Science, Lille, France, February 2000, Proceedings. Lecture Notes in Computer Science, vol. 1770, pp. 290–30...
2000 doi
-
[27]
In: Dastani, M., Sirjani, M
Keiren, J.J.A.: Benchmarks for parity games. In: Dastani, M., Sirjani, M. (eds.) Fundamentals of Software Engineering. pp. 127–142. Springer International Pub- lishing, Cham (2015)
2015
-
[28]
Laveaux, M., Groote, J.F., Willemse, T.A.C.: Correct and efficient antichain algorithms for refinement checking. Log. Methods Comput. Sci. 17(1) (2021), https://lmcs.episciences.org/7143
2021
-
[29]
Revuz, D.: Minimisation of acyclic deterministic automata in linear time. Theor. Comput. Sci. 92(1), 181–189 (1992). https://doi.org/10.1016/0304-3975(92) 90142-3, https://doi.org/10.1016/0304-3975(92)90142-3 Data Structures for Finite Downsets of Natural Vectors 21
1992 doi
-
[30]
In: ICFEM
Wang, T., Song, S., Sun, J., Liu, Y., Dong, J.S., Wang, X., Li, S.: More anti- chain based refinement checking. In: ICFEM. Lecture Notes in Computer Science, vol. 7635, pp. 364–380. Springer (2012)
2012
-
[31]
Zampuniéris, D.: The Sharing Tree Data Structure, Theory and Applications in Formal Verification. Ph.D. thesis, PhD thesis, Department of Computer Science, University of Namur, Belgium (1997) 22 M. Cadilhac et al. A Membership: best and worst-case scenarios Here we give intuit...
1997
-
[34]
This makes comparing the complexity of algorithms on covering sharing trees with the others studied in this work rather hard
Covering sharing trees may encode more than just the antichain of maximal elements.Indeed,duetothe approximate dominationchecksproposedin[12], some dominated vectors are not excluded from the encoded set. This makes comparing the complexity of algorithms on covering sharing tr...
-
[35]
deep and narrow
Algorithms to operate over two covering sharing trees, as proposed in [12], are much more graph-based. Indeed, these resemble binary decision diagram algorithms. In contrast the algorithms proposed in this work revert to iterat- ing over the encoded vectors for union and inter...
-
[294]
https://doi.org/10.1007/3-540-44977-9_31, https:// doi.org/10.1007/3-540-44977-9_31
Springer (2002). https://doi.org/10.1007/3-540-44977-9_31, https:// doi.org/10.1007/3-540-44977-9_31
2002 doi
-
[308]
Springer (2018).https://doi.org/10.1007/978-3-319-89960-2_16 , https: //doi.org/10.1007/978-3-319-89960-2_16
2018 doi
Reviewed August 7, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.