Reachability in Symmetric VASS

In this paper we investigate subclasses of $d$-vass which are symmetric, meaning their sets of transitions are invariant under certain permutations of the coordinates $\{1,\mathrm{\dots },d\}$. Our study is parametric in the choice of a group of permutations $G\le S_d$ of coordinates, and our objective is to analyze the gain in complexity to be achieved when the input to the reachability problem is restricted to $G$-vass, the subclass of those $d$-vass whose sets of transitions are invariant under permutations $\sigma \in G$. In one extreme case, when $G$ is the trivial permutation group $I_d$ containing just the identity permutation, $G$-vass are just general $d$-vass. In another extreme case, when $G=S_d$ is the symmetric group of degree $d$, transitions of $G$-vass are invariant under all permutations of coordinates. The two extreme cases may be combined. For instance, one can consider the permutation group $G=I_n\wr S_d\le S_{nd}$ of degree $nd$ containing all permutations that are identity inside each of the $n$-element blocks:

but permute arbitrarily the whole blocks.

Our principal motivation is to exploit symmetry of a model in order to lower the prohibitively high complexity of the reachability problem in the general case. Another motivation comes from the model of data vass [13, 15, 20] extending plain vass with data. In terms of Petri nets, the extension allows tokens to carry data value coming from some infinite countable set, and allows transitions to test (dis)equalities between data values of involved tokens. When $G=I_n\wr S_d\le S_{nd}$, the $G$-vass are exactly data vass of dimension $n$, where the set of data values is restricted to be finite¹¹1 The other way around, the $n$-dimensional data vass can be defined as $G$-vass, where $G=I_n\wr S_{\omega }$ combines the trivial group $I_n$ with the symmetric group $S_{\omega }$ of infinite countable degree. , of size $d$. It is not known if the reachability problem is decidable for data vass, and our current study may shed some more light on this hard open problem.

Intuitively speaking, the larger the group $G$, the lower the complexity of the reachability problem, since whenever $G\le H$, every $H$-vass is automatically a $G$-vass. The main contribution of this paper is twofold. First, we concentrate on the potentially easiest cases, namely symmetric groups $S_d$, and discover a huge complexity drop: regardless of dimension $d\ge 2$, the reachability problem is PSpace-complete for vass invariant under symmetric groups.²²2 In dimension 1 the permutation group $G$ is irrelevant, and the problem is NL- or NP-complete, for input represented in unary or binary, respectively [10]. We also prove the same complexity for another potentially easy case, namely for the alternating groups $A_d$: again, regardless of dimension $d\ge 3$, the reachability problem is PSpace-complete for vass invariant under alternating groups. Both the PSpace decision procedures are designed for a fixed dimension $d$, but work equally well when $d$ is part of input. We thus get uniform PSpace upper bound for vass invariant under symmetric (resp. alternating) groups. At the other side, we prove that cyclic groups $Z_d$ are hard, namely the reachability problem for $d$-vass invariant under $Z_d$ is as hard as in $\mathrm{\Theta }(d)$-vass.

The case of trivial group $G=I_d$ coincides with general $d$-vass. As our second contribution we investigate combinations of symmetric groups and trivial groups, providing one positive and one negative result. On one hand, when $G=I_n\wr S_d\le S_{nd}$ (as discussed above) and $n\ge 2$, the reachability problem is as hard as in case of $(n-1)d$-vass. From the perspective of data vass this may be interpreted as a bad news: the complexity grows with the increasing number $d$ of data values. On the other hand, we investigate another combination of the two groups, namely $G=S_d\wr I_n\le S_{dn}$ containing all permutations that independently and arbitrarily permute each of $d$-element blocks:

but preserve each of the blocks. In this case we provide an exponential-time reduction to $n$-vass, i.e., this time the complexity is independent of the degree $d$ of the symmetric group. The complexity in this case is thus (significantly) lower than for $I_n\wr S_d$. This is in agreement with $I_n\wr S_d$ being a subgroup of $S_d\wr I_n$, up to isomorphism of permutation groups.

For $d\in {\mathbb{N}}_{+}=\mathbb{N}\setminus \{0\}$, we define $d$-dimensional vector addition systems with states, denoted shortly as $d$-vass, or simply vass when the dimension $d$ is irrelevant or clear from the context. A $d$-vass $𝒱=(Q,T)$ consists of a finite set $Q$ of states and a finite set of transitions $T\subseteq Q\times {\mathbb{Z}}^d\times Q$. A configuration $c$ of $𝒱$ consists of a state $q\in Q$ and a nonnegative vector $𝐰\in {\mathbb{N}}^d$, and is written as $c=q(𝐰)$. A transition $t=(q,𝐯,q^{\prime })$ induces steps

