Coverability in 1-VASS with Disequality Tests

TL;DR

This paper investigates the coverability problem in 1-dimensional VASS with disequality tests, showing it is solvable in polynomial time, extending previous results on reachability in weighted graphs.

Contribution

It generalizes the control-state reachability problem to include disequality constraints, proving polynomial-time solvability for 1-VASS with these tests.

Findings

Coverability in 1-VASS with disequality tests is in P.

The problem remains solvable despite exponential shortest paths.

The work extends known complexity results for VASS reachability.

Abstract

We study a class of reachability problems in weighted graphs with constraints on the accumulated weight of paths. The problems we study can equivalently be formulated in the model of vector addition systems with states (VASS). We consider a version of the vertex-to-vertex reachability problem in which the accumulated weight of a path is required always to be non-negative. This is equivalent to the so-called control-state reachability problem (also called the coverability problem) for 1-dimensional VASS. We show that this problem lies in NC: the class of problems solvable in polylogarithmic parallel time. In our main result we generalise the problem to allow disequality constraints on edges (i.e., we allow edges to be disabled if the accumulated weight is equal to a specific value). We show that in this case the vertex-to-vertex reachability problem is solvable in polynomial time even though a shortest path may have exponential length. In the language of VASS this means that control-state reachability is in polynomial time for 1-dimensional VASS with disequality tests.

Figures

Equations

$$\pi ={\pi }_0\cdot {\gamma }_{q_1}^{n_1}\cdot {\pi }_1\cdots {\pi }_{k-1}\cdot {\gamma }_{q_k}^{n_k}\cdot {\pi }_k,$$

$${\delta }_n(C):=\{(q,x)\in {Conf}_{+}:m_1\le x\le m_2\text{ and }(q,x)\notin U_n\}.$$

$${\delta }_n(R):=\bigcup \left\{{\delta }_n(C):\text{C⊆R an n-active chain}\right\}.$$

$$z_0+W_q\cdot c+\mathrm{weight}({\pi }^{\prime })\equiv z_0+\mathrm{weight}({\pi }^{\prime })(\mathrm{mod}{W}_{q^{\prime }}).$$

$$\left\{(q,x)\in {\delta }_{n+1}(C)|x\in \left(x_{\max }^{(s)},x_{\max }\right]\cup \left[x_{\min },x_{\min }^{(1)}\right)\cup \bigcup _{i=1}^{s-1}\left(x_{\max }^{(i)},x_{\min }^{(i+1)}\right)\right\}$$

$$O=\left\{(q_f,x)\mid x\ge \ell \wedge \underset{i=1}{\overset{m}{\bigwedge }}(x\not\equiv a_i\mathrm{mod}W)\wedge \underset{i=1}{\overset{n}{\bigwedge }}(x\ne b_i)\right\},$$

$$P:=\{{\pi }_1\cdot {\pi }_2:\exists r\in Q({\pi }_1\in P_{p,r,k}\wedge {\pi }_2\in P_{r,q,k})\}$$

$${\mathrm{pol}{\mathrm{y}}^{\prime }}_7(|Q|)\ge |Q{|}^2+|Q|+3+\sum _{R\text{ non-trivial}}|{\delta }_n(R)|$$

$$\mathrm{pmin}({\pi }_1\cdot {\pi }_2)$$

Full text

Coverability in 1-VASS with Disequality Tests

Shaull Almagor

  

Nathann Cohen

  

Guillermo A. Pérez

  

Mahsa Shirmohammadi

  

James Worrell

1 Introduction

In this paper we study reachability problems in weighted graphs with constraints on the accumulated weight along a path. We show that the vertex-to-vertex reachability problem is in \NC if the constraint is that the accumulated weight must always be non-negative, and the problem is in polynomial time if we additonally allow disequality constraints on edges (i.e., constraints that prevent an edge from being taken in a path if the accumulated weight prior to taking the edge is equal to a specific value). In both cases a shortest path satisfying the constraints may have length exponential in the problem description. Several related problems have been studied in the literature, including the problem of finding a path from a source vertex to target vertex that has a specific total weight [12].

The problems we study can naturally be formalised as reachability problems for types of one-counter machines, and the majority of the related work has been presented in this context. Under this correspondence, the value of the counter represents the accumulated weight along a path, and tests on the counter encode constraints on allowable paths. Algorithmic properties of one-counter machines have been studied by many authors over several decades [2, 4, 6, 7, 8, 9, 10, 11]. The above references are a small subset of the extensive literature on one-counter machines, but they well illustrate that there are many variations on the basic model and that these variations can lead to the model having substantially different algorithmic properties. Particular features mentioned in the references above, driven by applications to automated verification and program analysis, include equality tests, disequality tests, inequality tests, parametric tests, binary updates, polynomial updates, and parametric updates.

Analysing the complexity of reachability in the presence of the features listed above leads to a rich complexity landscape. It is shown in [11] that control-state reachability is decidable in \NL for a “plain vanilla” model of one-counters machine—namely with a counter taking values in the nonnegative integers with operations increment, decrement, and zero testing. Thinking of one-counter machines as one-dimensional vector addition systems with states (1-VASS), it is natural to allow the counter to be updated by adding integer constants in binary. In this case, still with equality tests, control-state reachability becomes \NP-complete [10]. The \NP upper bound here is non-trivial since, due to the binary encoding of integers, a computation that reaches the goal state may have length exponential in the size of the machine. If one enriches the model further by introducing inequality tests (comparing the counter with an integer constant) then control-state reachability becomes \PSPACE-complete [7]. A model of intermediate complexity is one with equality and disequality tests (introduced in [6], with applications to temporal-logic model checking). In this case the complexity of control-state reachability is open (between \NP and \PSPACE).

In this paper we consider 1-VASS with disequality tests, but no equality tests. In terms of 1-VASS, our main result states that the control-state reachability problem is solvable in polynomial time for 1-VASS with disequality tests. This result confirms the intuition that disequality tests are weaker than equality tests. The main technical challenge to obtaining a polynomial-time bound is that a run witnessing that a given control state is reachable may have length exponential in the description of the counter machine. A standard way to overcome this obstacle in related settings is to show that one may restrict attention to computations that fit a regular pattern (usually in terms of iterating a “small” number of cycles). Here the presence of disequality tests proves to be surprisingly disruptive: it destroys the monotonicity of the transition relation and prevents from freely iterating positive-weight cycles. (For example, the lack of monotonicity means that it is \coNP hard to determine whether, given a control state $s_{0}$, for all counter values $u\in\mathbb{N}$ the configuration $(s_{0},u)$ is unbounded, i.e., can reach infinitely many configurations—see Figure 1—whereas the same problem for 1-VASS without tests is easily seen to be decidable in polynomial time.) Resolving the complexity of reachability for 1-VASS with both equality and disequality tests remains open. We hope that the techniques developed here can help solve this challenging problem.

To complement our main result, we show that for 1-VASS without tests control-state reachability (and hence also boundedness) is decidable in \NC, i.e., the subclass of ¶ consisting of problems solvable in polylogarithmic parallel time. Problems in \NC are in particular solvable in polylogarithmic space. Related to this, Rosier and Yen [16] have shown that boundedness for VASS is \NL-complete in case there are absolute bounds on the dimension and bit-size of integer vectors.

2 Definitions

We write $\mathbb{N}$ to denote the set of all nonnegative integers $0,1,2,\dots$ In presenting our results we assume familiarity of the reader with basic graph theory and computational complexity.

One-Dimensional Vector Addition Systems with States and Tests.

A 1-VASS with disequality tests is a tuple $\mathcal{V}=(Q,D,\Delta,w)$, where $Q$ is a set of states, $D=\{D_{q}\}_{q\in Q}$ is a collection of cofinite subsets $D_{q}\subseteq\mathbb{N}$, $\Delta\subseteq Q\times Q$ is a set of transitions, and $w:\Delta\rightarrow\mathbb{Z}$ is a function that assigns an integer weight to each transition. In the special case that each $D_{q}$ equals $\mathbb{N}$, we simply call $\mathcal{V}$ a 1-VASS (and we omit the collection $D$).

A configuration of $\mathcal{V}$ is a pair $(q,z)$ comprising a state $q\in Q$ and a nonnegative integer $z\in\mathbb{N}$ referred to as the counter value. We write $\mathit{Conf}$ for the set $Q\times\mathbb{N}$ of all configurations. We define a partial order on $\mathit{Conf}$ by $(q,z)\leq(q^{\prime},z^{\prime})$ if and only if $q=q^{\prime}$ and $z\leq z^{\prime}$. A configuration $(q,z)$ is valid if $z\in D_{q}$.

A path in $\mathcal{V}$ is a sequence of states $\pi=q_{1},\ldots,q_{n}$ such that $(q_{i},q_{i+1})\in\Delta$ for all $i\in\{1,\ldots,n-1\}$. We sometimes refer to such a path as a $q_{1}$-$q_{n}$ path. Let $\pi^{\prime}=p_{1},p_{2},\ldots,p_{m}$ be another path such that $q_{n}=p_{1}$, we define $\pi_{1}\cdot\pi_{2}:=q_{1},\ldots,q_{n},p_{2},\ldots,p_{m}$. Given states $p,q,r$, a set $P$ of $p$-$q$ paths, and a set $R$ of $q$-$r$ paths, we define $P\cdot R:=\{\pi\cdot\pi^{\prime}\mid\pi\in P,\pi^{\prime}\in R\}$. The weight of $\pi$ is defined to be $\mathrm{weight}(\pi):=\sum_{i=1}^{n-1}w(q_{i},q_{i+1})$. A (possibly empty) prefix of $\pi$ is said to be minimal if it has minimal weight among all prefixes of $\pi$. Define $\mathrm{pmin}(\pi)$ to be the weight of a minimal prefix of $\pi$.

A run is a sequence $(q_{1},z_{1}),\ldots,(q_{n},z_{n})$ of configurations of $\mathcal{V}$ such that there is a path $\pi=q_{1},\ldots,q_{n}$ with $z_{i+1}=z_{i}+w(q_{i},q_{i+1})$ for $i=1,\ldots,n-1$. We write $(q_{1},z_{1})\stackrel{{\scriptstyle\pi}}{{\rightarrow}}(q_{n},z_{n})$ to denote such a run. Observe that runs are not allowed to reach negative counter values. A valid run is a run whose configurations are all valid. Intuitively, a valid run through $q$ can proceed if and only if the current counter value is in $D_{q}$. We say that a configuration $(q^{\prime},z^{\prime})$ is reachable from $(q,z)$ if there is a valid run $\pi$ such that $(q,z)\stackrel{{\scriptstyle\pi}}{{\rightarrow}}(q^{\prime},z^{\prime})$.

