key: cord-0054926-t6sdo6bx
authors: Zuleger, Florian
title: The Polynomial Complexity of Vector Addition Systems with States
date: 2020-04-17
journal: Foundations of Software Science and Computation Structures
DOI: 10.1007/978-3-030-45231-5_32
sha: 04bcd939feb81215f7632b6f5ee7f6dc7b38b464
doc_id: 54926
cord_uid: t6sdo6bx

Vector addition systems are an important model in theoretical computer science and have been used in a variety of areas. In this paper, we consider vector addition systems with states over a parameterized initial configuration. For these systems, we are interested in the standard notion of computational time complexity, i.e., we want to understand the length of the longest trace for a fixed vector addition system with states depending on the size of the initial configuration. We show that the asymptotic complexity of a given vector addition system with states is either [Formula: see text] for some computable integer k, where N is the size of the initial configuration, or at least exponential. We further show that k can be computed in polynomial time in the size of the considered vector addition system. Finally, we show that [Formula: see text] , where n is the dimension of the considered vector addition system.

Vector addition systems (VASs) [13] , which are equivalent to Petri nets, are a popular model for the analysis of parallel processes [7] . Vector addition systems with states (VASSs) [10] are an extension of VASs with a finite control and are a popular model for the analysis of concurrent systems, because the finite control can for example be used to model shared global memory [12] . In this paper, we consider VASSs over a parameterized initial configuration. For these systems, we are interested in the standard notion of computational time complexity, i.e., we want to understand the length of the longest execution for a fixed VASS depending on the size of the initial configuration. VASSs over a parameterized initial configuration naturally arise in two areas: 1) The parameterized verification problem. For concurrent systems the number of system processes is often not known in advance, and thus the system is designed such that a template process can be instantiated an arbitrary number of times. The problem of analyzing the concurrent system for all possible system sizes is a common theme in the literature [9, 8, 1, 11, 4, 2, 3] . 2) Automated complexity analysis of programs. VASSs (and generalizations) have been used as backend in program analysis tools for automated complexity analysis [18] [19] [20] . The VASS considered by these tools are naturally parameterized over the initial configuration, modelling the dependency of the program complexity on the program input. The cited papers have proposed practical techniques but did not give complete algorithms.

Two recent papers have considered the computational time complexity of VASSs over a parameterized initial configuration. [15] presents a PTIME procedure for deciding whether a VASS is polynomial or at least exponential, but does not give a precise analysis in case of polynomial complexity. [5] establishes the precise asymptotic complexity for the special case of VASSs whose configurations are linearly bounded in the size of the initial configuration. In this paper, we generalize both results and fully characterize the asymptotic behaviour of VASSs with polynomial complexity: We show that the asymptotic complexity of a given VASS is either Θ(N k ) for some computable integer k, where N is the size of the initial configuration, or at least exponential. We further show that k can be computed in PTIME in the size of the considered VASS. Finally, we show that 1 ≤ k ≤ 2 n , where n is the dimension of the considered VASS.

We discuss our approach on the VASS V run , stated in Figure 1 , which will serve as running example. The VASS has dimension 3 (i.e., the vectors annotating the transitions have dimension 3) and four states s 1 , s 2 , s 3 , s 4 . In this paper we will always represent vectors using a set of variables Var , whose cardinality equals the dimension of the VASS. For V run we choose Var = {x, y, z} and use x, y, z as indices for the first, second and third component of 3-dimensional vectors. The configurations of a VASS are pairs of states and valuations of the variables to non-negative integers. A step of a VASS moves along a transition from the current state to a successor state, and adds the vector labelling the transition to the current valuation; a step can only be taken if the resulting valuation is non-negative. For the computational time complexity analysis of VASSs, we consider traces (sequences of steps) whose initial configurations consist of a valuation whose maximal value is bounded by N (the parameter used for bounding the size of the initial configuration). The computational time complexity is then the length of the longest trace whose initial configuration is bounded by N . For ease of exposition, we will in this paper only consider VASSs whose control-flow graph is connected. (For the general case, we remark that one needs to decompose a VASS into its strongly-connected components (SCCs), which can then be analyzed in isolation, following the DAG-order of the SCC decomposition; for this, one slightly needs to generalize the analysis in this paper to initial configurations with values Θ(N kx ) for every variable x ∈ Var , where k x ∈ Z.) For ease of exposition, we further consider traces over arbitrary initial states (instead of some fixed initial state); this is justified because for a fixed initial state one can always restrict the control-flow graph to the reachable states, and then the two options result in the same notion of computational complexity (up to a constant offset, which is not relevant for our asymptotic analysis).

