{"id":"247e9f35-dc7c-4d98-a1ab-72424b77500f","arxiv_id":"2502.09189","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"The paper gives new complexity bounds for list-, sharing-tree-, and k-d-tree-based antichain operations and shows empirically that current verification benchmarks do not favor k-d trees.","lead":"This paper compares three ways to store downward-closed sets of number vectors used in formal verification, and derives worst-case time bounds for membership, union, and intersection. The theory says k-d trees can beat plain lists when the set is exponentially larger than its dimension, but on current synthesis and parity-game benchmarks that rarely happens.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The stated k-d advantage threshold in §5.2/§5.5 is off by an exponential: the O(k^2 m^{1-1/k}) term only dominates when m ≥ k^k, not when m ≥ 2k log k, so the dynamic-switching recommendation is not theory-supported.","rationale":"The paper's core theoretical development is coherent: Theorem 3's region-counting argument for k-d tree membership is plausible, the list-based bounds are standard, and the sharing-tree construction and DFS bounds are internally consistent. The experiments are reported honestly, and the negative empirical finding about current benchmarks is credible as far as it goes. However, the threshold used to simplify the k-d tree bound and to justify dynamic switching is mathematically incorrect. The min in Theorem 3 is the second term only when m ≥ k^k, and the paper's '2k log k' is far too small. This matters because the practical claim 'dynamically switching from lists to k-d trees when 2k log k ≤ m ≤ n ≤ 2m can result in a good tradeoff' is exactly the bridge from the asymptotic theory to the implementation. The reader's verdict was already CONDITIONAL, and this concern reinforces the need for a revision rather than changing the overall assessment. I do not see a more load-bearing flaw in the central membership theorem itself, although the strict-membership queries used in union and intersection would deserve a fuller description, especially for the multiset of meets in Theorem 5. The threshold error is concrete, located, and testable, so it is the right focus for the stress-test pass.","tokens_in":20584,"tokens_out":36275,"duration_ms":393925,"concrete_test":"Check the threshold analytically: substitute m = 2k log k into the inequality k^2 m^{1-1/k} ≤ k m for k = 10 and k = 100; if the inequality fails, the stated threshold is wrong. Then re-run the dynamic-switching experiments from Section 6 with the corrected condition m ≥ k^k (for k = 10, m ≥ 10^10) to see whether the survival curves shift. Because the paper reports that even the over-eager threshold is rarely crossed, the empirical negative conclusion may survive, but the theoretical switching criterion in §5.5 must be revised.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Theorem 3 gives membership time O(min(km, k^2 m^{1-1/k})). The second term is the smaller one exactly when k^2 m^{1-1/k} ≤ k m, which is equivalent to k ≤ m^{1/k}, i.e. m ≥ k^k = 2^{k log k}. The paper instead states in Section 5.2 that the bound simplifies when m ≥ 2k log k, and Section 5.5 uses '2k log k' as the threshold for dynamically switching from lists to k-d trees. These are not equivalent, and the gap is exponential: for k=10, the paper's threshold is about 46, while k^k = 10^10. For m = 10^6, the claimed simplified bound O(k^2 m^{1-1/k}) is about 2.5×10^7, while the list bound km is 10^7, so switching would be predicted by the paper's criterion even though the k-d bound is theoretically worse. The full min bound in Theorem 3 is not itself invalidated, but the simplification threshold, the dynamic-switching recommendation, and the associated claim about when k-d trees become advantageous all rest on this incorrect inequality. The abstract's qualitative phrase 'exponentially larger' is compatible with the corrected condition only if 'exponentially larger' means m ≥ k^{c k} with c > 1; at m = k^k the two bounds are asymptotically equal, not strictly better.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":20825,"tokens_out":8251,"duration_ms":82305,"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":[{"comment":"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.","section":"Section 5.2, Theorem 3"},{"comment":"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.","section":"Sections 5.4 and 5.5"}],"minor_comments":[{"comment":"The definition of incomparability says 'neither u ≤ v nor u ≤ v'; the second inequality should be 'v ≤ u'.","section":"Definition 2"},{"comment":"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":"Section 4, opening"},{"comment":"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.","section":"Section 6.1"},{"comment":"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.","section":"Figures 1 and 2"}],"recommendation":"major_revision","confidential_remarks":"The threshold error is central enough to require a revision, but it is local and fixable: the min-form theorems can stand, while the simplification, the dynamic-switching recommendation, and the 'better than list assuming 2k log k' claims need to be corrected. After that correction, the paper's empirical message is likely to become stronger, since the corrected threshold is even harder to meet. I would also ask the authors to re-check the derived conditions in Theorems 4 and 5 once the threshold is fixed."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick take: the paper's core theoretical contribution is real and mostly right. The new k-d-tree membership bound with non-fixed dimension, O(min(km, k^2 m^{1-1/k})), is a genuine improvement over the fixed-dimension assumptions in the computational geometry literature, and the paper is honest about the negative empirical result on actual verification benchmarks. The complexity table for lists, sharing trees, and k-d trees is exactly what tool builders need.\n\nBut there is a load-bearing error in the simplification threshold. In §5.2 and again in §5.5, the paper says the bound simplifies to O(k^2 m^{1-1/k}) when m ≥ 2k log k, and uses that to recommend dynamically switching from lists to k-d trees. The algebra says otherwise: k^2 m^{1-1/k} ≤ km iff m ≥ k^k. For k=10, the paper's threshold is about 46, while k^k is 10^10. At m=10^6 the claimed simplified bound is about 2.5×10^7, worse than the list bound of 10^7, so the switching recommendation is not theory-supported. The min bound in Theorem 3 itself stands, and the qualitative claim that k-d trees win when antichains are exponentially larger than the dimension is consistent with m ≥ k^k. But the quantitative guidance is wrong and needs correction.\n\nSecond, the experiments cannot be reproduced from the submitted version: the text says source code and benchmarks will be made available after acceptance. That is a real caveat, given the paper's empirical claim is essentially a negative result about current workloads. The benchmark suite analysis (SYNTCOMP and Keiren) is thoughtful and the survival plots are readable, but it covers two application areas; the paper doesn't claim more than that.\n\nOn the positives, the sharing-tree antichain-ensuring analysis is new, the optimized k-d-tree construction (median computed per call instead of presorting) is a sensible response to dimension being part of the input, and the proof of Theorem 3, modulo the threshold issue, is coherent. The paper also cites prior work fairly, including its own TACAS 2023 paper.\n\nWho is this for? Verification tool builders who implement antichain-based algorithms and want complexity bounds that don't assume fixed dimension. It deserves a serious referee, but the revision needs to fix the threshold, correct the switching recommendation, and release the code and data.","headline":"Solid theoretical contribution with a real threshold bug in the simplification and a deferred-code caveat; worth refereeing but not in current form.","tokens_in":21421,"tokens_out":2478,"would_cite":true,"duration_ms":23642,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["antichain algorithms","downward-closed sets","k-d trees","sharing trees","membership problem","dimension-parameterized complexity","LTL realizability","parity games"],"falsifier":"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.","tokens_in":20346,"feed_emoji":"🌲","tokens_out":11413,"duration_ms":99889,"temperature":0.7,"pith_summary":"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.","feed_headline":"K-d trees beat lists only when antichains dwarf dimension","feed_subtitle":"Worst-case bounds predict the crossover; verification benchmarks rarely reach it.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"The computational-geometry textbook that supplies the k-d tree construction and the $O(m \\log m)$ building-time lemma.","marker":"[2]"},{"why":"The advanced-data-structures reference for the interesting-region counting argument used in the membership bound.","marker":"[6]"},{"why":"The prior LTL synthesis tool whose observation that simple k-d trees underperform lists motivated this study.","marker":"[7]"},{"why":"The prior k-d tree range-searching work whose fixed-dimension assumption the paper contrasts with its own.","marker":"[8]"},{"why":"The covering-sharing-tree representation used as an experimental baseline and architectural alternative.","marker":"[12]"},{"why":"The parity-game solver framework in which the downset-based algorithms are benchmarked.","marker":"[13]"},{"why":"The antichain algorithm for LTL synthesis whose union and intersection lemmas the paper reuses.","marker":"[19]"},{"why":"The reactive-synthesis competition benchmark suite used for the LTL experiments.","marker":"[25]"},{"why":"The parity-game benchmark suite used for the game-solving experiments.","marker":"[27]"},{"why":"The original sharing tree data structure that the sharing-tree algorithms are built from.","marker":"[31]"}],"fun_headline_variants":["K-d trees beat lists only when antichains dwarf dimension","Verification workloads rarely reach k-d tree's sweet spot","For k-d trees to win, antichains must outgrow dimension wildly","Antichain size must explode for k-d trees to outperform","Theory says k-d trees, but benchmarks stay in list territory"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["K-d trees beat lists only when antichains dwarf dimension","Verification workloads rarely reach k-d tree's sweet spot","For k-d trees to win, antichains must outgrow dimension wildly","Antichain size must explode for k-d trees to outperform","Theory says k-d trees, but benchmarks stay in list territory"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000244,"raw_usage":{"total_tokens":1538,"prompt_tokens":956,"completion_tokens":582,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":572,"completion_tokens_details":{"reasoning_tokens":493}},"tokens_in":572,"tokens_out":582,"duration_ms":5572,"temperature":1.0,"reasoning_tokens":493,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T22:21:10.895188+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"Cambridge University Press (2008).https: //doi.org/10.1017/CBO9780511800191","cited_arxiv_id":null,"evidence_quote":"The advanced-data-structures reference for the interesting-region counting argument used in the membership bound."},{"cited_title":"In: TACAS (2)","cited_arxiv_id":null,"evidence_quote":"The prior LTL synthesis tool whose observation that simple k-d trees underperform lists motivated this study."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The prior k-d tree range-searching work whose fixed-dimension assumption the paper contrasts with its own."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The covering-sharing-tree representation used as an experimental baseline and architectural alternative."},{"cited_title":"In: TACAS","cited_arxiv_id":null,"evidence_quote":"The parity-game solver framework in which the downset-based algorithms are benchmarked."},{"cited_title":"Formal Methods Syst","cited_arxiv_id":null,"evidence_quote":"The antichain algorithm for LTL synthesis whose union and intersection lemmas the paper reuses."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The reactive-synthesis competition benchmark suite used for the LTL experiments."},{"cited_title":"In: Dastani, M., Sirjani, M","cited_arxiv_id":null,"evidence_quote":"The parity-game benchmark suite used for the game-solving experiments."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The original sharing tree data structure that the sharing-tree algorithms are built from."}],"review_version":1}