In computational problems all numbers in the description of $\mathcal{V}$ are given in binary. Given a state $q$ we represent the cofinite set $D_{q}$ as the complement of an explicitly given subset of $\mathbb{N}$. Given this convention, we can assume without loss of generality that for all states $q$ the set $D_{q}$ is either $\mathbb{N}$ or $\mathbb{N}\setminus\{g\}$ for some $g\in\mathbb{N}$; see Appendix B. For states $q$ with $D_{q}=\mathbb{N}\setminus\{g\}$, we refer to the single missing value $g$ in the domain as the disequality guard on $q$.

The Coverability and Unboundedness Problems.

Let $\mathcal{V}=(Q,\Delta,D,w)$ be a 1-VASS with disequality tests, and let $s$ and $t$ be two distinguished states of $\mathcal{V}$. The Coverability Problem asks whether there exists a valid run in $\mathcal{V}$ from $(s,0)$ to $(t,z)$ for some $z\in\mathbb{N}$ (in which case we say that $(s,0)$ can cover $t$). The Unboundedness Problem asks whether the set of configurations reachable from $(s,0)$ is infinite (in which case we say that $(s,0)$ is unbounded).

The Coverability problem reduces to the Unboundedness problem by, intuitively, forcing $(t,0)$ to be unbounded using a positive cycle, and removing all states that cannot reach $t$ in the underlying graph of $\mathcal{V}$. In fact, the following holds.

Lemma 2.1**.**

There is an $\NC^{2}$-computable many-one reduction from the Coverability Problem to the Unboundedness Problem.

Henceforth, we focus on the complexity of deciding the Unboundedness Problem. In Section 3 we prove that the Unboundedness Problem for 1-VASS with disequality tests is decidable in polynomial time. Since $\NC^{2}\subseteq\P$, by Lemma 2.1 we also have that the Coverability Problem in this setting is decidable in polynomial time. In Section 4 we prove that the Unboundedness Problem for 1-VASS (without disequality tests) is in $\NC^{2}$, and we deduce that the Coverability Problem for 1-VASS is decidable in $\NC^{2}$.

3 Unboundedness for 1-VASS with Disequality Tests

Fix a $1$-VASS $\mathcal{V}=(Q,D,\Delta,w)$ with disequality tests and a distinguished state $s\in Q$. We are interested in determining whether the configuration $(s,0)$ is unbounded.

For a (possibly infinite) path $\pi=q_{1},q_{2},\ldots$, denote by $\mathrm{blocked}(\pi)$ the set of $z\in\mathbb{N}$ such that the unique induced run from $(q,z)$ either contains a negative counter value or violates a disequality guard. That is, $\pi$ does not lift to a valid run from the configuration $(q_{1},z)$.

Example 3.1**.**

In Figure 2, since $41$ is the guard on $s_{5}$ the run $(s_{4},93),(s_{5},41),(s_{6},93)$ is not valid and $93\in\mathrm{blocked}(s_{4},s_{5},s_{6})$. Observe that $\mathrm{blocked}(s_{4},s_{5},s_{6})=[0,52)\cup\{90,93,96\}$ and $\mathrm{blocked}((s_{4},s_{5},s_{6})^{\omega})=[0,52)\cup\{52\leq z\leq 96\mid z\equiv 0,3,6\pmod{9}\}$.

Recall that for a path $\pi$, $\mathrm{pmin}(\pi)$ is the weight of a minimum-weight prefix of $\pi$. Let $Q_{+}\subseteq Q$ be the set of states $q\in Q$ such that there is a positive-weight simple cycle on $q$ in the underlying graph of $\mathcal{V}$. For $q\in Q_{+}$ we pick a simple cycle $\gamma_{q}$ such that $\mathrm{pmin}(\gamma_{q})\geq\mathrm{pmin}(\gamma)$ for any other positive-weight simple cycle $\gamma$ on $q$; write $W_{q}$ for $\mathrm{weight}(\gamma_{q})$.111Note that $\gamma_{q}$ does not necessarily have maximal weight $W_{q}$ among the positive simple cycles on $q$. Define $\mathit{Conf}_{+}:=\{(q,z)\in\mathit{Conf}\mid q\in Q_{+},\,{z+\mathrm{pmin}(\gamma_{q})}\geq 0\}$.

Define a path to be primitive if no proper infix is a positive cycle (note though that a primitive path may itself be a positive cycle). We say that a run is primitive if the underlying path is primitive. Observe that if $\rho$ is a valid run, none of whose internal configurations (i.e. excluding the first and last configurations) lies in $\mathit{Conf}_{+}$, then $\rho$ is primitive.

Example 3.2**.**

In Figure 2, for $s_{1}\in Q_{+}$ we pick the simple cycle $\gamma_{s_{1}}=s_{1},s_{2},s_{1}$ with $W_{s_{1}}=6$. Since $\mathrm{pmin}(\gamma_{s_{1}})=-12$, we have that $\{z\mid(s_{1},z)\in\mathit{Conf}_{+}\}=[12,\infty)$. Moreover, the path $s_{4},s_{5},s_{6},s_{4}$ is primitive, but $s_{1},s_{2},s_{1},s_{3}$ is not primitive.

Proposition 3.3**.**

A configuration $(s,0)$ is unbounded if, and only if, $(s,0)$ can reach an unbounded configuration in $\mathit{Conf}_{+}$.

In order to decide whether $(s,0)$ is unbounded, by Proposition 3.3, it suffices to compute the set of unbounded configurations in $\mathit{Conf}_{+}$ and determine whether $(s,0)$ can reach this set. Define $\mathit{Conf}_{\infty}\subseteq\mathit{Conf}_{+}$ to be the set of all unbounded configurations in $\mathit{Conf}_{+}$. Observe that every configuration $(q,z)\in\mathit{Conf}_{+}$ with $z\notin\mathrm{blocked}(\gamma_{q}^{\omega})$ can take the cycle $\gamma_{q}$ arbitrarily many times and is thus included in $\mathit{Conf}_{\infty}$. However, even if $z\in\mathrm{blocked}(\gamma_{q}^{\omega})$, it may still be the case that $(q,z)$ is unbounded, by traversing more complicated paths.

Example 3.4**.**

In Figure 2, all configurations $(s_{4},z)$ with $z$ in $\mathbb{N}\setminus\mathrm{blocked}((s_{4},s_{5},s_{6})^{\omega})=\{52\leq z\leq 96\mid z\not\equiv 0,3,6\pmod{9}\}\cup(96,\infty)$ are trivially unbounded and thus included in $\mathit{Conf}_{\infty}$. It will transpire that $\{s_{4}\}\times\{54,60,63,69\}\subseteq\mathit{Conf}_{\infty}$ even though $\{54,60,63,69\}\in\mathrm{blocked}((s_{4},s_{5},s_{6})^{\omega})$.

In order to reason about the aforementioned complicated paths, we proceed as follows. In Section 3.1 we introduce residue classes and chains, which form a partition of $\mathit{Conf}_{+}$, and are the building blocks of our analysis. In Section 3.2 we characterize $\mathit{Conf}_{\infty}$ as the limit of an inductive construction. This enables us to reason about the structure of $\mathit{Conf}_{\infty}$ in Section 3.3. Finally, in Section 3.4 we show how to compute $\mathit{Conf}_{\infty}$ and decide unboundedness.

3.1 Residue Classes and Chains

Given $q\in Q_{+}$ and $0\leq r<W_{q}$, we call the set of configurations $\{(q,z)\in\mathit{Conf}_{+}\mid z\equiv r\pmod{W_{q}}\}$ a $q$-residue class. We simply speak of a residue class if we do not want to specify the state $q$. Given a $q$-residue class $R$, a set $C\subseteq R$ is called a $q$-chain if it is a maximal subset of $R$ for the property that every pair of configurations $(q,z),(q,z^{\prime})\in C$ with $z<z^{\prime}$ is connected by a valid run obtained by iterating the cycle $\gamma_{q}$. Again, we speak of a chain if we do not want to specify the state $q$.

We draw a distinction between bounded chains and unbounded chains, where a chain is bounded if and only if the associated set of counter values is bounded. An unbounded $q$-chain $C$ is contained in $\mathit{Conf}_{\infty}$ since the cycle $\gamma_{q}$ can be taken arbitrarily many times from any configuration in $C$ to yield a valid run.

Remark 3.5**.**

Let us write $\gamma_{q}=q_{1},q_{2},\dots$ For each $q_{1}$-residue class $R$, every $z$ such that $z+\mathrm{weight}(q_{1},\dots,q_{i})\not\in D_{q_{i}}$, for some $q_{i}$, induces at most two bounded chains. Namely, the set of configurations below $(q,z)$ form a chain; and the singleton ${\{(q,z)\}}$ is also (vacuously) a chain. Note that every residue class also has one unbounded chain. That is, the set of configurations above $(q,z)$ with $z$ the maximal “induced guard” on $q$. Since there are at most $|Q|$ guards, each residue class decomposes as a disjoint union of at most $2\lvert Q\rvert$ bounded chains and a single unbounded chain.

Intuitively, within each bounded chain we can iterate the cycle $\gamma_{q}$ until hitting a guard. We call a residue class $R$ trivial if it consists solely of a single unbounded chain. Note that the union of all bounded $q$-chains is equal to $\mathit{Conf}_{+}\cap\{q\}\times\mathrm{blocked}(\gamma_{q}^{\omega})$.

Example 3.6**.**

As indicated in Figure 3 for the running example, the residue classes $\{s_{4}\}\times(52+i+9{\mathbb{N}})$ with $i\in\{0,1,3,4,6,7\}$ are indeed trivial, while each residue class $\{s_{4}\}\times(52+i+9{\mathbb{N}})$ with $i\in\{2,5,8\}$ consists of two bounded chains $\{s_{4}\}\times\{52\leq z<88+i\mid z\equiv i\pmod{9}\}$ and $\{s_{4}\}\times\{88+i\}$, and a single unbounded chain $\{s_{4}\}\times(88+i+9{\mathbb{N}})$.

One of the main ideas in this section is to show that a configuration is unbounded if and only if it can reach an unbounded chain via a valid run whose underlying path $\pi$ has the form

[TABLE]

where $\pi_{0},\ldots,\pi_{k}$ are primitive paths and $n_{1},\ldots,n_{k}$ are non-negative integers. Moreover, we give a polynomial bound on the length of the $\pi_{i}$ and the magnitude of $k$ in terms of the size of the underlying 1-VASS (in general, the exponents $n_{i}$ may be exponential in the size of the 1-VASS). We also show how to detect the existence of such a path in polynomial time.

