PaperlayerView exact revision on arXiv

Source-linked AI summary

Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension

Jérôme Leroux, Sylvain Schmitz

arXiv:1903.08575v1cs.LO

TL;DR

VASS reachability matters for verification and related decision problems, but its known upper bound was not primitive-recursive even in fixed dimension. The paper refines decomposition algorithms and their termination proof, establishing ACKERMANN upper bounds generally and primitive-recursive bounds in fixed dimension.

  • Problem

    VASS reachability is a central decision problem, but its best known upper bound was not primitive-recursive even for fixed-dimensional systems.

    Source: §1 · pp. 2–3

  • Method

    The paper refines Mayr–Kosaraju–Lambert-style decomposition algorithms with a cycle-dimension termination argument and a method that avoids Karp and Miller coverability trees.

    Source: §1 · p. 3

  • Results

    The refined algorithm gives ACKERMANN upper bounds generally and Fd+4 upper bounds in fixed dimension d for VASS reachability and downward language inclusion.

    Source: §7 · p. 24

  • Takeaways & Limitations

    The downward language inclusion problem is ACKERMANN-complete, while whether VASS reachability admits a better algorithm remains unclear.

    Source: §7 · p. 24

    For dimensions three and above, Fd+4 is the best known upper bound, though the authors expect it could be refined further.

    Source: §7 · p. 24

Abstract

from arXiv · show

The reachability problem in vector addition systems is a central question, not only for the static verification of these systems, but also for many inter-reducible decision problems occurring in various fields. The currently best known upper bound on this problem is not primitive-recursive, even when considering systems of fixed dimension. We provide significant refinements to the classical decomposition algorithm of Mayr, Kosaraju, and Lambert and to its termination proof, which yield an ACKERMANN upper bound in the general case, and primitive-recursive upper bounds in fixed dimension. While this does not match the currently best known TOWER lower bound for reachability, it is optimal for related problems.

1. Introduction

VASS reachability is central to verification and other inter-reducible decision problems, but its complexity has a wide gap between known lower and upper bounds. The paper refines decomposition algorithms and their termination analysis, obtaining ACKERMANN upper bounds generally and primitive-recursive bounds in fixed dimension.

1. Introduction

  • VASS are equivalent to Petri nets and model discrete resources, while reachability underpins decidability results across several fields.The paper notes applications in logic, formal languages, and verification.Source: §1 · p. 2
  • The best known lower bound is TOWER-hard, while prior upper bounds reached Fω2; this left a large complexity gap.The decomposition algorithm’s non-primitive-recursive complexity also matters because its full output supports other decision problems.Source: §1 · pp. 2–3
  • The paper proves VASS reachability is in ACKERMANN = Fω and, in fixed dimension d, in Fd+4.These bounds improve on Fω2 generally and Fω·(d+1) in fixed dimension.Source: §1 · p. 3
  • The decomposition algorithm refines a structure until a condition guarantees an execution witnessing reachability.Mayr, Kosaraju, and Lambert use different structures and corresponding conditions in their algorithms.Source: §1 · p. 3
  • A new termination argument uses the dimensions of vector spaces spanned by cycles, yielding ACKERMANN bounds generally and primitive-recursive bounds in fixed dimension.A second insight avoids computing Karp and Miller coverability trees using Rackoff-inspired techniques; together the insights give Fd+4 in dimension d.Source: §1 · p. 3
  • The fixed-dimension downward-language inclusion problem is Fd-hard for d ≥3, close to the Fd+4 upper bound obtained from the decomposition algorithm.The full decomposition also supports deciding inclusion between downward-closures of labelled VASS languages.Source: §1 · p. 4

2. Background

A VASS combines finite control states with integer-vector transition weights and executes transitions while keeping every coordinate nonnegative. The reachability question asks whether one finite configuration can reach another along a valid path.