In order to analyze the computational time complexity of a considered VASS, our approach computes variable bounds and transition bounds. A variable bound is the maximal value of a variable reachable by any trace whose initial configuration is bounded by N . A transition bound is the maximal number of times a transition appears in any trace whose initial configuration is bounded by N . For V run , our approach establishes the linear variable bound Θ(N ) for x and y, and the quadratic bound Θ(N 2 ) for z. We note that because the variable bound of z is quadratic and not linear, V run cannot be analyzed by the procedure of [5] . Our approach establishes the bound Θ(N ) for the transitions s 1 → s 3 and s 4 → s 2 , the bound Θ(N 2 ) for transitions s 1 → s 2 , s 2 → s 1 , s 3 → s 4 , s 4 → s 3 , and the bound Θ(N 3 ) for all self-loops. The computational complexity of V run is then the maximum of all transition bounds, i.e., Θ(N 3 ). In general, our main algorithm (Algorithm 1 presented in Section 4) either establishes that the VASS under analysis has at least exponential complexity or computes asymptotically precise variable and transition bounds Θ(N k ), with k computable in PTIME and 1 ≤ k ≤ 2 n , where n is the dimension of the considered VASS. We note that our upper bound 2 n also improves the analysis of [15] , which reports an exponential dependence on the number of transitions (and not only on the dimension).

We further state a family V n of VASSs, which illustrate that k can indeed be exponential in the dimension (the example can be skipped on first reading). V n uses variables x i,j and consists of states s i,j , for 1 ≤ i ≤ n and j = 1, 2. We note that V n has dimension 2n. V n consists of the transitions Figure 1 depicts V n for n = 3, where the vector components are stated in the order x 1,1 , x 1,2 , x 2,1 , x 2,2 , x 3,1 , x 3,2 . It is not hard to verify for all 1 ≤ i ≤ n that Θ(N 2 i−1 ) is the precise asymptotic variable bound for x i,1 and x i,2 , that s i,1 → s i,2 , s i,2 → s i,1 and s i,1 → s i+1,1 , s i+1,2 → s i,2 in case i < n, and that Θ(N 2 i ) is the precise asymptotic transition bound for s i,1 → s i,1 , s i,2 → s i,2 (Algorithm 1 can be used to find these bounds).