Recall the structure of $\mathit{Conf}$ as a partially ordered set. We will use standard order-theoretic terminology and notation to refer to sets of configurations: in particular given sets of configurations $S,S^{\prime}\subseteq\mathit{Conf}$, we say that $S$ is downward closed in $S^{\prime}$ if for all $(q,z)\in S\cap S^{\prime}$ and $(q,z^{\prime})\in S^{\prime}$ with $z^{\prime}\leq z$, we have $(q,z^{\prime})\in S$.

3.2 Inductive Characterization of $\mathit{Conf}_{\infty}$

We now give an inductive backward-reachability construction of the set of all configurations in $\mathit{Conf}_{+}$ that can reach an unbounded chain. Since unbounded configurations can, in particular, reach unbounded chains (as above the maximal disequality guard, all chains are unbounded), this set is exactly $\mathit{Conf}_{\infty}$.

In order for our inductive construction to converge in a polynomial number of steps, we essentially consider meta-transitions of the form $\gamma_{q}^{k}\cdot\pi$ for $\gamma_{q}$ a simple cycle, $k\in\mathbb{N}$, and $\pi$ a primitive path. Formally, we define an increasing sequence $U_{0}\subseteq U_{1}\subseteq U_{2}\subseteq\cdots$ of subsets of $\mathit{Conf}_{+}$ such that $\bigcup_{n\in\mathbb{N}}U_{n}=\mathit{Conf}_{\infty}$. Define $U_{0}$ to be the union of the collection of unbounded chains. Given $n\in\mathbb{N}$ we inductively construct $U_{n+1}$ as follows. First, define $U_{n}^{\prime}\subseteq\mathit{Conf}_{+}$ as the set of configurations $(q,z)\not\in U_{n}$ whose distance to $U_{n}$ is minimal among all configurations in $\mathit{Conf}_{+}\setminus U_{n}$ (here the distance of a configuration $(q,z)$ to $U_{n}$ is the length of the shortest valid run from $(q,z)$ to $U_{n}$). Now define $U_{n+1}\subseteq\mathit{Conf}_{+}$ to be the smallest set such that $U_{n},U_{n}^{\prime}\subseteq U_{n+1}$ and $U_{n+1}\cap C$ is downward closed in every chain $C$. Then $\bigcup_{n\in\mathbb{N}}U_{n}$ is the set of configurations in $\mathit{Conf}_{+}$ that can reach an unbounded chain which, as noted above, is equal to $\mathit{Conf}_{\infty}$.

Remark 3.7**.**

By definition, a shortest run from a configuration $(q,z)\in U^{\prime}_{n+1}\setminus U_{n}$ to $U_{n}$ has no internal configurations in $\mathit{Conf}_{+}$, and is therefore primitive.

Example 3.8**.**

Figure 3 indicates the set $U_{0}$ for the running example. Note that $U_{0}$ contains all trivial residue classes. Observe that $U^{\prime}_{0}=\{(s_{4},63),(s_{4},69)\}$; see Figure 4(a). These two configurations belong to two distinct chains. The downward closure of $\{(s_{4},63)\}$ in its chain is $\{s_{4}\}\times\{54,63\}$, and the downward closure of $\{(s_{4},69)\}$ in its chain is $\{s_{4}\}\times\{60,69\}$. We have that $U_{1}=U_{0}\cup(\{s_{4}\}\times\{54,60,63,69\})$. The second iteration to compute $U_{2}$ only adds the configuration $(s_{1},12)$ to $U_{1}$; see Figure 4(b). The sequence stabilizes in this iteration.

3.3 The Structure of $\mathit{Conf}_{\infty}$

In this section we analyze the structure of $\mathit{Conf}_{\infty}$, based on its inductive characterization. This analysis will be key in obtaining a polynomial-time algorithm to compute $\mathit{Conf}_{\infty}$.

The guiding intuition is that for all $n$ the set $U_{n}$ is almost upward closed in each residue class $R$. By this we mean that if $(q,z)$ is the least configuration in $R\cap U_{n}$, then all but polynomially many configurations of $R$ above $(q,z)$ are also in $U_{n}$. More specifically, we show that for any bounded chain $C$ in $R$ that lies above $(q,z)$, although the number of configurations in $C$ may be exponential in $\lvert Q\rvert$, the size of $C\setminus U_{n}$ is bounded by a polynomial in $\lvert Q\rvert$. (Note here that the unique unbounded chain in $R$ is contained in $U_{0}$ and hence is contained in $U_{n}$ for all $n\in{\mathbb{N}}$.) Using this observation, we provide a polynomial bound on the number of iterations until the inductive construction converges. Indeed, in every iteration, unless a fixed point has been reached, there must exist some bounded chain $C$ such that the size of $C\setminus U_{n}$ strictly decreases. After showing that $C\setminus U_{n}$ is of polynomial size, we obtain a polynomial bound on the number of iterations until $U_{n}$ converges by Remark 3.5.

We start by characterizing the paths between chains.

Proposition 3.9**.**

Let $(q,z),(q^{\prime},z^{\prime})\in\mathit{Conf}_{+}$ and let $(q,z)\stackrel{{\scriptstyle\pi}}{{\rightarrow}}(q^{\prime},z^{\prime})$ be a (not necessarily valid) run such that $\pi$ is a primitive path. Then there exists a run $(q,z)\stackrel{{\scriptstyle\pi^{\prime}}}{{\rightarrow}}(q^{\prime},z^{\prime\prime})$ of length at most $\lvert Q\rvert^{2}+2$ such that

$\mathrm{pmin}(\pi^{\prime})\geq\mathrm{pmin}(\pi)$, 2. 2.

$z^{\prime\prime}\geq z^{\prime}$, and 3. 3.

the $q^{\prime}$-residue class of $(q^{\prime},z^{\prime\prime})$ is either trivial or identical to that of $(q^{\prime},z^{\prime})$.

Given a $q$-residue class $R$, in general $U_{n}$ is not an upward closed subset of $R$. The following definitions are intended to measure the defect of $U_{n}$ in this regard.

We say that a bounded chain $C$ that is contained in a residue class $R$ is $n$-active if there exists a configuration in $U_{n}\cap R$ that lies below some configuration in $C$. Let $C$ be an $n$-active chain. Recall that $U_{n}$ is downward closed in $C$ and hence $C\setminus U_{n}$ is upward closed in $C$. Suppose that $C\setminus U_{n}$ is non-empty, write $m_{1}:=\min\{x:(q,x)\in C\setminus U_{n}\}$ and $m_{2}:=\max\{x:(q,x)\in C\setminus U_{n}\}$, and define222We omit $q$ from the definition of $\delta_{n}(C)$ for brevity.

[TABLE]

Thus $\delta_{n}(C)$ contains all configurations in $C\setminus U_{n}$, as well as all configurations “between” elements of $C\setminus U_{n}$, apart from those that are themselves in $U_{n}$. If $C\setminus U_{n}=\emptyset$ then we define $\delta_{n}(C):=\emptyset$. Finally for a residue class $R$ we write

[TABLE]

For $(q,x_{\min})$ the least element in $R\cap U_{n}$ we have that $\lvert\{(q,x)\in R\setminus U_{n}:x_{\min}\leq x\}\rvert\leq\lvert\delta_{n}(R)\rvert$.

Example 3.10**.**

In Figure 4(a) consider the chain $C:=\{s_{4}\}\times\{54,63,72,81\}$, which is $1$-active as $(s_{4},54)\in U_{1}$. Since $C\setminus U_{1}=\{s_{4}\}\times\{72,81\}$ we have that $\delta_{1}(C)=\{s_{4}\}\times\{72,75,78,81\}$.

Lemma 3.11**.**

For all $n\in{\mathbb{N}}$ and every chain $C$ we have that $|\delta_{n}(C)|\leq|Q|\cdot|C\setminus U_{n}|$.

We now come to the central technical part of the paper, controlling the growth of $\delta_{n}(R)$ as a function of $n$:

Lemma 3.12**.**

There exists a polynomial $\mathrm{poly}_{2}$ such that for each residue class $R$ and all $n\in\mathbb{N}$ we have $\lvert\delta_{n+1}(R)\rvert\leq\max\{\lvert\delta_{n}(R^{\prime})\rvert:R^{\prime}\text{ a residue class}\}+\mathrm{poly}_{2}(\lvert Q\rvert)$ if $R$ contains a chain that is $(n+1)$-active but not $n$-active.

Before proceeding to prove Lemma 3.12, we demonstrate the underlying intuition. Consider a configuration $(q,z)\in R\cap U^{\prime}_{n+1}$ that has a primitive path $\pi$ to a configuration $(q^{\prime},z^{\prime})\in U_{n}$. To prove Lemma 3.12, we argue that $\pi$ lifts to a valid run from a “dense” subset of configurations in $\{(q,z^{\prime\prime})\in R:z^{\prime\prime}\geq z\}$. There are two main cases in this argument based on whether one of the larger configurations in the chain induces a valid run ending in a trivial residue class.

Example 3.13**.**

The first case occurs in obtaining $U_{1}$ from $U_{0}$ in the running example; see Figure 4(a). Consider the chain $C:=\{s_{4}\}\times\{54,63,72,81\}$. The primitive path $s_{4},s_{7},s_{8},s_{9},s_{10}$ from the largest configuration $(s_{4},81)$ in $C$ leads to a non-trivial $s_{10}$-residue class (out of $U_{0}$). However, one among the $n$-next largest configurations in $C$, for $n=\lvert\mathrm{blocked}(s_{4},s_{7},s_{8},s_{9},s_{10})\rvert\cdot\lvert Q\rvert$, lifts to a valid run to a trivial $s_{10}$-residue class. In the example, this is the case for $(s_{4},63)$. The second case occurs in obtaining $U_{2}$ from $U_{1}$ in the running example; see Figure 4(b). Consider the chain $C^{\prime}:=\{s_{1}\}\times\{12,18,24,\cdots,54\}$. The primitive path $s_{1},s_{3},s_{4}$, from none of the configurations in this chain, ends in a trivial $s_{4}$-residue class. However, we provide a subtle argument to bound $\lvert C^{\prime}\setminus U_{2}\rvert$ with $\lvert\delta_{1}(C)\rvert+\mathrm{poly}_{2}(\lvert Q\rvert)$.

Proof 3.14** (Proof of Lemma 3.12).**

