A vector addition system (VAS) is one of several mathematical modeling languages for the description of

distributed systems A distributed system is a system whose components are located on different networked computers, which communicate and coordinate their actions by passing messages to one another from any system. Distributed computing is a field of computer sci ...

. 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 P ...

and Jean-Jacques Pansiot in 1979. Both VAS and VASS are equivalent in many ways to

Petri net A Petri net, also known as a place/transition (PT) net, is one of several mathematical modeling languages for the description of distributed systems. It is a class of discrete event dynamic system. A Petri net is a directed bipartite graph that ...

s 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 In mathematics, and more specifically in graph theory, a directed graph (or digraph) is a graph that is made up of a set of vertices connected by directed edges, often called arcs. Definition In formal terms, a directed graph is an ordered pa ...

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

(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