A celebrated result on VASs is the EXPSPACE-completeness [16, 17] of the boundedness problem. Deciding termination for a VAS with a fixed initial configuration can be reduced to the boundedness problem, and is therefore also EXPSPACE-complete; this also applies to VASSs, whose termination problem can be reduced to the VAS termination problem. In contrast, deciding the termination of VASSs for all initial configurations is in PTIME. It is not hard to see that non-termination over all initial configurations is equivalent to the existence of non-negative cycles (e.g., using Dickson's Lemma [6] ). Kosaraju and Sullivan have given a PTIME procedure for the detection of zero-cycles [14] , which can be easily be adapted to non-negative cycles. The existence of zero-cycles is decided by the repeated use of a constraint system in order to remove transitions that can definitely not be part of a zero-cycle. The algorithm of Kosaraju and Sullivan forms the basis for both cited papers [15, 5] , as well as the present paper.

A line of work [18] [19] [20] has used VASSs (and their generalizations) as backends for the automated complexity analysis of C programs. These algorithms have been designed for practical applicability, but are not complete and no theoretical analysis of their precision has been given. We point out, however, that these papers have inspired the Bound Proof Principle in Section 5.

Basic Notation. For a set X we denote by |X| the number of elements of X. Let S be either N or Z. We write S I for the set of vectors over S indexed by some set I. We write S I×J for the set of matrices over S indexed by I and J. We write 1 for the vector which has entry 1 in every component. Given a ∈ S I , we write a(i) ∈ S for the entry at line i ∈ I of a, and a = max i∈I |a(i)| for the maximum absolute value of a. Given a ∈ S I and J ⊆ I, we denote by a| J ∈ S J the restriction of a to J, i.e., we set a| J (i) = a(i) for all i ∈ J. Given A ∈ S I×J , we write A(j) for the vector in column j ∈ J of A and A(i, j) ∈ S for the entry in column i ∈ I and row j ∈ J of A. Given A ∈ S I×J and K ⊆ J, we denote by A| K ∈ S I×K the restriction of A to K, i.e., we set A| K (i, j) = A(i, j) for all (i, j) ∈ I × K. We write Id for the square matrix which has entries 1 on the diagonal and 0 otherwise. Given a, b ∈ S I we write a+b ∈ S I for component-wise addition, c · a ∈ S I for multiplying every component of a by some c ∈ S and a ≥ b for component-wise comparison. Given A ∈ S I×J , B ∈ S J×K and x ∈ S J , we write AB ∈ S I×K for the standard matrix multiplication, Ax ∈ S I for the standard matrix-vector multiplication, A T ∈ S J×I for the transposed matrix of A and x T ∈ S 1×J for the transposed vector of x. 

We define the length of π by length(π) = k and the value of π by val (π) = i∈ [1,k] d i . Let instance(π, t) be the number of times π contains the transition t, i.e., the number of indices i such that t = s i di − → s i+1 . We remark that length(π) = t∈Trns(V) instance(π, t) for every path π of V. Given a finite path π 1 and a path π 2 such that the last state of π 1 equals the first state of π 2 , we write π = π 1 π 2 for the path obtained by joining the last state of π 1 with the first state of π 2 ; we call π the concatenation of π 1 and π 2 , and π 1 π 2 a decomposition of π. We say π is a sub-path of π, if there is a decomposition π = π 1 π π 2 for some π 1 , π 2 . A cycle is a path that has the same start-and end-state. A multi-cycle is a finite set of cycles. The value val (M ) of a multi-cycle M is the sum of the values of its cycles

Let V be a VASS. The set of valuations Val (V) = N Var consists of Varvectors over the natural numbers (we assume N includes 0). The set of config-

We lift the notions of length and instances from paths to traces in the obvious way: we consider the path π = s 0 d1 − → s 1 d2 − → · · · s k that consists of the transitions used by ζ, and set length(ζ) := length(π) and instance(ζ, t) = instance(π, t), for all t ∈ Trns(V). We denote by init(ζ) = ν 0 the maximum absolute value of the starting valuation ν 0 of ζ. We say that ζ reaches a valuation ν, if ν = ν k . The complexity of V is the function comp V (N ) = sup trace ζ of V,init(ζ)≤N length(ζ), which returns for every N ≥ 0 the supremum over the lengths of the traces ζ with init(ζ) ≤ N . The variable bound of a variable x ∈ Var is the function vbound x (N ) = sup trace ζ of V,init(ζ)≤N,ζ reaches valuation ν ν(x), which returns for every N ≥ 0 the supremum over the the values of x reachable by traces ζ with init(ζ) ≤ N . The transition bound of a transition t ∈ Trns(V) is the function tbound t (N ) = sup trace ζ of V,init(ζ)≤N instance(ζ, t), which returns for every N ≥ 0 the supremum over the number of instances of t in traces ζ with init(ζ) ≤ N .

Rooted Tree. A rooted tree is a connected undirected acyclic graph in which one node has been designated as the root. We will usually denote the root by ι. We note that for every node η in a rooted tree there is a unique path of η to the root. The parent of a node η = ι is the node connected to η on the path to the root. Node η is a child of a node η , if η is the parent of η. η is a descendent of η, if η lies on the path from η to the root; η is a strict descendent, if furthermore η = η . η is an ancestor of η , if η a descendent of η; η is a strict ancestor, if furthermore η = η . The distance of a node η to the root, is the number of nodes = η on the path from η to the root. We denote by layer(l) the set of all nodes with the same distance l to the root; we remark that layer(0) = {ι}.

All proofs are presented in the extended version [21] for space reasons.

We will make use of the following matrices associated to a VASS throughout the paper: Let V be a VASS. We define the update matrix D ∈ Z Var ×Trns(V) by setting D(t) = d for all transitions t = (s, d, s ) ∈ Trns(V). We define the flow matrix F ∈ Z St(V)×Trns(V) by setting F (s, t) = −1, F (s , t) = 1 for transitions t = (s, d, s ) with s = s, and F (s, t) = F (s , t) = 0 for transitions t = (s, d, s ) with s = s; in both cases we further set F (s , t) = 0 for all states s with s = s and s = s . We note that every column t of F either contains exactly one −1 and 1 entry (in case the source and target of transition t are different) or only 0 entries (in case the source and target of transition t are the same).

Example 1. We state the update and flow matrix for V run from Section 1:

from left to right) and row order x, y, z for D resp. s 1 , s 2 , s 3 , s 4 for F (from top to bottom).

We now consider the constraint systems (P ) and (Q), stated below, which have maximization objectives. The constraint systems will be used by our main algorithm in Section 4. We observe that both constraint systems are always satisfiable (set all coefficients to zero) and that the solutions of both constraint systems are closed under addition. Hence, the number of inequalities for which the maximization objective is satisfied is unique for optimal solutions of both constraint systems. The maximization objectives can be implemented by suitable linear objective functions. Hence, both constraint systems can be solved in PTIME over the integers, because we can use linear programming over the rationales and then scale rational solutions to the integers by multiplying with the least common multiple of the denominators.

constraint system (P ):

The solutions of (P ) and (Q) are characterized by the following two lemmata:

Lemma 2 (Cited from [14] ). μ ∈ Z Trns(V) is a solution to constraint system (P ) iff there exists a multi-cycle M with val (M ) ≥ 0 and μ(t) instances of transition t for every t ∈ Trns(V).

Let rank (r, z) : Cfg(V) → N be the function defined by rank (r, z)(s, ν) = r T ν + z(s). Then, rank (r, z) is a quasi-ranking function for V, i.e., we have

We now state a dichotomy between optimal solutions to constraint systems (P ) and (Q), which is obtained by an application of Farkas' Lemma. This dichotomy is the main reason why we are able to compute the precise asymptotic complexity of VASSs with polynomial bounds. Lemma 4. Let r and z be an optimal solution to constraint system (Q) and let μ be an optimal solution to constraint system (P ). Then, for all variables x ∈ Var we either have r(x) > 0 or (Dμ)(x) ≥ 1, and for all transitions t ∈ Trns(V) we either have