Pick the minimal element $(q,z_{0})\in R\cap U^{\prime}_{n+1}$. Moreover, let $(q^{\prime},z^{\prime})\in U_{n}$ and $(q,z_{0})\stackrel{{\scriptstyle\pi}}{{\rightarrow}}(q^{\prime},z^{\prime})$ be such that $\pi$ is a shortest run from $(q,z_{0})$ to $U_{n}$. By Remark 3.7, $\pi$ is a primitive path.

By Proposition 3.9 there is a run $(q,z_{0})\stackrel{{\scriptstyle\pi^{\prime}}}{{\rightarrow}}(q^{\prime},z^{\prime\prime})$, for some $z^{\prime\prime}\geq z^{\prime}$, such that $\pi^{\prime}$ has length at most $\lvert Q\rvert^{2}+2$, and the residue class $R^{\prime}$ of $(q^{\prime},z^{\prime\prime})$ is either trivial or the same as the residue class of $(q^{\prime},z^{\prime})$.

Note that we do not claim that $(q^{\prime},z^{\prime\prime})\in U_{n}$, nor that $\pi^{\prime}$ lifts to a valid run. In what follows we will argue that if there are more than some polynomial number of configurations above $(q,z_{0})$ in $C\setminus U^{\prime}_{n+1}$, where $C$ is an $(n+1)$-active chain of $R$, then $\pi^{\prime}$ does lift to a valid run from one of them. Moreover, the run leads to some configuration in the same residue class as $(q^{\prime},z^{\prime})$ or to a trivial residue class. Observe that, intuitively, this means we “pump” $\gamma_{q}$ before taking $\pi^{\prime}$ so if we wanted to reach the same residue class as $(q^{\prime},z^{\prime})$ we would need some nonnegative integer $c$ such that

[TABLE]

Based on this intuition, we now identify two cases according to the order of $W_{q}$ in the group $\mathbb{Z}/\mathbb{Z}W_{q^{\prime}}$ of integers modulo $W_{q^{\prime}}$, which is $\frac{W_{q^{\prime}}}{\gcd(W_{q},W_{q^{\prime}})}$. Recall that this quantity is the smallest integer $c\geq 1$ such that $W_{q}\cdot c\equiv 0\pmod{W_{q^{\prime}}}$.

Case (i):

$\frac{W_{q^{\prime}}}{\gcd(W_{q},W_{q^{\prime}})}>\lvert Q\rvert$. We first show that $\lvert C\setminus U_{n+1}\rvert\leq(\lvert Q\rvert^{2}+2)(\lvert Q\rvert+1)$ for every $(n+1)$-active chain $C$ in $R$.

Let $C$ be an $(n+1)$-active chain of $R$ and suppose for a contradiction that $\lvert C\setminus U_{n+1}\rvert>(\lvert Q\rvert^{2}+2)(\lvert Q\rvert+1)$. Since $C$ is $(n+1)$-active, for every configuration $(q,z)\in C\setminus U_{n+1}$ we have $z\geq z_{0}$. Further, since $\mathrm{pmin}(\pi^{\prime})+z_{0}\geq 0$, $\pi^{\prime}$ can only be blocked on a configuration due to a violation of a disequality guard. Since the length of $\pi^{\prime}$ is at most $|Q|^{2}+2$, it follows that at most $\lvert Q\rvert^{2}+2$ elements of $C\setminus U_{n+1}$ lie in $\{q\}\times\mathrm{blocked}(\pi^{\prime})$.

Recall that $C\setminus U_{n+1}$ is upward closed in $C$, so by the assumption that $\lvert C\setminus U_{n+1}\rvert>(\lvert Q\rvert^{2}+2)(\lvert Q\rvert+1)$, there exists a set $S:=\{(q,z_{1}+iW_{q}):0\leq i\leq\lvert Q\rvert\}$ of $\lvert Q\rvert+1$ “consecutive” elements of $C\setminus U_{n+1}$, for some $z_{1}$, such that no element of $S$ lies in $\{q\}\times\mathrm{blocked}(\pi^{\prime})$. Then $\pi^{\prime}$ lifts to a valid run from each element of $S$. Moreover, since the order of $W_{q}$ in $\mathbb{Z}/\mathbb{Z}W_{q^{\prime}}$ is assumed to be greater than $\lvert Q\rvert$, the images of the elements of $S$, after following $\pi^{\prime}$, lie in pairwise distinct $q^{\prime}$-residue classes. But the number of non-trivial $q^{\prime}$-residue classes is at most $\lvert Q\rvert$ and hence some configuration in $S$ has a run over $\pi^{\prime}$ to a trivial $q^{\prime}$-residue class and hence to $U_{n}$. But then such a configuration lies in $U_{n+1}$, which is a contradiction.

We conclude that $\lvert C\setminus U_{n+1}\rvert\leq(\lvert Q\rvert^{2}+2)(\lvert Q\rvert+1)$ for every $(n+1)$-active chain $C$ in $R$. But then $|\delta_{n+1}(C)|\leq\lvert Q\rvert(\lvert Q\rvert^{2}+2)(\lvert Q\rvert+1)$ by Lemma 3.11. Finally, since $R$ comprises at most $2\lvert Q\rvert$ bounded chains by Remark 3.5, we have that $\lvert\delta_{n+1}(R)\rvert\leq 2\lvert Q\rvert^{2}(\lvert Q\rvert^{2}+2)(\lvert Q\rvert+1)$.

Case (ii):

$\frac{W_{q^{\prime}}}{\gcd(W_{q},W_{q^{\prime}})}\leq\lvert Q\rvert$. For the residue classes $R$ and $R^{\prime}$ as above, define an injective partial mapping $\Phi:\delta_{n+1}(R)\rightarrow\delta_{n}(R^{\prime})$ by $\Phi(q,x)=(q^{\prime},x^{\prime})$ if and only if $x^{\prime}=x+\mathrm{weight}(\pi^{\prime})$ and $(q^{\prime},x^{\prime})\in\delta_{n}(R^{\prime})$. We will prove that $\Phi$ is defined on all but $\mathrm{poly}_{3}(\lvert Q\rvert)$ many configurations in $\delta_{n+1}(R)$, for some polynomial $\mathrm{poly}_{3}$, thereby showing that $|\delta_{n+1}(R)|\leq|\delta_{n}(R^{\prime})|+\mathrm{poly}_{3}(\lvert Q\rvert)$. To this end, it suffices to show that $\Phi$ is defined on all but $\mathrm{poly}_{4}(\lvert Q\rvert)$ many configurations in $\delta_{n+1}(C)$ for every $(n+1)$-active chain $C$ in $R$, for some polynomial $\mathrm{poly}_{4}$.

Let $C$ be an $(n+1)$-active chain in $R$ and let $C_{1},\ldots,C_{s}$ be a list, given in increasing order, of the chains in $R^{\prime}$ that are mapped into by $\Phi$ from some configuration in $\delta_{n+1}(C)$. Then $C_{1},\ldots,C_{s}$ are all $n$-active (as they are above $(q^{\prime},z^{\prime})\in U_{n}$). For $i\in\{1,\ldots,s\}$, write $(q,x^{(i)}_{\min})$ for the minimum configuration in $\delta_{n+1}(C)$ that is mapped by $\Phi$ to $C_{i}$ and write $(q,x^{(i)}_{\max})$ for the maximum configuration in $\delta_{n+1}(C)$ that is mapped to $C_{i}$. Then for each $i=1,\ldots,s$, every configuration $(q,x)\in\delta_{n+1}(C)$ such that $x^{(i)}_{\min}\leq x\leq x^{(i)}_{\max}$ and $x\not\in\times\mathrm{blocked}(\pi^{\prime})$ is mapped by $\Phi$ to $\delta_{n}(R^{\prime})$. Thus, writing $(q,x_{\max})$ and $(q,x_{\min})$ respectively for maximum and minimum configurations in $\delta_{n+1}(C)$, we have that $\Phi$ is defined on all non-blocked elements of $\delta_{n+1}(C)$ lying outside the set below.

[TABLE]

Since $\mathrm{blocked}(\pi^{\prime})$ contains at most $|Q|^{2}+2$ elements, it remains to prove that the set (2) has polynomial cardinality. We claim its size is at most $(2\lvert Q\rvert+1)\cdot\mathrm{poly}_{5}(\lvert Q\rvert)$, for some polynomial $\mathrm{poly}_{5}$. For this it will suffice to show that any sub-interval $I$ of $\delta_{n+1}(C)$ of the form $\{(q,x)\in\delta_{n+1}(C):a\leq x\leq b\}$, where $a,b\geq x_{\mathrm{min}}$, and such that it does not meet the domain of $\Phi$, has cardinality at most $\mathrm{poly}_{5}(\lvert Q\rvert)$. (Indeed, note that (2) is a union of at most $2\lvert Q\rvert+1$ such intervals since there are at most $2|Q|$ chains in $R$ by Remark 3.5.)

*Let $\mathrm{poly}_{6}(x):=(x^{2}+2)(x+1)+1$. Since $\mathrm{blocked}(\pi^{\prime})$ has cardinality at most $|Q|^{2}+2$, if we take $\mathrm{poly}_{6}(|Q|)$ consecutive elements of $C\setminus U_{n+1}$ then there are at least $\lvert Q\rvert+1$ consecutive elements that lie outside $\{q\}\times\mathrm{blocked}(\pi^{\prime})$ and at least one of these elements—say $(q,x)$—has a valid run over $\pi^{\prime}$ to the residue class $R^{\prime}$ by the assumption that $\frac{W_{q^{\prime}}}{\gcd(W_{q},W_{q^{\prime}})}\leq\lvert Q\rvert$. Since $(q,x)\not\in U_{n+1}$ we have that $(q^{\prime},x+\mathrm{weight}(\pi^{\prime}))\not\in U_{n}$ and hence $(q,x)$ is in the domain of $\Phi$. We conclude that any sequence of at least $\mathrm{poly}_{6}(|Q|)$ consecutive elements of $C\setminus U_{n+1}$ meets the domain of $\Phi$. Hence any sub-interval $I$, as defined above, contains at most $\mathrm{poly}_{6}(|Q|)$ elements of $C\setminus U_{n+1}$ and, by Lemma 3.11, contains at most $\lvert Q\rvert\cdot\mathrm{poly}_{6}(\lvert Q\rvert)$ elements in total. *

Proposition 3.15 follows from Lemma 3.12 by induction, as follows.

Proposition 3.15**.**

There exists a polynomial $\mathrm{poly}_{1}$ such that for each residue class $R$ and all $n\in\mathbb{N}$ we have $|\delta_{n}(R)|\leq\mathrm{poly}_{1}(\lvert Q\rvert)$.

Proof 3.16**.**

