{"id":"abb3c878-7f9b-4114-9cbe-3f85a79fec5d","arxiv_id":"2505.13749","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"For each fixed Presburger target set, reachability in integer, natural, and VASS one-counter systems is provably either NP-complete or in AC1, with a decidable criterion deciding which.","lead":"This paper proves that for one-counter automata, reachability to any fixed Presburger-definable target set is either NP-complete or solvable in AC1, a small parallel complexity class inside polynomial time, and that deciding which case applies is also decidable. Reading it is worthwhile because it unifies the previously separate reachability and coverability questions and improves the known upper bound for 1-VASS coverability from NC2 to AC1.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant objection identified; the dichotomy proofs, including the flagged harbor-chain step and the AC1 coverability algorithm, survive close reading.","rationale":"The reader's verdict was ACCEPT with moderate confidence, and the reader identified Proposition V.9 as the weakest assumption. After a good-faith close reading, I found no internal inconsistency or missing proof that would threaten the central claim. The density dichotomy is structured around the equivalence of positive local density, absence of unbounded isolation, and decomposability into transformed building blocks; the proofs in the appendices support the main-text sketches, and the WQO/ideal-decomposition machinery is applied in a way that appears sound, especially once one observes that in the no-unbounded-isolation case infinite gaps cannot occur. The NP-hardness reductions from subset sum are standard and the logspace reductions to acyclic automata are backed by Eisenbrand-Shmonin and Presburger solution-size bounds. The VASS coverability result, which improves NC2 to AC1, is the most surprising claim; I examined the semiring of coverability functions, the role of the amplitude approximation, and the induction for Proposition VII.5. The proof is intricate but the key inequalities A0^{2k} <= Ak Ak <= A0^{3k} hold on the checked examples, and the algorithm's acyclic reduction with positive-cycle pumping is plausible. I therefore do not raise a load-bearing concern. The verdict should remain UNCHANGED; the flagged step is still the right place for further external verification, which is why agreement_with_reader is partial rather than full agreement on the existence of a concern.","tokens_in":55346,"tokens_out":44114,"duration_ms":432598,"concrete_test":"Independently re-derive Lemma V.13 and its use of the ideal decomposition, testing the uniform rho = 2R(m+1) on a parametric family of interval-uniform sets; a failure would show up as a semilinear S with no unbounded isolation that cannot be decomposed into transformed building blocks.","verdict_should_be":"UNCHANGED","load_bearing_attack":"I read the paper as claiming three dichotomies for semilinear target sets, with the most intricate unmechanized step being Proposition V.9, specifically the implication (2) => (3) via ratio ideals and the harbor-chain Lemma V.13. I could not identify a concrete failure in this step. In the relevant direction, absence of unbounded isolation rules out infinite gaps, so the ratio matrices are finite and the ideal decomposition supplies a well-defined constant R; the choice rho = 2R(m+1) is then used uniformly. The proof of Lemma V.13 appears internally consistent: if both nearest larger intervals were too far, two large gaps would induce an omega-constellation, which is exactly the forbidden pattern. I also checked the VASS coverability argument, since the claimed AC1 bound for 1-VASS coverability is the headline concrete contribution. The iteration in Section VII.B and the semiring proof of Proposition VII.5 were tested on small examples, including a path with weights -2, +1, +1; the reconstruction works because the intermediate transitions are retained across iterations, so the composed table recovers the exact coverability function. No load-bearing concern emerged.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes and proves complexity dichotomies for a family of reachability problems in one-counter systems, where the target configuration is specified by a fixed Presburger formula φ(t,x) relating a parameter vector t to the counter value x. Three models are considered: integer semantics (Z-VASS), natural semantics (Parikh automata), and non-negative VASS semantics. In each case, the paper shows that φ-reachability is either NP-complete or in AC^1, and that the side of the dichotomy is decidable from a formula for the target set. The tractable side is characterized by positive local density D(S) for integer semantics, positive local+ density D_+(S) for natural semantics, and uniform quasi-upward closedness for VASS semantics. A highlight is an AC^1 algorithm for coverability in 1-VASS, improving the previous NC^2 upper bound. The proofs introduce several new tools: ratio ideals and ω-constellations, ρ-chains of intervals, a Laurent-polynomial quotient semiring, and a semiring of coverability functions.","tokens_in":55564,"tokens_out":39804,"duration_ms":406227,"significance":"This is a substantial and coherent contribution. It gives a complete complexity landscape for a natural interpolation between reachability and coverability, and the AC^1 upper bound for 1-VASS coverability is a concrete improvement over the best known bound. The new density measures and the semiring techniques are likely to be useful beyond the specific settings considered. The paper is carefully structured, with full proofs in appendices, and I found no circularity or parameter-fitting. In particular, the reader's flagged risk point, Proposition V.9 and the harbor-chain Lemma V.13, survives scrutiny: the uniform constant ρ=2R(m+1) and the ideal-decomposition argument are internally consistent, and the VCASS coverability proof in Section VII is sound. The results are significant enough to merit publication.","major_comments":[],"minor_comments":[{"comment":"The abstract contains a numbering error: 'For (i), (ii), and (i)' should read 'For (i), (ii), and (iii)', and 'pratically' should be 'practically' in Section I.","section":"Abstract and Introduction"},{"comment":"The claim that the sets T∞ and T−∞ are transformed building blocks is not immediate from Definition V.7, since S(ρ,m) always includes finite intervals followed by a right-infinite interval; a sentence explaining that a ray can be represented as a finite prefix plus an infinite tail, and that a left-infinite ray is handled by the sign flip, would improve readability.","section":"Section V.E and Appendix C.X"},{"comment":"In Lemma C.12 the displayed bound u_{i+1}/v_i ≤ m(ρ+1) appears to be off by a constant factor when the triangle inequality is applied directly; since the subsequent argument only needs a constant bound depending on m and ρ, this does not affect the result, but the constants in this appendix should be cleaned up.","section":"Appendix C.XIII"},{"comment":"The notation ar X^i is used before its precise meaning as an iterated composition is fixed; in particular, in equation (4), ar X^0 should be identified with the identity function, and this convention should be stated explicitly.","section":"Section VII.C"},{"comment":"The examples define S3[t] and S4[t,s] without stating the intended parameter range; for t<0 the intervals overlap or degenerate, so the examples should explicitly restrict to t≥0 and t,s≥0 as the accompanying text suggests.","section":"Examples III.5 and III.6"}],"recommendation":"minor_revision","confidential_remarks":"This is a high-quality paper. My reading agrees with the reader's assessment: no load-bearing technical error was found. The manuscript is dense and would benefit from a careful proofreading pass and from a few clarifying remarks about notation and constants, but the central results are sound and significant."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: the paper earns its length. It proves three dichotomy theorems for reachability with arbitrary semilinear target sets in one-counter automata: for each fixed Presburger formula, the problem is either NP-complete or in AC1, and the borderline is decidable. The headline payoff is coverability for 1-VASS in AC1, improving the previous NC2 bound. The framework (φ-reachability), the two density measures, and the uniform quasi-upward closedness criterion are genuinely new; this is not a \"first application of X to Y\" paper.\n\nThe paper is structurally sound. The main theorems are supported by full proofs in the appendices. The central equivalence Proposition V.9—positive density iff no unbounded isolation iff finite union of transformed building blocks—is the most intricate step; I read the harbor-chain Lemma V.13 and the ratio-ideal argument and could not find a gap. The AC1 coverability proof via the semiring F also survives close reading, and I tested the reconstruction step in Section VII.B on small examples, including a path with weights -2, +1, +1.\n\nSoft spots: the proofs are long and unmechanized, and the two most intricate parts (Proposition V.9 and the VASS coverability correctness proof around Proposition VII.5) would benefit from independent verification. The risk of a subtle error is real, but the stress-test found nothing load-bearing. There are typos—the abstract lists the models with a duplicated \"(i)\", and the introduction says \"coverablity\"—but nothing substantive. One small limitation: the AC1 side for the VASS dichotomy is obtained by reduction to 1-VASS coverability, so if Proposition VII.5 were to fail, only that upper bound would degrade to the already-known NC2; the dichotomy structure and the other two dichotomies would remain intact.\n\nWho is this for? Researchers in counter systems, VASS, and circuit complexity. It deserves a serious referee; I would send it to peer review and expect it to be accepted after a careful check of Sections V and VII. If I worked on one-counter automata, I would cite it. Bring it to reading group? Yes, if the group has taste for long theory papers.\n\nRecommendation: send to peer review with referees who can sit with the appendices. The paper is not obviously wrong, and the contributions are substantial.","headline":"A dense but substantial paper that likely delivers three real dichotomy theorems for semilinear targets in one-counter automata, including an AC1 coverability result for 1-VASS that deserves careful refereeing.","tokens_in":56094,"tokens_out":5612,"would_cite":true,"duration_ms":57351,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q17","68Q45","03D15"],"pacs":[],"model":"deepseek-v4-flash","headline":"Every Presburger-definable target set for a one-counter automaton is either NP-complete or solvable in the circuit class AC1, and deciding which side a formula falls on is decidable.","keywords":["complexity dichotomy","coverability","Presburger arithmetic","semilinear sets","one-counter automata","AC1","NP-completeness","local density"],"falsifier":"Exhibit a semilinear set $S$ with positive local density ($D(S)>0$) whose canonical interval decomposition, for some parameter $t$, contains a finite interval with no harbor—i.e., every larger interval is farther than $\\rho|I_i|$ away—or equivalently a set with no unbounded isolation that nonetheless cannot be decomposed into finitely many $\\rho$-chains of intervals. Since all ingredients are Presburger-definable, one could compute $D(S)$ and check the harbor condition directly to settle whether the dichotomy holds for that set.","tokens_in":55147,"feed_emoji":"⚖️","tokens_out":8074,"duration_ms":74001,"temperature":0.7,"pith_summary":"This paper proposes a way to study the gap between reachability and coverability in infinite-state systems: instead of asking whether a reachable configuration equals a given target or lies above it, allow the target to be any set definable in Presburger arithmetic. For systems with one counter and binary updates, it proves that this generalized reachability problem always falls on one of two sides: for every fixed target formula, the problem is either NP-complete or solvable in AC1, a parallel circuit class within polynomial time. It also shows that deciding which side a given formula is on is decidable, so the border can be computed mechanically. The payoff is a sharper understanding of why coverability is easy: the tractable cases are exactly those with a positive measure of 'local density' (for integer and natural semantics), or with a uniform quasi-upward-closed structure (for VASS semantics). In particular, coverability in binary one-counter VASS improves from the previously known NC2 upper bound to AC1.","feed_headline":"One-counter automata: every target set is NP-complete or AC1","feed_subtitle":"Three dichotomies draw the easy/hard line for Presburger-defined reachability—and improve 1-VASS coverability to AC1.","key_machinery":"The argument is carried by two constructions. First, for the integer and natural semantics, the ratio matrix of a semilinear set—the matrix whose entries record, for each gap and each interval in the canonical decomposition, the quotient of gap size to interval size—is analyzed through well-quasi-ordering ideal decompositions. A pattern called an $\\omega$-constellation (two gaps whose size grows unboundedly compared with every interval between them) characterizes the NP-complete side, and its absence yields a decomposition of the target set into $\\rho$-chains of intervals, which are the shapes the $\\mathsf{AC}^1$ algorithm can handle. Second, for the VASS semantics, the paper builds a semiring of coverability functions (strictly monotone functions with finitely many discontinuities) and shows that coverability can be decided by repeated squaring of an adjacency matrix over this semiring, with an approximation step that keeps each squaring in $\\mathsf{AC}^0$ and therefore the whole procedure in $\\mathsf{AC}^1$.","core_discovery":"The central discovery is a complexity dichotomy for reachability with Presburger target sets in one-dimensional counter systems. For each fixed semilinear set $S\\subseteq \\mathbb{Z}^{p+1}$, three problems—$\\textsf{Reach}_{\\mathbb{Z}}(S)$ for integer semantics, $\\textsf{Reach}_{\\mathbb{N}}(S)$ for natural semantics, and $\\textsf{Reach}_{\\textsf{VASS}}(S)$ for non-negative VASS semantics—are each either NP-complete or in $\\mathsf{AC}^1$. The boundary is characterized by a density measure: for integer semantics, $D(S)>0$ exactly characterizes the $\\mathsf{AC}^1$ side; for natural semantics, $D^+(S)>0$ does; and for VASS semantics, uniform quasi-upward closedness does. Moreover, the side of the dichotomy is decidable from a Presburger formula for $S$. As a direct consequence, coverability in binary-encoded one-counter VASS, previously known to be in $\\mathsf{NC}^2$, is placed in $\\mathsf{AC}^1$.","pith_inferences":["The density measures and the ratio-ideal machinery may transfer to other settings with decidable Presburger-expressible reachability relations, such as one-counter automata with zero tests or parametrized timed systems, where analogous dichotomies could be formulated.","The decidable boundary suggests that 'which formulas are easy' is itself a Presburger question; one could build an automated classifier that, given a formula, outputs a witness (a $\\rho$-chain decomposition or a subset-sum gadget).","If the same dichotomy held in fixed dimension $d\\ge 2$, it would not resolve reachability in VASS, but it would give a template for understanding the gap between PSPACE-complete coverability and non-elementary reachability in terms of target-set density.","The $\\mathsf{AC}^1$ coverability algorithm may be implementable and certifiable in practice, because it reduces to repeated matrix squaring over a semiring of small tables, a standard pattern in verification tools."],"forward_implications":["Coverability in binary-encoded 1-VASS is in $\\mathsf{AC}^1$, improving the previous $\\mathsf{NC}^2$ bound; the algorithm is an iterative translation using coverability tables.","For any fixed Presburger formula, the complexity side of the dichotomy is decidable, so a tool could automatically classify target sets as easy or hard without case-by-case analysis.","The border between coverability and reachability is not a single relation: many intermediate Presburger relations such as $x\\in[t,2t]$ are tractable, showing that the easy/hard boundary is a spectrum of target-set shapes.","In the VASS case, the dichotomy is sharp at the level of single points: adjoining or removing one point from each target fibre can move the problem from $\\mathsf{AC}^1$ to NP-complete (Examples III.14--III.16).","All three problems remain in NP, and the NP upper bound comes from small existential Presburger formulas for the reachability relations, so the dichotomy is complete in the sense that no intermediate complexity arises."],"supporting_citations":[{"why":"Supplies the previous $\\mathsf{NC}^2$ upper bound for coverability in 1-VASS that this paper improves to $\\mathsf{AC}^1$, and the disequality-test setting that motivates the VASS semantics.","marker":"[3]"},{"why":"Provides the Carathéodory-type bound for integer cones that is used in the logspace reduction of reachability to acyclic automata.","marker":"[12]"},{"why":"Gives the polynomial-sized existential Presburger formula for reachability in integer VASS that yields the NP upper bound for $\\textsf{Reach}_{\\mathbb{Z}}$.","marker":"[16]"},{"why":"Gives the linear arithmetic representation of reachability for one-counter automata that yields the NP upper bound for $\\textsf{Reach}_{\\textsf{VASS}}$.","marker":"[21]"},{"why":"Shows the Parikh image of an NFA has a polynomial-sized existential Presburger formula, used to obtain the exponential run-length bound in the acyclization step.","marker":"[26]"},{"why":"Supplies the standard definitions of the circuit classes $\\mathsf{AC}^0$, $\\mathsf{AC}^1$, $\\mathsf{TC}^1$, $\\mathsf{NC}^2$ and the inclusion facts used throughout.","marker":"[27]"},{"why":"Bounds the size of solutions of integer linear inequalities, used to derive the exponential run-length bound.","marker":"[28]"}],"fun_headline_variants":["Semilinear targets in 1-counter automata: NP-complete or AC1","Reachability to semilinear sets: NP-complete or AC1","Every semilinear target in one-counter automata: NP-complete or AC1","Dichotomy for semilinear reachability: NP-complete or AC1","One-counter VASS: semilinear reachability is NP-complete or AC1"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The $\\mathsf{AC}^1$ side of the dichotomy rests on a structural lemma that every bounded interval in a semilinear set without unbounded isolation is within a constant multiple of its own length of a strictly larger interval (the 'harbor' lemma); if that lemma failed for some semilinear set, positive local density would not yield the $\\rho$-chain decomposition, and the tractability half of the dichotomy would collapse.","fun_headline_variants_meta":{"raw":{"variants":["Semilinear targets in 1-counter automata: NP-complete or AC1","Reachability to semilinear sets: NP-complete or AC1","Every semilinear target in one-counter automata: NP-complete or AC1","Dichotomy for semilinear reachability: NP-complete or AC1","One-counter VASS: semilinear reachability is NP-complete or AC1"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001651,"raw_usage":{"total_tokens":6612,"prompt_tokens":1056,"completion_tokens":5556,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":672,"completion_tokens_details":{"reasoning_tokens":5453}},"tokens_in":672,"tokens_out":5556,"duration_ms":38622,"temperature":1.0,"reasoning_tokens":5453,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T20:10:36.869677+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Exhibit a semilinear set $S$ with positive local density ($D(S)>0$) whose canonical interval decomposition, for some parameter $t$, contains a finite interval with no harbor—i.e., every larger interval is farther than $\\rho|I_i|$ away—or equivalently a set with no unbounded isolation that nonetheless cannot be decomposed into finitely many $\\rho$-chains of intervals. Since all ingredients are Presburger-definable, one could compute $D(S)$ and check the harbor condition directly to settle whether the dichotomy holds for that set.","supporting_citations":[{"cited_title":"Coverability in 1-V ASS with Disequality Tests","cited_arxiv_id":null,"evidence_quote":"Supplies the previous $\\mathsf{NC}^2$ upper bound for coverability in 1-VASS that this paper improves to $\\mathsf{AC}^1$, and the disequality-test setting that motivates the VASS semantics."},{"cited_title":"Counting in Trees for Free","cited_arxiv_id":null,"evidence_quote":"Shows the Parikh image of an NFA has a polynomial-sized existential Presburger formula, used to obtain the exponential run-length bound in the acyclization step."},{"cited_title":"V ollmer","cited_arxiv_id":null,"evidence_quote":"Supplies the standard definitions of the circuit classes $\\mathsf{AC}^0$, $\\mathsf{AC}^1$, $\\mathsf{TC}^1$, $\\mathsf{NC}^2$ and the inclusion facts used throughout."},{"cited_title":"A bound on solutions of linear integer equalities and inequalities","cited_arxiv_id":null,"evidence_quote":"Bounds the size of solutions of integer linear inequalities, used to derive the exponential run-length bound."}],"review_version":1}