Example 5. Our main algorithm, Algorithm 1 presented in Section 4, will directly use constraint systems (P ) and (Q) in its first loop iteration, and adjusted versions in later loop iterations. Here, we illustrate the first loop iteration. We consider the running example V run , whose update and flow matrices we have stated in Example 1. An optimal solution to constraint systems (P ) and (Q) is given by μ = (1441111100) T and r = (220) T , z = (0011) T . The quasi-ranking function rank (r, z) immediately establishes that tbound t (N ) ∈ O(N ) for t = s 1 → s 3 and t = s 4 → s 2 , because 1) rank (r, z) decreases for these two transitions and does not increase for other transitions (by Lemma 3), and because 2) the initial value of rank (r, z) is bounded by O(N ), i.e., we have rank (r, z)(s, ν) ∈ O(N ) for every state s ∈ St(V run ) and every valuation ν with ν ≤ N . By a similar argument we get vbound x (N ) ∈ O(N ) and vbound y (N ) ∈ O(N ). The exact reasoning for deriving upper bounds is given in Section 5. From μ we can, by Lemma 2, obtain the cycles

We will later show that the cycles C 1 and C 2 give rise to a family of traces

Here we give an intuition on the construction: We consider a cycle C of V run that visits all states at least once. By (*), the updates along the cycles C 1 and C 2 cancel each other out. However, the two cycles are not connected. Hence, we execute the cycle C 1 some Ω(N ) times, then (a part of) the cycle C, then execute C 2 as often as C 1 , and finally the remaining part of C; this we repeat Ω(N ) times. This construction also establishes the bound vbound z (N ) ∈ Ω(N 2 ) because, by (*), we increase z with every joint execution of C 1 and C 2 . The precise lower bound construction is given in Section 6.

Our main algorithm -Algorithm 1 -computes the complexity as well as variable and transition bounds of an input VASS V, either detecting that V has at least exponential complexity or reporting precise asymptotic bounds for the transitions and variables of V (up to a constant factor): Algorithm 1 will compute values vExp(x) ∈ N such that vbound N (x) ∈ Θ(N vExp(x) ) for every x ∈ Var and values tExp(t) ∈ N such that tbound N (t) ∈ Θ(N tExp(t) ) for every t ∈ Trns(V).

Data Structures. The algorithm maintains a rooted tree T . Every node η of T will always be labelled by a sub-VASSs VASS(η) of V. The nodes in the same layer of T will always be labelled by disjoint sub-VASS of V. The main loop of Algorithm 1 will extend T by one layer per loop iteration. The variable l always contains the next layer that is going to be added to T . Initialization. We assume D to be the update matrix and F to be the flow matrix associated to V as discussed in Section 3. At initialization, T consists of the root node ι and we set VASS(ι) = V, i.e., the root is labelled by the input V. We initialize l = 1 as Algorithm 1 is going to add layer 1 to T in the first loop iteration. We initialize vExp(x) = ∞ for all variables x ∈ Var and tExp(t) = ∞ for all transitions t ∈ Trns(V).

The constraint systems solved during each loop iteration. In loop iteration l, Algorithm 1 will set tExp(t) := l for some transitions t and vExp(x) := l for some variables x. In order to determine those transitions and variables, Algorithm 1 instantiates constraint systems (P ) and (Q) from Section 3 over the set of transitions U = η∈layer(l−1) Trns(VASS(η)), which contains all transitions associated to nodes in layer l − 1 of T . However, instead of a direct instantiation using D| U and F | U (i.e., the restriction of D and F to the transitions U ), we need to work with an extended set of variables and an extended update matrix. We set Var ext := {(x, η) | η ∈ layer(l − vExp(x))}, where we set n − ∞ = 0 for all n ∈ N. This means that we use a different copy of variable x for every node η in layer l − vExp(x). We note that for a variable x with vExp(x) = ∞ there is only a single copy of x in Var ext because ι ∈ layer(0) is the only node in layer 0. We define the extended update matrix D ext ∈ Z Var ext ×U by setting

Constraint systems (I ) and (II ) stated in Figure 2 can be recognized as instantiation of constraint systems (P ) and (Q) with matrices D ext and F | U and variables Var ext , and hence the dichotomy stated in Lemma 4 holds. We comment on the choice of Var ext : Setting Var ext = {(x, η) | η ∈ layer(i)} for any i ≤ l − vExp(x) would result in correct upper bounds (while i > l − vExp(x) would not). However, choosing i < l − vExp(x) does in general result in sub-optimal bounds because fewer variables make constraint system (I ) easier and constraint system (II ) harder to satisfy (in terms of their maximization objectives). In fact, i = l − vExp(x) is the optimal choice, because this choice allows us to prove corresponding lower bounds in Section 6. We will further comment on key properties of constraint systems (I ) and (II ) in Sections 5 and 6, when we outline the proofs of the upper resp. lower bound.

