PaperlayerView exact revision on arXiv

Source-linked AI summary

Integer reachability in VASS with transfers: a refined complexity analysis

Tymoteusz Kucharek, Piotr Hofman

arXiv:2610.01440v1cs.FLcs.CC

TL;DR

Integer reachability is NP-complete for VASS but PSPACE-complete for VASS with transfers, motivating a structural explanation of that complexity gap. The paper analyzes transfer graphs through their bad vertices and establishes both a bounded-parameter NP result and hardness for graph families with linearly many bad vertices.

  • Problem

    Integer reachability is NP-complete for VASS but PSPACE-complete for VASS with transfers, and the paper asks which transfer structures account for the difference.

    Source: §1 · pp. 1–2

  • Method

    The paper classifies counters as good or bad from transfer-graph structure and uses the number of bad vertices to bound reachability witnesses and construct hardness reductions.

    Source: §1 · p. 2

  • Results

    Integer reachability is in NP for single-transfer VASS classes with a fixed bound on bad vertices, while graph families with at least linearly many bad vertices yield PSPACE-hardness.

    Source: §5 · p. 8, §6 · p. 11

  • Takeaways & Limitations

    Transfer-graph structure identifies classes with bounded bad-vertex counts where integer reachability is in NP and patterns sufficient for PSPACE-hardness.

    Source: §5 · p. 8, §6 · p. 11, §7 · p. 16

    A stated claim is specific to v and may not hold for other vertices v_j.

    Source: §5 · p. 9

Abstract

from arXiv · show

Integer reachability is NP-complete for vector addition systems with states (VASS), but becomes PSPACE-complete in the presence of transfer operations. We refine this complexity gap for single-transfer VASS by identifying structural features of transfers responsible for the increase in complexity. Each system induces a transfer graph whose vertices are counters and whose edges represent possible transfers. We classify its vertices as good or bad, according to the branching and cyclic structure of their reachable subgraphs. Let $b$ be the number of bad vertices. We show that every positive instance admits a polynomially verifiable certificate of size $|I|^{O(b+1)}$, where $|I|$ is the input size. Consequently, integer reachability for single-transfer VASS can be decided in nondeterministic time $|I|^{O(b+1)}$; in particular, it belongs to NP for every class with a bounded number of bad counters. Conversely, we show that bad counters provide sufficient structural power to encode space-bounded computation. For every transfer graph with $b$ bad vertices, we construct a single-transfer VASS that encodes the acceptance of a Turing machine using $b^{O(1)}$ tape cells. This yields PSPACE-hardness for every polynomial-time constructible family of transfer graphs containing linearly many bad vertices. Our results isolate the transfer patterns responsible for the complexity of integer reachability.

1 Introduction

The paper studies why integer reachability is harder for transfer VASS than for ordinary VASS, using transfer-graph structure to refine the complexity picture. It gives complementary tractability and hardness results parameterized by the number of bad vertices.

1 Introduction

  • Integer reachability is NP-complete for VASS and VASS with resets, but PSPACE-complete for VASS with transfers.The paper motivates its analysis by asking what makes transfer VASS hard.Source: §1 · p. 2
  • The transfer graph has counters as vertices and possible transfers as edges, and its good and bad vertices capture structural features of reachable subgraphs.Intuitively, a good vertex has a path as its reachable graph; the precise classification rules are deferred to Definitions 6 and 7.Source: §1 · p. 2
  • The witness-size bound depends exponentially on the number of bad vertices and polynomially on the number of good vertices.The paper identifies the number of bad vertices as a parameter correlated with the exponent in the reachability-witness bound.Source: §1 · p. 2
  • For any fixed number of bad vertices, the paper establishes an NP upper bound, while its lower-bound construction encodes Turing-machine acceptance using a number of tape cells tied to the bad-vertex count.The introduction describes the upper bound and matching lower bound as the main results.Source: §1 · p. 2
  • The results identify transfer structures for which integer reachability is tractable and clarify which transfer patterns make it hard.They are presented as explaining the complexity gap between NP and PSPACE.Source: §1 · p. 2

2 Preliminaries

The preliminaries establish graph vocabulary, define transfer VASS and their integer-valued configurations, and introduce the restricted single-transfer setting used in the paper.

2.1 Graphs

  • A directed graph is specified by vertices and edges, with neighborhood, reachability, path, cycle, lasso, and connected-component notions used to describe its structure.An out-spanning tree rooted at a vertex has one path from the root to each vertex.Source: §2.1 · pp. 2–3

2.2 Single-transfer VASS

  • A transfer VASS transition moves counter contents according to a transfer function and then adds an integer update; configurations use counters in Z^d.If no counter transfers into a counter, that counter is reset to the corresponding update value.Source: §2.2 · pp. 3–4
  • Single-transfer VASS restrict each transition's transfer function, and reachability in this restricted model is as hard as reachability in transfer VASS.For pure VASS, where every transfer function is the identity, integer reachability is NP-complete.Source: §2.2 · p. 4