2. Background

  • A VASS has a finite set of control states and transitions labeled by integer vectors; its dimension is the vector length.The paper focuses on VASS because it exploits properties of their underlying directed graphs.Source: §2 · pp. 4–5
  • A VASS path is a sequence of transitions whose consecutive states match; a complete path runs from the input state to the output state.Its displacement is the sum of its transition vectors, and its Parikh image records each transition’s number of occurrences.Source: §2 · p. 5
  • A configuration pairs a state with a vector of natural-number resources, and an action adds its vector component-wise while preserving nonnegativity.The VAS reachability problem asks whether some action sequence takes one finite configuration to another.Source: §2 · pp. 4–5
  • VASS reachability asks whether the output configuration can be reached from the input configuration by a valid execution.The corresponding VAS problem reduces to VASS reachability; the converse encoding increases dimension by three.Source: §2 · pp. 5–6

3. Decomposition Structures

This section formalizes the structures used by the decomposition algorithm and develops rank and linear-system tools for reasoning about their action languages.

3. Decomposition Structures

  • The decomposition algorithm proceeds globally using structures called KLM sequences, named after Kosaraju, Lambert, and Mayr.The paper identifies these underlying structures as KLM sequences.Source: §3 · p. 6

3.1. KLM Sequences.

  • Reachability for a VASS reduces to checking whether the corresponding KLM sequence’s action language is nonempty.That language comprises action words matching the sequence’s path and configuration conditions.Source: §3.1 · p. 6

3.2. Ranks and Sizes.

  • For a strongly connected VASS, every transition spans the same cycle-displacement space, letting ranks count transitions by that space’s dimension.A VASS rank is a tuple whose components count transitions with cycle-space dimensions; KLM-sequence ranks combine the ranks of their VASS components.Source: §3.2 · pp. 6–7

3.3. Characteristic System.

  • A characteristic system is a linear-equation overapproximation: every action-language word yields a model, so an unsatisfiable sequence has empty action language.The model for a word uses the Parikh image of each complete path in its decomposition.Source: §3.3 · pp. 7–8

3.4. Homogeneous Characteristic System.

  • The homogeneous system identifies which configuration and transition values can grow unboundedly, while the sum of bounded values is at most |ξ|^(|ξ|−1).For the input, transition-count, and output variables, unboundedness is characterized by a positive value in a model of the homogeneous system.Source: §3.4 · p. 9

4. The Decomposition Algorithm

The decomposition algorithm refines clean KLM sequences through rank-decreasing, language-preserving transformations, yielding normal sequences. Strict rank descent and finite branching ensure a finite decomposition forest, while a bounded-witness result gives a short word for each normal sequence.

4. The Decomposition Algorithm

  • The decomposition forest terminates because each non-normal sequence has finitely many lower-ranked children, and well-founded lexicographic ranks give finite branches.The forest has finitely many roots and finite branching, so König’s Lemma implies it is finite.Source: §4 · p. 10

4.1. Elementary Decomposition Steps.

  • Clean sequences are formed by decomposing into strongly connected components, saturating, and retaining sequences with satisfiable characteristic systems; bounded or unpumpable sequences are then unfolded and cleaned.Initialization and each decomposition step apply elementary transformations while preserving the represented language.Source: §4.1 · p. 10

4.1.1. Strongly Connected KLM Sequences.

  • In time exp(|ξ|), a non-strongly-connected sequence can be replaced by finitely many strongly connected sequences preserving its language, with strictly lower ranks and sizes at most |ξ|.Source: §4.1.1 · p. 10

4.1.2. Saturated KLM Sequences.

  • A strongly connected sequence can be decomposed in time exp(|ξ||ξ|) into saturated sequences preserving its language, with non-increasing ranks and sizes at most |ξ||ξ|.The construction replaces selected ω components with bounded values supplied by the characteristic system.Source: §4.1.2 · p. 11

4.1.3. Unbounded KLM Sequences.

  • Unboundedness is in NP; a strongly connected bounded sequence can be decomposed in time exp(|ξ||ξ|) into language-equivalent sequences of strictly lower rank and size at most |ξ||ξ|.Transitions whose use is bounded are unfolded, while transitions with unbounded use are retained.Source: §4.1.3 · pp. 12–13