between configurations, where ${𝐰}^{\prime }=𝐰+𝐯$. We refer to the vector $𝐯\in {\mathbb{Z}}^d$ as the effect of the transition $(q,𝐯,q^{\prime })$ or of an induced step. The norm of a transition $t=(q,𝐯,q^{\prime })$ is defined as $\Vert t\Vert :=\Vert 𝐯\Vert$. Similarly, for a configuration $c=q(𝐰)$, we define $\Vert c\Vert :=\Vert 𝐰\Vert$. The norm of a vass $𝒱$ is the maximal norm of its transitions, i.e., $\Vert 𝒱\Vert :={\max }_{t\in T}\Vert t\Vert$.

A run $\pi$ in $𝒱$ is a sequence of steps with the proviso that the target configuration of every step matches the source configuration of the next one:

We say that the run $\pi$ is from $c_0$ to $c_n$, call $c_0,c_n$ the source and the target configuration of the run, respectively, and write $c_0\stackrel{\pi }{⟶}{c}_n$. When the source configuration $c_0$ is clear from the context, we may identify a run (2) from $c_0$ with the sequence $t_1\mathrm{\dots }{t}_n$ of transitions fired. The effect of a run is the sum of effects of all steps, and its length is the number $n$ of steps. We also write $c\stackrel{}{⟶}{c}^{\prime }$ if there is some run from $c$ to $c^{\prime }$. We often use the natural operation of concatenation of runs: if $\alpha :c\stackrel{}{⟶}{c}^{\prime }$ and $\beta :c^{\prime }\stackrel{}{⟶}{c}^{\prime \prime }$ then $(\alpha ;\beta ):c\stackrel{}{⟶}{c}^{\prime \prime }$, assuming that the target configuration of the former run coincides with the source configuration of the latter one. For convenience, we allow ourselves to drop this assumption and use the convention that the latter run $\beta$ is implicitly shifted so that its source matches the target of $\alpha$, as long as the shifted $\beta$ is still a run. Under this convention, we write ${\alpha }^n$ for $n$-fold concatenation of $\alpha$.

In the sequel we refer to the state graph of a vass $𝒱=(Q,T)$, a directed graph $(Q,E)$ whose nodes are states $Q$, and edges $E\subseteq Q^2$ are those pairs $(q,q^{\prime })$ for which there is a transition $(q,𝐯,q^{\prime })\in T$, for some $𝐯\in {\mathbb{Z}}^d$. This graph may contain self-loops.

One of the most fundamental computational problems studied in the setting of vass is the reachability problem (for the sake of this paper we prefer to formulate the problem for a fixed dimension $d$):

$d$-vass-Reach: given a $d$-vass $𝒱$ together with two configurations, source $s$ and target $t$, one asks if $𝒱$ has a run from $s$ to $t$.

Complexity of this problem in subclasses of symmetric vass, to be defined below, is the main topic studied in this paper. An input to the problem is a triple $(𝒱,s,t)$. For simplicity, such a triple $(𝒱,s,t)$, or a pair $(𝒱,s)$ with just the source state, we also call a vass, hoping that this does not lead to confusion. We also use shorthands $||𝒱,s||:=\max \{||𝒱||,||s||\}$ and $||𝒱,s,t||:=\max \{||𝒱||,||s||,||t||\}$.

Let $S_d$ denote the symmetric group containing all permutations of $[d]$. Permutations of $[d]$ act on vectors $𝐰\in {\mathbb{Z}}^d$ by permuting dimensions, namely $\sigma \in S_n$ maps $𝐰$ to the vector $\sigma (𝐰)$ defined by $\sigma (𝐰)(i)=𝐰({\sigma }^{-1}(i))$, or equivalently $\sigma (𝐰)(\sigma (i))=𝐰(i)$. Treating a vector as a function $𝐰:[d]\to \mathbb{Z}$, we may write

We naturally extend this action to transitions, $t=(q,𝐯,q^{\prime })⟼\sigma (t)=(q,\sigma (𝐯),q^{\prime })$, and likewise to steps, runs, etc., as expected. Given a group of permutations $G\le S_d$, by a $G$-vass, we mean any $d$-vass $𝒱=(Q,T)$ whose transitions are invariant under the action of $G$, namely for every permutation $\sigma \in G$ and transition $t\in T$ we have $\sigma (t)\in T$. Thus, for every $G\le S_d$, we identify a subclass of $d$-vass admitting the invariance property. In the most restrictive case of $G=S_d$, we get the subclass of $d$-vass invariant under all permutations of dimensions. In the less restrictive case of trivial group $I_d=\{{\text{Id}}_d\}$, we get the whole class of all $d$-vass.

In our investigations we always assume that a group $G\le S_d$ (and hence also the dimension of vass) is fixed.³³3 Nevertheless, all our subsequent PSpace decision procedures are uniform with respect to dimension, namely they work within the same complexity bounds if dimension $d$ is part of input. The vass reachability problem, when its input is restricted to $G$-vass for a fixed permutation group $G$, we call $G$-vass-Reach. For the trivial group $G=I_d=\{{\text{Id}}_d\}$ we get $d$-vass-Reach.

