Vector addition system

Last updated December 11, 2023

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,^[1] and generalized to vector addition systems with states (VASS) by John E. Hopcroft and Jean-Jacques Pansiot in 1979.^[2] 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. 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.

Formal definitions and basic terminology

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

Transitions

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

Related Research Articles

In mathematics, a normed vector space or normed space is a vector space over the real or complex numbers on which a norm is defined. A norm is a generalization of the intuitive notion of "length" in the physical world. If $is a vector space over, where is a field equal to or to, then a norm on is a map, typically denoted by, satisfying the following four axioms:$

Non-negativity: for every $, .$
Positive definiteness: for every $, if and only if is the zero vector.$
Absolute homogeneity: for every $and,$
Triangle inequality: for every $and,$

In mathematics, topological groups are the combination of groups and topological spaces, i.e. they are groups and topological spaces at the same time, such that the continuity condition for the group operations connects these two structures together and consequently they are not independent from each other.

In mathematics, the $L p$ spaces are function spaces defined using a natural generalization of the $p$ -norm for finite-dimensional vector spaces. They are sometimes called Lebesgue spaces, named after Henri Lebesgue, although according to the Bourbaki group they were first introduced by Frigyes Riesz.

In mathematics, a topological vector space is one of the basic structures investigated in functional analysis. A topological vector space is a vector space that is also a topological space with the property that the vector space operations are also continuous functions. Such a topology is called a vector topology and every topological vector space has a uniform topological structure, allowing a notion of uniform convergence and completeness. Some authors also require that the space is a Hausdorff space. One of the most widely studied categories of TVSs are locally convex topological vector spaces. This article focuses on TVSs that are not necessarily locally convex. Banach spaces, Hilbert spaces and Sobolev spaces are other well-known examples of TVSs.

In mathematics, a subset of a topological space is called nowhere dense or rare if its closure has empty interior. In a very loose sense, it is a set whose elements are not tightly clustered anywhere. For example, the integers are nowhere dense among the reals, whereas the interval is not nowhere dense.

In mathematics, in particular abstract algebra, a graded ring is a ring such that the underlying additive group is a direct sum of abelian groups $such that . The index set is usually the set of nonnegative integers or the set of integers, but can be any monoid. The direct sum decomposition is usually referred to as gradation or grading .$

In mathematics, more specifically in the field of group theory, a solvable group or soluble group is a group that can be constructed from abelian groups using extensions. Equivalently, a solvable group is a group whose derived series terminates in the trivial subgroup.

In the mathematical discipline of set theory, forcing is a technique for proving consistency and independence results. Intuitively, forcing can be thought of as a technique to expand the set theoretical universe $to a larger universe by introducing a new "generic" object .$

In mathematics, a linear form is a linear map from a vector space to its field of scalars.

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 has two types of elements: places and transitions. Place elements are depicted as white circles and transition elements are depicted as rectangles. A place can contain any number of tokens, depicted as black circles. A transition is enabled if all places connected to it as inputs contain at least one token. Some sources state that Petri nets were invented in August 1939 by Carl Adam Petri—at the age of 13—for the purpose of describing chemical processes.

In geometry and group theory, a lattice in the real coordinate space $is an infinite set of points in this space with the properties that coordinate-wise addition or subtraction of two points in the lattice produces another lattice point, that the lattice points are all separated by some minimum distance, and that every point in the space is within some maximum distance of a lattice point. Closure under addition and subtraction means that a lattice must be a subgroup of the additive group of the points in the space, and the requirements of minimum and maximum distance can be summarized by saying that a lattice is a Delone set. More abstractly, a lattice can be described as a free abelian group of dimension which spans the vector space . For any basis of, the subgroup of all linear combinations with integer coefficients of the basis vectors forms a lattice, and every lattice can be formed from a basis in this way. A lattice may be viewed as a regular tiling of a space by a primitive cell.$

In functional analysis and related areas of mathematics, locally convex topological vector spaces (LCTVS) or locally convex spaces are examples of topological vector spaces (TVS) that generalize normed spaces. They can be defined as topological vector spaces whose topology is generated by translations of balanced, absorbent, convex sets. Alternatively they can be defined as a vector space with a family of seminorms, and a topology can be defined in terms of that family. Although in general such spaces are not necessarily normable, the existence of a convex local base for the zero vector is strong enough for the Hahn–Banach theorem to hold, yielding a sufficiently rich theory of continuous linear functionals.

