A vector addition system (VAS) is one of several mathematical modeling languages for the description of distributed systems. Vector addition systems were introduced by

Richard M. Karp Richard Manning Karp (born January 3, 1935) is an American computer scientist and computational theorist at the University of California, Berkeley. He is most notable for his research in the theory of algorithms, for which he received a Turing ...

and Raymond E. Miller in 1969, and generalized to vector addition systems with states (VASS) by

John E. Hopcroft John Edward Hopcroft (born October 7, 1939) is an American theoretical computer scientist. His textbooks on theory of computation (also known as the Cinderella book) and data structures are regarded as standards in their fields. He is the IBM Pro ...

and Jean-Jacques Pansiot in 1979. Both VAS and VASS are equivalent in many ways to Petri nets introduced earlier by

Carl Adam Petri Carl Adam Petri (12 July 1926 in Leipzig – 2 July 2010 in Siegburg) was a German mathematician and computer scientist. Life and work Petri created his major scientific contribution, the concept of the Petri net, in 1939 at the age of 13, for ...

Reachability in vector addition systems is Ackermann-complete (and hence nonelementary).

Informal definition

A ''vector addition system'' consists of a finite set of

integer An integer is the number zero (), a positive natural number (, , , etc.) or a negative integer with a minus sign (−1, −2, −3, etc.). The negative numbers are the additive inverses of the corresponding positive numbers. In the language ...

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

vectors. VASS have the same restriction that the counter values should never drop below zero.

Formal definitions and basic terminology

* A ''VAS'' is a finite set

V \subseteq \mathbb^d

for some

d \geq 1

. * A ''VASS'' is a finite directed graph

(Q, T)

such that

T \subseteq Q \times \mathbb^d \times Q

for some

d > 0

Transitions

* Let

V \subseteq \mathbb^d

be a VAS. Given a vector

u \in \mathbb^d

, the vector

u + v

can be ''reached'', in one transition, if

v \in V

and

u + v \in \mathbb^d

. * Let

(Q, T)

be a VASS. Given a ''configuration''

(p, u) \in Q \times \mathbb^d

, the configuration

(q, u + v)

can be ''reached'', in one transition, if

(p, v, q) \in T

and

u + v \in \mathbb^d

References

{{DEFAULTSORT:Vector addition system Formal specification languages Models of computation Concurrency (computer science) Diagrams Software modeling language

Informal definition

Formal definitions and basic terminology

Transitions

See also

References