Vector Addition System with States (VASS) are a ubiquitous model of infinite-state systems consisting of a set of non-negative counters which can be incremented and decremented. It is known that the reachability problem for VASS is Ackermann-complete. Because of this huge complexity, various over-approximations of VASS have been studied in the literature. One such over-approximation is continuous VASS (CVASS), in which the counters are (non-negative) rational numbers and whenever a vector is added to the current counter values, it is first scaled with an arbitrarily chosen rational factor between zero and one. It is known that the reachability problem for CVASS is NP-complete. In this paper, we initiate the study of fixed-dimensional CVASS, i.e., CVASS with a fixed number of counters. We study both the reachability and coverability problems, under both unary and binary encodings as well as over both the non-negative and the rational semantics. This gives rise to a collection of eight different problems. As our main result, we prove a complexity dichotomy for all of these eight problems when the transition vectors are over the rationals: For dimension 1, all of the eight problems are in AC¹, and so within 𝖯, whereas for any dimension at least 2, all of the eight problems are NP-complete. Furthermore, the hardness holds even when the underlying automaton is acyclic. To achieve this hardness result, we present a new technique called the Egyptian prime fractions technique. Finally, we also study these problems when the transition vectors are over the integers. Except for dimension 2, we classify the complexity of these problems over the non-negative semantics: For dimension 1, all of the problems are in AC¹, whereas for dimensions 3 and above, all of the problems are NP-complete.

We consider weighted automata over the tropical semiring ℤ_∞(min, +). Recently, it was shown that determinisation is decidable; in this paper we focus on the complexity when the alphabet is unary. In 2001, Lombardy showed this problem is decidable, a close inspection of his proof yields a coNP upper bound on the complexity. Earlier Gaubert showed that every weighted automaton in this setting can be effectively turned into an equivalent union of deterministic weighted automata. We prove Gaubert’s result efficiently, presenting it as a generalisation of Chrobak’s normal form for unary NFA. In particular, we prove that the equivalent union of deterministic weighted automata can be represented by a weighted automaton of quadratic size in the size of the original one, and this representation can be computed in polynomial time. Building on this, we show that determinisation, and even register minimisation (which generalises determinisation), is coNP-complete. We complete the paper with observations that the boundedness problem is also coNP-complete by reductions with determinisation. Lastly, we provide evidence that all of these problems are not FPT (by proving coW₁-hardness) when parametrised by the number of deterministic automata in the union.

The geometric dimension g of a Vector Addition System with States (VASS) is the dimension of the vector space generated by cycles in the VASS; this parameter refines the standard dimension d, the number of counters. Recently, it was discovered that the fastest-known algorithm for solving the reachability problem for VASS has the same complexity in terms of g as in terms of d. This suggests that the geometric dimension may in fact be a more adequate parameter for measuring the complexity of VASS reachability problems. We initiate a more systematic study of the geometric dimension. We discuss differences between two parameters: the geometric dimension and the SCC dimension. Our main technical result states that classical results about the coverability and boundedness problems can be improved from dimension d to geometric dimension g. Namely, coverability is witnessed by runs of length n^{2^𝒪(g)} instead of n^{2^𝒪(d)}, and unboundedness can be witnessed by runs of length n^{2^𝒪(g log g)} instead of n^{2^𝒪(d log d)}, where n is the size of the instance. We also study integer reachability and simultaneous unboundedness in VASS parameterised by the geometric dimension.

We consider a variant of VASS extended with integer counters, denoted VASS+ℤ. These are automata equipped with ℕ- and ℤ-counters; the ℕ-counters are required to remain nonnegative and the ℤ-counters do not have this restriction. We study the complexity of the reachability problem for VASS+ℤ when the number of ℕ-counters is fixed. We show that reachability is NP-complete in 1-VASS+ℤ (i.e. when there is only one ℕ-counter) regardless of unary or binary encoding. For d ≥ 2, using a KLMST-based algorithm, we prove that reachability in d-VASS+ℤ lies in the complexity class ℱ_{d+2}. Our upper bound improves on the naively obtained Ackermannian complexity by simulating the ℤ-counters with ℕ-counters. To complement our upper bounds, we show that extending VASS with integer counters significantly lowers the number of ℕ-counters needed to exhibit hardness. We prove that reachability in unary 2-VASS+ℤ is PSpace-hard; without ℤ-counters this lower bound is only known in dimension 5. We also prove that reachability in unary 3-VASS+ℤ is Tower-hard. Without ℤ-counters, reachability in 3-VASS has elementary complexity and Tower-hardness is only known in dimension 8.