In mathematics, a norm is a function from a real or complex vector space to the non-negative real numbers that behaves in certain ways like the distance from the origin: it commutes with scaling, obeys a form of the triangle inequality, and is zero only at the origin. In particular, the Euclidean distance in a Euclidean space is defined by a norm on the associated Euclidean vector space, called the Euclidean norm, the 2-norm, or, sometimes, the magnitude of the vector. This norm can be defined as the square root of the inner product of a vector with itself.

In functional analysis and related areas of mathematics an absorbing set in a vector space is a set $which can be "inflated" or "scaled up" to eventually always include any given point of the vector space. Alternative terms are radial or absorbent set . Every neighborhood of the origin in every topological vector space is an absorbing subset.$

In mathematics, an ordered vector space or partially ordered vector space is a vector space equipped with a partial order that is compatible with the vector space operations.

The behavior of a given DEVS model is a set of sequences of timed events including null events, called event segments, which make the model move from one state to another within a set of legal states. To define it this way, the concept of a set of illegal state as well a set of legal states needs to be introduced.

In mathematics, especially measure theory, a set function is a function whose domain is a family of subsets of some given set and that (usually) takes its values in the extended real number line $which consists of the real numbers and$

In computer science, specifically in the field of formal verification, well-structured transition systems (WSTSs) are a general class of infinite state systems for which many verification problems are decidable, owing to the existence of a kind of order between the states of the system which is compatible with the transitions of the system. WSTS decidability results can be applied to Petri nets, lossy channel systems, and more.

In functional analysis and related areas of mathematics, a complete topological vector space is a topological vector space (TVS) with the property that whenever points get progressively closer to each other, then there exists some point $towards which they all get closer. The notion of "points that get progressively closer" is made rigorous by Cauchy nets or Cauchy filters, which are generalizations of Cauchy sequences, while "point towards which they all get closer" means that this Cauchy net or filter converges to The notion of completeness for TVSs uses the theory of uniform spaces as a framework to generalize the notion of completeness for metric spaces. But unlike metric-completeness, TVS-completeness does not depend on any metric and is defined for all TVSs, including those that are not metrizable or Hausdorff.$

In functional analysis and related areas of mathematics, a metrizable topological vector space (TVS) is a TVS whose topology is induced by a metric. An LM-space is an inductive limit of a sequence of locally convex metrizable TVS.

References

↑ Karp, Richard M.; Miller, Raymond E. (May 1969). "Parallel program schemata". Journal of Computer and System Sciences. 3 (2): 147–195. doi: 10.1016/S0022-0000(69)80011-5 .
↑ Hopcroft, John E.; Pansiot, Jean-Jacques (1979). "On the reachability problem for 5-dimensional vector addition systems". Theoretical Computer Science. 8 (2): 135–159. doi:10.1016/0304-3975(79)90041-0. hdl: 1813/6102 .
↑ Czerwiński, Wojciech; Orlikowski, Łukasz (2021). Reachability in Vector Addition Systems is Ackermann-complete. 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS). arXiv: 2104.13866 .
↑ Leroux, Jérôme (2021). The Reachability Problem for Petri Nets is Not Primitive Recursive. 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS). arXiv: 2104.12695 .

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.

[1] Karp, Richard M.; Miller, Raymond E. (May 1969). "Parallel program schemata". Journal of Computer and System Sciences. 3 (2): 147–195. doi: 10.1016/S0022-0000(69)80011-5 .

[2] Hopcroft, John E.; Pansiot, Jean-Jacques (1979). "On the reachability problem for 5-dimensional vector addition systems". Theoretical Computer Science. 8 (2): 135–159. doi:10.1016/0304-3975(79)90041-0. hdl: 1813/6102 .

[3] Czerwiński, Wojciech; Orlikowski, Łukasz (2021). Reachability in Vector Addition Systems is Ackermann-complete. 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS). arXiv: 2104.13866 .

[4] Leroux, Jérôme (2021). The Reachability Problem for Petri Nets is Not Primitive Recursive. 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS). arXiv: 2104.12695 .

[1]

[2]

[3]

[4]