Keywords

1 Introduction

Vector Addition Systems with States (VASS) are a well-studied class of infinite-state systems (see the survey [37]). These are finite automata with counters that can be updated, but are never allowed to take negative values. Thus, a configuration consists of a state and a vector over the natural numbers. The central decision problems are the reachability and coverability problems. The reachability problem asks whether from a given start configuration one can reach the target configuration. The coverability problem is the same except that the target configuration need not be reached exactly, counter values are allowed to be greater. Both problems are not only mathematically elegant, but they have interesting theoretical applications [7] and implementations [6]. Coverability is provably a simpler problem that is better suited for applications; reachability tools are mostly applied to coverability benchmarks [14]. Yet coverability has applications in the verification of safety conditions in reactive systems [17, 21]. Such systems may require additional data structures to be accurately represented, like counters for example. Safety conditions often boil down to whether a particular state can be reached as opposed to a particular configuration [8].

Coverability and reachability have been studied for decades. The equivalent model of Petri nets was introduced already in the sixties [34]. For general VASS, Lipton proved in 1976 an EXPSPACE lower bound that applies to both coverability and reachability [31]. Two years later, Rackoff proved a matching EXPSPACE upper bound for coverability [35]. Later in 1981, Mayr proved that reachability is decidable [32] without providing an upper bound for the algorithm. The construction was simplified by Kosaraju [24] and Lambert [25], and a recent series of papers by Leroux and Schmitz ended in 2019 by proving an Ackermann upper bound [27]. A matching Ackermann lower bound was published in 2021 by two independent groups [12, 26].

Plenty of attention has been given to VASS with fixed dimension, that is when the number of counters k is invariable, denoted k-VASS. For fixed dimension VASS it matters much whether the counter updates are encoded in unary or binary. Already, Rackoff gives NL and PSPACE upper bounds for coverability in unary encoded and binary encoded k-VASS, respectively [35]. The coverability problem where there are no counters is just directed graph reachability that is NL-complete [3]. Thus, coverability in unary encoded k-VASS is NL-complete, for every fixed k. Coverability in binary encoded 1-VASS is in NC\({}^2\) [2], it can therefore be decided in deterministic polynomial time. If there are two or more binary counters, coverability is PSPACE-hard [5] via a reduction from reachability in bounded one-counter automata that is PSPACE-complete [18]. Therefore, coverability in binary encoded k-VASS is PSPACE-complete for every \(k \ge 2\). See Figure 1 for the complexities of coverability in VASS with a fixed number of unary and binary encoded counters. This is all in striking contrast to the reachability problem in fixed dimension VASS, since reachability in 8-VASS is already known to be nonelementary [13].

Fig. 1.
figure 1

The complexities of coverability in VASS with a fixed number of unary and binary encoded counters. All NL lower bounds arise from the zero counters case, here coverability is directed graph reachability and that is well known to be NL-complete [3]. In the case of one binary counter, regardless of the number of unary counters, we are aware only of this trivial NL lower bound. Furthermore, with one binary counter and at least two unary counters, we are not aware of a non-trivial upper bound (denoted “Open” in the table). When there are at least two binary counters and any number of unary counters, coverability is PSPACE-complete. The lower bound holds for 2-VASS with two binary counters [5] and the upper bound is given by Rackoff for any fixed dimension [35]. Recall that coverability in general VASS, where the number of counters is not fixed, is EXPSPACE-complete [35].

Full size image

There is a prominent line of work on 2-VASS with various encodings. The seminal paper in 1979 of Hopcroft and Pansiot [23] shows reachability in 2-VASS is decidable, proving that the reachability set is effectively semi-linear. Moreover, in the same paper the authors show, by an example, that the 3-VASS reachability set need not be semi-linear. Later, this was improved as it was shown that for 2-VASS the reachability relation is effectively semi-linear [28]. This proof shows that every 2-VASS can be characterised by a flat model, i.e. where the underlying finite automaton does not contain nested cycles. A more careful analysis of that paper, resulted in a PSPACE upper bound result for reachability in binary encoded 2-VASS [5]. Since coverability in binary encoded 2-VASS is PSPACE-hard [5], the authors were able to conclude that both coverability and reachability are PSPACE-complete. Just as coverability demonstrated the difference encoding makes to complexity, so does reachability; later it was proved that reachability in unary encoded 2-VASS is NL-complete [16].

Our Results and Techniques. We consider the coverability problem for 2-VASS with one unary counter. Here, updates of one counter are encoded in binary and the updates of the other are encoded in unary, see Figure 2 for an example. Notice that the unary counter need not be limited to polynomially bounded values. Otherwise, the value of the unary counter could be encoded into the states for an instance of coverability in binary encoded 1-VASS. Furthermore, we do not impose any restrictions on the initial and the target configurations, i.e. both coordinates of these vectors are encoded in binary. Our main result is that coverability in 2-VASS with one unary counter is in NP.

Coverability in binary encoded k-VASS is PSPACE-complete, for \(k \ge 2\). The lower bound limits the practicality of applications. Therefore, it is sensible to consider restricted variations and quantify their complexity. We remark that coverability in fixed dimension VASS had widely-open complexity if there was exactly one binary counter and at least one unary counter. See Figure 1 for a summary of the known results.

Fig. 2.
figure 2

Example 2-VASS with one unary counter V. Consider the instance of coverability consisting of V, the initial configuration q(0, 1), and the target configuration q(0, 10). Consider the path \(\pi = \lambda \rho \; \lambda \rho \cdots \lambda \rho \; \rho \cdots \rho \) which induces a run in V from the initial configuration q(0, 1). There are 990 repetitions of the pair of cycles \(\lambda \rho \) to witness the configuration q(990, 1). The cycles alternate so both counters remain non-negative throughout the run. This is followed by 10 iterations of the cycle \(\rho \) so the configuration q(0, 11) is witnessed, achieving coverability of the target configuration q(0, 10).

Full size image

The natural starting point is the characterisation of runs via linear path schemes [4]. Intuitively, the authors prove that if coverability or reachability holds then there is a witnessing path of a specific shape. Namely, all paths can be characterised by a bounded language defined by a regular expression of the form \(\tau _0 \gamma _1^* \tau _1 \ldots \tau _{k-1} \gamma _k^* \tau _k\). Here \(\tau _0, \dots , \tau _k\) are paths that connect disjoint cycles \(\gamma _1, \dots , \gamma _k\). Since the language is bounded, checking if there is a path for a given expression essentially amounts to an instance of integer linear programming. In particular, the authors argue that both k and \(|\tau _0 | + |\gamma _1 | + |\tau _1 | + \ldots + |\tau _{k-1} | + |\gamma _k | + |\tau _k |\) are pseudo-polynomially bounded [4]. However, a polynomial bound would immediately yield an NP upper bound as such a regular expression can be guessed. Given that coverability in 2-VASS with two binary counters is PSPACE-hard [5], we cannot simply directly apply the known results when dealing with 2-VASS with one binary and one unary counter. In Section 3, we provide a detailed discussion and a difficult yet motivating example in Figure 3.

To overcome this problem, we show that coverability can be witnessed by paths in compressed linear form. We relax the condition of the bounded language, by allowing to nest linear forms, provided that the exponents are fixed. Intuitively, an expression of the form \((\tau \gamma ^* \tau ')^*\) is still forbidden, but we allow for \((\tau \gamma ^e \tau ')^*\), where e is fixed but can be exponentially large (encoded using polynomially many bits). Such a form easily provides an NP upper bound.

We rely on two crucial observations to prove that we can focus on paths in compressed linear form. First, notice that the \(*\) operation in a linear path scheme corresponds to iterating some cycle in the VASS. Since \(\gamma _1, \ldots , \gamma _k\) need to be short, one naturally focuses on short cycles. The issue is that there are exponentially many cycles of polynomial size. In Section 4 we prove that for coverability there are only polynomially many ‘optimal’ cycles. In Section 5 we deal with the problem when some cycle \(\gamma \) occurs many times in a linear path scheme witnessing coverability, resulting in a polynomial bound on k, the width of the linear path scheme. Then we prove that, either we can merge some \(\gamma _i\) and \(\gamma _j\) thus reducing the width, or that there is a cycle that has positive effect on one counter and non-negative effect on the other counter. Intuitively, in the latter case, we can reduce the problem to coverability in 1-VASS by pumping such a cycle that forces one counter to take an arbitrarily large value. Moreover, such a cycle is witnessed by a linear path scheme. Since we need to pump this cycle, we require compressed linear forms to describe the repetitions of the cycle.

