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 and Raymond E. Miller in 1969, and generalized to vector addition systems with states (VASS) by John E. Hopcroft and Jean-Jacques Pansiot in 1979. Both VAS and VASS are equivalent in many ways to Petri nets introduced earlier by Carl Adam Petri.
Informal definition A vector addition system consists of a finite set of integer vectors 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 with arcs labelled by 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, 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 ( 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 and Pansiot. 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 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 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
… excerpt ends here. Continue reading the full article.
