Related papers: Decidability and Complexity of Decision Problems f…
Vector addition systems with states (VASS) are widely used for the formal verification of concurrent systems. Given their tremendous computational complexity, practical approaches have relied on techniques such as reachability relaxations,…
Pushdown Vector Addition Systems with States (PVASS) consist of finitely many control states, a pushdown stack, and a set of counters that can be incremented and decremented, but not tested for zero. Whether the reachability problem is…
We study the reachability problem for affine $\mathbb{Z}$-VASS, which are integer vector addition systems with states in which transitions perform affine transformations on the counters. This problem is easily seen to be undecidable in…
Vectors addition systems with states (VASS), or equivalently Petri nets, are arguably one of the most studied formalisms for the modeling and analysis of concurrent systems. A central decision problem for VASS is reachability: whether there…
A pushdown vector addition system with states (PVASS) extends the model of vector addition systems with a pushdown stack. The algorithmic analysis of PVASS has applications such as static analysis of recursive programs manipulating integer…
Vector addition systems with states (VASS) are a popular model for concurrent systems. However, many decision problems have prohibitively high complexity. Therefore, it is sometimes useful to consider overapproximating semantics in which…
This paper studies reachability, coverability and inclusion problems for Integer Vector Addition Systems with States (ZVASS) and extensions and restrictions thereof. A ZVASS comprises a finite-state controller with a finite number of…
Reachability in pushdown vector addition systems with states (PVASS) is among the longest standing open problems in Theoretical Computer Science. We show that the problem is decidable in full generality. Our decision procedure is similar in…
Vector addition systems (VAS) constitute an important model of computation and concurrency that is equally expressive as the Petri net model. Recently, a lot of research has been conducted on vector addition systems with states (VASS),…
The reachability problem is a central decision problem for formal verification based on vector addition systems with states (VASS), which are equivalent to Petri nets and form one of the most studied and applied models of concurrency.…
Vector addition systems with states (VASS) are a classic model in concurrency theory. Grammar vector addition systems (GVAS), equivalently, pushdown VASS, extend VASS by using a context-free grammar to control addition. In this paper, our…
A pushdown vector addition system with states (PVASS) extends the model of vector addition systems with a pushdown store. A PVASS is said to be \emph{bidirected} if every transition (pushing/popping a symbol or modifying a counter) has an…
Determining the complexity of the reachability problem for vector addition systems with states (VASS) is a long-standing open problem in computer science. Long known to be decidable, the problem to this day lacks any complexity upper bound…
Vector addition system with states is an ubiquitous model of computation with extensive applications in computer science. The reachability problem for vector addition systems is central since many other problems reduce to that question. The…
Vector Addition Systems with States (VASS), equivalent to Petri nets, are a well-established model of concurrency. The central algorithmic challenge in VASS is the reachability problem: is there a run from a given starting state and counter…
We investigate the dimension-parametric complexity of the reachability problem in vector addition systems with states (VASS) and its extension with pushdown stack (pushdown VASS). Up to now, the problem is known to be $\mathcal{F}_k$-hard…
We consider the problems of language inclusion and language equivalence for Vector Addition Systems with States (VASS) with the acceptance condition defined by the set of accepting states (and more generally by some upward-closed…
More than 30 years after their inception, the decidability proofs for reachability in vector addition systems (VAS) still retain much of their mystery. These proofs rely crucially on a decomposition of runs successively refined by Mayr,…
We investigate the reachability problem in symmetric vector addition systems with states (VASS), where transitions are invariant under a group of permutations of coordinates. One extremal case, the trivial groups, yields general VASS. In…
We study the complexity of the reachability problem for Vector Addition Systems with States (VASSes) in fixed dimensions. We provide four lower bounds improving the currently known state-of-the-art: 1) \np-hardness for unary flat $4$-VASSes…