# Vector addition system

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/Vector_addition_system
> Markdown URL: https://mediated.wiki/source/Vector_addition_system.md
> Source: https://en.wikipedia.org/wiki/Vector_addition_system
> Source revision: 1304135865
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

Mathematical modeling language

A **vector addition system** (**VAS**) is one of several mathematical modeling languages for the description of [distributed systems](/source/Distributed_systems). Vector addition systems were introduced by [Richard M. Karp](/source/Richard_M._Karp) and Raymond E. Miller in 1969,[1] and generalized to **vector addition systems with states** (**VASS**) by [John E. Hopcroft](/source/John_Hopcroft) and Jean-Jacques Pansiot in 1979.[2] Both VAS and VASS are equivalent in many ways to [Petri nets](/source/Petri_net) introduced earlier by [Carl Adam Petri](/source/Carl_Adam_Petri).

Example of a vector addition with states. In this VASS, e.g., q(1,2) can be reached from p(0,0), but q(0,0) cannot be reached from p(0,0).

## Informal definition

A *vector addition system* consists of a finite set of [integer](/source/Integer) [vectors](/source/Row_vector) with all vectors having the same length. An initial vector is seen as the initial values of multiple counters, and the vectors of the VAS are seen as updates. These counters may never drop below zero. More precisely, given an initial vector with non negative values, the vectors of the VAS can be added componentwise, given that every intermediate vector has non negative values. A *vector addition system with states* is a VAS equipped with control states. More precisely, it is a finite [directed graph](/source/Directed_graph) with [arcs](/source/Directed_graph#Basic_terminology) labelled by [integer](/source/Integer) vectors. VASS have the same restriction that the counter values should never drop below zero.

Vector addition systems can be seen as a weak [counter machine](/source/Counter_machine), which is unable to test that a counter is zero (but it can verify that a counter is positive, by trying to decrement it. If the test fails, execution terminates).

## Formal definitions and basic terminology

- A *VAS* is a finite set V ⊆ Z d {\displaystyle V\subseteq \mathbb {Z} ^{d}} for some d ≥ 1 {\displaystyle d\geq 1} .

- A *VASS* is a finite [directed graph](/source/Directed_graph) ( Q , T ) {\displaystyle (Q,T)} such that T ⊆ Q × Z d × Q {\displaystyle T\subseteq Q\times \mathbb {Z} ^{d}\times Q} for some d > 0 {\displaystyle d>0} .

### Transitions

- Let V ⊆ Z d {\displaystyle V\subseteq \mathbb {Z} ^{d}} be a VAS. Given a vector u ∈ N d {\displaystyle u\in \mathbb {N} ^{d}} , the vector u + v {\displaystyle u+v} can be *reached*, in one transition, if v ∈ V {\displaystyle v\in V} and u + v ∈ N d {\displaystyle u+v\in \mathbb {N} ^{d}} .

- Let ( Q , T ) {\displaystyle (Q,T)} be a VASS. Given a *configuration* ( p , u ) ∈ Q × N d {\displaystyle (p,u)\in Q\times \mathbb {N} ^{d}} , the configuration ( q , u + v ) {\displaystyle (q,u+v)} can be *reached*, in one transition, if ( p , v , q ) ∈ T {\displaystyle (p,v,q)\in T} and u + v ∈ N d {\displaystyle u+v\in \mathbb {N} ^{d}} .

## VASS and VAS

A VAS is obviously a special case of VASS. On the other hand, a VASS of dimension *n* can be simulated by a VAS of dimension *n*+3, as shown by [Hopcroft](/source/John_Hopcroft) and [Pansiot](https://en.wikipedia.org/w/index.php?title=Jean-Jacques_Pansiot&action=edit&redlink=1).[3] In this system, the additional three coordinates encode the state. Each transition of the VASS is simulated by a sequence of three VAS transitions, where the first two just manipulate the state-encoding coordinates.

## VASS and Petri Nets

A [Petri net](/source/Petri_net) can be seen as a VASS: consider a Petri net ( S , T , W ) {\displaystyle (S,T,W)} , where

- S = { 1 , … , n } {\displaystyle S=\{1,\dots ,n\}} is a [finite set](/source/Finite_set) of *places*

- *T* is a finite set of *transitions*

- W : ( S × T ) ∪ ( T × S ) → N {\displaystyle W:(S\times T)\cup (T\times S)\to \mathbb {N} } specifies the number of tokens that a transition consumes and produces.

Then a marking of the net can be seen as a vector in N d {\displaystyle \mathbb {N} ^{d}} , where d = | S | {\displaystyle d=|S|} , and a transition *t* as a pair of VASS transitions ( p , v , q ) , ( q , v ′ , p ) {\displaystyle (p,v,q),(q,v',p)} where *q* is an auxiliary control state, v i = − W ( i , t ) {\displaystyle v_{i}=-W(i,t)} and v j ′ = W ( t , j ) {\displaystyle v'_{j}=W(t,j)} . Similarly, a VAS can be formulated as a Petri net.

## Properties of VAS(S) and Decision Procedures

### Reachability

The [reachability problem](/source/Reachability_problem) for Petri nets is to decide, given a A VAS(S) and a state (a vector in the case of VAS, a vector and a control state in the case of VASS) whether another given state is reachable from it by a any finite sequence of transitions.

This problem was shown to be [EXPSPACE](/source/EXPSPACE)-hard[4] years before it was shown to be decidable at all.[5] In 2021, this problem was shown to be [Ackermann-complete](/source/Ackermann_function) (thus not [primitive recursive](/source/Primitive_recursive_function)), independently by Jerome Leroux[6] and by Wojciech Czerwiński and Łukasz Orlikowski.[7] The Ackermannian upper bound is due to Leroux and Schmitz[8] whose algorithm admits a [primitive-recursive](/source/Primitive_recursive_function) upper bound when the dimension is a constant.

The **mutual reachability problem** (aka reversible reachability) asks for two states, *x* and *y*, whether *x* is reachable from *y* and vice versa. This problem is much easier than unidirectional reachability, and was proved to be EXPSPACE-complete.[9]

### Coverability

Given two states of a VAS, *x* and *y*, the coverability question asks whether there is a sequence of transitions that takes the initial state *x* into a state x ′ {\displaystyle x'} such that x ′ ≥ y {\displaystyle x'\geq y} (comparison is element-wise). In a VASS, one also specifies the control states, and the problem is equivalent to the (superficially) simpler problem of asking whether a given control state, *q*, is reachable from initial state ( p , x ) {\displaystyle (p,x)} . The coverability problem is EXPSPACE-complete.[4]

### Boundedness

The boundedness problem for a VASS is: given initial state ( p , x ) {\displaystyle (p,x)} , is the set of states reachable from ( p , x ) {\displaystyle (p,x)} finite? This decision problem is also EXPSPACE-complete.[10]

## See also

- [Petri net](/source/Petri_net)

- [Finite-state machine](/source/Finite-state_machine)

- [Communicating finite-state machine](/source/Communicating_finite-state_machine)

- [Kahn process networks](/source/Kahn_process_networks)

- [Process calculus](/source/Process_calculus)

- [Actor model](/source/Actor_model)

- [Trace theory](/source/Trace_theory)

## References

1. **[^](#cite_ref-1)** Karp, Richard M.; Miller, Raymond E. (May 1969). ["Parallel program schemata"](https://doi.org/10.1016%2FS0022-0000%2869%2980011-5). *Journal of Computer and System Sciences*. **3** (2): 147–195. [doi](/source/Doi_(identifier)):[10.1016/S0022-0000(69)80011-5](https://doi.org/10.1016%2FS0022-0000%2869%2980011-5).

1. **[^](#cite_ref-2)** Hopcroft, John E.; Pansiot, Jean-Jacques (1979). "On the reachability problem for 5-dimensional vector addition systems". *Theoretical Computer Science*. **8** (2): 135–159. [doi](/source/Doi_(identifier)):[10.1016/0304-3975(79)90041-0](https://doi.org/10.1016%2F0304-3975%2879%2990041-0). [hdl](/source/Hdl_(identifier)):[1813/6102](https://hdl.handle.net/1813%2F6102).

1. **[^](#cite_ref-3)** Hopcroft, John; Pansiot, Jean-Jacques. "On the reachability problem for 5-dimensional vector addition systems". *Theoretical Computer Science*. **8** (2). Elsevier: 135–159.

1. ^ [***a***](#cite_ref-Lip76_4-0) [***b***](#cite_ref-Lip76_4-1) [Lipton, R.](/source/Richard_Lipton) (1976). ["The Reachability Problem Requires Exponential Space"](http://citeseer.ist.psu.edu/contextsummary/115623/0). *Technical Report 62*. Yale University: 305–329.

1. **[^](#cite_ref-5)** Mayr, Ernst W. "An Algorithm for the General Petri Net Reachability Problem". *SIAM Journal on Computing*. **13** (3). SIAM: 441–460.

1. **[^](#cite_ref-6)** Leroux, Jérôme (2021). *The Reachability Problem for Petri Nets is Not Primitive Recursive*. 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS). [arXiv](/source/ArXiv_(identifier)):[2104.12695](https://arxiv.org/abs/2104.12695).

1. **[^](#cite_ref-7)** Czerwiński, Wojciech; Orlikowski, Łukasz (2021). *Reachability in Vector Addition Systems is Ackermann-complete*. 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS). [arXiv](/source/ArXiv_(identifier)):[2104.13866](https://arxiv.org/abs/2104.13866).

1. **[^](#cite_ref-8)** Leroux, Jérôme; Schmitz, Sylvain. "Reachability in vector addition systems is primitive-recursive in fixed dimension". *34th Annual ACM/IEEE Symposium on Logic in Computer Scienc*. LICS. IEEE.

1. **[^](#cite_ref-9)** Leroux, Jérôme (2013). ["Vector addition system reversible reachability problem"](https://doi.org/10.2168/LMCS-9(1:5)2013). *Logical Methods in Computer Science*. **9** (1). [arXiv](/source/ArXiv_(identifier)):[1301.4874](https://arxiv.org/abs/1301.4874). [doi](/source/Doi_(identifier)):[10.2168/LMCS-9(1:5)2013](https://doi.org/10.2168%2FLMCS-9%281%3A5%292013).

1. **[^](#cite_ref-10)** Rackoff, Charles. "The covering and boundedness problems for vector addition systems". *Theoretical Computer Science*. **6** (2). Elsevier: 223–23.

---
Adapted from the Wikipedia article [Vector addition system](https://en.wikipedia.org/wiki/Vector_addition_system) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/Vector_addition_system?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.