The set of transitions of a $G$-vass is determined uniquely by representatives of orbits, i.e., by representatives of the equivalence relation on transitions: $t{\equiv }_G{t}^{\prime }$ if $t=\sigma (t^{\prime })$ for some $\sigma \in G$. Unfolding the action of $G$ on transitions, $(q,𝐯,p){\equiv }_G(q^{\prime },{𝐯}^{\prime },p^{\prime })$ if and only if $q=q^{\prime }$, $p=p^{\prime }$, and $𝐯=\sigma ({𝐯}^{\prime })$ for some $\sigma \in G$. Equivalence classes of ${\equiv }_G$ are called $G$-orbits of transitions, or simply orbits when the group is clear from the context. When measuring the size of input we assume a succinct representation, where transitions $T$ of a $G$-vass are given by orbit representatives, i.e., by a subset $\tilde{T}\subseteq T$ containing one transition from every orbit. By the size of such a representation $(Q,\tilde{T})$ of a $G$-vass $𝒱$ we mean the bitsize of its description, e.g.,

where $\Vert \tilde{T}\Vert ={\max }_{t\in \tilde{T}}\Vert t\Vert$. Note that $|𝒱|$ is independent of a choice of orbit representatives, and logarithmic in terms of $\Vert \tilde{T}\Vert$.

Whenever $G^{\prime }\le G\le S_d$, i.e., $G^{\prime }$ is a permutation subgroup of $G$, (a representation of) a $G$-vass may be canonically transformed into (a representation of) a $G^{\prime }$-vass in two different ways. Let $𝒱=(Q,T)$ be a $G$-vass. On one hand, $𝒱$ is itself a $G^{\prime }$-vass, as its transitions are automatically invariant under the action of $G^{\prime }$, but the representation of $𝒱$ seen as a $G^{\prime }$-vass may be exponentially larger than its representation when seen as $G$-vass (since the number of $G^{\prime }$-orbits of $T$ may be exponentially larger than the number of $G$-orbits of $T$). This yields an exponential (but not necessarily polynomial) reduction from $G$-vass-Reach to $G^{\prime }$-vass-Reach. On the other hand, a representation of $𝒱$ is automatically a representation of another $G^{\prime }$-vass ${𝒱}^{\prime }=(Q,T^{\prime })$, where the set of transitions $T^{\prime }\subseteq T$ may be of exponentially smaller size than $T$, but the number of $G^{\prime }$-orbits of $T^{\prime }$ is the same as the number of $G$-orbits of $T$. Clearly, every run of ${𝒱}^{\prime }$ is a run of $𝒱$, but the converse does not hold in general.

An important relaxation of reachability is $\mathbb{Z}$-reachability, where one considers a relaxed notion of configurations, namely $\mathbb{Z}$-configurations $Q\times {\mathbb{Z}}^d$ instead of $Q\times {\mathbb{N}}^d$. Contrary to configurations, values in $\mathbb{Z}$-configurations may drop below 0. We define $\mathbb{Z}$-runs exactly like runs, but using $\mathbb{Z}$-configurations instead of configurations. Each $\mathbb{Z}$-run, and hence also each run, induces a unique path in the state graph. Conversely, every path in the state graph gives rise to multiple different $\mathbb{Z}$-runs, depending on the choice of source vector, and of transitions witnessing consecutive edges of a path.

The $\mathbb{Z}$-reachability problem asks, given a $G$-vass $(𝒱,s,t)$, if $𝒱$ has a $\mathbb{Z}$-run from $s$ to $t$. We prove that the problem lies in NP, regardless of the choice of dimension $d$ of vass and of the group $G\le S_d$. This observation will be used later in proofs of main results.

The lemma does not follow immediately from NP upper bound for $\mathbb{Z}$-reachability in vass, as the input is represented more succinctly in our case. In the proof we use the integer analogue of Caratheodory’s theorem [7] to get a small solution property: if there is a $\mathbb{Z}$-run between two given configurations then there is one using only a subset of transitions of polynomial size. By guessing this subset we reduce to the $\mathbb{Z}$-reachability problem in vass, which is in NP.

We show a reduction from the bounded reachability problem for $1$-vass, which is known to be PSpace-complete [8]. The input to this problem consists of a $1$-vass $(𝒱,s,f)$ and a number $M\in \mathbb{N}$ represented in binary, and we ask if $𝒱$ has a run $s\stackrel{}{⟶}f$ with all configurations bounded by $M$. For simplicity, we assume that the vector of a configuration of a $1$-vass $q(n)$ is just a nonnegative integer $n\in \mathbb{N}$, and the effect of a transition $(q,z,p)$ is just an integer $z\in \mathbb{Z}$. W.l.o.g. we assume that effects of transitions of a $1$-vass are nonzero and at most $M$.