4.2. Rigid KLM Sequences.

  • In polynomial time, the algorithm detects non-rigidity in a strongly connected sequence and produces a language-equivalent sequence of strictly lower rank.The same lemma gives a polynomial-time test for whether the sequence is not rigid.Source: §4.2 · p. 14

4.2.1. Pumpable KLM Sequences.

  • Pumpability is decidable in exponential space, and unpumpable sequences can be unfolded using a double-exponential bound while decreasing rank.This refines the Karp–Miller-tree bound, whose worst-case complexity is Ackermannian; the unfolding preserves a language decomposition.Source: §4.2.1 · pp. 15–16
  • Whether a KLM sequence ξ is pumpable is in EXPSPACE; for strongly connected, unpumpable ξ, computation takes exp(|ξ|2+dd) time and yields ξ′∈Ξ with rank(ξ′)<lex rank(ξ) and |ξ′|≤|ξ|2+dd for every ξ′.Source: §4.2.1 · p. 16

4.3.1. Cleaning Lemma.

  • Any KLM sequence can be transformed in time exp(g(|ξ|)) into finitely many clean sequences preserving its language, with nonincreasing lexicographic rank and size at most g(|ξ|).Source: §4.3.1 · p. 18

4.3.2. Decomposition Lemma.

  • A clean, nonnormal KLM sequence can be decomposed in time exp(h(|ξ|)) into clean sequences preserving its language, with strictly lower lexicographic rank and size at most h(|ξ|).Source: §4.3.2 · p. 18

4.3.3. Bounded Witness Lemma.

  • In space O(ℓ(|ξ|)), every normal ξ yields a word σ∈Lξ of length at most ℓ(|ξ|), where ℓ(x)=x3x.A normal sequence is satisfiable, strongly connected, saturated, rigid, pumpable, and unbounded.Source: §4.3 · p. 17, §4.3.3 · p. 18

5. Complexity Upper Bounds

The section bounds decomposition-forest branches using controlled descending ordinal ranks, then applies those bounds to the decomposition algorithm and VASS reachability. It establishes an ACKERMANN upper bound generally and an Fd+4 bound for fixed dimension d.

5.1. Controlled Sequences of Ranks.

  • Ordinal rank is represented in ω^(d+1) using the components of the KLM-sequence rank.The representation preserves the lexicographic order of ranks as ordinal order.Source: §5.1 · p. 19
  • Ranks along a decomposition-forest branch form a descending ordinal sequence whose lengths can be bounded because successive KLM sequences are controlled.The ordinal rank reformulates the lexicographic ranking; controlled sequences have bounded length.Source: §5.1 · p. 19, §5.1.1 · p. 20

5.1.2. Subrecursive Functions.

  • Hardy and Cichoń hierarchies express iterated growth, and the Hardy hierarchy reaches Ackermannian growth at H^(ω^ω).The section uses these fast-growing functions to classify the complexity bounds.Source: §5.1.2 · pp. 20–21

5.1.3. Length Function Theorem.

  • The maximal length of (n0, h)-controlled descending ordinal sequences in ω^(d+1) is h^(ω^(d+1))(n0), for n0 ≥ d + 1.The theorem supplies the branch-length bound used in the later complexity analysis.Source: §5.1.3 · p. 21
  • A reachable configuration pair has a witness bounded using the length-function estimates for descending ranks along decomposition-forest branches.The small-witness property gives a length bound in terms of g, h, and ℓ.Source: §5.1.3 · p. 21

5.2.2. Complexity Upper Bounds.

  • The decomposition algorithm computes the full decomposition within a fixed elementary function of h^(ω^(d+1))(g(|ξ0|)).The decomposition forest has elementary branching and each step takes elementary time in its KLM sequence size.Source: §5.2.2 · p. 22
  • VASS reachability is in ACKERMANN, and in Fd+4 when dimension d is fixed.The proof bounds the time for computing the full decomposition and relates it to reachability.Source: §5.2.2 · pp. 22–23

5.2.3. Combinatorial Algorithm.

  • A combinatorial alternative enumerates paths up to the small-witness length bound and stops when it finds a witness or exhausts the search.The bound itself can be computed in time elementary in its value.Source: §5.1.3 · p. 21, §5.2.3 · p. 23