We note that Algorithm 1 does not use the optimal solution μ to constraint system (I ) for the computation of the vExp(x) and tExp(t), and hence the computation of the optimal solution μ could be removed from the algorithm. The solution μ is however needed for the extraction of lower bounds in Sections 6 and 8, and this is the reason why it is stated here. The extraction of lower bounds is not explicitly added to the algorithm in order to not clutter the presentation.

After an optimal solution r, z to constraint system (II ) has been found, Algorithm 1 collects all transitions t with (D T ext r + F | T U z)(t) < 0 in the set R (note that the optimization criterion in constraint system (II ) tries to find as many such t as possible). Algorithm 1 then sets tExp(t) := l for all t ∈ R. The transitions in R will not be part of layer l of T . The transitions of the next layer. The following lemma states that the new layer l of T contains all transitions of layer l − 1 except for the transitions R; the lemma is due to the fact that every transition in U \ R belongs to a cycle and hence to some SCC that is part of the new layer l.

We consider the new layer constructed during loop iteration l of Algorithm 1: we have U \ R = η∈layer(l) Trns(VASS(η)).

For each x ∈ Var with vExp(x) = ∞, Algorithm 1 checks whether r(x, ι) > 0 (we point out that the optimization criterion in constraint systems (II ) tries to find as many such x with r(x, ι) > 0 as possible). Algorithm 1 then sets vExp(x) := l for all those variables.

The check for exponential complexity. In each loop iteration, Algorithm 1 checks whether there are x ∈ Var , t ∈ Trns(V) with l < vExp(x) + tExp(t) < ∞. If this is not the case, then we can conclude that V is at least exponential (see Theorem 9 below). If the check fails, Algorithm 1 increments l and continues with the construction of the next layer in the next loop iteration.

Termination criterion. The algorithm proceeds until either exponential complexity has been detected or until vExp(x) = ∞ and tExp(t) = ∞ for all x ∈ Var and t ∈ Trns(V) (i.e., bounds have been computed for all variables and transitions).

Invariants. We now state some simple invariants maintained by Algorithm 1, which are easy to verify:

-For every node η that is a descendent of some node η we have that VASS(η) is a sub-VASS of VASS(η ). -The value of vExp and tExp is changed at most once for each input; when the value is changed, it is changed from ∞ to some value = ∞. -For every transition t ∈ Trns(V) and layer l of T , we have that either tExp(t) ≤ l or there is a node η ∈ layer(l) such that t ∈ Trns(VASS(η)). 

(from left to right) and row order (x, ηA), (y, ηA), (x, ηB), (y, ηB), (z, ι) (from top to bottom)

(from left to right) and row order (x, η 1), (y, η1), (x, η2),  (y, η2), (x, η3), (y, η3),  (x, η4), (y, η4), (z, ηA) , (z, ηB) (from top to bottom) The proof of Theorem 9 is stated in Section 8. We now assume that Algorithm 1 does not return "V has at least exponential complexity". Then, Algorithm 1 must terminate with tExp(t) = ∞ and vExp(x) = ∞ for all t ∈ Trns(V) and x ∈ Var . The following result states that tExp and vExp contain the precise exponents of the asymptotic transition and variable bounds of V:

The upper bounds of Theorem 10 will be proved in Section 5 (Theorem 16) and the lower bounds in Section 6 (Corollary 20).

We will prove in Section 7 that the exponents of the variable and transition bounds are bounded exponentially in the dimension of V: Theorem 11. We have vExp(x) ≤ 2 |Var | for all x ∈ Var and tExp(t) ≤ 2 |Var | for all t ∈ Trns(V).

Finally, we obtain the following corollary from Theorems 10 and 11:

V (N ) ∈ 2 Ω(N ) or comp V (N ) ∈ Θ(N i ) for some computable 1 ≤ i ≤ 2 |Var | .

In the remainder of this section we will establish the following result: Theorem 13. Algorithm 1 (with the below stated optimization) can be implemented in polynomial time with regard to the size of the input VASS V.

We will argue that A) every loop iteration of Algorithm 1 only takes polynomial time, and B) that polynomially many loop iterations are sufficient (this only holds for the optimization of the algorithm discussed below).

Let V be a VASS, let m = |Trns(V)| be the number of transitions of V, and let n = |Var | be the dimension of V. We note that |layer(l)| ≤ m for every layer l of T , because the VASSs of the nodes in the same layer are disjoint.

