Reachability in Vector Addition System with States Parameterized by Geometric Dimension

Let $d\ge 0$ be an integer. A $d$-dimensional vector addition system with states ($d$-VASS) is a pair $G=(Q,T)$ where $Q$ is a finite set of states and $T\subseteq Q\times {\mathbb{Z}}^d\times Q$ is a finite set of transitions. Clearly a VASS can also be viewed as a directed graph with edges labelled by integer vectors. Given a word $\pi =(p_1,{𝒂}_1,q_1)(p_2,{𝒂}_2,q_2)\mathrm{\dots }(p_n,{𝒂}_n,q_n)\in T^{\ast }$ over transitions, we say that $\pi$ is a path from $p_1$ to $q_n$ if $q_i=p_{i+1}$ for all $i=1,\mathrm{\dots },n-1$. It is a cycle if we further have $p_1=q_n$. Such a path is usually presented in the following form:

where $t_i=(p_i,{𝒂}_i,q_i)$. The effect of $\pi$ is defined to be $\mathrm{\Delta }(\pi ):={\sum }_{i=1}^n{𝒂}_i$.

We present a stronger algorithm that given a VASS $G$ as input, computes a basis for $\mathrm{Cyc}(G)$. Observe that every cycle lies within some maximal strongly connected component (SCC) of $G$. Once we have an algorithm that computes a basis for the cycle spaces of every SCC of $G$, a basis for $\mathrm{Cyc}(G)$ is just a maximal linearly independent subset of the union of these bases, which can be computed by Gaussian elimination in polynomial time. So the problem reduces to computing a basis for $\mathrm{Cyc}(G)$ in case $G$ is strongly connected.

Fix a strongly connected $d$-VASS $G=(Q,T)$. We introduce an operation called cycle shrinking. Let $\theta$ be a simple cycle in $G$ that is not a self-loop and has the form

First we define a “shift function” $s:Q\to {\mathbb{Z}}^d$ as follows. If $q=p_k$ for some $k\in [n]$, we set $s(q):=\mathrm{\Delta }(\theta [1..k])=\mathrm{\Delta }(t_1)+\mathrm{\dots }+\mathrm{\Delta }(t_k)$; otherwise we set $s(q):=\mathrm{𝟎}$. Note that $s(p_0)=s(p_n)=\mathrm{\Delta }(\theta )$. Let $P=\{p_1,\mathrm{\dots },p_n\}$ be the set of states that occurs on $\theta$. Now we define a new VASS $G/\theta =(Q^{\theta },T^{\theta })$ that “shrinks” $\theta$ into a single states as follows.

• $\mathrm{■}$

  $Q^{\theta }:=(Q\setminus P)\cup \{\theta \}$.

• $\mathrm{■}$

  Let $h:Q\to Q^{\theta }$ be defined as $h(q)=\theta$ if $q\in P$ and $h(q)=q$ otherwise. The transitions are given by $T^{\theta }:=\{(h(p),s(p)+𝒂-s(q),h(q)):(p,𝒂,q)\in T\}$.

It should be clear that as $\theta$ is not a self-loop, and that $G/\theta$ can be constructed in polynomial time given $G$ and $\theta$. Note that $\Vert T^{\theta }\Vert \le (2|Q|+1)\Vert T\Vert$, so the size of $G/\theta$ is bounded by $|G/\theta |\le |G|+d\cdot |T|\cdot \lceil \log (2|Q|+1)\rceil$. Observe that $h$ is a graph homomorphism from $G$ onto $G/\theta$. Thus $G/\theta$ is strongly connected as long as $G$ is. Besides, we can show that $G/\theta$ preserves the cycle space of $G$.