3 The reachability problem

The section formalizes integer reachability for transfer VASSes and uses composed transfer summaries to characterize runs. It relates bounds on the number of summaries to the size of verifiable reachability certificates.

3 The reachability problem

  • The decision problem asks whether one configuration reaches another in a single-transfer VASS, with configurations binary encoded as part of the input.The input also includes the VASS itself.Source: §3 · p. 5
  • A run is labeled by composed transfer functions, and the set of labels it induces is called its set of summary functions.The final summary function is the identity.Source: §3 · p. 5
  • Reachability in a transfer VASS can be converted to equivalent reachability in a pure VASS whose states track control states and transfer summaries.The construction is exponential in size because the set of transfer summaries is exponential.Source: §3 · p. 5
  • If a run induces at most m summary functions, integer reachability has a certificate of size polynomial in m times the input size, verifiable in polynomial time.The proof restricts the constructed pure VASS to states indexed by the run's summary functions.Source: §3 · pp. 5–6
  • The paper investigates whether positive instances admit runs inducing a polynomially bounded number of summary functions, using transfer graphs and bad vertices to characterize well-behaved subclasses.The key contributions include definitions of transfer graphs and bad vertices.Source: §3 · p. 6

4 Transfer graphs and bad vertices

A transfer graph records possible transfers between counters, and its bad vertices capture structural patterns used to analyze reachability complexity. Good vertices have a constrained reachable-subgraph structure.

4 Transfer graphs and bad vertices

  • A vertex is bad if it lies on a simple cycle of length at least three, branches to at least two neighbours, or reaches structures meeting either condition.Good vertices are precisely those that are not bad.Source: §4 · p. 6
  • A transfer graph has counters as vertices and an edge for each possible transfer from one counter to another.The graph depends only on the transfers associated with the VASS transitions.Source: §4 · p. 6
  • Converting transfer-VASS reachability to single-transfer VASS takes linear time and adds one counter, but can increase the number of bad vertices from zero to all counters.The reduction preserves the reachability problem.Source: §4 · p. 7

4.1 Structure of the graph

  • For a good vertex u, the subgraph induced by vertices reachable from u lies along a single path, with possible additional edges only to the preceding vertex.The lemma's structure follows from the exclusion of branching and longer cycles in the reachable subgraph.Source: §4.1 · p. 7

5 Upper bound on integer reachability parametrized by transfer graph

Section 5 bounds reachability certificates by controlling summary-function sequences through transfer-graph structure, yielding NP membership when the number of bad vertices is bounded.

5 Upper bound on integer reachability parametrized by transfer graph

  • Theorem 10 analyzes a run through its induced summary-function sequence and the sequence's restriction to P(G).The proof divides the sequence at indices where its restriction to P(G) changes.Source: §5 · pp. 7, 9
  • For every fixed bound on bad vertices, integer reachability for single-transfer VASS is in NP.The proof bounds the number of summary functions and uses it to obtain polynomial-size reachability certificates.Source: §5 · p. 8
  • For each good vertex, its values across a summary sequence change at most |N*(v)| −1 times.The proof first establishes this property for good vertices, then uses it in the theorem's bound.Source: §5 · p. 8
  • Between changes on P(G), the sequence is constant there, while its values on bad vertices are determined by finitely many choices.This bounds how much the summary functions can vary between those indices.Source: §5 · pp. 9–10

6 Lower bound on integer reachability parametrized by transfer graph

The section develops a lower-bound construction that uses bad counters in a prescribed transfer graph as memory to encode space-bounded computation in a single-transfer VASS. The construction yields PSPACE-hardness for polynomial-time constructible graph families with linearly many bad vertices.

6 Lower bound on integer reachability parametrized by transfer graph

  • For a graph G with n bad vertices, a polynomial-time construction gives a single-transfer VASS with transfer graph exactly G that reaches its target iff the machine accepts within a space bound linear in n.The construction encodes runs of a binary-alphabet Turing machine; Lemma 19 states the corresponding reachability equivalence.Source: §6 · pp. 10–11
  • PSPACE-hardness follows for every polynomial-time constructible graph family whose graphs contain linearly many bad vertices.The reduction uses PSPACE-complete space-bounded Turing-machine acceptance and the construction of Lemma 19.Source: §6 · p. 11

6.1 The Proof of Lemma 19

  • The proof of Lemma 19 extracts a large clean-simple subgraph, applies the encoding there, then adds missing transfers without changing reachability between the original VASS states.The added states and transitions allow missing transfers but do not connect to the original control states.Source: §6.1 · p. 11