Fix an arbitrary dimension $d\ge 2$. Given a $1$-vass $(𝒱,s,f)$ and $M$, where $𝒱=(Q,T)$, we construct a $G$-vass ${𝒱}^{\prime }=(Q^{\prime },T^{\prime })$ of dimension $d$ whose states $Q^{\prime }:=Q\cup \left\{⟨q,t⟩\right|q\in Q,t\in T\}$ extend $Q$ by additional auxiliary states, and whose transitions $T^{\prime }$ are defined below. The idea is to represent a configuration $q(n)$ of $𝒱$ bounded by $M$ ($n\le M$), by a configuration

of ${𝒱}^{\prime }$, while pairs $⟨q,t⟩$ are additional auxiliary states. We define the set $T^{\prime }$ of transitions by providing a set of orbit representatives $\tilde{T}\subseteq T^{\prime }$. Below, we use $z\in {\mathbb{N}}_{+}$ to range over positive integers, and use the vectors

that have value $M+z$ (resp. $-M-z$) on all coordinates except coordinate $d$ which has the opposite value. We also use $𝐯=(M,\mathrm{\dots },M,-M)$. The set $\tilde{T}$ is defined as follows:

• $\mathrm{■}$

  For every $t=(p,z,q)\in T$, we put into $\tilde{T}$ two transitions (recall that $z\in {\mathbb{N}}_{+}$)

  $$\tilde{t}=(p,{𝐯}_z,⟨q,t⟩)t^{-}=(⟨q,t⟩,-𝐯,q);$$

• $\mathrm{■}$

  For every $t=(p,-z,q)\in T$, we put into $\tilde{T}$ two transitions

  $$t^{+}=(p,𝐯,⟨p,t⟩)\tilde{t}=(⟨p,t⟩,{𝐯}_{-z},q).$$

As all vectors ${𝐯}_z,{𝐯}_{-z}$ and $𝐯$ are constant except for one coordinate, we notice that the size of $T^{\prime }=\left\{\sigma (t)\right|t\in \tilde{T},\sigma \in G\}$ is at most $|T^{\prime }|\le d\cdot |\tilde{T}|$. This is however not relevant for the reduction, as ${𝒱}^{\prime }$ is represented by $\tilde{T}$, and not by $T^{\prime }$.

We argue that there is a run $s\stackrel{}{⟶}f$ in $𝒱$ whose all configurations are bounded by $M$, if and only if $\overline{s}\stackrel{}{⟶}\overline{f}$ in ${𝒱}^{\prime }$. For the “only if” direction we observe that every step $c\stackrel{t}{⟶}{c}^{\prime }$ in $𝒱$ which is bounded by $M$ is simulated by two steps $\overline{c}\stackrel{}{⟶}{c}^{\prime }\stackrel{}{⟶}{\overline{c}}^{\prime }$ in ${𝒱}^{\prime }$, for some intermediate configuration $c^{\prime }$ with an auxiliary state. Indeed, when $t=(p,z,q)$, a step $p(n)\stackrel{t}{⟶}q(n+z)$ of $𝒱$ which is bounded by $M$ ($n+z\le M$), is simulated in ${𝒱}^{\prime }$ by the following two steps:

In the other case, when $t=(p,-z,q)$, a step $p(n)\stackrel{t}{⟶}q(n-z)$ of $𝒱$ which is bounded by $M$ ($n\le M$), is simulated in ${𝒱}^{\prime }$ by the following two steps:

For the “if” direction, we consider a configuration $\overline{q(n)}=q(n,\mathrm{\dots },n,2M-n)$, and analyze all possible two-step runs in ${𝒱}^{\prime }$ starting from $\overline{q(n)}$: $\overline{q(n)}\stackrel{}{⟶}{c}^{\prime }\stackrel{}{⟶}{c}^{\prime \prime }.$ By definition of $T^{\prime }$, we deduce that the only possible such two-step runs are of the form (3) or (4). Indeed, the first transition may be only $\tilde{t}$ for some $t=(q,z,p)\in T$, or $t^{+}$ for some $t=(q,-z,p)\in T$, and then the next transition is uniquely determined by the auxiliary state. In particular, we observe that only transitions from $\tilde{T}$ can be used, i.e., all other transitions $T^{\prime }\setminus \tilde{T}$ are useless if one starts from a configuration of the form $\overline{p(n)}$. In consequence, if $\overline{s}\stackrel{}{⟶}\overline{f}$ in ${𝒱}^{\prime }$, we have also a run $s\stackrel{}{⟶}f$ in $𝒱$ whose all configurations are bounded by $M$, as required. Correctness of the reduction follows. $◀$

