arxiv: 2604.24095 · v1 · submitted 2026-04-27 · 💻 cs.FL · cs.LO

Recognition: unknown

Improving Reachability in Vector Addition Systems through Pumpability

Weijun Chen , Yuxi Fu , Yangluo Zheng

Authors on Pith no claims yet

Pith reviewed 2026-05-07 17:38 UTC · model grok-4.3

classification 💻 cs.FL cs.LO

keywords vector addition systemsreachabilitypumpability analysisVASScomplexity boundsPetri nets

0 comments

The pith

Reachability in d-dimensional vector addition systems is solvable within F_{d-2} time by refining pumpability analysis from VASS.

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

The paper establishes tighter upper bounds on the reachability problem for vector addition systems, a model equivalent to Petri nets for concurrency. It refines the pumpability analysis originally developed for vector addition systems with states to apply directly to plain VAS, yielding an F_{d-2} bound instead of the F_d bound that previously carried over. This improvement matters because reachability questions determine whether one marking can evolve into another under vector additions, and lower bounds bring practical verification closer for systems modeled this way. The authors also handle low dimensions explicitly, proving PSPACE for 4-VAS and ELEMENTARY for 5-VAS, and show that reachability in geometrically 2-dimensional VASS equals that of ordinary 2-VASS via a new projection method.

Core claim

Based on a pumpability analysis of VAS that refines Rackoff's extraction for VASS, the d-dimensional VAS reachability problem lies in F_{d-2}. This improves the inherited F_d bound from VASS. For low dimensions the same technique produces a PSPACE bound for 4-VAS and an ELEMENTARY bound for 5-VAS. Reachability in geometrically 2-dimensional VASS is shown equivalent to 2-VASS reachability through a simplified projection technique.

What carries the argument

Pumpability analysis that refines Rackoff's extraction technique when applied directly to VAS without states, together with a simplified projection that equates geometrically 2-dimensional VASS reachability to 2-VASS.

If this is right

Reachability in 4-dimensional VAS lies in PSPACE.
Reachability in 5-dimensional VAS lies in ELEMENTARY.
Reachability in geometrically 2-dimensional VASS is equivalent to reachability in 2-VASS.
The overall complexity for d-dimensional VAS drops two levels in the fast-growing hierarchy relative to the VASS case.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The projection simplification may extend to higher fixed dimensions and yield further bound improvements.
Equivalent models such as Petri nets without explicit states could inherit the same tightened bounds.
The separation between VAS and VASS bounds suggests that state control adds measurable hardness even in fixed dimension.

Load-bearing premise

The pumpability analysis correctly adapts and refines Rackoff's extraction technique when applied to VAS that lack finite state control.

What would settle it

A concrete 4-dimensional VAS instance whose reachability question requires more than polynomial space would falsify the PSPACE claim.

read the original abstract

Vector addition systems (VAS) constitute an important model of computation and concurrency that is equally expressive as the Petri net model. Recently, a lot of research has been conducted on vector addition systems with states (VASS), which are VASes equipped with a finite state control. Results on VASS naturally carry over to VAS, but no straightforward improvement is available. In this paper, we investigate the reachability problem in VAS in fixed dimensions. Based on a pumpability analysis of VAS that refines Rackoff's extraction for VASS, we obtain an F_{d-2} upper bound for the d-dimensional VAS reachability problem, improving the F_d upper bound inherited from the d-dimensional VASS reachability problem. Low-dimensional VASes are also considered. In particular, we establish a PSPACE upper bound for reachability in 4-dimensional VAS and an ELEMENTARY upper bound for 5-dimensional VAS, while the same upper bounds were known only for 2-VASS and 3-VASS, respectively. The result for 4-VAS particularly hinges on a simplified projection technique developed for geometrically 2-dimensional VASSes, whose reachability problem is shown to be equivalent to 2-VASS.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper refines pumpability to claim an F_{d-2} bound for d-dimensional VAS reachability plus PSPACE for 4D and ELEMENTARY for 5D, but the adaptation from VASS needs checking on the state-less case.

read the letter