Let $\alpha_{n}$ be the number of chains in $\mathit{Conf}_{+}$ that are $n$-active. Since $n$-active chains are by definition bounded, we have that $\alpha_{n}\leq 2\lvert Q\rvert^{2}$ for all $n\in\mathbb{N}$ (see Remark 3.5). We argue by induction on $n$ that $\lvert\delta_{n}(R)\rvert\leq\alpha_{n}\cdot\mathrm{poly}_{2}(\lvert Q\rvert)$ for all $n\in\mathbb{N}$ and all residue classes $R$. We conclude that $\lvert\delta_{n}(R)\rvert\leq 2\lvert Q\rvert^{2}\cdot\mathrm{poly}_{2}(\lvert Q\rvert)$.

The base case is trivial as there are no [math]-active chains and $\delta_{0}(R)$ is empty for all residue classes. The induction step has two cases. First, suppose that $\alpha_{n+1}=\alpha_{n}$, i.e., all chains in $\mathit{Conf}_{+}$ that are $(n+1)$-active were already $n$-active. Since $U_{n}\subseteq U_{n+1}$, we have that $\delta_{n+1}(C)\subseteq\delta_{n}(C)$ for all chains $C$ in $R$. We conclude that $\delta_{n+1}(R)\subseteq\delta_{n}(R)$ and so $\lvert\delta_{n+1}(R)\rvert\leq\lvert\delta_{n}(R)\rvert$. Since $\lvert\delta_{n}(R)\rvert\leq\alpha_{n}\cdot\mathrm{poly}_{2}(\lvert Q\rvert)$ by induction hypothesis, and $\alpha_{n}=\alpha_{n+1}$ we get that $\lvert\delta_{n+1}(R)\rvert\leq\alpha_{n+1}\cdot\mathrm{poly}_{2}(\lvert Q\rvert)$.

The second case is that $\alpha_{n+1}>\alpha_{n}$. Then by Lemma 3.12 we have $\lvert\delta_{n+1}(R)\rvert\leq\max\{\lvert\delta_{n}(R^{\prime})\rvert:R^{\prime}\text{ a residue class}\}+\mathrm{poly}_{2}(\lvert Q\rvert)$. Since the right-hand side of the latter is at most $\leq\alpha_{n}\cdot\mathrm{poly}_{2}(\lvert Q\rvert)+\mathrm{poly}_{2}(\lvert Q\rvert)$, by induction hypothesis, and $\alpha_{n+1}>\alpha_{n}$ we get that $\lvert\delta_{n+1}(R)\rvert\leq\alpha_{n+1}\cdot\mathrm{poly}_{2}(\lvert Q\rvert)$.

Recall that $(U_{n})_{n\in{\mathbb{N}}}$ is a monotone sequence. Furthermore, observe that by the proof of Lemma 3.12 the sequence $|\delta_{n}(R)|$ either strictly decreases, or possible increases if $R$ contains a chain that is $(n+1)$-active but not $n$-active. Since the latter can only take place $|Q|$ times, then $|\delta_{n}(R)|$ can take a polynomial number of distinct values before converging. Thus, as a consequence of Proposition 3.15 we have:

Corollary 3.17**.**

The sequence $(U_{n})_{n\in\mathbb{N}}$ stabilizes in at most $\mathrm{poly}_{1}(\lvert Q\rvert)$ steps.

3.4 Computing $\mathit{Conf}_{\infty}$ and Deciding Unboundedness

In this section we show how to compute $\mathit{Conf}_{\infty}$ in polynomial time and how to decide in polynomial time whether the initial configuration $(s,0)$ can reach $\mathit{Conf}_{\infty}$.

We start by showing that if a configuration can reach $U_{n}$ via a primitive run, then it can also reach $U_{n}$ via a polynomial-length run (see Appendix G for the proof).

Proposition 3.18**.**

There exists a polynomial $\mathrm{poly}_{7}$ such that the following holds. Let $(q,z),(q^{\prime},z^{\prime})\in\mathit{Conf}_{+}$ and let $(q,z)\stackrel{{\scriptstyle\pi}}{{\rightarrow}}(q^{\prime},z^{\prime})$ be a valid run such that $(q^{\prime},z^{\prime})\in U_{n}$ and $\pi$ is primitive. Then there is a valid run $(q,z)\stackrel{{\scriptstyle\pi^{\prime}}}{{\rightarrow}}(q^{\prime},z^{\prime\prime})$ such that $(q^{\prime},z^{\prime\prime})\in U_{n}$ and $\pi^{\prime}$ has length at most $\mathrm{poly}_{7}(|Q|).$

Recall that $U^{\prime}_{n+1}$ consists of all configurations in $\mathit{Conf}_{+}$ with minimal distance to $U_{n}$. Combining Remark 3.7 and Proposition 3.18, we have that the minimal distance from a configuration $(q,z)\in U^{\prime}_{n+1}\setminus U_{n}$ to $U_{n}$ is at most $\mathrm{poly}_{7}(|Q|)$. It follows that we can restrict the search for configurations that can reach $U_{n}$, to those within a polynomially-bounded distance to $U_{n}$. By itself this is not sufficient to obtain a polynomial-time algorithm to decide whether $U_{n}$ is reachable. However, using our analysis of the structure of $U_{n}$ in Section 3.3, we are able to formulate the bounded reachability problem above in a form that admits a polynomial-time algorithm.

Specifically, we consider the Bounded Coverability problem with a Disequality Objective: Given as input a 1-VASS $\mathcal{V}=(Q,D,\Delta,w)$ with a distinguished state $q_{f}$, a positive integer $L$ (written in unary), an initial configuration $(q_{0},x_{0})$, and a coverability objective of the form

[TABLE]

where $\ell,W$ and the $a_{i}$ and $b_{i}$ are non-negative integers given in binary, decide whether $O$ is reachable from $(q_{0},x_{0})$ via a valid run of length at most $L$.

Proposition 3.19**.**

The Bounded Coverability problem with a Disequality Objective is decidable in polynomial time.

We now show how to compute $\mathit{Conf}_{\infty}$ in polynomial time. By Corollary 3.17, the sequence $\{U_{n}\}_{n\in\mathbb{N}}$ converges in at most $\mathrm{poly}_{1}(\lvert Q\rvert)$ steps. It remains to show how to compute $U_{n+1}$ from $U_{n}$ in polynomial time for each $n$.

Recall that all unbounded chains are contained in $U_{0}$ and hence are contained in $U_{n}$ for all $n$. Recall also that the total number of bounded chains is at most $2\lvert Q\rvert$ and that $U_{n}$ is downward closed in each bounded chain. Thus $U_{n}$ is determined by giving, for every bounded chain $C$ such that $U_{n}\cap C\neq\emptyset$, the maximum configuration in $U_{n}\cap C$. In particular, $U_{n}$ can be described in space polynomial in the description of the given 1-VASS.

Recall that $U_{n+1}$ is obtained from $U_{n}$ by adding the configurations in $\mathrm{Conf}_{+}\setminus U_{n}$ that have minimum distance to $U_{n}$ and then closing downward in each bounded chain. By Remark 3.7 and Proposition 3.18, a configuration in $\mathrm{Conf}_{+}\setminus U_{n}$ that has minimum distance to $U_{n}$ has distance at most $\mathrm{poly}_{7}(\lvert Q\rvert)$. The idea to compute $U_{n+1}$ from $U_{n}$ is as follows:

For each bounded chain $C$, and each configuration $(q,x)\in C\setminus U_{n}$ that is among the top $\mathrm{poly}_{1}(\lvert Q\rvert)$ configurations in $C$, we determine the distance of $(q,x)$ to $U_{n}$ up to a bound of $\mathrm{poly}_{7}(\lvert Q\rvert)$. To do this we use the procedure described in Proposition 3.19, having first written $U_{n}$ as a polynomial-size union of sets of the form (3)—see below for details. The reason that it suffices to look only among the top $\mathrm{poly}_{1}(\lvert Q\rvert)$ configurations in each bounded chain is because we know from Proposition 3.15 that $\lvert C\setminus U_{n+1}\rvert\leq\mathrm{poly}_{1}(\lvert Q\rvert)$ for every $(n+1)$-active chain $C$.

We next show how to decompose $U_{n}$ into a polynomial union of sets of the form (3) in order to apply Proposition 3.19. Fixing $q\in Q_{+}$, let $R_{1},\ldots,R_{m}$ be a list of the non-trivial $q$-residue classes and for each $i\in\{1,\ldots,m\}$, write $a_{i}$ for the corresponding residue modulo $W_{q}$ and define $\ell_{i}:=\min(R_{i}\cap U_{n})$. Moreover, let $b_{1},\ldots,b_{k}$ be a list of the counter values such that for all $1\leq j\leq k$ we have $b_{j}\geq\ell_{i}$ and $(q,b_{j})\in R_{i}\setminus U_{n}$ for some $i$. Note that $m\leq\lvert Q\rvert$ and $k\leq m\,\mathrm{poly}_{1}(\lvert Q\rvert)$, and the corresponding classes and numbers can be enumerated in polynomial time. We decompose the set of configurations $\{(q,z)\in U_{n}\}$ into the following two components:

$\{(q,z):z\geq\mathrm{pmin}(\gamma_{q})\wedge\bigwedge_{i=1}^{m}z\not\equiv a_{i}\pmod{W_{q}}\}$, i.e., all configurations in trivial $q$-residue classes, 2. 2.

for all $j\in\{1,\ldots,m\}$, the set $\{(q,z):z\geq\ell_{j}\wedge\bigwedge_{i:i\neq j}z\not\equiv a_{i}\pmod{W_{q}}\wedge\bigwedge_{i=1}^{k}z\neq b_{i}\}$, which includes $R_{j}\cap U_{n}$ for the non-trivial residue class $R_{j}$.

Finally, it remains to decide whether the configuration $(s,0)$ is unbounded. By Proposition 3.3, $(s,0)$ is unbounded if and only if it can reach $\mathit{Conf}_{\infty}$. Now a shortest run from $(s,0)$ to $\mathit{Conf}_{\infty}$ is necessarily primitive: if an internal configuration in such a run lies in $\mathit{Conf}_{+}$ then it is also in $\mathit{Conf}_{\infty}$—a contradiction. By Proposition 3.18, a shortest run from $(s,0)$ to $\mathit{Conf}_{\infty}$ has length at most $\mathrm{poly}_{7}(\lvert Q\rvert)$. Thus we can decide whether such a run exists in polynomial time using Proposition 3.19. In conclusion we have

Theorem 3.20**.**

The Unboundedness Problem and the Coverability Problem for 1-VASS with disequality tests are decidable in polynomial time.

4 Unboundedness for 1-VASS