A) Clearly, removing the decreasing transitions and computing the strongly connected components can be done in polynomial time. It remains to argue about constraint systems (I ) and (II ). We observe that |Var ext | = |{(x, η) | η ∈ layer(l − vExp(x))}| ≤ n · m and |U | ≤ m. Hence the size of constraint systems (I ) and (II ) is polynomial in the size of V. Moreover, constraint systems (I ) and (II ) can be solved in PTIME as noted in Section 3. B) We do not a-priori have a bound on the number of iterations of the main loop of Algorithm 1. (Theorem 11 implies that the number of iterations is at most exponential; however, we do not use this result here). We will shortly state an improvement of Algorithm 1 that ensures that polynomially many iterations are sufficient. The underlying insight is that certain layers of the tree do not need to be constructed explicitly. This insight is stated in the lemma below: We now present the optimization that achieves polynomially many loop iterations. We replace the line l := l+1 by the two lines RelevantLayers := {tExp(t)+ vExp(x) | x ∈ Var , t ∈ Trns(V)} and l := min{l | l > l, l ∈ RelevantLayers}. The effect of these two lines is that Algorithm 1 directly skips to the next relevant layer. Lemma 14, stated above, justifies this optimization: First, no new variable or transition bound is discovered in the intermediate layers l < i < l . Second, each intermediate layer l < i < l has the same number of nodes as layer l, which are labelled by the same sub-VASSs as the nodes in l (otherwise there would be a transition with transition bound l < i < l ); hence, whenever needed, Algorithm 1 can construct a missing layer l < i < l on-the-fly from layer l.

We now analyze the number of loop iterations of the optimized algorithm. We recall that the value of each vExp(x) and tExp(t) is changed at most once from ∞ to some value = ∞. Hence, Algorithm 1 encounters at most n · m different values in the set RelevantLayers = {tExp(t) + vExp(x) | x ∈ Var , t ∈ Trns(V)} during execution. Thus, the number of loop iterations is bounded by n · m.

We begin by stating a proof principle for obtaining upper bounds. 

We call such a function w a complexity witness and the associated inc t functions the increase certificates.

Let t ∈ U be a transition on which w decreases, i.e., we have w(

Proof Outline of the Upper Bound Theorem. Let V be a VASS for which Algorithm 1 does not report exponential complexity. We will prove by induction on loop iteration l that vbound N (x) ∈ O(N l ) for every x ∈ Var with vExp(x) = l and that tbound N (t) ∈ O(N l ) for every t ∈ Trns(V) with tExp(t) = l. We now consider some loop iteration l ≥ 1. Let U = η∈layer(l−1) Trns(VASS(η)) be the transitions, Var ext be the set of extended variables and D ext ∈ Z Var ext ×U be the update matrix considered by Algorithm 1 during loop iteration l. Let r, z be some optimal solution to constraint system (II ) computed by Algorithm 1 during loop iteration l. The main idea for the upper bound proof is to use the quasi-ranking function from Lemma 3 as witness function for the Bound Proof Principle. In order to apply Lemma 3 we need to consider the VASS associated to the matrices in constraint system (II ): Let V ext be the VASS over variables Var ext associated to update matrix D ext and flow matrix F | U . From Lemma 3 we get that rank (r, z) : Cfg(V ext ) → N is a quasi-ranking function for V ext . We now need to relate V to the extended VASS V ext in order to be able to use this quasi-ranking function. We do so by extending valuations over Var to valuations over Var ext . For every state s ∈ St(V) and valuation ν : Var → N, we define the extended valuation ext s (ν) : Var ext → N by setting

As a direct consequence from the definition of extended valuations, we have that (s, ext s (ν)) ∈ Cfg(V ext ) for all (s, ν) ∈ Cfg(V), and that (s 1 , ext s1 (ν 1 ))

We now define the witness function w by setting w(s, ν) = rank (r, z)(s, ext s (ν)) for all (s, ν) ∈ Cfg(V).

We immediately get from Lemma 3 that w maps configurations to the nonnegative integers and that condition 1) of the Bound Proof Principle is satisfied. Indeed, we get from the first item of Lemma 3 that w(s, ν) ≥ 0 for all (s, ν) ∈ Cfg(V), and from the second item that w(s 1 , ν 1 ) ≥ w(s 2 , ν 2 ) for every step

, the witness function w decreases for transitions t with tExp(t) = l. It remains to establish condition 2) of the Bound Proof Principle. We will argue that we can find increase certificates inc t (N ) ∈ O(N l−tExp(t) ) for all t ∈ Trns(V) \ U . We note that tExp(t) < l for all t ∈ Trns(V) \ U , and hence the induction assumption can be applied for such t. We can then derive the desired bounds from the Bound Proof Principle because of t∈Trns

The following lemma will allow us to consider traces ζ N with init(ζ N ) ∈ O(N ) instead of init(ζ N ) ≤ N when proving asymptotic lower bounds.