We highlight that both our crucial observations rely on that we work with coverability, not reachability. We further highlight that we address these crucial observations through our technical contributions that often depend on the fact there is one unary counter.

Further Related Work. Asymmetric treatment of the counters has been already considered for VASS. Recall that Minsky machines can be seen as VASS with the additional ability of zero-testing. For this model coverability is undecidable [33], even with two counters. This raised natural questions of what happens where only one of the counters is able to be reset or tested for zero. This, and more generally, reachability in VASS with hierarchical zero-tests are known to be decidable [36]. There is a further investigation into VASS with one zero-test [20]. Recently, work has appeared containing detailed analysis about 2-VASS where counters have different powers [19, 29]. Finally, one of the most famous open problems in the community is whether reachability is decidable for 1-VASS with a pushdown stack. For these systems, coverability is known to be decidable [30]. The best known lower bound is that coverability, thus reachability also, is PSPACE-hard [15]. Our model, 2-VASS with one unary counter, can be seen as 1-VASS with a singleton alphabet pushdown stack.

The complexity of reachability in binary encoded 3-VASS remains an intriguing open problem. It is PSPACE-hard, like in dimension two, and the only known upper bound is primitive recursive, but not even elementary [27]. Recent works on reachability in fixed dimension VASS [9, 11, 13] provide new examples and a better understanding of the VASS model. Interestingly, many techniques applied to fixed dimension VASS are very closely related to recent progress on the nonelementary and Ackermann lower bounds for general VASS [10, 12, 26]. We finally and additionally motivate coverability in VASS with one binary counter and (at least) one unary counter as an avenue for finding new techniques to approach VASS problems with.

2 Preliminaries

Given an integer \(z \in \mathbb {Z}\) we denote \(\textrm{bitsize}(z) = \log _2(|z | + 1) + 1\). For a vector \(\textbf{v} \,{:}{=}\, (v_1,v_2)\) we use \((\textbf{v})_1 \,{:}{=}\, v_1\) and \((\textbf{v})_2 \,{:}{=}\, v_2\) to be the projections to the first and second coordinates, respectively. We use \(|\textbf{v}|_{\max } \,{:}{=}\, \max \{|v_1|,|v_2|\} + 1\) to denote the size of vector \(\textbf{v}\). We write \(\textbf{v} \le \textbf{w}\) if the inequalities hold on each coordinate. We write \(\textbf{v} < \textbf{w}\) if at least one of the inequalities is strict.

A 2-VASS with one unary counter \(V = (Q, T)\) consists of a finite set of control states Q and a set of transitions \(T \subseteq Q \times \mathbb {Z}\times \{-1, 0, 1\} \times Q\). We shall refer to the first counter as the binary counter and the second counter as the unary counter. The size of V is \(|V | = |Q | + \sum _{(p,b,u,q) \in T} \textrm{bitsize}(b)\). With \(|V |_{\max } \,{:}{=}\, |Q | + |T |\cdot |T |_{\max }\) we denote the total ‘pseudo-polynomial size’ of the automaton, where \(|T |_{\max }\) denotes the maximum absolute value that occurs in the transitions. Note that in a standard 2-VASS both counters are in binary, i.e. the domain of updates for the second counter is also \(\mathbb {Z}\).

A path \(\pi \) in V is a, possibly empty, sequence of transitions \(\pi = (t_i)_{i=1}^m\) such that \(t_i = (q_{i-1}, b_i, u_i, q_i) \in T\). A path is simple if \(q_0, \ldots , q_m\) are distinct. A path is a cycle if \(q_0 = q_m\) and \(m > 0\) (thus empty cycles are forbidden). We call it a \(q_0\)-cycle to emphasise the first and last state of the cycle. A cycle is simple if \(q_1, \ldots , q_m\) are distinct. A cycle is short if \(m \le |Q |\). The length of a path is the number of transitions in the path, denoted \(\textrm{len}(\pi ) = m\). We write \(\pi [i..j]\) to denote the path that is the subsequence of transitions \((t_i, \ldots , t_j)\) in \(\pi \).

A configuration \((p, \textbf{u}) \in Q \times \mathbb {N}^2\), denoted \(p(\textbf{u})\), is a state paired with the current binary and unary counter values. A run is a sequence of configurations \((q_i(\textbf{v}_i))_{i=0}^m\) such that \((q_{i-1}, (\textbf{v}_i)_1 - (\textbf{v}_{i-1})_1, (\textbf{v}_i)_2 - (\textbf{v}_{i-1})_2, q_i) \in T\). A run can equivalently be defined by the sequence of configurations induced by following a path \(\pi \) starting from an initial configuration \(q_0(\textbf{v}_0)\). We denote this run \(q_0(\textbf{v}_0)\xrightarrow {\pi }q_m(\textbf{v}_m)\). We also write \(q_0(\textbf{v}_0)\xrightarrow {*}q_m(\textbf{v}_m)\) to indicate the existence of a run between two configurations.

In this paper we study the coverability problem for VASS.

figure a