Consider a $G$-vass $(𝒱,s,t)$, where $s=q(𝐰)$ and $t=q^{\prime }({𝐰}^{\prime })$. We say that $(𝒱,s)$ is forward pumpable if $𝒱$ has a run $q(𝐰)\stackrel{}{⟶}q(𝐰+𝐞)$ for some $𝐞\ge \overline{1}$. Symmetrically, $(𝒱,t)$ is backward pumpable if $({𝒱}^{\text{rev}},t)$ is forward pumpable where ${𝒱}^{\text{rev}}$, the reverse of $𝒱$, is obtained by replacing each transition $(q,𝐯,q^{\prime })$ of $𝒱$ by its reverse $(q^{\prime },-𝐯,q)$. Equivalently, $𝒱$ has a run $q^{\prime }({𝐰}^{\prime }+{𝐞}^{\prime })\stackrel{}{⟶}{q}^{\prime }({𝐰}^{\prime })$ for some ${𝐞}^{\prime }\ge \overline{1}$. Finally, $(𝒱,s,t)$ is pumpable if $(𝒱,s)$ is forward pumpable, and $(𝒱,t)$ is backward pumpable. We prove that reachability reduces to $\mathbb{Z}$-reachability, when the group $G$ is transitive and vass are pumpable.

Let $G\le S_d$. We start by proving the following equality for all $i,j\in [d]$:

When $i=j$, the equality follows immediately from the Orbit-Stabilizer Theorem. Otherwise, suppose $i\ne j$ and take any permutation ${\sigma }_{ij}\in G$ such that ${\sigma }_{ij}(i)=j$ (it exists as $G$ is transitive). By post-composing with ${\sigma }_{ij}$ we get a bijection $\sigma \mapsto {\sigma }_{ij}\circ \sigma$ between permutations $\sigma \in G$ that satisfy $\sigma (i)=i$, and permutations $\sigma \in G$ that satisfy $\sigma (i)=j$. In consequence, we get the equality (5):

Consider a $G$-vass $𝒱$ and two configurations $s=q(𝐯)$ and $t=q^{\prime }({𝐯}^{\prime })$, and suppose $𝒱$ has a $\mathbb{Z}$-run $\gamma$ from $q(𝐯)$ to $q^{\prime }({𝐯}^{\prime })$, and two runs

for some $𝐞,{𝐞}^{\prime }\ge \overline{1}$. We argue that $𝒱$ has a run $q(𝐯)\stackrel{}{⟶}{q}^{\prime }(𝐯)$. W.l.o.g. we can assume that $\alpha$ is increasing, i.e., every coordinate of $𝐯+𝐞$ is greater than the greatest coordinate of $𝐯$ (otherwise we replace $\alpha$ by its $n$-fold concatenation ${\alpha }^n:q(𝐯)\stackrel{}{⟶}q(𝐯+n𝐞)$, for sufficiently large $n\in \mathbb{N}$). Symmetrically, we can assume that ${\alpha }^{\prime }$ is decreasing, i.e., every coordinate of ${𝐯}^{\prime }+{𝐞}^{\prime }$ is greater than the greatest coordinate of ${𝐯}^{\prime }$.

Let $G=\{{\sigma }_1,\mathrm{\dots },{\sigma }_m\}$, where ${\sigma }_1={\text{Id}}_d$ is the identity permutation on $[d]$, and let

As $\alpha$ is increasing and ${\sigma }_1(\alpha )=\alpha$, the concatenation of runs

is forcedly a run from $q(𝐯)$ to $q(𝐯+\mathrm{\Delta })$. Symmetrically, as ${\alpha }^{\prime }$ is decreasing and ${\sigma }_1({\alpha }^{\prime })={\alpha }^{\prime }$, the concatenation of runs ${\tilde{\alpha }}^{\prime }={\sigma }_m({\alpha }^{\prime });\mathrm{\dots };{\sigma }_2({\alpha }^{\prime });{\sigma }_1({\alpha }^{\prime })$ is forcedly a run from $q^{\prime }({𝐯}^{\prime }+{\mathrm{\Delta }}^{\prime })$ to $q^{\prime }({𝐯}^{\prime })$. We argue that $\mathrm{\Delta }(j)=\mathrm{\Delta }(k)$ for every $j,k\in [d]$, i.e., the effect of $\tilde{\alpha }$ is a constant vector. Indeed, by point-wise expansion of the equality

and using the equality (5) to deduce that for every $\mathrm{\ell }$, the value of $\mathrm{\ell }$th coordinate $𝐞(\mathrm{\ell })$ of $𝐞$ appears the same number of times on both sides of the equality below, we compute:

Therefore, $\mathrm{\Delta }=\overline{n}$ for some $n\in {\mathbb{N}}_{+}$. Analogously we prove that ${\mathrm{\Delta }}^{\prime }=\overline{n^{\prime }}$ for some $n^{\prime }\in {\mathbb{N}}_{+}$. Let $\tilde{\mathrm{\Delta }}=\overline{(n\cdot n^{\prime })}$. Since $\tilde{\mathrm{\Delta }}=n^{\prime }\cdot \mathrm{\Delta }=n\cdot {\mathrm{\Delta }}^{\prime }$, we may construct two runs that pump forward and backward by the same vector $\tilde{\mathrm{\Delta }}$:

Thus, for sufficiently large $m\in {\mathbb{N}}_{+}$, the $m$-fold iterations of $\beta$ and ${\beta }^{\prime }$ are enough to lift the $\mathbb{Z}$-run $\gamma$ into a run, i.e., to ensure that ${\beta }^m;\gamma ;{({\beta }^{\prime })}^m$ is a run from $q(𝐯)$ to $q^{\prime }({𝐯}^{\prime })$. $◀$

Given $d\in {\mathbb{N}}_{+}$ and a transitive permutation group $G\le S_d$, we say that $G$ is fair if there is a polynomial $P$ such that for every $R\in \mathbb{N}$ and every $G$-vass $(𝒱,s)$ with $S:=||𝒱,s||$ and $N:=\Vert 𝒱\Vert$, the implication $(1)⟹(2)$ holds, where

1. (1)

   $𝒱$ has a run $s\stackrel{}{⟶}p(𝐰)$ for some $p\in Q$ and $𝐰$ of norm $\Vert 𝐰\Vert >P(N)\cdot (S+R)$,

2. (2)

   $𝒱$ has a run $s\stackrel{}{⟶}p(𝐰)$ for some $p\in Q$ and $𝐰\ge \overline{S+R+1}$.

In words: whenever $(𝒱,s)$ has a run whose target vector exceeds $P(N)\cdot (S+R)$ on some coordinate, $(𝒱,s)$ is guaranteed to have a run whose target vector is greater than $S+R$ on all coordinates; and the property holds for any chosen $R\in \mathbb{N}$.

We start with some preparatory definitions. A vass is called strongly connected if its state graph is so. A vass $𝒱=(Q,T)$ is called sequential, if it can be partitioned into a number of strongly connected vass ${𝒱}_1=(Q_1,T_1),\mathrm{\dots },{𝒱}_k=(Q_k,T_k)$ with pairwise disjoint state spaces, called components of $𝒱$, and $k-1$ transitions $u_i=(q_i,{𝐯}_i,q_i^{\prime })$, for $i\in [k-1]$, where $q_i\in Q_i$ and $q_i^{\prime }\in Q_{i+1}$, called bridges of $𝒱$ (see Fig. 1). For every non-sequential vass $(𝒱,s,t)$ there is a finite set $W=\{{𝒱}^1,\mathrm{\dots },{𝒱}^{\mathrm{\ell }}\}$ such that each ${𝒱}^j$ is a sequential vass, and $s\stackrel{}{⟶}t$ in $𝒱$ if and only if $s\stackrel{}{⟶}t$ in ${𝒱}^j$ for some $j\in [\mathrm{\ell }]$. The set $W$, called sequential decomposition of $𝒱$ in the sequel, may be computed based on the decomposition of the state graph of $𝒱$ into strongly connected components.

Assume an input $G$-vass $(𝒱,s,t)$, where $𝒱=(Q,T)$, $s=q(𝐯)$ and $t=p(𝐰)$, represented by orbit representatives $\tilde{T}\subseteq T$. The PSpace decision procedure to check if $s\stackrel{}{⟶}t$, to be described below, proceeds in several steps.

As the first step, the decision procedure decomposes the state graph of $𝒱$ into strongly connected components, and nondeterministically picks up one sequential vass from the sequential decomposition of $(𝒱,s,t)$. From now on we may thus assume, w.l.o.g., that $𝒱$ is sequential with $k$ components ${𝒱}_1,\mathrm{\dots },{𝒱}_k$, the configuration $s$ belongs to the first component, and $t$ to the last one. The number $k$ of components is bounded by the number $|Q|$ of states of $𝒱$. Let $R:=|Q|\cdot \Vert 𝒱\Vert$. Thus, for every two states $p,p^{\prime }$ from the same component of $𝒱$, there is a path from $p$ to $p^{\prime }$ that decreases each counter by at most $R$.

For $M\in {\mathbb{N}}_{+}$, we say that a configuration $p(𝐰)$ is bounded by $M$ if $\Vert 𝐰\Vert \le M$. We also say that the first component $({𝒱}_1,s)$ is bounded by $M$ if every configuration $c$ reachable in this component from $s$ (i.e, $c$ satisfying $s\stackrel{}{⟶}c$) is bounded by $M$. Symmetrically, we say that the last component $({𝒱}_k,t)$ is reverse bounded by $M$ if every configuration $c$ reverse reachable from $t$ (i.e., $c$ satisfying $c\stackrel{}{⟶}t$) in this component is bounded by $M$.

