{"id":"138a5aa2-f313-46a1-9387-e7d4d9d93907","arxiv_id":"2506.22561","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"The reachability set of every 2-dimensional branching VASS has a computable semilinear representation, so reachability is decidable for this class.","lead":"Branching VASS are a model of concurrent programs where processes can merge. This paper proves that for two-dimensional systems, all reachable states can be finitely described and computed, settling a previously open question.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Lemma D.6's construction of a cycle in V_{n'0} is unjustified when n'0 is the unique minimal node, leaving a real gap in Lemma 7.3 on which termination rests.","rationale":"The reader correctly identifies Lemma 7.3 as the load-bearing point of the termination proof. My stress-test agrees with that diagnosis and sharpens it to a specific unhandled case in the proof of Lemma D.6, which is the main support for Lemma 7.3. The concern is not an attack on the theorem: the statement of Theorem 7.11 may well be true, and the identified gap appears fixable by choosing the common descendant n'0 outside the finite set Nmin, which is always possible in an infinite primary directed graph because every node has a proper descendant. However, as written, the manuscript does not make this choice, and the proof of Lemma D.6 contains a step ('Notice that t_j is a transition of V_{n'0}') that is false in the case n'0 ∈ Nmin. Because the termination argument depends on Lemma 7.3, the proof is not yet fully rigorous at that point. I therefore recommend conditional acceptance: the central claim is plausible and the gap is localized, but the authors should either add the missing hypothesis to the definition of n'0 with a one-line justification, or provide an alternative argument for Lemma D.6 that handles the self-mapping case. The proposed test asks for exactly this re-derivation, which would settle whether the concern lands or dissolves.","tokens_in":39917,"tokens_out":28519,"duration_ms":286982,"concrete_test":"Independently re-derive Lemma D.6 under the explicit additional hypothesis n'0 ∉ Nmin, verifying that every constructed transition t_j is then a valid transition of V_{n'0} because λ(m) →+ n'0 for all background nodes m. If the re-derivation succeeds, the gap is closed by adding one sentence to Section 7.2; if it fails, or if one can exhibit a small algorithmic exploration with Nmin = {n'0} and an elementary cycle whose background set includes n'0, then Lemma 7.3 is not established as stated and the termination proof needs a different repair.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The proof of Lemma 7.3 (Section 7.2) relies on Lemma D.6 (Appendix D.2), which transforms an elementary cycle θ' of V_n into a cycle θ of V_{n'0} by replacing each background node m by λ(m)∈Nmin. To conclude that the displacement of θ lies in some E_m, θ must be a cycle of V_{n'0}. But V_{n'0} is instantiated with F_{n'0} = {q_s(z_s) | s →+ n'0}, the strict ancestors of n'0. If n'0 ∈ Nmin, then Nmin = {n'0}: any other minimal element would strictly precede n'0, contradicting minimality. Hence λ(m) = n'0 for every m ∈ Des(n0). Whenever a background node m equals n'0 or is mapped to n'0, the constructed transition t_j uses the configuration q_{n'0}(z_{n'0}), which is not in F_{n'0}; so t_j is not a transition of V_{n'0}. Section 7.2's choice of n'0 as a common descendant of Nmin ∪ (N \\ Des(n0)) does not exclude n'0 ∈ Nmin. Since Lemma 7.3 is the key decomposition behind Lemma 7.7 and the finite-generation of Con(P_N), this is a genuine gap in the termination argument. The gap appears repairable: in an infinite primary directed algorithmic exploration, n'0 has a proper descendant, so one can choose n'0 outside Nmin (e.g., a common descendant of the finite set Nmin ∪ (N \\ Des(n0)) that is not itself in Nmin), making all λ(m) strict ancestors of n'0 and restoring the validity of the t_j as transitions of V_{n'0}.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper claims that the reachability set of every two-dimensional branching vector addition system (2-BVASS) is semilinear and that a semilinear presentation is computable from the system, thereby settling the reachability problem for this class. The proposed algorithm Explore builds a finite acyclic exploration graph whose nodes carry semilinear sets of configurations; Section 5 proves that the explorations produced are sound and complete. The termination proof extracts an infinite primary and directed sub-exploration from any infinite run, shows that the cone spanned by all periods is finitely generated via a mode-stabilization argument and a decomposition of elementary cycle vectors, and derives a contradiction from non-redundancy. Detailed proofs are deferred to an appendix.","tokens_in":40300,"tokens_out":27841,"duration_ms":277797,"significance":"If the proof is correct, this is a substantial advance: it is the first decidability result for branching VASS beyond dimension one and a natural generalization of the Hopcroft--Pansiot theorem for classical 2-VASS. The algorithm is constructive and the proof does not rely on fitting parameters or on the decidability of BVASS reachability. The paper is generally well written and the appendix is detailed, with the soundness and completeness parts argued carefully. However, the termination proof contains a load-bearing gap in Lemma D.6 that needs to be repaired; the manuscript should therefore not be accepted in its current form.","major_comments":[{"comment":"The proof constructs transitions t_j of V_{n'0} by replacing each background node m of a transition of V_n by lambda(m) in Nmin. This is valid only when every lambda(m) is a strict ancestor of n'0, because V_{n'0} is the instantiation with F_{n'0} = {q_s(z_s) | s ->+ n'0}. The text only guarantees lambda(m) ->* n'0. If n'0 is in Nmin, which can happen when Nmin is a singleton, then lambda(m)=n'0 for all m in Des(n0), and q_{n'0}(z_{n'0}) is not an element of F_{n'0}; hence the constructed t_j need not be transitions of V_{n'0}, and theta need not be a cycle of V_{n'0}. Consequently the conclusion that the displacement v of theta lies in some E_m with n'0 ->* m ->* n1 does not follow. This affects Lemma 7.3, and through it Lemma 7.7 and the finite-generation of Con(P_N), so it is load-bearing for the termination proof. The gap appears repairable: since the exploration is primary and infinite, every node has a proper descendant, so n'0 can be chosen as a common descendant of Nmin union (N \\ Des(n0)) that is not itself in Nmin; then every lambda(m) is a strict ancestor of n'0. The manuscript must be revised to make this choice and the strictness explicit.","section":"Section 7.2 / Appendix D.2 (Lemma D.6)"}],"minor_comments":[{"comment":"\"Vectors addition systems\" should be \"Vector addition systems\" in the abstract and in the first paragraph of the introduction.","section":"Abstract and Section 1"},{"comment":"The variables s_j and s'_j are used in the display v' = v + sum_{j=1}^k (z_{s'_j} - z_{s_j}) but are never defined; in addition, the two displayed formulas for v and v' appear to be interchanged relative to the definitions of b_j and t_j. Please rewrite this paragraph with explicit indexing of the multiset M_j.","section":"Appendix D.2, proof of Lemma D.6"},{"comment":"The phrase \"by by m \\preceq n\" contains a duplicated word and should read \"by m \\preceq n\".","section":"Section 7.4, proof of Lemma 7.9"}],"recommendation":"major_revision","confidential_remarks":"The main concern is the gap in Lemma D.6. It is localized and appears fixable by choosing n'0 outside Nmin, but because the termination proof depends on it, the paper should not be accepted before the authors supply a revised proof. If the repair is confirmed, the result would be a strong and appropriate contribution for this journal."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Two things to know. First, the main theorem is real: if the termination proof holds, this settles the first open dimension for BVASS reachability and gives a computable semilinear presentation. Second, the proof as written has a hole in the appendix, in Lemma D.6, which the authors need to patch before I'd call the termination argument airtight.\n\nThe paper does a lot well. The soundness/completeness part (Section 5) is clean, the abstraction to explorations and the dynamic cycle acceleration are genuinely new, and the geometric termination argument (modes, primary/directed cores) is inventive. The authors are honest that they get no complexity bound, and they don't overclaim. The external references (Hopcroft–Pansiot, standard wqo facts) are used correctly. No circularity, no fitted parameters.\n\nThe soft spot is the termination proof, specifically Lemma D.6 in Appendix D.2. The lemma transports an elementary cycle of V_n to a cycle of V_{n'0} by replacing background nodes m with minimal nodes λ(m) in Nmin. The problem: n'0 is chosen as a common descendant of Nmin ∪ (N\\Des(n0)). If n'0 happens to be the unique minimal node in Nmin, then λ(m)=n'0 for all m in Des(n0), and the constructed transitions use the configuration q_{n'0}(z_{n'0}), which is not a strict ancestor of n'0 and therefore not in F_{n'0}. So the transported cycle is not actually a cycle of V_{n'0}. That is a genuine gap in the written proof, and since Lemma 7.3 and Lemma 7.7 rest on it, the termination argument as written does not go through.\n\nThe gap looks repairable: in an infinite primary directed exploration, the minimal node has a proper descendant, so one can choose n'0 outside Nmin. That would make every λ(m) a strict ancestor of n'0 and restore the argument. But it needs to be written down.\n\nWho is this for? People working on VASS/BVASS reachability, semilinear sets, and verification. It is an important result, and the paper deserves a serious referee, but I would not accept the current version without the authors addressing the Lemma D.6 issue. The rest of the proof is dense but coherent.","headline":"Strong result, repairable gap: the termination proof as written has a hole in Lemma D.6 that the authors need to fix before I'd sign off on it.","tokens_in":40818,"tokens_out":4647,"would_cite":true,"duration_ms":45133,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q85","68Q60"],"pacs":[],"model":"deepseek-v4-flash","headline":"Every two-dimensional branching vector addition system has a computable semilinear reachability set, making its reachability problem decidable.","keywords":["branching vector addition systems","reachability problem","semilinear sets","Petri nets","two-dimensional BVASS","decidability","cycle acceleration","cone stabilization"],"falsifier":"Exhibit a 2-BVASS and an execution of Explore that produces an infinite sequence of non-redundant nodes not covered by ancestors; equivalently, find a primary and directed algorithmic exploration whose periodic sets P_n do not stabilize, for instance whose global cone Con(⋃_n P_n) is not finitely generated. Lemma 7.4 and Corollary 7.10 assert no such exploration exists, so a concrete search over small 2-BVASS instances for such an infinite exploration would settle the claim.","tokens_in":39751,"feed_emoji":"🧮","tokens_out":5034,"duration_ms":52864,"temperature":0.7,"pith_summary":"The paper proves that every two-dimensional branching vector addition system (a Petri-net-like model where transitions may merge configurations by summing them) has a reachability set that is semilinear: a finite union of linear sets, presented explicitly by an algorithm. This makes the reachability problem decidable in dimension two, extending the classical result for ordinary two-dimensional VASS and the known one-dimensional branching case. A sympathetic reader should care because exact reachable sets, rather than over-approximations, are not usually available for such expressive models; the proof shows how cycle acceleration can be made retroactive without losing termination.","feed_headline":"Reachability is decidable for 2-D branching VASS","feed_subtitle":"The reachable configurations of a 2-D branching VASS form a finite, computable semilinear set.","key_machinery":"The central object is an algorithmic exploration: an acyclic node-labeled graph where each node n is labeled by (a_n, q_n, z_n, P_n), with P_n a periodic subset of $N^{2}$ obtained by the cycle-acceleration step P_n := Add^*_{I_n}(∑_{m→n} P_m). The iterable set I_n collects n-elementary vectors (displacements of elementary cycles available from ancestors) and n-consecutive vectors (differences of base vectors of same-state ancestors). The termination argument's geometric engine is the v-stabilization of a cone C⊆$Q^{2}$_≥0, defined as (C + Q_≥0 v) ∩ $Q^{2}$_≥0, together with the h-mode of a cone, which tracks which non-positive vectors stabilize it; Lemma 7.2 says h-modes stabilize along non-decreasing cone chains, and Lemma 7.3 decomposes every elementary vector of a descendant node into earlier elementary vectors, ancestor periodic sets, and consecutive vectors.","core_discovery":"The central claim is Theorem 7.11: for every 2-BVASS B, the reachability set JBK is semilinear and a presentation is computable from B. The algorithm Explore builds a finite acyclic exploration whose nodes carry (state, base vector, periodic set) labels; soundness and completeness show the union of the node sets equals JBK, and termination is proved by contradiction. Assuming an infinite exploration exists, the authors extract an infinite primary and directed sub-exploration, interpret the acceleration step geometrically as v-stabilization of cones in $Q^{2}$_≥0, prove the global cone is finitely generated via a decomposition of elementary-cycle vectors, and then use a Dickson-style argument to force a redundant non-leaf node, contradicting non-redundancy.","pith_inferences":["The paper gives no complexity bound; a natural next question is the size of the computed semilinear presentation, which may grow non-elementarily even though the algorithm terminates.","The primary and directed core-witness lemma in Section 6 is a general statement about infinite spannable graphs and may be reusable to prove termination of other worklist-based symbolic algorithms that build infinite acyclic graphs.","The two-dimensional cone machinery (axes, h-modes, v-stabilization) exploits Q^2_≥0 in an essential way; extending the result to dimension three would require a new geometric invariant, since the stabilizer of a cone is no longer a cone in higher dimensions.","Because branching transitions can be instantiated using reachable configurations, the algorithm's acceleration is retroactive—cycles discovered later pump earlier nodes; similar retroactive acceleration could be tried for other branching or pushdown generalizations, but termination would need a new argument outside dimension two."],"forward_implications":["The reachability problem for 2-BVASS is decidable: given an initial and a target configuration, one can compute the semilinear presentation and test membership.","The reachability set of a 2-BVASS is effectively semilinear, so reachability questions reduce to Presburger arithmetic in dimension two.","The decidability frontier for BVASS reachability moves from dimension one to dimension three, which remains open.","The acyclic exploration with retroactive cycle acceleration provides a template for exact forward analysis of branching models, not merely coverability approximations."],"supporting_citations":[{"why":"Supplies the classical two-dimensional VASS semilinear presentation algorithm that this work extends, and provides the cone/periodic-set lemmas (Lemma 2.1 and Lemma A.3) used throughout the proof.","marker":"[19]"},{"why":"Introduces the BVASS model and its Karp-Miller-tree coverability analysis, giving the semantics and known decidability results that frame the reachability question.","marker":"[34]"},{"why":"Provides the closure properties of semilinear and finitely-generated periodic sets used to compute Add^*_I(Per(G)) effectively in Lemma 4.4 and Corollary A.13.","marker":"[16]"},{"why":"Establishes the one-dimensional BVASS reachability result that motivates the two-dimensional extension and sets the known baseline for lower dimensions.","marker":"[17]"}],"fun_headline_variants":["Reachability for 2-D branching VASS is decidable","2-D branching VASS reachability sets are computable semilinear","Decidable reachability in 2-D branching VASS","Computable semilinear sets for 2-D branching VASS","Semilinear reachability for 2-D branching VASS"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The proof's termination depends on Lemma 7.3, which asserts that in every primary and directed algorithmic exploration, the elementary-cycle vectors of any descendant node decompose into a finite sum of earlier elementary vectors, periodic sets outside the main descendant set, and consecutive vectors; this relies on the stabilization of h-modes and on a carefully chosen node n1. If that decomposition fails, the global cone cannot be shown finitely generated, and the contradiction forcing finite exploration collapses.","fun_headline_variants_meta":{"raw":{"variants":["Reachability for 2-D branching VASS is decidable","2-D branching VASS reachability sets are computable semilinear","Decidable reachability in 2-D branching VASS","Computable semilinear sets for 2-D branching VASS","Semilinear reachability for 2-D branching VASS"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001175,"raw_usage":{"total_tokens":4806,"prompt_tokens":844,"completion_tokens":3962,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":460,"completion_tokens_details":{"reasoning_tokens":3876}},"tokens_in":460,"tokens_out":3962,"duration_ms":28787,"temperature":1.0,"reasoning_tokens":3876,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T22:05:55.967952+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Exhibit a 2-BVASS and an execution of Explore that produces an infinite sequence of non-redundant nodes not covered by ancestors; equivalently, find a primary and directed algorithmic exploration whose periodic sets P_n do not stabilize, for instance whose global cone Con(⋃_n P_n) is not finitely generated. Lemma 7.4 and Corollary 7.10 assert no such exploration exists, so a concrete search over small 2-BVASS instances for such an infinite exploration would settle the claim.","supporting_citations":[{"cited_title":"A polynomial-time algorithm for reachability in branching VASS in dimension one","cited_arxiv_id":null,"evidence_quote":"Establishes the one-dimensional BVASS reachability result that motivates the two-dimensional extension and sets the known baseline for lower dimensions."}],"review_version":1}