The aim of this paper is to deliver broad understanding of a class of languages of boundedly-ambiguous VASSs, that is k-ambiguous VASSs for some natural k. These are languages of Vector Addition Systems with States with the acceptance condition defined by the set of accepting states such that each accepted word has at most k accepting runs. We develop tools for proving that a given language is not accepted by any k-ambiguous VASS. Using them we show a few negative results: lack of some closure properties of languages of k-ambiguous VASSs and undecidability of the k-ambiguity problem, namely the question whether a given VASS language is a language of some k-ambiguous VASS. In fact we show an even more general undecidability result stating that for any class containing all regular languages and only k-ambiguous VASS languages for some k ∈ ℕ it is undecidable whether a language of a given 1-dimensional VASS belongs to this class. Finally, we show that the regularity problem is decidable for k-ambiguous VASSs.

The reachability problem in 3-dimensional vector addition systems with states (3-VASS) is known to be PSpace-hard, and to belong to Tower. We significantly narrow down the complexity gap by proving the problem to be solvable in doubly-exponential space. The result follows from a new upper bound on the length of the shortest path: if there is a path between two configurations of a 3-VASS then there is also one of at most triply-exponential length. We show it by introducing a novel technique of approximating the reachability sets of 2-VASS by small semi-linear sets.

Vector Addition Systems with States (VASS), equiv-alent to Petri nets, are a well-established model of concurrency. A d-VASS can be seen as directed graph whose edges are labelled by d-dimensional integer vectors. While following a path, the values of$d$nonnegative integer counters are updated according to the integer labels. The central algorithmic challenge in VASS is the reachability problem: is there a run from a given starting node and counter values to a given target node and counter values? When the input is encoded in binary, reachability is computationally intractable: even in dimension one, it is NP-hard. In this paper, we comprehensively characterise the tractability border of the problem when the input is encoded in unary. For our main result, we prove that reachability is NP-hard in unary encoded 3-VASS, even when structure is heavily restricted to be a simple linear-path scheme. This improves upon a recent result of Czerwiński and Orlikowski [LICS 2022], in both the number of counters and expressiveness of the considered model, as well as answers open questions of Englert, Lazić, and Totzke [LICS 2016] and Leroux [PETRI NETS 2021]. The underlying graph structure of a simple linear path scheme (SLPS) is just a path with self-loops at each node. We also study the exceedingly weak model of computation that is SPLS with counter updates in { -1, 0, + 1 }. Here, we show that reachability is NP-hard when the dimension is bounded by O(a(k)), where$a$is the inverse Ackermann function and$k$bounds the size of the SLPS. We complement our result by presenting a polynomial-time algorithm that decides reachability in 2-SLPS when the initial and target configurations are specified in binary. To achieve this, we show that reachability in such instances is well-structured: all loops, except perhaps for a constant number, are taken either polynomially many times or almost maximally. This extends the main result of Englert, Lazić, and Totzke [LICS 2016] who showed the problem is in NL when the initial and target configurations are specified in unary.

International audience

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 (VASSes in dimension 4), 2) PSpace-hardness for unary 5-VASSes, 3) ExpSpace-hardness for binary 6-VASSes and 4) Tower-hardness for unary 8-VASSes.

Vector Addition Systems and equivalent Petri nets are a well established models of concurrency. The central algorithmic problem for Vector Addition Systems with a long research history is the reachability problem asking whether there exists a run from one given configuration to another. We settle its complexity to be Ackermann-complete thus closing the problem open for 45 years. In particular we prove that the problem is$\mathcal{F}_{k}$-hard for Vector Addition Systems with States in dimension 6k, where$\mathcal{F}_{k}$is the$k$-th complexity class from the hierarchy of fast-growing complexity classes.

We investigate computational complexity of the reachability problem for vector addition systems (or, equivalently, Petri nets), the central algorithmic problem in verification of concurrent systems. Concerning its complexity, after 40 years of stagnation, a non-elementary lower bound has been shown recently: the problem needs a tower of exponentials of time or space, where the height of tower is linear in the input size. We improve on this lower bound, by increasing the height of tower from linear to exponential. As a side-effect, we obtain better lower bounds for vector addition systems of fixed dimension.