{"id":"6e638c1a-7200-4530-a18d-5dd1d3c2ce49","arxiv_id":"2607.09558","paper_version":1,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":8.5,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"BVAS reachability is decidable because non-reachability is always witnessed by a semilinear inductive invariant, yielding a simple enumerative algorithm.","lead":"The paper proves that BVAS reachability is decidable by showing every unreachable configuration is excluded by a semilinear inductive invariant. This settles a 30-year open problem and implies decidability of MELL provability.","discovery_kind":"new_method","skeptic_critique":{"model":"grok-4.5","headline":"No significant objection identified","rationale":"The central claim (Theorem 3.3) is an existence statement proved by an iterative construction that terminates because a well-founded rank on finite sets of directed iruns decreases at every step. Every non-trivial geometric or order-theoretic ingredient (asymptotic definability of P_ρ, safe linearization via WSVAS, face-stripping decomposition, homogeneity preservation) is given a full proof inside the manuscript or its appendices. The only external citation that the reader flagged is itself re-proved in Appendix B, so the dependency is not a hidden assumption. Complexity remains open, but that is orthogonal to decidability. Therefore the reader's ACCEPT / HIGH / low-risk assessment stands; no adjustment is warranted.","tokens_in":43122,"tokens_out":475,"duration_ms":6382,"concrete_test":"Independently re-derive the amalgamation construction of Appendix B (Lemma B.2) for the concrete 3-dimensional BVAS of Example 3.1 on the three runs ρ, σ, τ of Figure 1; verify that the constructed amalgamating run σ satisfies both ρ ⊴ σ, τ ⊴ σ and the target-sum identity. If the construction fails for this instance the whole argument collapses; if it succeeds the imported lemma is confirmed for the running example.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The reader's weakest_assumption correctly flags Lemma 3.10 (the wpo+amalgamation property of (IRuns(S), ⊴)) as foundational: without it the periodic sets P_ρ are not well-defined and the attractor construction fails. However the manuscript does not merely import the claim; Appendices B and C supply complete, self-contained inductive proofs of both the wpo property (via Kruskal on decorated runs) and amalgamation (by structural induction that explicitly constructs the amalgamating run). The same amalgamation is re-proved for the auxiliary WSVAS model used in the safe-linearization step. Consequently the dependency is internal and checkable rather than an external soft spot. No other load-bearing gap appears: the face-stripping theorem, the safe-linearization lemma, and the rank-decreasing update of the abstract graph are all proved in full.","agreement_with_reader":"agree"},"referee_report":{"model":"grok-4.5","summary":"The paper proves that BVAS reachability is decidable. The key technical result (Theorem 3.3) states that for every initialized BVAS S and every semilinear set Φ containing Reach(S), there exists a semilinear inductive invariant I for S with I ⊆ Φ. The proof proceeds by iteratively enlarging a semilinear attractor A while maintaining a homogeneous finite set W of directed iruns (pairs (ρ, C) of an initialized run and a finitely-generated cone) that cover all iruns whose targets lie outside A; a well-founded rank on W decreases until W becomes empty, at which point A is the desired invariant. The construction relies on a new safe-linearization lemma for an auxiliary model of well-structured VAS, a face-stripping decomposition of the difference of two finitary cylindric sets, and the wpo+amalgamation property of the embedding order on initialized runs.","tokens_in":43328,"tokens_out":673,"duration_ms":13777,"significance":"Decidability of BVAS reachability has been open for more than thirty years and is inter-reducible with provability in multiplicative-exponential linear logic; the result therefore settles two long-standing questions at once. The argument supplies a conceptually new forward-only invariant construction that avoids the missing Pre* operator of the classical VAS approach, introduces the notions of attractor and directed irun, and develops the face-stripping theorem and the WSVAS model as reusable geometric tools. Full self-contained proofs of the foundational wpo and amalgamation properties appear in the appendices, so the dependency on prior geometric work is internal and checkable. No complexity upper bound is obtained, but the existence of a simple enumerative decision procedure is already a major advance.","major_comments":[],"minor_comments":[{"comment":"The overview at the end of Section 3 is helpful but dense; a short schematic diagram of the two-step update (attractor enlargement then face-stripping of the bottom SCC) would make the global strategy easier to follow on a first reading.","section":null},{"comment":"Notation for the various periodic sets (P_ρ, P_w, Q_w, Q_Γ) is introduced gradually; a short table collecting the definitions would reduce the need to flip back and forth.","section":null},{"comment":"In the statement of the Face-Stripping Theorem (Theorem 6.1) the phrase “disjoint decomposition” is footnoted; it would be clearer to spell out once that empty sets are allowed.","section":null},{"comment":"A few typographical slips remain (e.g., “BV AS” with a space, occasional missing articles). A careful copy-edit pass would polish the presentation.","section":null}],"recommendation":"accept","confidential_remarks":"The manuscript is long and technically heavy, but the result is of the highest importance for the community. I see no reason to delay publication for further polishing; the appendices already make the key lemmas checkable."},"author_rebuttal":null,"desk_editor":{"model":"grok-4.5","letter":"This paper settles BVAS reachability (and therefore MELL provability). The punchline is Theorem 3.3: non-reachability is always witnessed by a semilinear inductive invariant, so you get decidability by the usual parallel enumeration of runs and candidate invariants.\n\nWhat is new is the forward-only machinery. Ordinary VAS invariants lean on a Pre*/Post* symmetry that simply does not exist once executions branch. They replace it with attractors (sets closed under “one leaf in the set, rest reachable”), an abstract graph of directed iruns that stays homogeneous by SCC, a reduction of the side-branch case to a well-structured VAS, and a face-stripping theorem that peels the residual cone so the rank of the abstract graph strictly decreases. All of that is original and carefully layered.\n\nThe write-up is long but honest. Every geometric and order-theoretic step is proved in the main text or the appendices; the wpo+amalgamation property of iruns (the only external-looking dependency) is re-proved from scratch via Kruskal and structural induction, and the same amalgamation is re-established for the auxiliary WSVAS model. No free parameters, no circular definitions, no post-hoc exclusions. Complexity is left open, which is a genuine limitation but does not touch the decidability claim.\n\nSoft spots are minor: the argument is intricate enough that an undetected gap in one of the cone or amalgamation inductions remains possible, and the algorithm is purely enumerative, so no complexity upper bound is obtained. Neither issue undermines the existence proof.\n\nThis is for people who work on infinite-state systems, counter automata, or linear logic. It deserves a serious referee. I would accept it for peer review without hesitation and would cite the decidability result myself.","headline":"They close the 30-year BVAS reachability problem with a clean forward-only invariant construction; the math is fully written out and the amalgamation dependency is internal, not soft.","tokens_in":43943,"tokens_out":459,"would_cite":true,"duration_ms":7415,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q60","03B25","68Q85"],"pacs":[],"model":"grok-4.5","headline":"If a configuration is unreachable in a branching vector addition system, a semilinear inductive invariant separates it, so reachability is decidable by enumeration.","keywords":["branching vector addition systems","reachability problem","semilinear inductive invariants","attractors","well-structured systems","multiplicative exponential linear logic","Presburger arithmetic"],"falsifier":"Exhibit a concrete low-dimensional BVAS together with an unreachable target for which every candidate semilinear set that excludes the target fails to be inductive, or find a counter-example to amalgamation of the embedding order on initialized runs.","tokens_in":44018,"feed_emoji":"🌳","tokens_out":682,"duration_ms":6566,"temperature":0.7,"texified_at":"2026-08-05T21:17:21.582372+00:00","pith_summary":"Branching vector addition systems (BVAS) model how resources can be combined and redistributed along tree-shaped computations. Their reachability problem asks whether a target configuration can arise from given initial configurations by applying a finite set of additive branching rules. The problem had stayed open for decades. This paper shows that non-reachability is always witnessed by a semilinear inductive invariant: a Presburger-definable set that contains the initials, is closed under the rules, and excludes the target. The proof builds such a witness by iteratively growing a single attractor while tracking residual executions outside it with a homogeneous abstract graph of directed runs. When the graph empties, the attractor is already the desired invariant. The result immediately yields a simple decision procedure: enumerate candidate executions in one process and candidate semilinear invariants in another until one succeeds. The same theorem settles the long-open decidability of multiplicative exponential linear logic.","texify_model":"deepseek-v4-flash","texify_usage":{"total_tokens":5374,"prompt_tokens":592,"completion_tokens":4782,"prompt_tokens_details":{"cached_tokens":0},"prompt_cache_hit_tokens":0,"prompt_cache_miss_tokens":592,"completion_tokens_details":{"reasoning_tokens":4289}},"feed_headline":"Branching VAS reachability is decidable by invariants","feed_subtitle":"Unreachable targets are always separated by a semilinear inductive set, settling a 30-year open problem","key_machinery":"Safety witnesses (A, W): a semilinear attractor A together with a finite homogeneous set W of directed iruns that cover every initialized run not already inside A. The construction repeatedly extracts a bottom strongly-connected component of W, safely linearizes a portion of its reachable configurations into the attractor, then face-strips the residual difference so that the new directed-irun set is strictly smaller in a well-founded rank.","core_discovery":"For every initialized BVAS S and every semilinear set Φ that contains the reachability set of S, there exists a semilinear inductive invariant I for S with I ⊆ Φ. Consequently, if a configuration c is not reachable then $N^d \\setminus \\{c\\}$ contains a semilinear inductive invariant, and BVAS reachability is decidable by parallel enumeration of executions and candidate invariants.","pith_inferences":[],"forward_implications":[],"fun_headline_variants":["BVAS reachability decided via semilinear inductive invariants","Unreachable BVAS targets always separated by semilinear invariants","Semilinear inductive invariants settle BVAS reachability","Enumerative check of invariants decides BVAS reachability","Inductive semilinear sets prove BVAS reachability decidable"],"cache_read_input_tokens":32896,"weakest_assumption_plain":"The whole argument rests on the claim that initialized runs ordered by the natural embedding form a well-partial-order that also satisfies amalgamation; if amalgamation fails for some system, the periodic sets attached to runs stop being well-defined and the attractor enlargement collapses.","fun_headline_variants_meta":{"raw":{"variants":["BVAS reachability decided via semilinear inductive invariants","Unreachable BVAS targets always separated by semilinear invariants","Semilinear inductive invariants settle BVAS reachability","Enumerative check of invariants decides BVAS reachability","Inductive semilinear sets prove BVAS reachability decidable"]},"model":"grok-4.5","effort":"low","cost_usd":0.006304,"raw_usage":{"total_tokens":1468,"prompt_tokens":626,"num_sources_used":0,"completion_tokens":80,"cost_in_usd_ticks":63040000,"prompt_tokens_details":{"text_tokens":626,"audio_tokens":0,"image_tokens":0,"cached_tokens":0},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":762,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":626,"tokens_out":80,"duration_ms":7858,"temperature":1.0,"reasoning_tokens":762,"cache_read_input_tokens":0,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-13T02:08:57.736179+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"Exhibit a concrete low-dimensional BVAS together with an unreachable target for which every candidate semilinear set that excludes the target fails to be inductive, or find a counter-example to amalgamation of the embedding order on initialized runs.","supporting_citations":[],"review_version":1}