6.1.2 Proof of Lemma 26

  • The Lemma 26 proof translates bounded-space machine acceptance to automata-with-memory reachability, then uses counter encodings and transfer-based tests to verify guessed configurations and make incorrect guesses prevent reaching the target.The automaton-with-memory reduction is polynomial-time; its memory cells are represented by counters storing -1 or 1.Source: §6.1.2 · pp. 12–14
  • The clean-simple graph can be partitioned so its good vertices supply positive and negative sets, while bad vertices supply at least n/5 cell counters.The construction places green good vertices in CPos, red good vertices in CNeg, and splits bad vertices among the sets; all but some type-3 bad vertices are in CCell.Source: §6.1.2 · p. 16
  • Each memory cell is represented by a counter in CCell, and automaton testing transitions are implemented with testing gadgets while updates change the corresponding counter.The testing gadgets are supplied by Propositions 32, 33, and 34; the construction also gives Y-shaped and lasso transfer graphs for Propositions 33 and 34.Source: §6.1.2 · pp. 15–16
  • Initial and final markings preserve the automaton states, set counters outside CCell to zero, and assign cell counters their corresponding memory values.Source: §6.1.2 · p. 16

7 Conclusion

The conclusion identifies bad vertices as the transfer-graph structure underlying the complexity of integer reachability in single-transfer VASS.

7 Conclusion

  • Integer reachability is in NP for single-transfer VASS when the number of bad vertices is bounded.This follows from the bound on the number of summary functions.Source: §7 · p. 16
  • Every polynomial-time constructible family of transfer graphs with sufficiently many bad vertices yields PSPACE-hardness.The conclusion states this for families containing linearly many bad vertices.Source: §7 · p. 16
  • Together, the upper and lower bounds characterize transfer structures responsible for the complexity gap.Source: §7 · p. 16

A Missing proofs from Section 4

The proof replaces complicated transfer functions with sequences of simple transfers, using an extra counter to handle cycles.

A Missing proofs from Section 4

B Missing proofs from Section 6

The ShiftY and ShiftLasso subroutines use checked nondeterministic guesses to shift counter contents while ensuring incorrect guesses leave invalid configurations. Repeated shifts expose the original value needed to choose the procedure’s final control state.

ShiftY

  • A correct ShiftY guess cyclically shifts the path counters, while an incorrect guess makes the resulting configuration invalid.The procedure guesses whether the value in lm is 1 or −1, then uses transfers to implement the shift.Source: B Missing proofs from Section 6 · p. 18
  • Repeated ShiftY calls move the original l1 content to lm, so the final guess determines whether control goes to p−1 or p1.The loop applies ShiftY for 1 ≤ j ≤ m and begins at p1,init.Source: B Missing proofs from Section 6 · p. 19
  • ShiftY stores only the last guessed value in control, avoiding an exponential blow-up.Source: B Missing proofs from Section 6 · p. 19

ShiftLasso

  • ShiftLasso preserves invalidity on invalid inputs; correct guesses preserve the counter vector while cyclically shifting the l1,…,lm path.Its stated checks include guesses of lm and, when correct, c2.Source: B Missing proofs from Section 6 · pp. 18–19
  • ShiftLasso temporarily alters lm to check its guessed value, transfers it to ce, shifts the l-path, then restores the cycle’s counter distribution.A wrong guess leaves an invalid vector; the cycle is rotated back under the assumption that the guess was correct.Source: B Missing proofs from Section 6 · pp. 19–20
  • RotateCycle temporarily zeros the cursor counter and uses n − 1 transfers for a one-step cycle shift, retaining the cursor guess across partial rotations.Source: B Missing proofs from Section 6 · p. 20

C Simple graphs

The section simplifies transfer graphs while preserving many bad vertices, using their structural organization to guide edge removals. It also gives a polynomial-time reduction from bounded-space Turing-machine acceptance to reachability.

Simple-graph simplification

  • Removing edges from G1 to G2 preserves the number of bad vertices when edges go only from G1 to G2 and good vertices in G1 remain good.The proof applies this claim to separate graph regions during simplification.Source: C Simple graphs · p. 23

Simple-graph structure

  • Bad type-2 vertices connected by an edge lie in the same strongly connected component, and a type-4 vertex cannot belong to such a component.Source: C Simple graphs · pp. 24–25

Simple-graph simplification

  • A weighted graph on good vertices guides edge removals that yield a clean-simple subgraph retaining at least half the bad vertices.The construction seeks a red-green coloring with at least half the total edge weight crossing colors.Source: C Simple graphs · pp. 26–27

Turing-machine reduction

  • The reduction encodes tape symbols 0 and 1 as −1 and 1, respectively, and uses control states for machine states and memory positions.Source: C Simple graphs · p. 27
  • Each Turing-machine step is simulated by an enabled test transition followed by an update transition, and acceptance leads through cleanup to a fixed final configuration.The cleanup phase resets memory cells to (−1), accommodating arbitrary tape contents at acceptance.Source: C Simple graphs · pp. 27–28
  • A polynomial-time reduction maps bounded-space Turing-machine acceptance to reachability, establishing PSPACE-hardness for automata with memory.The construction has O(n · |δ| + n) transitions, with n given in unary.Source: C Simple graphs · pp. 27–28
Loading 2610.01440v1…