As the second step, the decision procedure iteratively removes either the first or the last component from $(𝒱,s,t)$ until the following two conditions are met, for $N:=\Vert 𝒱\Vert$ and $S=||𝒱,s,t||$:

• $\mathrm{■}$

  the first component is not bounded by $P(N)\cdot (S+R)$, and

• $\mathrm{■}$

  the last component is not reverse bounded by $P(N)\cdot (S+R)$,

where $P$ is the polynomial given by the definition of a fair group. In particular, the first condition implies (1) for $({𝒱}_1,s)$, and the second one implies (1) for $({𝒱}_k^{\text{rev}},t)$. Suppose the first component is bounded by $P(N)\cdot (S+R)$ (the symmetric case, when the last component is reverse bounded by $P(N)\cdot (S+R)$, is treated in the same way). One iteration of the removal procedure proceeds as follows, depending on whether $k=1$ or $k>1$:

If this component is the only one, the procedure checks in PSpace if $s\stackrel{}{⟶}t$, and terminates. The check is done by a standard nondeterministic walk through the graph of configurations reachable from $s$, which starts at the source configuration $s$, and in every iteration moves to a nondeterministically chosen successor of the current configuration. It terminates when $t$ is reached (and answers positively), or when the counter of so far visited configurations exceeds

the total number of configurations bounded by $P(N)\cdot (S+R)$. The memory size, namely the bitsize of a single configuration, and of the value of the counter, are both polynomially bounded, and hence the whole procedure works in (nondeterministic) PSpace.

Otherwise, let $u_1=(p,𝐮,p^{\prime })$ be the first bridge. We observe that if $𝒱$ has a run $s\stackrel{}{⟶}t$, then its last configuration $p(𝐰)$ in the first component is necessarily bounded by $P(N)\cdot (S+R)$. In consequence, since the bridge transition may increase the norm by at most $N$, the first configuration $p^{\prime }({𝐰}^{\prime })$ of the run in the second component, where ${𝐰}^{\prime }=𝐰+𝐮$, is forcedly bounded by $P(N)\cdot (S+R)+N$. Relying on this observation, the decision procedure nondeterministically chooses a vector $𝐰$ with $\Vert 𝐰\Vert \le P(N)\cdot (S+R)$, and checks in PSpace if $q(𝐯)\stackrel{}{⟶}p(𝐰)$ in the first component, similarly as above. Then the procedure removes the first component from $𝒱$, and takes $s^{\prime }=p^{\prime }({𝐰}^{\prime })=p^{\prime }(𝐰+𝐮)$ as the source configuration, thus obtaining a new $G$-vass $({𝒱}^{\prime },s^{\prime },t)$ with one less component than $(𝒱,s,t)$.

This removal is iteratively repeated until either the procedure terminates, or produces a $({𝒱}^{\prime },s^{\prime },t)$ with the first component not bounded by $P(N^{\prime })\cdot (S^{\prime }+R)$, and the last component not reverse bounded by $P(N^{\prime })\cdot (S^{\prime }+R)$, where $N^{\prime }:=\Vert {𝒱}^{\prime }\Vert$ and $S^{\prime }:=||{𝒱}^{\prime },s^{\prime },t^{\prime }||$. The bound on the norm $N^{\prime }$ of the vass cannot increase, and so $N^{\prime }\le N$. However, in each iteration the bound on norm $S^{\prime }$ of the new source vector ${𝐰}^{\prime }$ increases, compared to the bound $S$ on the norm of the previous source vector $𝐯$, by a multiplicative factor $𝒪(P(N)\cdot |Q|)$, namely

and therefore the bitsize of the source vector increases by (bounding roughly) at most $𝒪(\log (P(N)\cdot |Q|))\cdot d$. As the number of iterations is bounded by $|Q|$, the final bitsize is polynomial in the input size, and therefore all the iterations are doable in PSpace. Note that due to iterative increase of $S^{\prime }$, the first (resp. last) component not bounded (resp. not reverse bounded) by $P(N^{\prime })\cdot (S^{\prime }+R)$ in some iteration may become bounded (resp. reverse bounded) in subsequent iterations.

Finally, the procedure arrives at a sequential $G$-vass $(𝒱,s,t)$, $s=q(𝐯)$, $t=p(𝐰)$, whose first component is not bounded by $P(N)\cdot (S+R)$, and whose last component is not reverse bounded by $P(N)\cdot (S+R)$. As $G$ is fair, there is a configuration $c$ reachable from $s$ in the first component, and a configuration $c^{\prime }$ reverse reachable from $t$ in the last component (i.e., $t$ is reachable from $c^{\prime }$), both with vectors $\ge \overline{S+R+1}$:

As $R$ is large enough so that every two states in the same component are connected by a path that decreases each counter by at most $R$, we have some runs

