A vector addition system consists of a finite set of integer vectors. 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 with arcs labelled by integer vectors. VASS have the same restriction that the counter values should never drop below zero.

• A VAS is a finite set ${\displaystyle V\subseteq \mathbb {Z} ^{d}}$  for some ${\displaystyle d\geq 1}$ .
• A VASS is a finite directed graph ${\displaystyle (Q,T)}$  such that ${\displaystyle T\subseteq Q\times \mathbb {Z} ^{d}\times Q}$  for some ${\displaystyle d>0}$ .

Transitions edit

• Let ${\displaystyle V\subseteq \mathbb {Z} ^{d}}$  be a VAS. Given a vector ${\displaystyle u\in \mathbb {N} ^{d}}$ , the vector ${\displaystyle u+v}$  can be reached, in one transition, if ${\displaystyle v\in V}$  and ${\displaystyle u+v\in \mathbb {N} ^{d}}$ .
• Let ${\displaystyle (Q,T)}$  be a VASS. Given a configuration ${\displaystyle (p,u)\in Q\times \mathbb {N} ^{d}}$ , the configuration ${\displaystyle (q,u+v)}$  can be reached, in one transition, if ${\displaystyle (p,v,q)\in T}$  and ${\displaystyle u+v\in \mathbb {N} ^{d}}$ .

• Petri net
• Finite state machine
• Communicating finite-state machine
• Kahn process networks
• Process calculus
• Actor model
• Trace theory