The main point is that this work takes Rackoff's extraction technique from VASS and refines it with a pumpability analysis to drop the upper bound on d-dimensional VAS reachability by two levels in the fast-growing hierarchy. It also pins down better concrete bounds for small dimensions: PSPACE for 4-VAS and ELEMENTARY for 5-VAS, where only weaker results were known before. The projection equivalence between geometrically 2-dimensional VASS and plain 2-VASS is a clean supporting result that helps the 4D case. These are the parts that actually move the literature. The low-dimensional improvements are presented clearly enough that they could be useful in verification contexts even before the general bound is fully settled. The paper avoids circularity by building directly on the existing VASS results without fitting parameters back to itself. The soft spot is whether the pumpability refinement fully replaces the role of finite control states. Rackoff's original bounds used states to limit pump sequences and witness lengths, and VAS have none, so the analysis has to supply new geometric or combinatorial arguments to save exactly those two levels. If those arguments are incomplete, the improvement might shrink to F_{d-1} or stay at F_d. The abstract states the claims without sketches, so the strength rests on details that need close reading. This paper is for people who track Petri-net and VAS complexity. A reader already familiar with the VASS bounds will get value from the dimension-specific results and the general technique. It deserves a serious referee because the claims are concrete, the low-dim cases are in principle falsifiable, and the work engages the prior literature honestly even if revisions are needed on the extraction details.

Referee Report

2 major / 2 minor

Summary. The paper claims that a pumpability analysis of vector addition systems (VAS), refining Rackoff's extraction technique for VASS, yields an F_{d-2} upper bound on reachability in d-dimensional VAS (improving the inherited F_d bound). It further claims PSPACE for 4-VAS and ELEMENTARY for 5-VAS, with the former depending on a simplified projection establishing equivalence between geometrically 2-dimensional VASS reachability and 2-VASS reachability.

Significance. If correct, the two-level improvement in the fast-growing hierarchy for general d and the concrete low-dimensional tightenings would be a notable advance for a core problem in concurrency theory and Petri-net verification. The work explicitly builds on Rackoff's extraction and known VASS bounds while targeting the state-less VAS case directly.

major comments (2)

[Abstract and §1] Abstract and §1 (Introduction): the claim that pumpability refines Rackoff's extraction to save exactly two levels when applied to state-less VAS requires an explicit argument that the missing finite control states do not force the extraction depth back to F_{d-1} or F_d; without a concrete comparison of witness-length bounds or pump-sequence extraction in the two models, the F_{d-2} improvement is not yet load-bearing.
[Low-dimensional results] Low-dimensional results section: the PSPACE bound for 4-VAS rests on the equivalence between geometrically 2-dimensional VASS reachability and 2-VASS via the simplified projection technique. The manuscript must supply a self-contained proof that this projection preserves the exact complexity class and does not introduce hidden exponential factors.

minor comments (2)

[Notation and definitions] Clarify the precise definition of 'pumpability' on first use and ensure it is distinguished from related notions such as pumping in Petri-net languages.
[Introduction] Add an explicit citation to Rackoff's original extraction result in the introduction for traceability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive suggestions. We address the two major comments point by point below, indicating the revisions we will incorporate.

read point-by-point responses

Referee: [Abstract and §1] Abstract and §1 (Introduction): the claim that pumpability refines Rackoff's extraction to save exactly two levels when applied to state-less VAS requires an explicit argument that the missing finite control states do not force the extraction depth back to F_{d-1} or F_d; without a concrete comparison of witness-length bounds or pump-sequence extraction in the two models, the F_{d-2} improvement is not yet load-bearing.

Authors: We agree that an explicit side-by-side comparison would make the two-level improvement more transparent. The manuscript defines pumpability directly on the vector components of VAS (without state tracking) and shows that the resulting pump-sequence extraction avoids the additional state-cycle enumeration present in Rackoff's VASS procedure. This yields witness-length bounds governed by the recurrence for F_{d-2} rather than F_d. To address the concern, we will insert a new paragraph (or short subsection) in §1 that recalls the VASS extraction depth, states the VAS variant, and tabulates the corresponding primitive-recursive bounds, thereby making the saving explicit without altering the technical development. revision: yes
Referee: [Low-dimensional results] Low-dimensional results section: the PSPACE bound for 4-VAS rests on the equivalence between geometrically 2-dimensional VASS reachability and 2-VASS via the simplified projection technique. The manuscript must supply a self-contained proof that this projection preserves the exact complexity class and does not introduce hidden exponential factors.