In this section we show that the Unboundedness Problem for 1-VASS (i.e., with no disequality tests) is in $\NC^{2}$. Recall that $\NC^{i}$ is the class of decision problems solvable in time $O(\log^{i}n)$, with $n$ the size of the input, on a parallel computer with a polynomial number of processors [13, 1].

Let $\mathcal{V}=(Q,\Delta,w)$ be a 1-VASS with a distinguished state $s\in Q$. We want to decide whether the configuration $(s,0)$ is unbounded. Since $\mathcal{V}$ has no disequality tests, deleting a negative-weight or zero-weight cycle that appears as an infix of a valid run yields another valid run. It follows that $(s,0)$ is unbounded if and only if there is a valid run from $(s,0)$ consisting of a simple path (of length at most $\lvert Q\rvert$) followed by a positive-weight simple cycle (again, of length at most $\lvert Q\rvert$). We call such a run a lasso.

Let $\mathcal{V}=(Q,\Delta,w)$ be a 1-VASS and let $\pi=q_{1},\ldots,q_{n}$ be a path in $\mathcal{V}$. Recall that a (possibly empty) prefix of $\pi$ is said to be minimal if it has minimal weight among all prefixes of $\pi$. Likewise a (possibly empty) suffix of $\pi$ is said to be maximal if it has maximal weight among all suffixes. It is clear that $q_{1},\ldots,q_{m}$ is a minimal prefix of $\pi$ if and only if $q_{m},\ldots,q_{n}$ is a maximal suffix. In such a case let us call $q_{m}$ a nadir of $\pi$ (the nadir is the lowest point reached in any run over $\pi$). Recall that $\mathrm{pmin}(\pi)$ is the weight of a minimal prefix of $\pi$; correspondingly we define $\mathrm{smax}(\pi)$ to be the weight of a maximal suffix.

Given paths $\pi$ and $\pi^{\prime}$, say that $\pi$ is dominated by $\pi^{\prime}$ if $\mathrm{pmin}(\pi)\leq\mathrm{pmin}(\pi^{\prime})$ and $\mathrm{smax}(\pi)\leq\mathrm{smax}(\pi^{\prime})$. Observe that if $\pi$ is dominated by $\pi^{\prime}$ then $\mathrm{weight}(\pi)\leq\mathrm{weight}(\pi^{\prime})$.

Example 4.1**.**

In Figure 5, the path $s_{0},s_{1},s_{4}$ dominates $s_{0},s_{2},s_{4}$. However, despite it being the case that $\mathrm{weight}(s_{0},s_{3},s_{4})>\mathrm{weight}(s_{0},s_{2},s_{4})$, $s_{0},s_{3},s_{4}$ does not dominate $s_{0},s_{2},s_{4}$ since the weight of a minimal prefix of the former is smaller than that of the latter.

Fix two states $p,q\in Q$ and let $P$ be a set of $p$-$q$ paths. We say that a set $P^{\prime}$ of $p$-$q$ paths is a Pareto set for $P$ if for every $\pi\in P$ there exists $\pi^{\prime}\in P^{\prime}$ such that $\pi$ is dominated by $\pi^{\prime}$.

We observe some simple properties of Pareto sets:

Lemma 4.2**.**

Let $p,q,r\in Q$. Then all of the following statements hold:

If $P_{1},P_{2},P_{3}$ are sets of $p$-$q$* paths such that $P_{1}$ is a Pareto set of $P_{2}$ and $P_{2}$ is a Pareto set of $P_{3}$, then $P_{1}$ is a Pareto set of $P_{3}$.* 2. 2.

If $P,R$ are sets of $p$-$q$* paths with respective Pareto sets $P^{\prime},R^{\prime}$, then $P^{\prime}\cup R^{\prime}$ is a Pareto set for $P\cup R$* 3. 3.

If $P$ is a set of $p$-$q$* paths and $R$ is a set of $q$-$r$ paths with respective Pareto sets $P^{\prime},R^{\prime}$, then $P^{\prime}\cdot R^{\prime}$ is a Pareto set of $P\cdot R$.*

Proposition 4.3**.**

Let $p,q\in Q$. Then every set $P$ of $p$-$q$ paths of length at most $k$ has a Pareto set $P^{\prime}$ of cardinality at most $|Q|$ such that each path in $P^{\prime}$ has length at most $2k$. Moreover such a set $P^{\prime}$ can be computed from $P$ in $\NC^{1}$.

An $\NC^{2}$ Upper Bound

Theorem 4.4**.**

The Unboundedness Problem and the Coverability Problem for 1-VASS are decidable in $\NC^{2}$.

Proof 4.5**.**

By Lemma 2.1, it will suffice to show that Unboundedness is in $\NC^{2}$.

Let $\mathcal{V}=(Q,\Delta,w)$ be a 1-VASS. Given $p,q\in Q$ and $m\in\mathbb{N}$, denote by $\mathrm{Paths}_{p,q,m}$ the set of all $p$-$q$ paths in $\mathcal{V}$ of length at most $m$.

Given a state $s\in Q$, recall that $(s,0)$ is unbounded if and only if there exists a lasso run that starts at $(s,0)$. To determine the existence of such a run we compute a Pareto set $P_{q}$ for $\mathrm{Paths}_{s,q,\lvert Q\rvert}$ and a Pareto set $P^{\prime}_{q}$ for $\mathrm{Paths}_{q,q,\lvert Q\rvert}$ for every state $q\in Q$. Having done this we look for $q\in Q$ and paths $\pi\in P_{q}$ and $\pi^{\prime}\in P^{\prime}_{q}$ such that $\pi\cdot\pi^{\prime}$ induces a valid run from $(s,0)$ and $\pi^{\prime}$ has positive weight.

It remains to show how to compute a Pareto set of $\mathrm{Paths}_{p,q,\lvert Q\rvert}$ for all pairs of states $p,q\in Q$ (together with the values $\mathrm{weight}(\pi)$ and $\mathrm{pmin}(\pi)$ for every path $\pi$ in the Pareto set) in $\NC^{2}$.

For $k=1,\ldots,\lceil\log|Q|\rceil$, we show how to compute a family $\mathcal{P}_{k}=\{P_{p,q,k}\}_{p,q\in Q}$ such that for all $p,q\in Q$:

$P_{p,q,k}$* is a Pareto set for $\mathrm{Paths}_{p,q,2^{k}}$;* 2. 2.

$P_{p,q,k}\subseteq\mathrm{Paths}_{p,q,4^{k}}$; 3. 3.

$|P_{p,q,k}|\leq|Q|$.

By Item 1, if $k=\lceil\log|Q|\rceil$ then $P_{p,q,k}$ is a Pareto set for $\mathrm{Paths}_{p,q,|Q|}$. (Note that for $k=\lceil\log|Q|\rceil$, $\mathcal{P}_{k}$ consists of paths of length at most $|Q|^{2}$.)

The construction of $\mathcal{P}_{k}$ is by induction on $k$. Suppose we have computed $\mathcal{P}_{k}$ with Properties 1-3 above. Fix $p,q\in Q$. In order to compute $P_{p,q,k+1}$ we observe that

[TABLE]

is a Pareto set for $\mathrm{Paths}_{p,q,2^{k+1}}$ by Items 2 and 3 of Lemma 4.2. Applying Proposition 4.3, we obtain a Pareto set $P^{\prime}$ for $P$ of cardinality at most $|Q|$. By Item 1 of Lemma 4.2, $P^{\prime}$ is a Pareto set for $\mathrm{Paths}_{p,q,2^{k+1}}$. Finally, it is clear from the length bound in Proposition 4.3 that all paths in $P^{\prime}$ have length at most $4^{k+1}$. Thus we define $P_{p,q,k+1}:=P^{\prime}$.

It remains to establish the $\NC^{2}$ complexity bound for computing $\mathcal{P}_{\lceil\log|Q|\rceil}$. For this it suffices to show that for all $k$ the computation of $\mathcal{P}_{k+1}$ from $\mathcal{P}_{k}$ can be carried out in $\NC^{1}$. But we may compute each set $P_{p,q,{k+1}}$ in parallel (over $p,q\in Q$), and the computation of each such set can be done in $\NC^{1}$ by Proposition 4.3.

5 Conclusion

We have shown that control-state reachability for 1-VASS with disequality tests can be solved in polynomial time. The complexity of reaching a given configuration in this model is open (being equivalent to control-state reachability in the presence of both equality and disequality tests), lying between NP and PSPACE. For multi-dimensional VASS with disequality tests, the classical argument of Rackoff [15] easily generalises to show that control-state reachability remains in EXPSPACE. By contrast, decidability of reachability is open to the best of our knowledge. For comparison, recall that without disequality tests reachability is decidable but non-elementary [5].

Appendix A Proof of the reduction in Figure 1

Let us recall that for every value $u\in{\mathbb{N}}$, the assignment $\mathrm{val}_{u}:{\{X_{1},\ldots,X_{m}\}}\to{\{0,1\}}$ is defined by $\mathrm{val}_{u}(X_{i})=1$ if and only if $p_{i}\mid u$. For convenience, define the domain $D_{s}\subseteq\mathbb{N}$ containing all allowable counter values in state $s$ (exclude all disequality guards on $s$).

The key observation is the following: let $u\in\{0,\ldots,P-1\}$, and consider a clause $C_{i}=\ell_{i_{1}}\vee\ell_{i_{2}}\vee\ell_{i_{3}}$, where $\ell_{i_{j}}$ is a literal of variable $X_{i_{j}}$, then $\mathrm{val}_{u}$ satisfies $C_{i}$ iff there exists some $k\in{\mathbb{N}}$ such that $u+kp_{i_{1}}p_{i_{2}}p_{i_{3}}\notin D_{i}$.

Indeed, note that for every $j\in{\{1,2,3\}}$ and every $k\in{\mathbb{N}}$ we have that $p_{i_{j}}|u$ iff $p_{i_{j}}|u+kp_{i_{1}}p_{i_{2}}p_{i_{3}}$. Recall that ${\rm val}_{u}(X_{i_{j}})=1$ iff $p_{i_{j}}|u$, and observe that since $u<P$, there exists $k\in{\mathbb{N}}$ such that $u+kp_{i_{1}}p_{i_{2}}p_{i_{3}}\in\{P,P+1,\ldots,P+p_{i_{1}}p_{i_{2}}p_{i_{3}}-1\}$. We thus have that $\mathrm{val}_{u}$ satisfies $C_{i}$ iff $\mathrm{val}_{u+kp_{i_{1}}p_{i_{2}}p_{i_{3}}}$ satisfies $C_{i}$, iff $u+kp_{i_{1}}p_{i_{2}}p_{i_{3}}\notin D_{i}$.

