Vector Addition System¶
An infinite-state transition system whose configurations are nonnegative integer counter vectors and whose finitely specified steps add integer displacement vectors only when no counter would become negative.
Core Idea¶
A vector addition system (VAS) is a finitely presented, generally infinite-state transition system over nonnegative integer counters. In one standard formulation, a marked d-dimensional VAS is a pair (A, x₀), where A is a finite subset of integer displacement vectors Z^d and the initial configuration x₀ lies in N^d. From configuration x, an action a ∈ A may fire exactly when x+a ∈ N^d; firing produces the successor x+a. A run is a finite or infinite sequence of enabled firings.
Scope of Application¶
Concurrent and distributed processes. Counters can record populations of processes in local states, pending messages, available resources, outstanding requests, or tokens in buffers. An update represents one atomic event consuming and producing quantities. Interleaving of enabled updates abstracts scheduling while retaining resource feasibility.
Petri-net analysis. Petri-net markings are nonnegative token-count vectors, and firings transform markings through integer effects subject to enabling. The close correspondence lets VAS techniques analyze Petri-net reachability, coverability, boundedness, termination, and liveness. Esparza and Nielsen's survey treats the independently developed formalisms as mathematically equivalent at the level relevant to these decision problems.
Clarity¶
The decisive test is the transition equation plus its guard:
x ─a→ y iff a ∈ A, y=x+a, and y ∈ N^d.
This formula identifies both what changes and why a candidate action can be blocked. An action (-2,3) consumes two units from the first counter and produces three in the second. It is enabled at (2,0) and produces (0,3), but is disabled at (1,100) despite the large second coordinate. Feasibility is componentwise.
Manages Complexity¶
VAS compresses an unbounded collection of concrete population states into three finite ingredients: dimension, start vector, and update set. It forgets identities of interchangeable entities and retains their counts. An event that moves one of a million identical workers from “idle” to “busy” is one displacement vector, not a million individually named transitions.
Abstract Reasoning¶
A disciplined VAS analysis follows these steps:
- Choose counters and units. State exactly what each coordinate counts and ensure values are nonnegative integers. 2. Define atomic updates. For every event, give one displacement vector and verify which consumption requirements its negative components enforce. 3. Choose the initial marking. Reachability is relative to the marked start, not only to the update set. 4. Check enabling by prefixes. A candidate action word is a run only if every intermediate sum remains in
N^d.
Knowledge Transfer¶
The exact abstraction transfers among Petri-net verification, VASS theory, counter abstractions of concurrent programs, population protocols, discrete reaction systems, workflow nets, and resource-allocation models when the same roles remain literal: nonnegative integer counts, finitely many additive updates, lower-bound enabling, and interleaved firing.
Transfer must preserve what was discarded. If individual identity, FIFO order, time, probability, data values, or causal provenance changes the property, a count-only VAS may be too coarse. Two configurations with equal count vectors are identical to the VAS even if the underlying histories differ.
Relationships to Other Abstractions¶
Current abstraction Vector Addition System Domain-specific
Parents (1) — more general patterns this builds on
-
Vector Addition System is a kind of State and State Transition Prime
The candidate strictly instantiates State and State Transition: the current vector is a sufficient state, enabled additions form the transition relation, the initial marking fixes the generated behavior, and the reachable graph captures.
Hierarchy path (1) — routes to 1 parentless root
- Vector Addition System → State and State Transition → Phase Space
Neighborhood in Abstraction Space¶
Vector Addition System sits in a sparse region of the domain-specific corpus (88th percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.
Family — Unclustered & Miscellaneous (1565 abstractions)
Nearest neighbors
- Controlled Invariant Subspace — 0.82
- Special Ordered Set — 0.80
- Euclidean Space — 0.80
- Control-Theoretic Orbit — 0.79
- Sequential Dynamical System — 0.79
Computed from structural-signature embeddings · 2026-09-08