Sistema de adición vectorial

Un sistema de adición vectorial ( VAS ) es uno de los diversos lenguajes de modelado matemático para la descripción de sistemas distribuidos . Los sistemas de adición vectorial fueron introducidos por Richard M. Karp y Raymond E. Miller en 1969, ^{[ 1 ]} y generalizados a sistemas de adición vectorial con estados ( VASS ) por John E. Hopcroft y Jean-Jacques Pansiot en 1979. ^{[ 2 ]} Tanto VAS como VASS son equivalentes en muchos sentidos a las redes de Petri introducidas anteriormente por Carl Adam Petri .

Un sistema de suma vectorial (SSA) consta de un conjunto finito de vectores enteros , todos con la misma longitud. Un vector inicial se considera como los valores iniciales de múltiples contadores, y los vectores del SSA se consideran actualizaciones. Estos contadores nunca pueden ser negativos. Más precisamente, dado un vector inicial con valores no negativos, los vectores del SSA se pueden sumar componente a componente, siempre que cada vector intermedio tenga valores no negativos. Un SSA con estados es un SSA equipado con estados de control. Más precisamente, es un grafo dirigido finito con arcos etiquetados por vectores enteros . Los SSA tienen la misma restricción: los valores de los contadores nunca deben ser negativos.

Los sistemas de suma vectorial pueden considerarse como una máquina de contador débil , incapaz de comprobar si un contador es cero (pero sí puede verificar si es positivo, intentando decrementarlo. Si la comprobación falla, la ejecución finaliza).

• Un VAS es un conjunto finito${\displaystyle V\subseteq \mathbb {Z} ^{d}}$para algunos${\displaystyle d\geq 1}$.
• Un VASS es un grafo dirigido finito.${\displaystyle (Q,T)}$de tal manera que${\displaystyle T\subseteq Q\times \mathbb {Z} ^{d}\times Q}$para algunos${\displaystyle d>0}$.

Un VAS es obviamente un caso especial de VASS. Por otro lado, un VASS de dimensión n puede simularse mediante un VAS de dimensión n + 3, como demostraron Hopcroft y Pansiot . ^{[ 3 ]} En este sistema, las tres coordenadas adicionales codifican el estado. Cada transición del VASS se simula mediante una secuencia de tres transiciones VAS, donde las dos primeras simplemente manipulan las coordenadas que codifican el estado.

Una red de Petri puede verse como un VASS: consideremos una red de Petri.${\displaystyle (S,T,W)}$, dónde

• ${\displaystyle S=\{1,\dots ,n\}}$es un conjunto finito de lugares
• T es un conjunto finito de transiciones
• ${\displaystyle W:(S\times T)\cup (T\times S)\to \mathbb {N} }$especifica la cantidad de tokens que consume y produce una transición.

Entonces, una marcación de la red puede verse como un vector en${\displaystyle \mathbb {N} ^{d}}$, dónde${\displaystyle d=|S|}$y una transición t como un par de transiciones VASS${\displaystyle (p,v,q),(q,v',p)}$donde q es un estado de control auxiliar,${\displaystyle v_{i}=-W(i,t)}$y ${\displaystyle v'_{j}=W(t,j)}$. De manera similar, un VAS puede formularse como una red de Petri.

• Red de Petri
• Máquina de estados finitos
• Máquina de estados finitos comunicante
• Redes de procesos de Kahn
• Cálculo de procesos
• Actor y modelo
• Teoría de la traza