6. Application: Downward Language Inclusion

The section applies the full-decomposition upper bound to deciding inclusion between downward-closures of labelled VASS languages. This problem is ACKERMANN-complete generally, with the stated fixed-dimension bounds.

Downward Language Inclusion.

  • Downward language inclusion asks whether the downward-closure of one labelled VASS language is included in that of another.A downward-closure contains words obtainable by deleting letters from words in the original language.Source: §6 · p. 23
  • Although every downward-closure is regular, that fact alone does not ensure an automaton can be computed from a labelled VASS and configurations.Given a full decomposition, an automaton for the downward-closure can be constructed in logarithmic space.Source: §6 · pp. 23–24
  • The VASS downward language inclusion problem is in ACKERMANN and in Fd+4 when labelled VASS dimension is fixed to d.The upper bound follows by constructing finite automata from full decompositions and deciding regular-language inclusion.Source: §6 · p. 24

Lower Bounds.

  • The VASS downward language inclusion problem is ACKERMANN-hard and Fd-hard for fixed dimension d ≥ 3.Together with the upper bound, this makes the general problem ACKERMANN-complete.Source: §6 · p. 24

7. Concluding Remarks

The paper refines decomposition algorithms to obtain Ackermannian-time bounds generally and primitive-recursive bounds for fixed-dimensional VASSes. The downward language inclusion problem is ACKERMANN-complete, while reachability remains open to potentially better algorithms.

7. Concluding Remarks.

  • The refined decomposition algorithm runs in Ackermannian time generally and primitive-recursive time for fixed-dimensional VASSes.These bounds yield ACKERMANN and Fd+4 upper bounds for reachability and downward language inclusion, respectively.Source: §7 · p. 24
  • VASS downward language inclusion is ACKERMANN-complete, whereas reachability is only known to be TOWER-hard and may admit a better algorithm.The reachability upper bound does not match its stated lower bound.Source: §7 · p. 24
  • For binary encoding, reachability is NP-complete in dimension one and PSPACE-complete in dimension two; for unary encoding, both are NL-complete.For dimensions three and above, Fd+4 is the best known upper bound in the passage, and the authors expect it could be refined.Source: §7 · p. 24

Appendix A. Pumpability

The appendix section provides details of the proof of Lemma 4.15.

Appendix A. Pumpability.

A.1. Rackoff Extraction.

Rackoff-inspired extraction lemmas shorten executions while ensuring every final counter is at least C−|G|. The proof bounds the word length by induction on the number of initially finite coordinates.

A.1. Rackoff Extraction.

  • |σ| < C(d+1)^(d+1), with every final counter at least C−|G|, under the lemma’s coordinate-threshold assumption.The lemma assumes C ≥ |G| and that each coordinate reaches the stated threshold along the execution.Source: §A.1 · p. 26
  • Lemma A.2 counts coordinates that are initially finite and produces a word reaching a configuration whose coordinates are all at least C−|G|.The excerpt defines the count as |{i | c0(i) ∈ N}|; the preceding text says Lemma A.1 follows from Lemma A.2.Source: §A.1 · p. 26
  • The induction parameter is the number of initially finite coordinates; when there are none, a simple path supplies the base case.For the induction step, the proof considers the first point where a finite coordinate reaches the threshold.Source: §A.1 · p. 27
  • Removing cycles before the first threshold hit and applying induction to the remaining suffix bounds the execution length.The proof combines the prefix and suffix bounds using C ≥ 2.Source: §A.1 · p. 27
  • The construction keeps every intermediate vector nonnegative by tracking coordinates in I separately from those in H\I.For coordinates in H\I, the proof uses the lower bound on the suffix endpoint and bounds the possible decrement along the word.Source: §A.1 · p. 27

A.2. Unfoldings.

The section defines forward and backward unfoldings and uses forward unfoldings to decompose the language of a KLM sequence. Its proof relies on threshold crossings and a contradiction based on increasing finite coordinates.

