Pith. sign in

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 →

arxiv 2502.09189 v1 pith:PHZK7XSO submitted 2025-02-13 cs.LO cs.DScs.FL

classification cs.LOcs.DScs.FL
keywords antichainalgorithmsdownward-closedsetsk-dtreessharingmembershipproblemdimension-parameterizedcomplexityLTLrealizabilityparitygames
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Antichain-based verification algorithms store downward-closed sets of natural vectors by keeping only their maximal elements, and they repeatedly test membership, union, and intersection of these antichains. This paper gives a complexity analysis of the standard list-based, sharing-tree-based, and k-d-tree-based data structures for these operations that, unlike the existing literature, treats the dimension $k$ as part of the input rather than as a fixed constant. The central theoretical result is a k-d tree membership algorithm running in $O(\min(km, k^2 m^{1-1/k}))$ time for an antichain of size $m$, from which the paper derives union and intersection bounds. These bounds imply that k-d trees are asymptotically better than lists and sharing trees when the antichain size $m$ is exponentially larger than $k$. The empirical part measures the size-to-dimension ratio on benchmark suites from reactive-system synthesis and parity games and finds that current workloads rarely reach that regime, which explains why k-d trees underperform lists in practice.

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.

Watch

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

Editorial extensions of the paper, not claims the author makes directly.

  • 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.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 4 minor

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)
  1. [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.
  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)
  1. [Definition 2] The definition of incomparability says 'neither u ≤ v nor u ≤ v'; the second inequality should be 'v ≤ u'.
  2. [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.
  3. [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.
  4. [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

0 steps flagged · score 0.0 of 10

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 0 free parameters · 4 assumptions · 0 invented entities

The paper introduces no new physical or mathematical entities. The data structures analyzed are existing or novel algorithmic constructs, not postulated objects. The axioms listed are the standard model of computation, Dickson's lemma, the known balance property of median-split k-d trees, and the representativeness of the chosen benchmarks.

assumptions (4)
  • domain assumption RAM model with constant-time comparisons of natural numbers and constant-time indirect addressing (Section 'Algorithm analysis').
    All complexity bounds in the paper depend on this computational model. It is standard for algorithm analysis but is an assumption about the machine.
  • standard math Dickson's lemma: every antichain of natural vectors is finite (used in Definition 2).
    This justifies representing a downset by its finite antichain of maximal elements.
  • 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).
    The balanced structure of the k-d tree underlies the O(m^{1-1/k}) bound on interesting nodes.
  • domain assumption SYNTCOMP and Keiren benchmarks are representative of antichain workloads in formal verification (assumed in the empirical conclusions of Section 6).
    The empirical claim that k-d trees are rarely advantageous in practice relies on these benchmarks reflecting typical conditions.

how reviews work

0 comments
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

Figures reproduced from arXiv: 2502.09189 by the authors.

Figure 1
Figure 1. Survival plots of downset-based LTL-realizability. [PITH_FULL_IMAGE:figures/full_fig_p015_1.png] view at source ↗
Figure 2
Figure 2. Survival plots of downset-based parity-game solving. [PITH_FULL_IMAGE:figures/full_fig_p018_2.png] view at source ↗
Figure 3
Figure 3. Survival plots of downset-based LTL-realizability focusing on the test [PITH_FULL_IMAGE:figures/full_fig_p027_3.png] view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: Survival plot of k-d-tree-based parity-game solving [PITH_FULL_IMAGE:figures/full_fig_p027_4.png]
Figure 5
Figure 5. Figure 5: Memory usage of data structures on parity games [PITH_FULL_IMAGE:figures/full_fig_p028_5.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

35 extracted references · 28 canonical work pages

  1. [1]

    MIT Press (2008)

    Baier, C., Katoen, J.: Principles of model checking. MIT Press (2008)

  2. [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

  3. [3]

    RAIRO Theor

    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. [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)

  5. [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)

  6. [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. [7]

    In: TACAS (2)

    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)

  8. [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
  1. [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

  2. [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

  3. [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

  4. [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

  5. [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–

  6. [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...

  7. [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)

  8. [16]

    Doyen, L., Raskin, J.: Antichains for the automata-based approach to model- checking. Log. Methods Comput. Sci.5(1) (2009)

  9. [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)

  10. [18]

    Falgas-Ravry, V., Räty, E., Tomon, I.: Dedekind’s problem in the hypergrid (2023), https://arxiv.org/abs/2310.12946

  11. [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)

  12. [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)

  13. [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)

  14. [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)

  15. [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...

  16. [24]

    Acta Informatica 55(8), 627–647 (2018)

    Hunter,P.,Pérez,G.A.,Raskin,J.:Lookingatmeanpayoffthroughfoggywindows. Acta Informatica 55(8), 627–647 (2018)

  17. [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.,...

  18. [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...

  19. [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)

  20. [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

  21. [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

  22. [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)

  23. [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...

  24. [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...

  25. [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...

  26. [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

  27. [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

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.