Now the algorithm for computing a basis of $\mathrm{Cyc}(G)$ where $G$ is strongly connected should be clear. As listed in Algorithm 1, we repeatedly shrink a cycle in $G$ until there remains only one state. Then its cycle space is the span of effects of self-loops in it. A basis of $\mathrm{Cyc}(G)$ can be computed using Gaussian elimination. Since a cycle shrinking reduces the number of states by at least one, after at most $|Q|$ iterations we must stop with a single state remained. Note that the size of VASS is always bounded by $|G|+d\cdot |Q|\cdot |T|\lceil \log (2|Q|+1)\rceil \le {|G|}^2$ in each iteration. Thus the algorithm runs in polynomial time.

Given a VASS $G=(Q,T)$ and a configuration $p(𝒖)\in Q\times {\mathbb{N}}^d$, we write ${Reach}_G(p(𝒖))$ for all configurations that is reachable from $p(𝒖)$: ${Reach}_G(p(𝒖)):=\{q(𝒗)\in Q\times {\mathbb{N}}^d:p(𝒖)\stackrel{\ast }{\to }q(𝒗)\}$. The next lemma shows that the “dimension” of any reachable set is bounded by $gdim(G)$, in the sense that it is contained in a finite union of affine copies of $\mathrm{Cyc}(G)$. Here the sum of a vector $𝒗\in {\mathbb{Q}}^d$ and a set $S\subseteq {\mathbb{Q}}^d$ is defined as $𝒗+S:=\{𝒗+𝒔:𝒔\in S\}$.

Note that one may need exponentially many (roughly $O(\chi {(G)}^d)$) affine copies of $\mathrm{Cyc}(G)$ to cover ${Reach}_G(p(𝒖))$. The next lemma shows that any fixed run from $p(𝒖)$ is confined in, however, at most $|Q|$ affine copies of $\mathrm{Cyc}(G)$.

These two lemmas follow easily from the fact that we can view a run as a simple path interleaved with cycles. Their proofs can be found in the full version of this paper.

An orthant is one of the $2^d$ regions in ${\mathbb{Q}}^d$ split by the $d$ axes. Formally, given a vector $t\in {\{+1,-1\}}^d$, the orthant $Z_t$ defined by $t$ is the set $Z_t:=\{𝒖\in {\mathbb{Q}}^d:𝒖(i)\cdot t(i)\ge 0\text{ for all }i\in [d]\}$. The non-negative orthant ${\mathbb{Q}}_{\ge 0}^d=Z_{(+1,+1,\mathrm{\dots },+1)}$ is a major concern in this paper.

Let $I\subseteq [d]$ be a subset of indices. For a vector $𝒖\in {\mathbb{Q}}^d$, we define its projection onto indices in $I$ as a function ${𝒖|}_I\in {\mathbb{Q}}^I$ given by $({𝒖|}_I)(i)=𝒖(i)\text{ for all }i\in I$. We tacitly identify the function ${𝒖|}_I\in {\mathbb{Q}}^I$ as a vector in ${\mathbb{Q}}^{|I|}$. For a set of vectors $V\subseteq {\mathbb{Q}}^d$, we define $V{|}_I:=\{𝒗{|}_I:𝒗\in V\}$. It should be clear that the projection of a vector space onto indices in $I$ is again a vector space in ${\mathbb{Q}}^{|I|}$, and the projection of an orthant $Z_t$ onto $I$ is an orthant in ${\mathbb{Q}}^{|I|}$ defined by ${t|}_I$.

Sign-reflecting projection helps us project the vectors in a vector space to some of its components so that the pre-image of a certain orthant still belongs to one orthant. Moreover, we have that such a projection is one-to-one.

We mainly care about sign-reflecting projections for a plane, i.e. a $2$-dimensional subspace of ${\mathbb{Q}}^d$. In this case a good sign-reflecting projection is given by the following lemma.

Intuitively 4.5 projects a plane onto an axis plane. The preimages of those two axes will play an important role in our work, as stated in the following lemma.