A.2. Unfoldings.

  • An (i, B, r)-unfolding tracks coordinate i in a bounded set with an ω overflow state; backward unfolding is defined symmetrically.Its transitions preserve the coordinate value below B and move to ω when the update reaches or exceeds B.Source: §A.2 · p. 28
  • For a nonempty set I of nonfixed components with finite FaccG(x)(i), the language Lξ is a union of languages from forward unfoldings over r ∈ N_B.The lemma identifies an i ∈ I for which this decomposition holds.Source: §A.2 · p. 28
  • The proof uses the first time every coordinate in I reaches B to split the execution, and rules out a later return to qin.If qin returned, the argument constructs a path that increases every coordinate in I, contradicting the finite FaccG(x) values.Source: §A.2 · pp. 28–29
  • The prefix is shortened using Lemma A.1, then a simple path back to qin preserves nonnegativity while increasing the coordinates in I.The resulting word has positive net change in each coordinate in I.Source: §A.2 · pp. 28–29

Appendix B. Unbounded Equations

Appendix B uses a linear-algebra decomposition to analyze unbounded values in characteristic systems. It relates unbounded model values to positive values in a restricted system and bounds the sum of bounded values.

Appendix B. Unbounded Equations

  • Every vector in X decomposes into a vector in X plus a finite sum of vectors in X0.Minimal nonzero pairs in P have bounded norm and decompose every pair in P [23, Theorem 1].Source: Appendix B · pp. 29–30
  • For each listed coordinate or transition value, unboundedness over models of Eξ holds exactly when some model of E0ξ gives that value a positive value.The result covers m_j(i), φ_j(t), and n_j(i); the sum of bounded values is at most |ξ||ξ|−1.Source: Appendix B · p. 30
  • A model h of Eξ can be combined with n copies of a model h0 of E0ξ to obtain another model of Eξ.This observation is used to derive the stated unboundedness criterion.Source: Appendix B · p. 30

Appendix C. Normal KLM Sequences

Appendix C proves Lemma 4.19 for normal KLM sequences.

Appendix C. Normal KLM Sequences

  • The appendix assumes ξ is a normal KLM sequence with the stated sequence form and component graphs Gj.The passage specifies Gj = (Qj, qin,j, qout,j, Tj) for each index j.Source: Appendix C · p. 30

C.1. Models of Normal KLM Sequences.

The appendix develops bounded-model, flow-function, and pumping ingredients for normal KLM sequences. Together, these ingredients support short words that can be fired while increasing selected components.

C.1. Models of Normal KLM Sequences.

  • Small models of the KLM sequence’s equation systems provide the bounded-model ingredient used in the construction.The proof uses models of Eξ and E0ξ, including models with bounded norm.Source: §C.1 · p. 31

C.2. Flow Functions.

  • For each KLM component, a flow function tracks transition effects between its entry and exit configurations.The function assigns values to states so each transition updates the value by its transition vector.Source: §C.2 · p. 31

C.3. Pumping in Normal KLM Sequences.

  • For a pumpable component, short words can be chosen to increase selected finite components while remaining fireable.The proof uses cycles that increase those components; flow functions establish nonnegativity for the other finite components along the word.Source: §C.2 · p. 31, §C.3 · p. 32

C.4. Proof of Lemma 4.19.

Every normal KLM sequence has a bounded-length witness, computable in space O(ℓ(|ξ|)). The proof builds it from bounded models and cycle words, then assembles paths through the strongly connected components.

C.4. Proof of Lemma 4.19.

  • A normal KLM sequence ξ has a witness σ ∈ Lξ of length at most ℓ(|ξ|), computable in space O(ℓ(|ξ|)).The lemma defines ℓ(x) as x3x.Source: §C.4 · p. 32
  • The proof combines equation-system models with cycle words to construct the witness’s component paths.It uses models and the word pairs from Claim C.4, then forms cycles whose Parikh images cover transitions.Source: §C.4 · p. 32
  • Positive transition counts in each strongly connected component yield a path word between its entry and exit states.Euler’s Lemma supplies the path with the prescribed Parikh image.Source: §C.4 · p. 33
Loading 1903.08575v1…