Authors: The equivalence is proved in the low-dimensional section by exhibiting a projection that maps any geometrically 2-dimensional VASS instance to an ordinary 2-VASS instance while preserving reachability. The projection is computable in polynomial time and produces an instance whose size is linear in the input, so no exponential blow-up is introduced. Nevertheless, we accept that the current write-up could be more self-contained on the complexity accounting. We will expand the proof with an explicit lemma that (i) states the size and time bounds of the projection and (ii) recalls that 2-VASS reachability is in PSPACE, thereby confirming that the overall procedure remains in PSPACE without hidden factors. revision: yes

Circularity Check

0 steps flagged

No circularity in derivation chain

full rationale

The paper refines Rackoff's prior extraction technique (external to this work) via a pumpability analysis to derive an F_{d-2} bound for d-dimensional VAS reachability, improving on the inherited F_d bound from VASS. Low-dimensional results (PSPACE for 4-VAS, ELEMENTARY for 5-VAS) rest on a projection technique and equivalence between geometrically 2-dimensional VASS and 2-VASS, both developed and shown within the paper itself. No equations or steps reduce the claimed bounds back to fitted parameters, self-definitions, or load-bearing self-citations by construction; the chain remains independent of its outputs.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on standard definitions of VAS and VASS, the correctness of Rackoff's extraction technique from prior literature, and the validity of geometric projections for low-dimensional cases. No free parameters or invented entities are introduced.

axioms (2)

domain assumption Reachability in VASS is decidable with known F_d upper bound via Rackoff's technique
Invoked when inheriting the F_d bound and refining it for VAS
domain assumption Pumpability analysis can be adapted from VASS to plain VAS without introducing new undecidability
Central to obtaining the F_{d-2} improvement

pith-pipeline@v0.9.0 · 5512 in / 1414 out tokens · 60094 ms · 2026-05-07T17:38:51.111523+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

6 extracted references · 1 canonical work pages

[1]

48550/ARXIV.2602.15483

URL: https://doi.org/10.48550/arXiv.2602.15483, arXiv:2602.15483, doi:10. 48550/ARXIV.2602.15483. 3 Wojciech Czerwinski, Ismaël Jecker, Slawomir Lasota, Jérôme Leroux, and Lukasz Orlikowski. New lower bounds for reachability in vector addition systems. In Patricia Bouyer and Srikanth Srinivasan, editors,43rd IARCS Annual Conference on Foundations of Softw...

work page doi:10.48550/arxiv.2602.15483 2023
[2]

let X0 :={x∈X|⟨n,x⟩= 0}; thencone(X0) = span(X0)
[3]

∥n∥≤(d + 1)·(r∥X∥)r, wherer := dim(span(X)). Proof. According to the Farkas-Minkowski-Weyl Theorem (see e.g. [19, Corollary 7.1a]), there is a matrixA∈Zk×d for somek such that cone(X) = {x∈Qd|Ax≥0}. Let a1,...,ak∈Zd be the rows ofA, we may taken0 :=∑k i=1ai as a candidate ofn
[4]

Indeed,⟨ai,x⟩≥0 for anyx∈cone(X), so⟨n0,x⟩≥0 as well
[5]

For allx∈X0, we must have⟨ai,x⟩= 0 for each i∈[k] as 0 =⟨n0,x⟩=∑k i=1⟨ai,x⟩is a sum of non-negative values

Now letX0 :={x∈X|⟨n0,x⟩= 0}. For allx∈X0, we must have⟨ai,x⟩= 0 for each i∈[k] as 0 =⟨n0,x⟩=∑k i=1⟨ai,x⟩is a sum of non-negative values. Takey∈span(X0), then⟨ai,y⟩= 0 for eachi∈[k]. Therefore,Ay = 0 which impliesy∈cone(X). Notice that in the expression ofy as a non-negative linear combination of vectors ofX we cannot have non-zero coefficients for anyx+∈X...
[6]

Hence, we can replaceθ1 byθ′ 1 as a new pumping cycle

=−n1λ0·∆(θ2)≥1. Hence, we can replaceθ1 byθ′ 1 as a new pumping cycle. Letςbe the short path obtained by Claim C.1 and letn2 :=|ς|·∥T∥. Construct a new pathρ:= (θ′ 1)n2ςθn1n2λ0 2 . We claim thatp(x) ρ − →q(y) is a run. It suffices to show that the infixςis a legal run: p(x +n2·∆(θ′ 1)) =p(x−n2n1λ0·∆(θ2)) ς − →q(y−n1n2λ0·∆(θ2)). (28) Sincex−n2n1λ0·∆(θ2)≥n2...