The lower bound proof uses the notion of a pre-path, which relaxes the notion of a path: A pre-path σ = t 1 · · · t k is a finite sequence of transitions t i = s i di − → s i . Note that we do not require for subsequent transitions that the end state of one transition is the start state of the next transition, i.e., we do not require s i = s i+1 . We generalize notions from paths to pre-paths in the obvious way, e.g., we set val (σ) = i∈ [1,k] d i and denote by instance(σ, t), for t ∈ Trns(V), the number of times σ contains the transition t. We say the pre-path σ can be executed from valuation ν, if there are valuations ν i ≥ 0 with ν i+1 = ν i + d i+1 for all 0 ≤ i < k and ν = ν 0 ; we further say that σ reaches valuation ν , if ν = ν k . We will need the following relationship between execution and traces: in case a pre-path σ is actually a path, σ can be executed from valuation ν, if and only if there is a trace with initial valuation ν that uses the same sequence of transitions as σ. Two pre-paths σ = t 1 · · · t k and σ = t 1 · · · t l can be shuffled into a pre-path σ = t 1 · · · t k+l , if σ is an order-preserving interleaving of σ and σ ; formally, there are injective monotone functions f : [1, k] → [1, k + l] and g : [1, l] [1, k] and t g(i) = t i for all i ∈ [1, l] . Further, for d ≥ 1 and pre-path σ, we denote by σ d = σσ · · · σ d the pre-path that consists of d subsequent copies of σ.

For the remainder of this section, we fix a VASS V for which Algorithm 1 does not report exponential complexity and we fix the computed tree T and bounds vExp, tExp. We further need to use the solutions to constraint system (I ) computed during the run of Algorithm 1: For every layer l ≥ 1 and node η ∈ layer(l), we fix a cycle C(η) that contains μ(t) instances of every t ∈ Trns(VASS(η)), where μ is an optimal solution to constraint system (I ) during loop iteration l. The existence of such cycles is stated in Lemma 18 below. We note that this definition ensures val (C(η)) = t∈Trns(VASS(η)) D(t) · μ(t). Further, for the root node ι, we fix an arbitrary cycle C(ι) that uses all transitions of V at least once.

Let μ be an optimal solution to constraint system (I ) during loop iteration l of Algorithm 1. Then there is a cycle C(η) for every η ∈ layer(l) that contains exactly μ(t) instances of every transition t ∈ Trns(VASS(η)).

Step I) We define a pre-path τ l , for every l ≥ 1, with the following properties: 1) instance(τ l , t) ≥ N l+1 for all transitions t ∈ η∈layer(l) Trns(VASS(η)).

2) val (τ l ) = N l+1 η∈layer(l) val (C(η)). 3) val (τ l )(x) ≥ 0 for every x ∈ Var with vExp(x) ≤ l. 4) val (τ l )(x) ≥ N l+1 for every x ∈ Var with vExp(x) ≥ l + 1. 5) τ l is executable from some valuation ν with a) ν(x) ∈ O(N vExp(x) ) for x ∈ Var with vExp(x) ≤ l, and b) ν(x) ∈ O(N l ) for x ∈ Var with vExp(x) ≥ l + 1.

The difficulty in the construction of the pre-paths τ l lies in ensuring Property 5). The construction of the τ l proceeds along the tree T using that the cycles C(η) have been obtained according to solutions of constraint system (I ).

Step II) It is now a direct consequence of Properties 3)-5) stated above that we can choose a sufficiently large k > 0 such that for every l ≥ 0 the pre-path ρ l = τ k 0 τ k 1 · · · τ k l (the concatenation of k copies of each τ i , setting τ 0 = C(ι) N ), can be executed from some valuation ν and reaches a valuation ν with

for all x ∈ Var with vExp(x) ≤ l, and 3) ν (x) ≥ kN l+1 for all x ∈ Var with vExp(x) ≥ l + 1.

The above stated properties for the pre-path ρ lmax , where l max is the maximal layer of T , would be sufficient to conclude the lower bound proof except that we need to extend the proof from pre-paths to proper paths.

Step III) In order to extend the proof from pre-paths to paths we make use of the concept of shuffling. For all l ≥ 0, we will define paths γ l that can be obtained by shuffling the pre-paths ρ 0 , ρ 1 , . . . , ρ l . The path γ lmax , where l max is the maximal layer of T , then has the desired properties and allows to conclude the lower bound proof with the following result:

for all variables x ∈ Var and we have instance(ζ N , t) ≥ N tExp(t) for all transitions t ∈ Trns(V).

With Lemma 17 we get the desired lower bounds from Theorem 19:

for all x ∈ Var and tbound N (t) ∈ Ω(N tExp(t) ) for all t ∈ Trns(V).

For the remainder of this section, we fix a VASS V for which Algorithm 1 does not report exponential complexity and we fix the computed tree T and bounds vExp, tExp. Additionally, we fix a vector z l ∈ Z St(V) for every layer l of T and a vector r η ∈ Z Var for every node η ∈ layer(l) as follows: Let r, z be an optimal solution to constraint system (II ) in iteration l + 1 of Algorithm 1. We then set z l = z. For every η ∈ layer(l) we define r η by setting r η (x) = r(x, η ), where η ∈ layer(l − vExp(x)) is the unique ancestor of η in layer l − vExp(x). The following properties are immediate from the definition:

For every layer l of T and node η ∈ layer(l) we have: 1) z l ≥ 0 and r η ≥ 0.

2) r T η d + z l (s 2 ) − z l (s 1 ) ≤ 0 for every transition s 1 d − → s 2 ∈ Trns(VASS(η)); moreover, the inequality is strict for all transitions t with tExp(t) = l + 1.

3) Let η ∈ layer(i) be a strict ancestor of η. Then, r T η d + z i (s 2 ) − z i (s 1 ) = 0 for every transition s 1 d − → s 2 ∈ Trns(VASS(η)). 4) For every x ∈ Var with vExp(x) = l+1 we have r η (x) > 0 and r η (x) = r η (x) for all η ∈ layer(l). 5) For every x ∈ Var with vExp(x) > l + 1 we have r η (x) = 0. 6) For every x ∈ Var with vExp(x) ≤ l there is an ancestor η ∈ layer(i) of η such that r η (x) > 0 and r η (x ) = 0 for all x with vExp(x ) > vExp(x).

For a vector r ∈ Z Var , we define the potential of r by setting pot(r) = max{vExp(x) | x ∈ Var , r(x) = 0}, where we set max ∅ = 0. The motivation for this definition is that we have r T ν ∈ O(N pot(r) ) for every valuation ν reachable by a trace ζ with init(ζ) ≤ N . We will now define the potential of a set of vectors Z ⊆ Z Var . Let M be a matrix whose columns are the vectors of Z and whose rows are ordered according to the variable bounds, i.e., if the row associated to variable x is above the row associated to variable x, then we have vExp(x ) ≥ vExp(x). Let L be some lower triangular matrix obtained from M by elementary column operations. We now define pot(Z) = column r of L pot(r), where we set ∅ = 0. We note that pot(Z) is well-defined, because the value pot(Z) does not depend on the choice of M and L.

We next state an upper bound on potentials. Let l ≥ 0 and let B l = {vExp(x) | x ∈ Var , vExp(x) < l} be the set of variable bounds below l. We set varsum(l) = 1, for B l = ∅, and varsum(l) = B l , otherwise. The following statement is a direct consequence of the definitions:

Proposition 22. Let Z ⊆ Z Var be a set of vectors such that r(x) = 0 for all r ∈ Z and x ∈ Var with vExp(x) > l. Then, we have pot(Z) ≤ varsum(l + 1).

We define pot(η) = pot({r η | η is a strict ancestor of η}) as the potential of a node η. We note that pot(η) ≤ varsum(l + 1) for every node η ∈ layer(l) by Proposition 22. Now, we are able to state the main results of this section: Theorem 11 is then a direct consequence of Lemma 24 and 25 (using k ≤ |Var |).

The following lemma from [15] states a condition that is sufficient for a VASS to have exponential complexity 2 . We will use this lemma to prove Theorem 9:

Lemma 26 (Lemma 10 of [15] ). Let V be a connected VASS, let U, W be a partitioning of Var and let C 1 , . . . , C m be cycles such that a) val (C i )(x) ≥ 0 for all x ∈ U and 1 ≤ i ≤ m, and b) i val (C i )(x) ≥ 1 for all x ∈ W . Then, there is a c > 1 and paths π N such that 1) π N can be executed from initial valuation N · 1, 2) π N reaches a valuation ν with ν(x) ≥ c N for all x ∈ W and 3) (C i ) c N is a sub-path of π N for each 1 ≤ i ≤ m.

We now outline the proof of Theorem 9: We assume that Algorithm 1 returned "V has at least exponential complexity" in loop iteration l. According to Lemma 18, there are cycles C(η), for every node η ∈ layer(l), that contain μ(t) instances of every transition t ∈ Trns(VASS(η)). One can then show that the cycles C(η) and the sets U = {x ∈ Var | vExp(x) ≤ l}, W = {x ∈ Var | vExp(x) > l} satisfy the requirements of Lemma 26, which establishes Theorem 9.

A language-based comparison of extensions of Petri nets with and without whole-place operations

On the expressive power of communication primitives in parameterised systems

Liveness of parameterized timed networks

Decidability in parameterized verification

Efficient algorithms for asymptotic bounds on termination time in VASS

Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors

Decidability issues for Petri nets -a survey

On the omega-language expressive power of extended Petri nets

Reasoning about systems with many processes

On the reachability problem for 5-dimensional vector addition systems

Parameterized model checking of fault-tolerant distributed algorithms by abstraction

A widening approach to multithreaded program verification

Parallel program schemata

Detecting cycles in dynamic graphs in polynomial time (preliminary version)

Polynomial vector addition systems with states

The Reachability Problem Requires Exponential space

The covering and boundedness problems for vector addition systems

A simple and scalable static analysis for bound analysis and amortized complexity analysis

Difference constraints: An adequate abstraction for complexity analysis of imperative programs

Complexity and resource bound analysis of imperative programs using difference constraints

The polynomial complexity of vector addition systems with states