in the first and the last component, respectively, with $\overline{𝐯},\overline{𝐰}\ge \overline{S+1}$. As $\Vert s\Vert ,\Vert t\Vert \le S$, this means that ${𝒱}^{\prime }$ is pumpable. Since $G$ is transitive, Lemma 4 applies. In the last step, the decision procedure checks if there is a $\mathbb{Z}$-run from $s$ to $t$, which is doable in NP due to Lemma 1. $◀$

Consider an $S_d$-Vass $𝒱=(Q,T)$ and a configuration $s=q(𝐯)$. Let $S:=||𝒱,s||$, let $R\in \mathbb{N}$ be any constant, and $B:=3S+2R$. We demonstrate that $S_d$ is fair, and that this property is witnessed by the constant polynomial $P(x)=3d$. Towards this we prove a slightly stronger fact: we assume that $𝒱$ has a run $\pi :q(𝐯)\stackrel{}{⟶}p(𝐰)$ with $\Vert 𝐰\Vert >B\cdot d$, and construct a run ${\pi }^{\prime }:q(𝐯)\stackrel{}{⟶}p({𝐰}^{\prime })$ whose target vector satisfies ${𝐰}^{\prime }\ge \overline{S+R+1}$.

W.l.o.g. assume that $𝐰(d)>B\cdot d$. For $i=1,\mathrm{\dots },d-1$ we inductively construct runs ${\pi }_i:q(𝐯)\to p({𝐰}_i)$ satisfying

We start with ${\pi }_0:=\pi$. Assuming ${\pi }_{i-1}$ has already been constructed, we construct ${\pi }_i$ as follows. If ${𝐰}_{i-1}(i)>S+R$ then we take ${\pi }_i:={\pi }_{i-1}$. Otherwise, we split ${\pi }_{i-1}$ into ${\pi }_{i-1}=\alpha ;\beta ,$

where $\beta$ is the longest suffix of the run in which the value of coordinate $d$ does not drop below $B\cdot (d-i)$.

Therefore, , as otherwise $\beta$ would be longer. Let $\mathrm{\Delta }={𝐰}_{i-1}-𝐮$ be the difference between the target and source of $\beta$. We observe that the value of coordinate $d$ is increased by $\beta$ by at least

while the value of coordinate $i$ is increased by at most $\mathrm{\Delta }(i)\le {𝐰}_{i-1}(i)\le S+R.$ Therefore, $\mathrm{\Delta }(d)-\mathrm{\Delta }(i)>S+R$. In consequence, $\beta$ contains some $k$ steps

induced by transitions $t_1=(q_1,{𝐞}_1,q_1^{\prime }),\mathrm{\dots },t_k=(q_k,{𝐞}_k,q_k^{\prime })$ with effects

such that ${𝐞}_{\mathrm{\ell }}(d)>{𝐞}_{\mathrm{\ell }}(i)$ for $\mathrm{\ell }\in [k]$, that is, each of the steps increases the difference between the values of coordinate $d$ and $i$, and moreover

that is, the steps jointly increase the difference between the values of coordinate $d$ and $i$ by more than $S+R$. We may choose a minimal set of transitions $t_1,\mathrm{\dots },t_k$ satisfying (7). Hence, knowing that one step can change the difference between the values of coordinate $d$ and $i$ by at most by $2S$, we may safely assume

that is, the steps jointly increase the difference between the values of coordinate $d$ and $i$ by at most $3S+R$. Let $\sigma =\left(\begin{array}{c}id\\ di\end{array}\right)\in S_n$ be the permutation that swaps coordinates $d$ and $i$ and preserves the others. We define a run ${\pi }_i:q(𝐯)⟶p({𝐰}_i)$ by replacing each transition $t_{\mathrm{\ell }}$ in ${\pi }_{i-1}$ with the transition $\sigma (t_{\mathrm{\ell }})$. Due to the inequality (8), the coordinate $d$ never drops below

in ${\pi }_i$, and ${𝐰}_i(d)>B\cdot (d-i+1)-(3S+R)>B\cdot (d-i)$. Furthermore, due to the inequality (7) we get ${𝐰}_i(i)>S+R$, because the coordinate $i$ was increased by more than $S+R$. Other coordinates are not affected, i.e., their values are the same in ${\pi }_{i-1}$ and ${\pi }_i$. Therefore, the run ${\pi }_i$ satisfies the condition (6), as required.

Finally, we arrive at a run ${\pi }^{\prime }={\pi }_{d-1}:q(𝐯)⟶p({𝐰}_{d-1})$ with ${𝐰}_{d-1}(i)\ge S+R+1$ for every $i\in [d]$, and this completes the proof. $◀$

Membership in PSpace follows immediately by Lemmas 5 and 6, and PSpace-hardness follows by Lemma 2. $◀$