We call vectors ${𝒖}_1,{𝒖}_2$ given by this lemma the canonical horizontal / vertical vector derived from ${𝒗}_1,{𝒗}_2$ for $P$ with respect to ${\mathbb{Q}}_{\ge 0}^d$. We remark that this notion can be generalized to orthants other than ${\mathbb{Q}}_{\ge 0}^d$. As any vector in $P$ is uniquely represented as a linear combination of ${𝒖}_1$ and ${𝒖}_2$, we can obtain a bound for components of vectors in $P$ in terms of their projections.

4.7 gives bounds on the components in the support of the plane. So we would like the cycle space of a VASS $G$ to have full support, i.e. $supp(\mathrm{Cyc}(G))=[d]$. In this section we develop a technique called support projection to transform an arbitrary geometrically 2-dimensional VASS to one with such good property, without increasing its traversal number and the characteristic.

Let $G=(Q,T)$ be a geometrically 2-dimensional $d$-VASS. Let $S=supp(\mathrm{Cyc}(G))$ and $\overline{S}=[d]\setminus S$. For vectors $𝒗\in {\mathbb{Z}}^S$ and $\overline{𝒗}\in {\mathbb{Z}}^{\overline{S}}$, we define their composition $𝒗{\circ }_S\overline{𝒗}\in {\mathbb{Z}}^d$ naturally by $(𝒗{\circ }_S\overline{𝒗})(i)=𝒗(i)$ if $i\in S$ and $(𝒗{\circ }_S\overline{𝒗})(i)=\overline{𝒗}(i)$ if $i\in \overline{S}$. Since $S$ is always clear from the context, we will simply write $𝒗\circ \overline{𝒗}$ for this composition.

The support projection of $G$ is the $|S|$-dimensional VASS $G^S=(Q^S,T^S)$ where

A state of the form $(q,𝒗)$ in $G^S$ is denoted $q^{𝒗}$ for conciseness.

There is a huge expansion in the size of $G^S$, as $|Q^S|=|Q|\cdot {(2\chi (G))}^{|\overline{S}|}$. On the other hand, we can show that support projection does not increase traversal number and characteristic, and the projected VASS has full support as we expected.

Depending on whether the cycle space of a VASS can be sign-reflectively projected onto an axes-plane with respect to the non-negative orthant ${\mathbb{Q}}_{\ge 0}^d$, we classify geometrically 2-dimensional VASSes into the following two classes.

In this subsection we focus on degenerate VASSes. We show that every run from $\mathrm{𝟎}$ in a degenerate VASS is thin in the sense of the following definitions. An illustration of thin runs can be found in 1(a).

Indeed, we can relax the definition of beams by letting the direction $𝒗$ range over all integer vectors in ${\mathbb{Z}}^d$. Let $𝒗\in {\mathbb{Z}}^d$ and $W\in \mathbb{N}$. The generalized beam ${ℬ}_{𝒗,W}^{\mathbb{Z}}$ is defined by

With 4.13, 4.12 is equivalent to stating that each configuration is located in some generalized $A$-beam. This makes it easier to argue if a run is thin, as demonstrated in the following lemma. We remark that the following result does not depend on whether the VASS has full support.

In this subsection we fix a geometrically $2$-dimensional $d$-VASS $G=(Q,T)$ that is proper, and assume that $supp(\mathrm{Cyc}(G))=[d]$. So by 4.5, there exists $i_1\ne i_2\in [d]$ such that $I:=\{i_1,i_2\}$ is a sign-reflecting projection of $\mathrm{Cyc}(G)$ with respect to ${\mathbb{Q}}_{\ge 0}^d$. Moreover, let ${𝒖}_1,{𝒖}_2\in {\mathbb{N}}^d$ be the canonical horizontal and vertical vectors given by 4.6. We have ${𝒖}_1(i_2)=0$ and ${𝒖}_2(i_1)=0$. Observe that we can assume $\Vert {𝒖}_1\Vert ,\Vert {𝒖}_2\Vert \le 2\chi {(G)}^2$, as they can be derived from effects of simple cycles in $G$.