Now, assume $\varphi$ is satisfiable, and let $\pi$ be a satisfying assignment. We associate with $\pi$ the number $u=\prod_{j:\pi(X_{j})=1}p_{j}\pmod{P}$ (note that taking modulo $P$ simply means that if the product is exactly $P$, we take $u=0$). Clearly $\pi=\mathrm{val}_{u}$. We claim that $(s_{0},u)$ is bounded. Indeed, the only paths possible from $(s_{0},u)$ start by choosing a state $s_{i}$, and then repeatedly applying the cycle of cost $c_{i}$. However, since $\mathrm{val}_{u}$ satisfies all clauses, then by the above, all such paths are blocked by a disequality guard after taking the $c_{i}$ for $k$ times, for some $k\in{\mathbb{N}}$ (which depends on $i$). Thus, $(s_{0},u)$ is bounded.

Conversely, assume $(s_{0},u)$ is bounded for some value $u$, we claim that $\mathrm{val}_{u}$ satisfies $\varphi$. Indeed, by the same reasoning above, it follows that for every cycle of cost $c_{i}$, we have $u+kc_{i}\notin D_{i}$ for some $k\in{\mathbb{N}}$, so $\mathrm{val}_{u}$ satisfies $C_{i}$. Since this is true for all clauses, we have that $\mathrm{val}_{u}$ satisfies $\varphi$.

We conclude that $\varphi$ is satisfiable iff some configuration $(s_{0},u)$ is bounded, which completes the reduction.

Finally, we note that the reduction indeed takes polynomial time — indeed, the construction clearly has polynomially many states. Also, the first $m$ primes $p_{1},\ldots,p_{m}$ can be listed in time polynomial in $m$, and are representable in polynomially many bits. Therefore, the binary representation of the transition values and the amount of missing elements in the domain of each state are both polynomial.

Appendix B Single disequality guards suffice

Given a 1-VASS $\mathcal{V}=(Q,\Delta,D,w)$ with disequality tests, we can assume that for all states $q$ the set $D_{q}$ is either $\mathbb{N}$ or $\mathbb{N}\setminus\{g\}$ for some $g\in\mathbb{N}$. This assumption is without loss of generality, as a state $q$ with $D_{q}=\mathbb{N}\setminus\{a_{1},\ldots,a_{n}\}$ can be replaced with a sequence of new states $q_{1},\cdots,q_{n}$, connected with [math]-weight transitions, such that $D_{q_{i}}=\mathbb{N}\setminus\{a_{i}\}$ for $i\in\{1,\ldots,n\}$. The transformation yields only a polynomial blow-up in the size of the 1-VASS, and there is a natural correspondence between runs in the original 1-VASS and the modified one.

Appendix C Proof of Lemma 2.1

Consider a 1-VASS $\mathcal{V}=(Q,\Delta,D,w)$ with disequality tests, and let $s,t\in Q$. We reduce the Coverability problem to the Unboundedness problem as follows.

We obtain from $\mathcal{V}$ a new 1-VASS $\mathcal{V}^{\prime}$ as follows. First, we remove from $\mathcal{V}$ all the states that cannot reach $t$ in the underlying graph. Second, we introduce a new state $t^{\prime}$ with a self-loop of weight $+1$, that is reachable from $t$ with a transition of weight [math]. The output of the reduction is $\mathcal{V}^{\prime}$ with the distinguished state $s$.

Recall that reachability in directed graphs can be decided in $\NL\subseteq\NC^{2}$, and hence this reduction is $\NC^{2}$-computable.

Henceforth assume that $s$ can reach $t$ in the underlying graph of $\mathcal{V}$ (otherwise $s$ cannot cover $t$, and the reduction can output a trivial negative instance). We proceed to prove the correctness of the reduction.

First, if $(s,0)$ can cover $t$ in $\mathcal{V}$, then in particular it can only cover $t$ using states in $\mathcal{V}^{\prime}$. We now have that $(s,0)$ is unbounded in $\mathcal{V}^{\prime}$, by covering $t$, and then taking the transition to $t^{\prime}$ and repeating the self loop unboundedly. Note that crucially, there are no disequality guards on $t^{\prime}$, and therefore once $t$ is reached, we can take the transition to $t$ and repeat the self loop unboundedly.

Conversely, suppose $(s,0)$ is unbounded in $\mathcal{V}^{\prime}$, then either there is a valid run in $\mathcal{V}$ from $(s,0)$ to $(t^{\prime},z)$ for some $z$, in which case $(s,0)$ can cover $t$ in $\mathcal{V}$, or $(s,0)$ is unbounded already in $\mathcal{V}$ and, moreover, it is unbounded in $\mathcal{V}$ using only states that can reach $t$ in the underlying graph. We claim that in the latter case, $(s,0)$ can cover $t$ in $\mathcal{V}$. Indeed, from $(s,0)$ there is a valid run to a configuration $(q,z)$ with $z$ that is large enough, such that a simple path from $q$ to $t$ in the underlying graph lifts to a valid run from $(q,z)$ to $(t,z^{\prime})$ for some $z^{\prime}$. Specifically, taking $z>|Q|\cdot W\cdot G$ where $W$ is the maximal absolute value of the weight of a transition in $\mathcal{V}$, and $G$ is the maximal disequality guard, suffices for such a run.

Appendix D Proof of Proposition 3.3

Clearly if $(s,0)$ can reach an unbounded configuration in $\mathit{Conf}_{+}$ then it is unbounded.

Conversely, if $(s,0)$ is unbounded, then there is a state $q$ such that for all $z_{0}\in\mathbb{N}$, there exist $z,z^{\prime}\geq z_{0}$ and a valid run $\pi$ starting in $(s,0)$ that visits $(q,z)$ and ends in $(q,z^{\prime})$. Thus, there is a positive cycle $\gamma$ on $q$. The positive cycle $\gamma$ on $q$ may not be simple, but it certainly visits a state $p$ with a simple positive cycle $\gamma_{p}$ on it. Pick $z_{0}$ such that $z_{0}>\mathrm{pmin}(\gamma)+x$. for all $x\in\mathrm{blocked}(\gamma_{p}^{\omega})$ (Note that $\mathrm{blocked}(\gamma_{p}^{\omega})$ is finite since $\gamma_{p}$ is a positive cycle. The maximum is thus well-defined.) Hence, there is a valid run from $(s,0)$ to $(p,y)$ where $y>\max(\mathrm{blocked}(\gamma_{p}^{\omega}))$. Observe that $(p,y)\in\mathit{Conf}_{+}$ and it is unbounded.

Appendix E Proof of Proposition 3.9

Suppose that $\pi$ has length strictly greater than $\lvert Q\rvert^{2}+2$. By the Pigeonhole principle, we can find $\lvert Q\rvert+1$ distinct proper prefixes (i.e. prefixes that are not just the initial state, or the entire path) of $\pi$ that end in the same state. That is, $\lvert Q\rvert$ proper cycles on the same state. Let $\pi_{1},\ldots,\pi_{\lvert Q\rvert+1}$ be a list of these prefixes, given in order of increasing length, and let the corresponding suffixes be $\pi^{\prime}_{1},\ldots,\pi^{\prime}_{\lvert Q\rvert+1}$. We now consider two cases.

First, suppose that there exist $i<j$ such that $\mathrm{weight}(\pi_{i})$ and $\mathrm{weight}(\pi_{j})$ have the same residue modulo $W_{q^{\prime}}$. Then define $\pi^{\prime}:=\pi_{i}\cdot\pi^{\prime}_{j}$. In this case path $\pi^{\prime}$ lifts to a run from $(q,z)$ to $(q^{\prime},z^{\prime\prime})$ such that $(q^{\prime},z^{\prime\prime})$ lies in the same $q^{\prime}$-residue class as $(q^{\prime},z^{\prime})$. The second case is that the respective residue classes of $\mathrm{weight}(\pi_{1}),\ldots,\mathrm{weight}(\pi_{\lvert Q\rvert+1})$ modulo $W_{q^{\prime}}$ are all distinct. Then there exists $i>1$ such that, defining $\pi^{\prime}:=\pi_{1}\cdot\pi^{\prime}_{i}$, the path $\pi^{\prime}$ lifts to a run from $(q,z)$ to $(q^{\prime},z^{\prime\prime})$ such that $(q^{\prime},z^{\prime\prime})$ lies in a trivial $q^{\prime}$-residue class (as there are at most $|Q|$ non-trivial residue classes).

Continuing in this fashion we can recursively remove cycles from the original path $\pi$ to eventually obtain a path $\pi^{\prime}$ that has length at most $\lvert Q\rvert^{2}+2$ and such that Item 3 is satisfied. Consider all maximal infixes that were removed from $\pi$ to obtain $\pi^{\prime}$. Note that each such infix must necessarily be a cycle as they arise from iteratively removing cycles. Since $\pi$ was primitive, all of them must have non-positive weight. Hence, Items 1 and 2 also hold333Note that we do not claim that the intermediate paths obtained in the procedure are primitive nor that the individual cycles removed in this process are negative. Rather the observation is that $\pi^{\prime}$ can equivalently be obtained from $\pi$ in one step by simultaneously removing a disjoint family of infixes, where each infix is a cycle (necessarily non-positive)..

Appendix F Proof of Lemma 3.11

Consider two “consecutive” configurations $(q,z),(q,z+W_{q})\in C\setminus U_{n}$, then all configurations $(q,z^{\prime})$ for $z\leq z^{\prime}<z+W_{q}$ lie in pairwise-distinct $q$-residue classes. In particular, since there are at most $|Q|$ non-trivial residue classes, and since trivial residue classes are contained in $U_{0}$, we have that at most $|Q|$ such elements are in $\delta_{n}(C)$.

Appendix G Proof of Proposition 3.18

By Proposition 3.15 we can find a polynomial $\mathrm{poly^{\prime}}_{7}$ such that

[TABLE]

for all $n\in\mathbb{N}$.

Set $\mathrm{poly}_{7}(|Q|):=|Q|\cdot(\mathrm{poly}^{\prime}_{7}(|Q|))^{2}+|Q|^{2}+4$, and consider a valid, primitive path $\pi$ such that $\mathrm{length}(\pi)>\mathrm{poly}_{7}(|Q|)$ and $(q,z)\stackrel{{\scriptstyle\pi}}{{\to}}(q^{\prime},z^{\prime})$.