Do note that the initial configuration \(p(\textbf{u})\) and the target configuration \(q(\textbf{v})\) have both the binary and unary components encoded as binary integers. The reachability problem for VASS—which we will not study in this paper—requires \(\textbf{v}' = \textbf{v}\).

Consider a path \(\pi = (t_i)_{i=1}^m\), where \(t_i = (q_{i-1}, b_i, u_i, q_i)\). The effect of \(\pi \) is the sum of the counter updates, i.e. the vector \(\textrm{eff}(\pi ) \,{:}{=}\, \sum _{i=1}^m (b_i,u_i)\). We often focus on the two projections: the binary effect \(\textrm{eff}_b(\pi ) \,{:}{=}\, \sum _{i=1}^m b_i\), and the unary effect \(\textrm{eff}_u(\pi ) \,{:}{=}\, \sum _{i=1}^m u_i\).

We say that a cycle \(\gamma \) is monotone if \(\textrm{eff}(\gamma ) \ge \textbf{0}\) or \(\textrm{eff}(\gamma ) \le \textbf{0}\). Otherwise, we say that \(\gamma \) is non-monotone. Note the two variants of a non-monotone cycle: a positive-negative cycle \(\textrm{eff}_b(\gamma ) > 0\) and \(\textrm{eff}_u(\gamma ) < 0\), and a negative-positive cycle \(\textrm{eff}_b(\gamma ) < 0\) and \(\textrm{eff}_u(\gamma ) > 0\).

Let \(\gamma \) be a cycle. Given \(e \in \mathbb {N}\) we write \(\gamma ^e\) for the path obtained by e repetitions of \(\gamma \). We refer to e as the exponent. A linear path scheme is a regular expression of the form \(\tau _0 \gamma _1^* \tau _1 \cdots \tau _{k-1} \gamma _k^* \tau _k\), where the paths \(\tau _0, \tau _1, \ldots , \tau _k\) connect disjoint cycles \(\gamma _1, \ldots , \gamma _k\). Note that a collection of cycles is disjoint if no two cycles have a common state. Given \(\ell = (\tau _0, \gamma _1, \tau _1, \dots , \tau _{k-1}, \gamma _k, \tau _k)\), we say the a path \(\pi \) is in linear form \(\ell \) if \(\pi = \pi _\ell = \tau _0 \gamma _1^{e_1} \tau _1 \cdots \tau _{k-1} \gamma _k^{e_k} \tau _k\) for some exponents \(e_1, \ldots , e_k\). Note that in this definition every path has a linear form, e.g. \(\tau _0 = \pi \) is valid. To leverage the definition, we will ask whether paths are in a linear form of certain size. The size of a linear form \(\ell \) is \(\sum _{i=0}^{k} \textrm{len}(\tau _i) + \sum _{i = 1}^k \textrm{len}(\gamma _i)\). The size of \(\pi _\ell \) is \( \sum _{i=0}^{k} \textrm{len}(\tau _i) + \sum _{i = 1}^k \textrm{len}(\gamma _i) + \sum _{i = 1}^k \textrm{bitsize}(e_i)\), i.e. includes the exponents. We refer to k as the width of the linear form.

3 Coverability in 2-VASS with One Unary Counter

In this section we briefly discuss why the state-of-the-art techniques are not enough to prove that coverability in 2-VASS with one unary counter is in NP. Blondin et al. [4] show that for a given 2-VASS V there exists a set of linear path schemes S such that if \(p(\textbf{u})\xrightarrow {*}q(\textbf{v})\) in V, then there exists a path \(\pi \) in a linear path scheme \(\rho \in S\) such that \(p(\textbf{u})\xrightarrow {\pi }q(\textbf{v})\). For every linear path scheme \(\rho \in S\) the width of \(\rho \), and therefore the width of every path, is bounded above by \(\textsf {poly}(|Q|,|T|_{\max })\) [4, Theorem 3.1]. Such a path \(\pi \) is not necessarily a polynomial size witness, as the width depends on \(|T |_{\max }\) polynomially. We provide an example of a 2-VASS with one unary counter where the width of every linear form \(\ell \) for a path is exponential in the input size. This demonstrates that the combinatorial structure of linear path schemes is not self-sufficient to show that there always exists a polynomial size witness of coverability.

Fig. 3.
figure 3

Example 2-VASS with one unary counter V, where \(N = 2^{n}\), where n is an input parameter (thus making N exponentially large). Consider the coverability instance with the initial configuration q(0, 1), and the target configuration q(N, 1). Let \(\lambda = t_{qa}\alpha ^{N^2}t_{ab}\beta ^{N^2}t_{bq}\) and \(\rho = t_{qp}t_{pc}\gamma ^{N^2}t_{cd}\delta ^{N^2}t_{dq}\), where \(t_{xy}\) is the transition from state x to state y. Observe that \(\textrm{eff}(\lambda ) = (N, -1)\) and \(\textrm{eff}(\rho ) = (-N+1, 1)\), thus \(\textrm{eff}(\lambda \rho ) = (1,0)\). It is easy to then see that \(q(0,1)\xrightarrow {(\lambda \rho )^N}q(N,1)\). Intuitively the cycles \(\lambda \) and \(\rho \) alternate so both counters remain non-negative throughout the run. In the appendix, we prove that there does not exist a linear form of polynomial size for a path that induces a coverability run.

Full size image

Paths in Compressed Linear Form. Nevertheless, there is a natural way to succinctly describe the path presented in Figure 3. Let \(\sigma = \lambda \rho \), and note that

$$\begin{aligned} \sigma ^N = \left( t_{qa} \; \alpha ^{N^2} \; t_{ab} \; \beta ^{N^2} \; t_{bq}t_{qp}t_{pc} \; \gamma ^{N^2} \; t_{cd} \; \delta ^{N^2} \; t_{dq}\right) ^{N}. \end{aligned}$$

All paths and cycles are ‘small’, and the bitsize of N and \(N^2\) are polynomial in n, so \(\sigma \) itself is a path in linear form. We introduce the following generalisation of linear form paths that encapsulates the idea behind paths of this kind of arrangement.

Definition 1 (Compressed linear form path)

A path \(\pi \) is in compressed linear form if \(\pi = \rho _0 \sigma _1^{f_1} \rho _1 \cdots \rho _{k-1} \sigma _k^{f_k} \rho _k\) for some connected paths in linear form \(\rho _0, \rho _1, \ldots , \rho _k\); cycles in linear form \(\sigma _1, \ldots , \sigma _k\); and exponents \(f_1, \ldots , f_k\). The size of a compressed linear form path is the sum of the sizes of all \(\rho _i\) and \(\sigma _i\) (including the bitsize of their exponents) plus the bitsize of the exponents \(f_i\) (Fig. 4).

Fig. 4.
figure 4

A compressed linear form path.

Full size image

The following theorem is our main contribution.

Theorem 1

Let V be a 2-VASS with one unary counter and fix two configurations \(p(\textbf{u})\) and \(q(\textbf{v})\). If \(p(\textbf{u})\xrightarrow {*}q(\textbf{v})\), then there exists a path in compressed linear form \(\pi \) such that \(p(\textbf{u})\xrightarrow {\pi }q(\textbf{v}')\) and \(\textbf{v}' \ge \textbf{v}\). The size of the compressed linear form path is polynomial in \(|V | + \textrm{bitsize}(\textbf{u}) + \textrm{bitsize}(\textbf{v})\).

Corollary 1

Coverability in 2-VASS with one unary counter is in NP.

Proof

By Theorem 1 it suffices to consider paths in compressed linear form of polynomial size, that can be guessed in NP. It suffices to observe that a coverability instance on a given compressed linear form amounts to an instance of integer linear programming. Intuitively, this is because the nested cycles are fixed. Thus to check whether a run drops below zero it suffices to check before applying a cycle and after applying it for the last time (see e.g.  [5, Section V, Lemma 14]).    \(\square \)

We highlight that it is rather unexpected that only one extra ‘level’ of linear form paths is enough to obtain polynomial size witnesses of coverability in a 2-VASS with one unary counter, since the problem is PSPACE-complete for general 2-VASS. Roughly speaking, the example given in Figure 3 observes the most complex behaviour possible and this instance of coverability is witnessed by a compressed linear form path. More specifically, compressed linear form paths containing only one linear form cycle suffice as witnesses for coverability in 2-VASS with one unary counter. Therefore, all witnesses can be represented by a compressed linear form path \(\rho \sigma ^N \tau \) where \(\rho \) and \(\tau \) are linear form paths to and from the single linear form cycle \(\sigma \) which is iterated N times.

The rest of the paper is dedicated to proving Theorem 1. We heavily exploit both distinguishing features of the problem: the fact that one counter receives unary encoded updates (as opposed to both counters in binary) and the fact that we aim to assert coverability (as opposed to reachability). Our approach is as presented in the introduction. In 4 we observe that we can polynomially bound the total number of distinct short cycles. We formalise this and show that there are only polynomially many ‘irreplaceable’ short cycles. In 5 we provide a ‘reshuffling procedure’. If some short cycle \(\gamma \) repeats exponentially many times we aim to modify the path \(\pi \) by moving the cycles \(\gamma \) close to each other. Then either every short cycle \(\gamma \) will appear only in polynomially many ‘bundles’ \(\gamma ^e\), or we find a cycle \(\sigma \) such that \(\textrm{eff}(\sigma ) > \textbf{0}\). In the latter case, by pumping \(\sigma \) we are essentially left with one counter. Finally, in Section 6 we conclude the proof of Theorem 1.

4 Replacing Short Cycles

In this section, we show that there are only polynomially many short cycles that need occur in a run witnessing coverability. Fix a path \(\pi = (q_{i-1}, b_i, u_i, q_i)_{i=1}^k\). Let \(0 \le i_b, i_u \le k\) be the first indices such that \(g_b = \sum _{i=1}^{i_b} b_i\) and \(g_u = \sum _{i=1}^{i_u}u_i\) are at their lowest, respectively. Note that \(g_b, g_u \le 0\) since by convention if we consider \(i_b, i_u = 0\) then the sum evaluates to 0. We call and denote these two numbers the binary guard \(\textrm{grd}_b(\pi ) = g_b\) and the unary guard \(\textrm{grd}_u(\pi ) = g_u\). The following claim immediately follows from these definitions.

Claim 1

Both \(\textrm{grd}_b(\pi [i_b+1 .. k]) = 0\) and \(\textrm{grd}_u(\pi [i_u+1 .. k]) = 0\).

Much like the nadir of a cycle in a one-counter net, defined in [1], we define the binary-nadir state as \(q_{i_b}\), i.e. the first state in which the binary counter first attains the lowest value when executing \(\pi \). We call the binary-nadir decomposition \(\pi = \pi _1^b \pi _2^b\), for \(\pi _1^b = \pi [1 .. i_b]\) and \(\pi _2^b = \pi [i_b+1 .. k]\), as intimated in Claim 1. Notice that this decomposition necessitates the binary guard of the path \(\pi \) is equal to the binary effect of the prefix \(\pi _1^b\), \(\textrm{grd}_b(\pi ) = \textrm{eff}_b(\pi _1^b) = \textrm{grd}_b(\pi _1^b)\). Furthermore, the suffix of the binary-nadir decomposition has zero binary guard \(\textrm{grd}_b(\pi _2^b) = 0\). We primarily utilise binary-nadir states and binary-nadir decompositions, hence the omission of matching unary-nadir states and unary-nadir-decompositions.

Definition 2 (Replaceable cycles)

Let \(\gamma \) be a q-cycle and let p be the binary-nadir state of \(\gamma \). We say that \(\gamma \) is replaceable if there exists a q-cycle \(\gamma '\) with the same binary-nadir state p, such that

  1. (a)

    \(\textrm{eff}_b(\gamma ') \ge \textrm{eff}_b(\gamma )\) and \(\textrm{eff}_u(\gamma ') \ge \textrm{eff}_u(\gamma )\),

  2. (b)

    \(\textrm{grd}_b(\gamma ') \ge \textrm{grd}_b(\gamma )\) and \(\textrm{grd}_u(\gamma ') \ge \textrm{grd}_u(\gamma )\), and

  3. (c)

    \(\textrm{len}(\gamma ') \le \textrm{len}(\gamma )\).

Additionally, at least one inequality is strict and we write \(\gamma \prec \gamma '\).

We say a cycle is irreplaceable if it is not replaceable. We also say that an irreplaceable q-cycle \(\gamma \) with the binary-nadir state p is characterised by the five values: \(\textrm{eff}_b(\gamma )\), \(\textrm{eff}_u(\gamma )\), \(\textrm{grd}_b(\gamma )\), \(\textrm{grd}_u(\gamma )\), and \(\textrm{len}(\gamma )\).

Lemma 1 (Replacing cycles)

Let \(\pi = \pi _1 \gamma \pi _2\), where \(\gamma \) is a q-cycle. Suppose \(p(\textbf{u})\xrightarrow {\pi }q(\textbf{v})\) then the following hold.

  • If \(\gamma \) is replaceable, then there exists an irreplaceable q-cycle \(\gamma \prec \gamma '\) such that \(p(\textbf{u})\xrightarrow {\pi _1 \gamma ' \pi _2}q(\textbf{v}')\).

  • If \(\gamma \) is irreplaceable, then for every irreplaceable q-cycle \(\gamma '\) that has the same characterisation as \(\gamma \), \(p(\textbf{u})\xrightarrow {\pi _1 \gamma ' \pi _2}q(\textbf{v}')\).

In both cases \(\mathbf{v'} \ge \textbf{v}\) and \(\textrm{len}(\pi ) \ge \textrm{len}(\pi _1 \gamma ' \pi _2)\).

For convenience, we define the polynomial \(R(|Q |) \,{:}{=}\, |Q |^4(|Q |+1)(2|Q |+1)^2\).

Lemma 2

There exists at most \(R(|Q |)\) many irreplaceable short cycles with different characterisations.

Proof

We fix two states q and p and consider only q-cycles \(\gamma \) with the binary-nadir state p. Thus in the final argument one must multiply everything by \(|Q |^2\). Since we consider short cycles, the unary effect and the unary guard are small, i.e. \(-|Q | \le \textrm{eff}_u(\gamma ) \le |Q |\) and \(-|Q | \le \textrm{grd}_u(\gamma ) \le 0\).

Towards a contradiction, suppose there exists more than \(|Q |^2(|Q |+1)(2|Q |+1)^2\) many such irreplaceable q-cycles with different characterisations. By the pigeonhole principle there must exist two cycles, denoted in binary-nadir decomposition \(\gamma = \gamma _1\gamma _2\) and \(\gamma ' = \gamma '_1\gamma '_2\), that have the same values \(\textrm{eff}_u(\gamma _1) = \textrm{eff}_u(\gamma '_1)\), \(\textrm{eff}_u(\gamma _2) = \textrm{eff}_u(\gamma '_2)\), \(\textrm{grd}_u(\gamma ) = \textrm{grd}_u(\gamma ')\), \(\textrm{len}(\gamma _1) = \textrm{len}(\gamma '_1)\), and \(\textrm{len}(\gamma _2) = \textrm{len}(\gamma '_2)\).

We know that the irreplaceable q-cycles \(\gamma \) and \(\gamma '\) have different characterisations, so it must be the case that their binary effects differ \(\textrm{eff}_b(\gamma ) \ne \textrm{eff}_b(\gamma ')\). Otherwise, the cycle with the lesser binary guard is replaceable, because the unary effect, unary guard, and length do not differ. Without loss of generality, suppose \(\textrm{eff}_b(\gamma ) > \textrm{eff}_b(\gamma ')\), then \(\textrm{grd}_b(\gamma ) < \textrm{grd}_b(\gamma ')\). Otherwise, \(\gamma '\) would be replaceable as \(\gamma \prec \gamma '\).

Now consider the q-cycle \(\sigma = \gamma _1'\gamma _2\), also with the binary-nadir state p. We will show that \(\gamma \prec \sigma \) contradicting the fact that \(\gamma \) is an irreplaceable q-cycle. First, observe that \(\sigma \) has greater binary effect than \(\gamma \) as

$$\begin{aligned} \textrm{eff}_b(\sigma ) = \textrm{eff}_b(\gamma _1') + \textrm{eff}_b(\gamma _2) > \textrm{eff}_b(\gamma _1) + \textrm{eff}_b(\gamma _2) = \textrm{eff}_b(\gamma ), \end{aligned}$$

where the inequality holds because \(\textrm{grd}_b(\gamma ) < \textrm{grd}_b(\gamma ')\). Second, \(\sigma \) and \(\gamma \) have equal unary effect because \(\textrm{eff}_u(\gamma _1') = \textrm{eff}_u(\gamma _1)\). Third, we show that \(\sigma \) has a greater binary guard than \(\gamma \). Since \(\gamma _2\) is the suffix of the binary-nadir decomposition of \(\gamma \), it must be true that \(\textrm{grd}_b(\gamma _2) = 0\). By Claim 1 \(\textrm{grd}_b(\sigma ) = \textrm{grd}_b(\gamma _1')\). Combining these facts, \(\textrm{grd}_b(\sigma ) = \textrm{grd}_b(\gamma ') > \textrm{grd}_b(\gamma )\). Fourth, \(\sigma \) has at least the unary guard of \(\gamma \) because, in particular, the unary guard of the prefix of a path is at most the unary guard of the entire path.

$$\begin{aligned} \textrm{grd}_u(\sigma )&\; = \min \{\textrm{grd}_u(\gamma '_1), \textrm{eff}_u(\gamma '_1) + \textrm{grd}_u(\gamma _2)\} \\&\; \ge \min \{\textrm{grd}_u(\gamma '), \textrm{eff}_u(\gamma '_1) + \textrm{grd}_u(\gamma _2)\} \\&\; = \min \{\textrm{grd}_u(\gamma ), \textrm{eff}_u(\gamma _1) + \textrm{grd}_u(\gamma _2)\} = \textrm{grd}_u(\gamma ) . \end{aligned}$$

Fifth and finally, \(\sigma \) and \(\gamma \) have equal length because \(\textrm{len}(\gamma '_1) = \textrm{len}(\gamma _1)\). We have at least one strict inequality. Thus, we have reached the desired contradiction.    \(\square \)

5 Reshuffling Linear Form Paths

5.1 Reshuffling Procedure

There can be many linear forms for a path \(\pi \). We will try to find an ‘optimal’ one, so we introduce a cost function to quantify linear forms. Recall that a linear form \(\ell \) is a sequence of paths \(\tau _0, \tau _1, \ldots , \tau _k\) and a sequence of cycles \(\gamma _1, \ldots , \gamma _k\). If \(\pi \) is in the linear form \(\ell = (\tau _0, \gamma _1, \tau _1, \dots , \tau _{k-1}, \gamma _k, \tau _k)\) then we write \(\pi _\ell = \tau _0 \gamma _1^{e_1} \tau _1 \cdots \tau _{k-1} \gamma _k^{e_k} \tau _{k}\), where \(\pi = \pi _\ell \) (the index is here to stress the exact linear form). For this section, we will consider linear forms only containing short cycles \(\gamma \), they will play a key role in the following arguments.

We define a cost function that assigns, to a linear form \(\ell \), the following pair of naturals \(C(\ell ) \,{:}{=}\, \left( \sum _{i=0}^k \textrm{len}(\tau _i), k \right) \). For convenience, we define the polynomial \(P(|Q |) \,{:}{=}\, 2(|Q |^2 + 1)(|Q |^2 + 2) \cdot R(|Q |)\), where R is the polynomial defined for Lemma 2. We say that a linear form \(\ell \) is narrow if \(C(\ell ) \le (|Q |(P(|Q |)+1), P(|Q |))\), otherwise we say that \(\ell \) is wide. We say that the triple \((\pi ', \sigma , \pi '')\) is a monotone cycle decomposition of a path \(\pi \) if \(\sigma \) is a monotone cycle, \(\pi = \pi ' \sigma \pi ''\), and \(\textrm{len}(\sigma ) < \textrm{len}(\pi )\).

Lemma 3 (Reshuffling)

Let \(\pi \) be a path such that \(p(\textbf{u})\xrightarrow {\pi }q(\textbf{v})\). Then there exists a path \(\rho \) such that \(p(\textbf{u})\xrightarrow {\rho }q(\textbf{w})\) where \(\textbf{w} \ge \textbf{v}\), \(\textrm{len}(\rho ) \le \textrm{len}(\pi )\), and either

  1. (i)

    there exists a narrow linear form for \(\rho \), or

  2. (ii)

    there exists a monotone cycle decomposition of \(\rho \).

Proof

We start with a series of preparations. In the early part of this proof, we provide simple observations to ascertain some auspicious properties of our path. In the later part of this proof, we present the ‘reshuffling procedure’ and conclude with one of the cases in the statement of this lemma. In this proof we will compare linear forms using the lexicographic order \(\prec _{lex}\), that is known to be a linear-order and a well-order. Formally,

$$\begin{aligned} C(\ell ') \prec _{lex}C(\ell ) \iff&(C(\ell '))_1< (C(\ell ))_1 \text { or, } \\&(C(\ell '))_1 = (C(\ell ))_1 \text { and } (C(\ell '))_2 < (C(\ell ))_2. \end{aligned}$$

We start with a path \(\pi '\) such that \(p(\textbf{u})\xrightarrow {\pi '}q(\textbf{v}')\) where \(\textbf{v}' \ge \textbf{v}\), \(\textrm{len}(\pi ') \le \textrm{len}(\pi )\), and \(\pi '\) has a linear form \(\ell '\) that has the least cost among all linear forms for all like-paths. That means there does not exist another path \(\pi ''\) such that \(p(\textbf{u})\xrightarrow {\pi ''}q(\textbf{v}'')\) where \(\textbf{v}'' \ge \textbf{v}\), \(\textrm{len}(\pi '') \le \textrm{len}(\pi )\), and \(\pi ''\) has a linear form \(\ell ''\) such that \(C(\ell '') \prec _{lex}C(\ell ')\).

For the first observation, suppose there exists \(0 \le i \le k\) such that \(\textrm{len}(\tau _i) > |Q |\). Then the path \(\tau _i\) can be written as \(\tau _i = \tau ' \gamma \tau ''\), where \(\gamma \) is a short cycle. We can define the linear form \(\ell ''\) by modifying \(\ell '\) where \(\tau _i\) is swapped for \(\tau ' \gamma \tau ''\). Although this increments the number of cycles k, we decrease the total length of the paths as \(\textrm{len}(\tau ') + \textrm{len}(\tau '') < \textrm{len}(\tau _i)\) (recall that empty cycles are forbidden). Thus \(C(\ell '') \prec _{lex}C(\ell ')\) contradicting the assumption that \(\ell \) has minimum cost. Therefore, we assume that \(\textrm{len}(\tau _i) \le |Q |\) for all \(0 \le i \le k\).

For the second observation, we define \(U \,{:}{=}\, \{0 \le i \le m: (\textbf{v}_i)_2 < |Q |\}\) to be the set of indices of configurations in the run that have unary counter value less than \(|Q |\). Observe that if \(|U | > |Q |^2 + 1\) then there are two indices \(0< i < j \le m\) such that the two corresponding configurations in the run have matching states \(q_{i} = q_{j}\) and equal unary counter values \((\textbf{v}_{i})_2 = (\textbf{v}_{j})_2\). Then, regardless of sign of its binary effect, \(\pi '[i..j]\) is a monotone cycle. Here, case (ii) immediately holds by decomposing \(\pi '\) itself using the monotone cycle \(\pi '[i .. j]\), given that \(i > 0\) and \(j \le m\) implies \(\textrm{len}(\pi '[i .. j]) = j - i < m = \textrm{len}(\pi ')\). Therefore, we assume \(|U | \le |Q |^2 + 1\). We continue with the aim of satisfying the conditions of case (ii) by finding a monotone cycle decomposition.

Let \(d = |\{\gamma _1, \ldots , \gamma _k\} |\) be the number of distinct cycles in the linear form \(\ell '\). By Lemma 1 and Lemma 2, we can assume that \(d \le R(|Q |)\). Otherwise, we can exchange replaceable q-cycles for irreplaceable q-cycles using the first point in Lemma 1. It is possible that for a particular characterisation, we can observe more than one irreplaceable q-cycle. Then using the second point in Lemma 1, we can arbitrarily select one of these irreplaceable q-cycles with equal characterisations to exchange all others with. By applying these cycle replacements to \(\pi '\), we obtain a different path \(\rho \). Definition 2 ensures that we do so without decreasing the effect (a), without allowing the counters to take a negative value (b), and without increasing the length of the path (c). Therefore \(p(\textbf{u})\xrightarrow {\rho }q(\textbf{w})\) and \(\textbf{w} \ge \textbf{v}' \ge \textbf{v}\), and \(\textrm{len}(\rho ) \le \textrm{len}(\pi ') \le \textrm{len}(\pi )\). We remark since cycles have been exchanged one-for-one, then \(\rho \) takes a linear form \(\ell \) with the same path segments as \(\ell '\). Therefore, it is clear that neither the number of cycles k, nor the sum of the lengths of the paths between cycles, have changed. We also know that \(\ell \) is a linear form for \(\rho \) with minimum cost \(C(\ell ) = C(\ell ')\), as per the initialisation in this proof.

Suppose \(\rho = \rho _\ell = \tau _0 \gamma _1^{e_1} \tau _1 \cdots \tau _{k-1} \gamma _k^{e_k} \tau _k\). Let \((q_j(\textbf{v}_j))_{j=0}^m\) be the run obtained by following the path \(\rho _\ell \) from the initial configuration \(q_0(\textbf{v}_0) = p(\textbf{u})\) to the final configuration \(q_m(\textbf{v}_m) = q(\textbf{w})\). We may assume that \(\ell \) is wide. Otherwise, case (i) is immediately satisfied. We also know that \(\textrm{len}(\rho _\ell ) \ge \max \{(C(\ell ))_1, (C(\ell ))_2\} > P(|Q |)\). We may also assume that each cycle \(\gamma _1, \ldots , \gamma _k\) is non-monotone, i.e. it is positive-negative or negative-positive. Otherwise, case (ii) immediately holds by decomposing \(\rho \) itself using some monotone cycle \(\gamma _i\), given that \(\textrm{len}(\gamma _i) \le |Q |< P(|Q |) < \textrm{len}(\rho _\ell )\). Notice this is valid since each \(e_i > 0\) by the minimality of \(C(\ell )\), otherwise you can write \(\cdots \tau _{i-1} \gamma _i^0 \tau _i\cdots \) with one less cycle, decreasing \((C(\ell ))_2\).

From the first observation, we get \(\sum _{i=0}^k \textrm{len}(\tau _i) \le (k+1) |Q |\). Given that \(\ell \) is wide, either \(|Q |(P(|Q |)+1) < (C(\ell '))_1 = \sum _{i=0}^k \textrm{len}(\tau _i) \le (k+1) |Q |\) that implies \(P(|Q |) < k\), or \(P(|Q |) < (C(\ell '))_2 = k\). Regardless, \(P(|Q |) < k\) holds. Recall that \(|U | \le |Q |^2 + 1\) from the second observation. Since there are relatively ‘few’ configurations indexed by U, there must exist a relatively ‘distant’ pair of consecutive configurations indexed by U. More formally, there are i and j such that \(0 \le i < j \le k\) and \(j - i \ge 2(|Q |^2+2)R(|Q |)\) and all configurations that occur in the run over the path segment \(\tau _{i} \gamma _{i+1}^{e_{i+1}} \cdots \gamma _{j}^{e_j} \tau _{j}\) have unary counter value at least \(|Q |\). Notice that \(j - i\) is the number of cycles in this path segment. Since \(j - i \ge 2(|Q |^2 + 2)R(|Q |)\) and by pigeonhole principle on the number of irreplaceable cycles, there is a common irreplaceable cycle \(\gamma \) repeated at least \(x = 2(|Q |^2 + 2)\) many times. We will focus on the first x such occurrences of this cycle. Let \(s_1, \ldots , s_x\) be the indices of this cycle \(\gamma \), i.e. \(\gamma = \gamma _{s_1} = \ldots = \gamma _{s_x}\). To highlight these cycles, we decompose this path segment into

$$\begin{aligned} \tau _{i} \gamma _{i+1}^{e_{i+1}} \cdots \gamma _{j}^{e_j} \tau _{j} = \varLambda _0 \gamma ^{f_1} \varLambda _1 \cdots \varLambda _{x-1} \gamma ^{f_x} \varLambda _x, \end{aligned}$$

where \(f_j \,{:}{=}\, e_{s_j}\) and \(\varLambda _j\) are the concatenated paths (and cycles) in between iterations of \(\gamma \), see Figure 5. To reiterate, we know that all configurations that occur in the run over this path segment have at least \(|Q |\) unary counter value and \(\gamma \) is a short cycle.

Fig. 5.
figure 5

The decomposition of the path segment into \(\varLambda _0 \gamma ^{f_1} \varLambda _1 \cdots \varLambda _{x-1} \gamma ^{f_x} \varLambda _x\), as above. Notice that the unary counter is always at least \(|Q |\) as no configurations indexed by U are present.

Full size image

Reshuffling Procedure. In the rest of the proof we will modify the path segment (above) of the path \(\rho _\ell \) with a procedure that we call reshuffling. At the end of this procedure we will find a monotone cycle and satisfy case (ii) of this lemma. We either find this cycle directly, or we obtain a linear form \(\ell ''\) such that \(C(\ell '') \prec _{lex}C(\ell )\) contradicting the assumption that \(\ell \) has minimal cost.

Note that \(x = 2(|Q |^2 + 2)\) is even, and for every pair of consecutive cycles \(\gamma _{2j-1}\) and \(\gamma _{2j}\) (for \(1 < 2j \le x\)), consider the subsegment \(\gamma ^{f_{2j-1}} \varLambda _{2j-1} \gamma ^{f_{2j}}\). There are two scenarios depending on the variant of the non-monotone cycle \(\gamma \). In the scenario where \(\gamma \) is positive-negative, we move an iteration of \(\gamma \) from right to left obtaining \(\gamma ^{f_{2j-1}+1} \varLambda _{2j-1} \gamma ^{f_{2j}-1}\). In the scenario where \(\gamma \) is negative-positive, we move an iteration of \(\gamma \) in the opposite direction obtaining \(\gamma ^{f_{2j-1}-1} \varLambda _{2j-1} \gamma ^{f_{2j}+1}\).

We repeat this procedure until one of two conditions are met. The first is when there are no iterations of \(\gamma \) on one side, so either \(f_{2j-1}\) or \(f_{2j}\) becomes 0. The second is when there appears a configuration, in the run over the path subsegment after reshuffling, with unary counter value less than \(|Q |\). See Figure 6 for a pictorial presentation of reshuffling in the scenario where \(\gamma \) is positive-negative.

Fig. 6.
figure 6

Reshuffling around a path \(\varLambda \) (blue) where \(\gamma \) (red) is positive-negative. Before reshuffling, the path subsegment \(\cdots \gamma \varLambda \gamma \cdots \) all configurations have unary counter value at least \(|Q |\) in the run (left). After reshuffling, the path subsegment \(\cdots \gamma \gamma \varLambda \cdots \), there is a configuration with unary counter value less than \(|Q |\) in the run (right).

Full size image

We claim that after each reshuffling step, the corresponding run remains executable, so we must check that both counters remain non-negative. Notice that by only moving a cycle, the total effect of the path subsegment remains the same. Therefore, if the run was executable before reshuffling, we can safely assume that the prefix before the path subsegment and the suffix after the path subsegment are still executable. For that reason, consider the counter values of configurations occurring in the run over the reshuffled path subsegment. We focus on a single step of the reshuffling procedure that concerns the subsegment \(\gamma ^{f_{2j-1}} \varLambda _{2j-1} \gamma ^{f_{2j}}\).

Suppose \(\gamma \) is a positive-negative cycle. Then the reshuffling procedure moves \(\gamma \) from right to left. We claim that since \(f_{2j-1} > 0\) and \(\varLambda _0 \gamma ^{f_1} \varLambda _1 \cdots \varLambda _{2j-1} \gamma ^{f_{2j-1}}\) is executable, the subsegment \(\varLambda _0 \gamma ^{f_1} \varLambda _1 \cdots \varLambda _{2j-1} \gamma ^{f_{2j-1}+1}\) is executable from the initial configuration. This is because one prerequisite of the reshuffling procedure is that all configurations occurring in the run over the path subsegment have at least \(|Q |\) unary counter value. Moreover, the cycle \(\gamma \) has length at most \(|Q |\) so \(\textrm{grd}_u(\gamma ) \ge -|Q |\) means the unary counter value remains non-negative. As for the binary counter value, since a single execution of \(\gamma \) increases the binary counter and an iteration of \(\gamma \) was already executed before reshuffling, \(\varLambda _0 \gamma ^{f_1} \varLambda _1 \cdots \varLambda _{2j-1} \gamma ^{f_{2j-1}+1}\) is executable. In the same way, from the initial configuration, \(\varLambda _0 \gamma ^{f_1} \varLambda _1 \cdots \varLambda _{2j-1} \gamma ^{f_{2j-1}+1} \varLambda _{2j} \gamma _{2j}^{f_{2j}-1}\) is executable. This is because \(\textrm{eff}_u(\gamma ) \ge -|Q |\), and again, all configurations occurring in the run over the path subsegment have at least \(|Q |\) unary counter value, and also because of the monotonicity on the binary counter.

The argument when \(\gamma \) is a negative-positive cycle is analogous. This concludes the correctness analysis of the reshuffling procedure.

Finishing Reshuffling. We analyse what happens when reshuffling is finished. Suppose that there exists a pair \(2j-1\) and 2j such that the reshuffling finishes under the first condition where all iterations of \(\gamma \) have been moved to one side of \(\varLambda _{2j-1}\). In this case we obtain a new linear form \(\ell ''\) for \(\rho \), where one collection of the cycle \(\gamma \) has been removed (decrementing k). So \((C(\ell ''))_2 = k - 1 < (C(\ell ))_2\) and the two adjacent path segments can be combined without changing the summed length of paths so \((C(\ell ''))_1 = (C(\ell ))_1\). Therefore, \(C(\ell '') \prec _{lex}C(\ell )\) contradicting the assumption \(\ell \) has the minimal cost.

Otherwise, for every \(1 \le j \le x/2\) the reshuffling of pair \(2j-1\) and 2j finishes under condition the second condition. So there is a configuration with unary counter value less than \(|Q |\) in the run induced from the path \(\rho \) for each pair \(2j-1\) and 2j (see Figure 7). Recall that \(\frac{x}{2} = |Q |^2 + 2\), that is the number of pairs. Akin to the first observation (in the beginning of this proof), we use the pigeonhole principle on the number of such configurations to obtain two configurations with matching states and equal unary counter values. The path segment inducing the part of the run between these two configurations is a monotone cycle, regardless of the binary effect. Again, it must be true that the length of this cycle is less than the length of the whole path, so we obtain a monotone cycle decomposition of \(\rho \). Thus case (ii) of the lemma holds.    \(\square \)

Fig. 7.
figure 7

After reshuffling is finished under condition the second condition, we can find a zero unary effect cycle using the (sufficiently many) configurations with unary counter less \(|Q |\).

Full size image

5.2 Applying Reshuffling

Lemma 3 does not necessarily return a narrow linear form for a path \(\pi \) witnessing coverability. Instead it may return a monotone cycle decomposition \((\rho , \sigma , \tau )\) of \(\pi \). Our next goal is to show that there exists polynomial size certificates for \(\rho \) and \(\sigma \) (Lemma 4), and then to show that there exists a polynomial size certificate for \(\tau \) (Lemma 5). Like linear forms, there can be many monotone cycle decompositions for a path. Following, we will use the cost function assigning monotone cycle decompositions to pairs of natural numbers \(D((\rho , \sigma , \tau )) \,{:}{=}\, (\textrm{len}(\rho \sigma ), \textrm{len}(\sigma ))\). Note that we can compare two decompositions using their cost, even if they are for two different paths.

Lemma 4

Suppose \(p(\textbf{u})\xrightarrow {*}q(\textbf{v})\) yet there is no narrow linear form \(\ell \) for any path \(\pi \) such that \(p(\textbf{u})\xrightarrow {\pi }q(\textbf{w})\) and \(\textbf{w} \ge \textbf{v}\), then there exists a path \(\pi '\) such that

  1. (a)

    \(p(\textbf{u})\xrightarrow {\pi '}q(\textbf{w}')\) where \(\textbf{w}' \ge \textbf{v}\),

  2. (b)

    there is a monotone cycle decomposition \((\rho , \sigma , \tau )\) of \(\pi '\) where \(\textrm{eff}(\sigma ) > \textbf{0}\), and

  3. (c)

    there are narrow linear forms for both \(\rho \) and \(\sigma \).

Proof

We will again use the lexicographical order \(\prec _{lex}\) to compare the cost of monotone cycle decompositions. Let \(\pi \) be a path of minimum length such that \(p(\textbf{u})\xrightarrow {\pi }q(\textbf{w})\) where \(\textbf{w} \ge \textbf{v}\). Let \(c = (\rho , \sigma , \tau )\) be the monotone cycle decomposition of \(\pi \) that minimizes the cost D(c) under the \(\prec _{lex}\) order. Such a decomposition must exist, otherwise applying Lemma 3 would return a narrow linear form \(\ell '\) for \(\rho \) such that \(p(\textbf{u})\xrightarrow {\rho }q(\textbf{w}')\) and \(\textbf{w}' \ge \textbf{w} \ge \textbf{v}\), contradicting an assumption of this lemma. Observe that \(\textrm{eff}(\sigma ) > \textbf{0}\), otherwise one can remove \(\sigma \) and consider the shorter path \(\rho \tau \), contradicting the minimal length of \(\pi \). Next, we argue that \(\rho \) and \(\sigma \) do not have monotone cycle decompositions, we then leverage Lemma 3 to obtain the narrow linear forms required.

Path \(\rho \) cannot be decomposed further. Towards a contradiction, assume that there is a monotone cycle decomposition \(c' = (\rho ', \sigma ', \tau ')\) of \(\rho \). Observe that the following monotone cycle decomposition \(c' = (\rho ', \sigma ', \tau ' \sigma \tau )\) of \(\pi \) has lower cost \(D(c') \prec _{lex}D(c)\) as \((D(c'))_1 = \textrm{len}(\rho ') + \textrm{len}(\sigma ') < \textrm{len}(\rho ) + \textrm{len}(\sigma ) = (D(c))_1\). This contradicts the assumption that \((\rho , \sigma , \tau )\) has minimum cost.

Suppose \(p(\textbf{u})\xrightarrow {\rho }p'(\textbf{x})\). Since there is no monotone cycle decomposition, applying Lemma 3 to \(\rho \) returns a path \(\rho '\) with a narrow linear form such that \(p(\textbf{u})\xrightarrow {\rho '}p'(\textbf{x}')\) where \(\textbf{x}' \ge \textbf{x}\) and \(\textrm{len}(\rho ') \le \textrm{len}(\rho )\).

Cycle \(\sigma \) cannot be decomposed further. Towards a contradiction, assume that there is a monotone cycle decomposition \((\rho ', \sigma ', \tau ')\) of \(\sigma \). Observe that the following monotone cycle decomposition \(c' = (\rho \rho ', \sigma ', \tau ' \tau )\) of \(\pi \) has lower cost \(D(c') \prec _{lex}D(c)\) as \((D(c'))_1 = \textrm{len}(\rho ) + \textrm{len}(\rho ') + \textrm{len}(\sigma ') \le \textrm{len}(\rho ) + \textrm{len}(\sigma ) = (D(c))_1\) and \((D(c'))_2 = \textrm{len}(\sigma ') < \textrm{len}(\sigma ) = (D(c))_2\). This contradicts the assumption that \((\rho , \sigma , \tau )\) has minimum cost.

Suppose \(p'(\textbf{x})\xrightarrow {\sigma }p'(\textbf{y})\). Since there is no monotone cycle decomposition, applying Lemma 3 to \(\sigma \) returns a path \(\sigma '\) with a narrow linear form such that \(p'(\textbf{x})\xrightarrow {\sigma '}p'(\textbf{y}')\) where \(\textbf{y}' \ge \textbf{y}\) and \(\textrm{len}(\sigma ') \le \textrm{len}(\sigma )\). In particular, it is also true that \(\textrm{eff}(\sigma ') \ge \textrm{eff}(\sigma ) > \textbf{0}\).

Replacing \(\rho '\) for \(\rho \) and \(\sigma '\) for \(\sigma \) in \(\pi \) yields a path \(\pi '\). Clearly if \(p(\textbf{u})\xrightarrow {\pi }q(\textbf{w})\) where \(\textbf{w} \ge \textbf{v}\), then \(p(\textbf{u})\xrightarrow {\pi '}q(\mathbf{w'})\) where \(\textbf{w}' \ge \textbf{w} \ge \textbf{v}\). Finally, \((\rho ', \sigma ', \tau )\) is monotone cycle decomposition of \(\pi '\) such that \(\textrm{eff}(\sigma ') > \textbf{0}\) and \(\rho '\) and \(\sigma '\) have narrow linear forms, as required.    \(\square \)

We now aim to obtain a narrow linear form for \(\tau \). Note that Lemma 4 gives us a monotone cycle \(\sigma \) with positive effect on at least one counter, i.e. \(\textrm{eff}(\sigma ) > \textbf{0}\). By pumping \(\sigma \) we can force one of the counters to take an arbitrarily large value (following, the vector \(\textbf{x}\) reflects this large value for Lemma 5). Then, loosely speaking, the problem reduces to coverability in 1-VASS. However, proving the existence of a polynomial size compressed linear form path in Theorem 1 requires more care. Note that Lemma 5 is stated for 2-VASS (not necessarily with one unary counter). First we need to recall the following bound on counter values observed throughout runs. Recall that \(|V |_{\max } \,{:}{=}\, |Q | + |T | \cdot |T |_{\max }\) is the pseudo-polynomial size of the input.

Theorem 2

(Corollary from Theorem 3.2 in [4]). Consider a 2-VASS (with both counters in binary) \(V = (Q,T)\) and let \(p(\textbf{u})\xrightarrow {*}q(\textbf{v})\), then there exists a run \(p(\textbf{u}) = q_0(\textbf{v}_0)\), \(q_1(\textbf{v}_{1}), \ldots , q_m(\textbf{v}_m) = q(\textbf{v})\) such that \(|\textbf{v}_0 |_{\max }, |\textbf{v}_1 |_{\max }, \ldots ,\) \(|\textbf{v}_m |_{\max } \le (|V |_{\max } + |\textbf{u} |_{\max } + |\textbf{v} |_{\max })^{\mathcal {O}(1)}\).

In the following lemma, that is proved in the appendix, given a 2-VASS V, the initial configuration \(p(\textbf{u})\), and target configuration \(q(\textbf{v})\), we write B in place of \((|V |_{\max } + |\textbf{u} |_{\max } + |\textbf{v} |_{\max })^{\mathcal {O}(1)}\) from Theorem 2 and we fix \(\textbf{x} = (4B|Q |^2|V |_{\max }^2, 0)\).

Lemma 5

Consider a 2-VASS (with both counters in binary) \(V = (Q,T)\) and let \(p(\textbf{u})\xrightarrow {*}q(\textbf{v})\), then there exists a narrow linear form path \(\pi '\) such that \(p(\mathbf{u + x})\xrightarrow {\pi '}q(\textbf{v}')\) for some \(\textbf{v}' \ge \textbf{v}\).

6 Proof of Theorem 1

Before proving Theorem 1, we employ the fact that for a general 2-VASS, not necessarily with one unary counter, the exponents of cycles in linear forms can be pseudo-polynomially bounded.

Lemma 6

(Corollary from Lemma 18 in [5]). Let \(\pi \) be path in a 2-VASS with a linear form \(\pi = \tau _0 \gamma _1^{f_1} \tau _1 \ldots \gamma _k^{f_k} \tau _k\) such that \(p(\textbf{u})\xrightarrow {\pi }q(\textbf{v})\). Then there exist a path \(\pi ' = \tau _0 \gamma _1^{e_1} \tau _1 \cdots \tau _{k-1} \gamma _k^{e_k} \tau _k\) such that \(p(\textbf{u})\xrightarrow {\pi '}q(\textbf{v}')\) where \(\textbf{v}' \ge \textbf{v}\) and \(\textrm{bitsize}(e_1), \ldots , \textrm{bitsize}(e_k)\) are all bounded by a polynomial in \(|V | + \textrm{bitsize}(\textbf{u}) + \textrm{bitsize}(\textbf{v})\).

Proof

of Theorem 1. Let \(p(\textbf{u})\xrightarrow {\pi }q(\textbf{v})\) for some path \(\pi \). If there is a narrow linear form \(\ell \) for \(\pi \) then by Lemma 6 we obtain \(\pi ' = \tau _0 \gamma _1^{e_1} \tau _1 \cdots \tau _{k-1} \gamma _k^{e_k} \tau _k\) such that \(p(\textbf{u})\xrightarrow {\pi '}q(\textbf{v}')\) where \(\textbf{v}' \ge \textbf{v}\) and \(\textrm{bitsize}(e_1), \ldots , \textrm{bitsize}(e_k)\) are all bounded above by a polynomial in \(|V | + \textrm{bitsize}(\textbf{u}) + \textrm{bitsize}(\textbf{v})\). Since \(\ell \) is a narrow linear form, we know that \(k \le P(|Q |)\) so \(\sum _{i = 1}^k \textrm{len}(\gamma _i) \le k|Q | \le |Q |P(|Q |)\) and we also know that \(\sum _{i=0}^{k} \textrm{len}(\tau _i) \le |Q |(P(|Q |)+1)\). Together, this implies the linear form path \(\pi '\) is of polynomial size.

It remains to consider the case when there is no narrow linear form \(\ell \) for \(\pi \). By Lemma 4 (via Lemma 3) there exists a path \(\pi '\) such that \(p(\textbf{u})\xrightarrow {\pi '}q(\textbf{v}')\) and \(\textbf{v}' \ge \textbf{v}\). Moreover, there is a monotone cycle decomposition \((\rho , \sigma , \tau )\) of \(\pi '\) such that \(\textrm{eff}(\sigma ) > \textbf{0}\) and there are narrow linear forms for both \(\rho \) and \(\sigma \).

Assume that \((\textrm{eff}(\sigma ))_1 > 0\). This is without loss of generality because if \((\textrm{eff}(\sigma ))_1 = 0\) then one can flip the coordinates in V, \(\textbf{u}\) and \(\textbf{v}\) (for the remainder of the proof it will not matter that one counter is unary). Let \(p'(\textbf{m})\) be the configuration such that \(p(\textbf{u})\xrightarrow {\;\rho \;}p'(\textbf{m})\xrightarrow {\sigma \tau }q(\textbf{v}')\). Observe that since \(\textrm{eff}(\sigma ) > \textbf{0}\) for every \(i \in \mathbb {N}\) the path \(\rho \sigma ^i\) induces the run \(p(\textbf{u})\xrightarrow {\rho \sigma ^i}p'(\textbf{m}+ i\cdot \textrm{eff}(\sigma ))\). Consider \(x = (\textbf{x})_1 = 4B|Q |^2|V |_{\max }^2\) (for Lemma 5), clearly x is large enough so that \(p(\textbf{u})\xrightarrow {\rho \sigma ^x}p'(\textbf{m}')\) and \(\textbf{m}' \ge \textbf{m} + \textbf{x}\). By Lemma 5 there exists a narrow linear form for a path \(\tau '\) such that \(p'(\textbf{m}')\xrightarrow {\tau '}q(\textbf{v}'')\) and \(\textbf{v}'' \ge \textbf{v}'\).

We conclude by considering the compressed linear form path \(\rho \sigma ^x \tau '\) such that \(p(\textbf{u})\xrightarrow {\rho \sigma ^x \tau '}q(\textbf{v}'')\) and \(\textbf{v}'' \ge \textbf{v}' \ge \textbf{v}\). Since \(\rho \), \(\sigma \), and \(\tau '\) have narrow linear forms, we can also bound the exponents using Lemma 6 as in the beginning of this proof. Finally, \(\textrm{bitsize}(x)\) is polynomial in \(|V | + \textrm{bitsize}(\textbf{u}) + \textrm{bitsize}(\textbf{v})\) much like the exponents of the cycles in the linear forms. Therefore, the size of the compressed linear form \(\rho \sigma ^x \tau '\) is polynomial in \(|V | + \textrm{bitsize}(\textbf{u}) + \textrm{bitsize}(\textbf{v})\).    \(\square \)

7 Conclusion and Future Work

In this paper we proved that coverability in 2-VASS with one unary counter is in NP, a drop in complexity from PSPACE for general 2-VASS. We achieve this by using our new techniques. Most notably, we polynomially bounded the number of short cycles that need to be used (Section 4). Then, we attempt to find a polynomial linear form path by replacing short cycles and reshuffling the path (Section 5).

A natural extension is to consider whether coverability in 3-VASS with one binary counter and two unary counters is also in NP. More generally, there is the problem of determining the complexity of coverability in k-VASS with one binary counter and \(k-1\) unary counters. The technique for polynomially bounding the number of short cycles that need be used can easily be generalised to these higher dimension VASS with only one binary counter. However, it is not clear how to modify and use our reshuffling technique. Another open problem is whether reachability in 2-VASS with one unary counter is also in NP. Note that completeness would immediately follow from the fact that reachability in binary encoded 1-VASS is NP-hard [22].