Since $\pi$ has length greater than $|Q|\cdot(\mathrm{poly}^{\prime}_{7}(|Q|))^{2}+2$, there exists a state $q^{\prime\prime}\in Q$ that occurs at least $(\mathrm{poly}^{\prime}_{7}(|Q|))^{2}$ times in internal configurations within the first $|Q|\cdot(\mathrm{poly}^{\prime}_{7}(|Q|))^{2}+2$ configurations of $\pi$. Thus, there exists a sequence of proper prefixes $\pi_{1}<\ldots<\pi_{\mathrm{poly}^{\prime}_{7}(|Q|)}$ of $\pi$ that all end in $q^{\prime\prime}$ and such that one of the following two cases holds.

1. (i)

The numbers $\mathrm{weight}(\pi_{i})$ all have the same residue modulo $W_{q^{\prime}}$. 2. (ii)

The numbers $\mathrm{weight}(\pi_{i})$ have pairwise distinct residues modulo $W_{q^{\prime}}$.

Indeed, since there are $(\mathrm{poly}^{\prime}_{7}(|Q|))^{2}$ prefixes to choose from, either Case (i) holds, or there are strictly less than $\mathrm{poly}^{\prime}_{7}(|Q|)$ prefixes per residue class. If the latter holds then there must be least $\mathrm{poly}^{\prime}_{7}(|Q|)$ such distinct residue classes, so Case (ii) holds.

In either case, we decompose the computation $\pi$ as $\pi=\pi_{\mathrm{poly}^{\prime}_{7}(|Q|)}\cdot\pi^{\prime}$. Observe that since $\pi$ is primitive, then so is $\pi^{\prime}$. Applying Proposition 3.9 to $\pi^{\prime}$ we obtain a path $\pi^{\prime\prime}$ of length at most $|Q|^{2}+1$ such that $\pi_{\mathrm{poly}^{\prime}_{7}(|Q|)}\cdot\pi^{\prime\prime}$ leads from $(q,x)$ to either the same residue class as $(q^{\prime},z^{\prime})$ or to a trivial $q^{\prime}$-residue class.

It is important to note that we cannot assume $\pi^{\prime\prime}$ is not blocked after the prefix $\pi_{\mathrm{poly}^{\prime}_{7}(|Q|)}$. However, since $|\mathrm{blocked}(\pi^{\prime\prime})|\leq|Q|^{2}$, we can remove from the list of prefixes at most $|Q|^{2}$ prefixes such that the remaining prefixes do not cause $\pi^{\prime\prime}$ to block. (Indeed, we will not modify the path by literally removing prefixes but rather cycles which correspond to the path from a prefix to a longer prefix. For now, we are only speaking about removing elements from the collection of prefixes we can choose from.) W.l.o.g, let $\pi_{1},\ldots\pi_{d}$ be the remaining prefixes.

Consider the family of paths $\theta_{i}:=\pi_{i}\cdot\pi^{\prime\prime}$ for $i\in\{1,\ldots,d\}$. Note that every $\theta_{i}$ is of length at most $\mathrm{poly}_{7}(|Q|)$, and since the $\theta_{i}$ are obtained by removing $q^{\prime\prime}$-cycles, and since $\pi$ is primitive, the configurations reached by $\theta_{i}$ are above $(q^{\prime},z^{\prime})$. We claim that one of the $\theta_{i}$ is a valid run from $(q,z)$ to $U_{n}$.

We separate the analysis according to the cases above.

• •

In Case (i), if $\pi^{\prime\prime}$ leads to a trivial residue class, then all the $\theta_{i}$ reach $U_{n}$, and we are done. Otherwise, $\pi^{\prime\prime}$ leads to the same residue class as $(q^{\prime},z^{\prime})$. By our choice of $\mathrm{poly}^{\prime}_{7}(|Q|)$ in (5), we have that $d>\sum_{R\text{ non-trivial}}|\delta_{n}(R)|$. That is, there are more prefixes that do not cause $\pi^{\prime\prime}$ to block than there are missing elements above $(q^{\prime},z^{\prime})$ in $U_{n}$. We conclude that some $\theta_{i}$ reaches $U_{n}$.

• •

In Case (ii), the paths $\theta_{i}$ all reach distinct residue classes. In particular, since there are more than $|Q|$ such prefixes — i.e. $d>|Q|$ by our choice of $\mathrm{poly}^{\prime}_{7}(|Q|)$ — then some $\theta_{i}$ reach trivial residue classes, and thus reach $U_{n}$.

Appendix H Proof of Proposition 3.19

We carry out a forward reachability analysis starting from the initial configuration $(q_{0},x_{0})$. The algorithm runs for $L+1$ rounds. In the $k$-th round, we maintain for each state $q$ a set $S_{q,k}$ of configurations $(q,x)$ that are reachable from $(q_{0},x_{0})$ by valid runs of length $k$. Let $R_{q,k}$ denote the set of all configurations $(q,x)$ that are reachable from $(q_{0},x_{0})$ by valid runs of length $k$. We maintain the invariant that if some configuration $(q,x)\in R_{q,k}$ can reach the objective $O$ in $L-k$ steps via a path $\pi$ then some configuration $(q,x^{\prime})\in S_{q,k}$ can also reach $O$ via the same path $\pi$. We output that the objective is reachable if and only if one of the sets $S_{q_{f},k}$ for some $k\in\{0,\ldots,L\}$ intersects $O$. This last step is clearly sound, given the invariant.

The key to obtaining a polynomial-time runtime bound is to suitably prune the sets $S_{q,k}$ to keep them of polynomial size. In order to compute $\{S_{q,{k+1}}\}_{q\in Q}$ from $\{S_{q,k}\}_{q\in Q}$ we proceed as follows. First define $\{S^{\prime}_{q,k}\}_{q\in Q}$ to be the indexed set of all valid configurations reachable in one step from $\{S_{q,k}\}_{q\in Q}$. Now we obtain $S_{q,k+1}$ from $S^{\prime}_{q,k}$ by the following two steps:

• •

First, we delete from $S^{\prime}_{q,k}$ all configurations $(q,x)$ such that there are $(n+L)$ configurations $(q,x^{\prime})$ in $S^{\prime}_{q,k}$ with $x^{\prime}>x$ and $x^{\prime}\equiv x\pmod{W}$.

• •

Secondly, we delete from $S^{\prime}_{q,k}$ all configurations $(q,x)$ such that there are $(n+L)(m+1)$ configurations $(q,x^{\prime})$ in $S^{\prime}_{q,k}$ with $x^{\prime}>x$.

Clearly each set $S_{q,k}$ has cardinality at most $(n+L)(m+1)$, and moreover, it can be computed from the collection of sets $\{S_{q^{\prime},k-1}\mid q^{\prime}\in Q\}$ in polynomial time.

It remains to argue that the invariant is maintained between rounds. To this end, suppose some state $(q,x)\in R_{q,k+1}$ can reach the objective in $L-k-1$ steps via a path $\pi$. Then there exists a state $(q^{\prime},x^{\prime})\in R_{q^{\prime},k}$ that can reach the objective in $L-k$ steps via the path $q^{\prime}\pi$. By the loop invariant there exists a state $(q^{\prime},x^{\prime\prime})\in S_{q^{\prime},k}$ that can also reach the objective via the path $q^{\prime}\pi$. Hence there is a state $(q,y)\in S^{\prime}_{q^{\prime},k}$ that can reach the objective via the path $\pi$. Now if $(q,y)$ is deleted in the first stage of pruning then there is some configuration $(q,y^{\prime})$ such that $y^{\prime}>y$, $y^{\prime}\equiv y\pmod{W}$, and $\pi$ yields a valid computation from $(q,y^{\prime})$ to the objective $O$. After the first stage of pruning, each residue class in $S^{\prime}_{q,k}$ contains at most $n+L$ elements. Hence if $(q,y^{\prime})$ is deleted in the second stage of pruning, there are at least $n+L$ configurations $(q,y^{\prime\prime})$ in $S_{q,k+1}$ that are above $(q,y^{\prime})$ and are such that the run over $\pi$ from $(q,y^{\prime})$ leads to a configuration $(q_{f},z)$ with $\bigwedge_{i=1}^{m}{z\not\equiv a_{i}}\bmod W$. Now from one of these configurations $\pi$ yields a valid run that reaches $O$ since one of $n+L$ choices of $(q,y^{\prime\prime})$ will avoid $\mathrm{blocked}(\pi)$ and lead to a configuration $(q_{f},z)$ such that $\bigwedge_{i=1}^{n}z\neq b_{i}$.

Appendix I Proof of Lemma 4.2

Items 1 and 2 are obvious. Item 3 follows from the fact that if $\pi_{1}\in P$ is dominated by $\pi^{\prime}_{1}\in P^{\prime}$ and $\pi_{2}\in R$ is dominated by $\pi^{\prime}_{2}\in R^{\prime}$ then $\pi_{1}\cdot\pi_{2}$ is dominated by $\pi_{1}^{\prime}\cdot\pi_{2}^{\prime}$. Indeed,

[TABLE]

We can similarly argue that $\mathrm{smax}(\pi_{1}\cdot\pi_{2})\leq\mathrm{smax}(\pi^{\prime}_{1}\cdot\pi^{\prime}_{2})$.

Appendix J Proof of Proposition 4.3

Fix a state $r\in Q$. Consider all $p$-$r$ paths that appear as a minimal prefix of some path in $P$. Pick a single such prefix $\pi_{1}$ of maximum weight. Likewise consider all $r$-$q$ paths that appear as a maximal suffix of some path in $P$ and pick a single such suffix $\pi_{2}$ of maximum weight. Now form the path $\pi:=\pi_{1}\cdot\pi_{2}$. This path dominates any path in $P$ with nadir $r$. We define $P^{\prime}$ to be the set of paths $\pi$ formed in this way as $r$ runs through $Q$. By taking $k$ large enough, we can suppose without loss of generality, that the absolute weight of all paths in $P^{\prime}$ is at most $2^{k}$. That is, it can be encoded in binary using $k+1$ bits.

The $\NC^{1}$ bound on computing $P^{\prime}$ relies on the well-known fact that the sum of a list of binary integers can be computed in $\NC^{1}$ [17, Chapter 1]. To obtain $P^{\prime}$ we compute the weight of each prefix and suffix of every path in $P$ in parallel. According to [17], this can be done in time $O(\log k)$ on a parallel computer with $|P|k$ processors: one for each element of $P$ and each midpoint $0\leq m\leq k$. Finally, for each state $r\in Q$ in parallel, we find a maximum-weight prefix of a path in $P$ that connects $p$ and $r$ and a maximum-weight suffix of a path in $P$ that connects $r$ and $q$. It is straightforward to prove the latter is also in $\NC^{1}$ since sorting a list of numbers can be done in $\NC^{1}$, [14, 3] thus completing the proof.