We can now prove Lemma A.1. By using Lemma A.4, we obtain $\pi^{\prime}_{f}$
from $\pi_{f}$ in (C2) such that $path(\pi^{\prime}_{f})=path(\pi_{f})$,
$(q,\bm{u})\xrightarrow{\pi^{\prime}_{f}}_{\mathbb{Q}}(q,\bm{x})$ and
${\llbracket\delta_{t}\rrbracket}\subseteq{\llbracket\bm{x}\rrbracket}$ for
each $t\in\pi^{\prime}_{f}$. Similarly we obtain
$(q,\bm{y})\xrightarrow{\pi^{\prime}_{b}}_{\mathbb{Q}}(q,\bm{v})$ from
$\pi_{b}$ with corresponding support conditions. Let $\pi$ from (C1) be
$\alpha_{1}t_{1}\ldots\alpha_{m}t_{m}$, then for $j\in[m]$ define

$a_{j}=\frac{\Psi(\pi^{\prime}_{f})(t_{j})}{\Psi(path(\pi)(t_{j})},$
$b_{j}=\frac{\Psi(\pi^{\prime}_{b})(t_{j})}{\Psi(path(\pi)(t_{j})},$ $\text{
let }0<\lambda\leq 1\text{ small such that }\forall
j\in[m],c_{j}=\alpha_{j}-\lambda(a_{j}+b_{j})\geq 0,\text{ and }$
$\sigma=c_{1}t_{1}\ldots c_{m}t_{m}$

We can now fire this small fraction $\lambda$ of $\pi^{\prime}_{f}$ and
$\pi^{\prime}_{b}$ in order to arrive at vectors which satisfy the conditions
(2) and (3) of Lemma A.3:

$(q,\bm{u})\xrightarrow{\lambda\pi^{\prime}_{f}}_{\mathbb{Q}_{+}}(q,\bm{x}^{\prime})\text{
where
}{\llbracket\bm{x}\rrbracket}\subseteq{\llbracket\bm{x}^{\prime}\rrbracket},\text{
and}$
$(q,\bm{y}^{\prime})\xrightarrow{\lambda\pi^{\prime}_{b}}_{\mathbb{Q}_{+}}(q,\bm{v})\text{
where
}{\llbracket\bm{y}\rrbracket}\subseteq{\llbracket\bm{y}^{\prime}\rrbracket}.$

Furthermore, we have:

$(q,\bm{x}^{\prime})\xrightarrow{\lambda\sigma}_{\mathbb{Q}}(q,\bm{y}^{\prime}).$

Applying Lemma A.3 to the above run, we get:

$(q,\bm{x}^{\prime})\xrightarrow{\sigma^{\prime}}_{\mathbb{Q}_{+}}(q,\bm{y}^{\prime}),$

and the desired run
$\pi^{\prime}=\lambda\pi^{\prime}_{f}\cdot\sigma^{\prime}\cdot\lambda\pi^{\prime}_{b}$
with
${\llbracket\pi^{\prime}\rrbracket}={\llbracket\pi\rrbracket}={\llbracket\pi^{\prime}\rrbracket}$
and $\Psi(\pi^{\prime})=\Psi(\pi)$.

##  Appendix B Proofs for Section 5

###  B.1. Proof details of Lemma 5.2

The lemma is immediate when $r$ is a nope rule of the form
$(q,\mathbf{nop},q^{\prime})$. We will first prove it in the case when $r$ is
an increment rule of the form $(q,\mathbf{inc}_{i},q^{\prime})$. For the
soundness part, suppose $C\xrightarrow{r}C^{\prime}$. Then, notice that
$g(C)\xrightarrow{1/2^{m}\ r^{b}}D^{\prime}\xrightarrow{1/2^{m}\
r^{e}}g(C^{\prime})$. To prove the completeness part, suppose
$g(C)\xrightarrow{\alpha r^{b}}D^{\prime}\xrightarrow{\beta r^{e}}D$ for some
$\alpha,\beta,D$ and $D^{\prime}$. Since $r^{b}$ decrements $st$ by 1 and also
has a zero-test on $st$, it follows that $g(C)(st)-\alpha=0$ and so
$\alpha=g(C)(st)=1/2^{m}$. By construction of the rule $r^{b}$, it follows
that the values of the counters $c_{i},c_{1-i},st$ and $te$ in $D^{\prime}$
are $g(C)(c_{i})+1/2^{m},g(C)(c_{1-i}),0$ and $1/2^{m}$ respectively. Now,
since $r^{e}$ decrements $te$ by 1 and also has a zero-test on $te$, it
follows that $D^{\prime}(te)-\beta=0$ and so $\beta=D^{\prime}(te)=1/2^{m}$.
By construction of the rule $r^{e}$, it follows that
$\mathsf{state}(D)=q^{\prime}$ and the values of the counters
$c_{i},c_{1-i},st$ and $te$ in $D$ are $D(c_{i}),D(c_{1-i}),1/2^{m}$ and $0$
respectively. Since $D(c_{i})=g(C)(c_{i})+1/2^{m}$ and
$D(c_{1-i})=g(C)(c_{1-i})$, it follows that if we let
$C\xrightarrow{r}C^{\prime}$ in the machine $\mathcal{M}$, then
$g(C^{\prime})=D$.

For the case when $r$ is a doubling rule of the form
$(q,\mathbf{double}_{i},q^{\prime})$, a similar argument applies, where
$\alpha$ and $\beta$ (in both the soundness and the completeness part) will be
$g(C)(c_{i})$ and $2g(C)(c_{i})$ respectively.

###  B.2. Proof details of Theorem 5.3

Suppose $c_{init}$ can reach a final configuration $c_{fin}=(q_{f},n,n)$ for
some number $n$ in $m$ steps. By repeated applications of the soundness part
of the Gadget Simulation lemma (Lemma 5.2), it follows that $g(c_{init})$ can
reach $D:=g(c_{fin})$ in $2m$ steps. Since $\mathsf{state}(D)=q_{f}$ and
$D(c_{0})=D(c_{1})$, it follows that if we set $\alpha=D(st),\beta=D(c_{0})$,
then by construction of $f^{b}$ and $f^{e}$ we have $D\xrightarrow{\alpha
f^{b},\beta f^{e}}(\overline{q_{f}},\mathbf{0})$.

Suppose $g(c_{init})$ can reach the configuration
$(\overline{q_{f}},\mathbf{0})$ in $2(m+1)$ steps in $\mathcal{C}_{1}$. By
construction of $\mathcal{C}_{1}$, any execution from $C:=g(c_{init})$ to
$C^{\prime}:=(\overline{q_{f}},\mathbf{0})$ must be of the form
$C\xrightarrow{\alpha_{1}r_{1}^{b},\beta_{1}r_{1}^{e}}C_{1}\xrightarrow{\alpha_{2}r_{2}^{b},\beta_{2}r_{2}^{e}}C_{2}\dots
C_{m-1}\xrightarrow{\alpha_{m}r_{m}^{b},\beta_{m}r_{m}^{e}}C_{m}\xrightarrow{\alpha_{m+1}f^{b},\beta_{m+1}f^{e}}C^{\prime}$
for some fractions $\alpha_{1},\beta_{1},\dots,\alpha_{m+1},\beta_{m+1}$ and
some rules $r_{1},\dots,r_{m}$ of the machine $\mathcal{M}$. By the
completeness part of the Gadget Simulation lemma (Lemma 5.2), it follows that
there exists configurations $D_{1},D_{2},\dots,D_{m}$ such that each
$C_{i}=g(D_{i})$ and
$c_{init}\xrightarrow{r_{1}}D_{1}\xrightarrow{r_{2}}D_{2}\dots
D_{m-1}\xrightarrow{r_{m}}D_{m}$. Since $\alpha_{m+1}f^{b}$ is fireable from
$C_{m}$, it must be the case that $\mathsf{state}(C_{m})=q_{f}$. By
construction of the finish gadget, it follows that
$C_{m}(c_{0})=C_{m}(c_{1})$. By construction of the mapping $g$, it follows
that $D_{m}$ is of the form $(q_{f},n,n)$ for some number $n$. Hence,
$c_{init}$ can reach some final configuration in $m$ steps in $\mathcal{M}$.

###  B.3. Proof details of Lemma 5.4

Suppose $C^{\prime}$ is the same as $C$ except that $C^{\prime}(st)=C(st)/2$
and $C^{\prime}(count)=C(count)+1/m$. Let
$\alpha_{1}=C(st)/2,\alpha_{2}=C(st)/2,\alpha_{3}=1/m,\alpha_{4}=1/m$. It can
be verified that
$C\xrightarrow{\alpha_{1}i^{1}}C_{1}\xrightarrow{\alpha_{2}i^{2}}C_{2}\xrightarrow{\alpha_{3}i^{3}}C_{4}\xrightarrow{\alpha_{4}i^{4}}C^{\prime}$.

Suppose
$C\xrightarrow{\alpha_{1}i^{1}}C_{1}\xrightarrow{\alpha_{2}i^{2}}C_{2}\xrightarrow{\alpha_{3}i^{3}}C_{4}\xrightarrow{\alpha_{4}i^{4}}C^{\prime}$
is a run such that $C(te)=0$ and $C(x)=1/m$. Since $i^{1}$ decrements $st$ by
2 and also has a zero-test on $st$, it must be the case that
$\alpha_{1}=C(st)/2$. Hence,

$C_{1}(st)=0,C_{1}(te)=C(st)/2,C_{1}(x)=1/m,C_{1}(count)=C(count)$

Since $i^{2}$ decrements $te$ by 1 and also has a zero-test on $te$, it must
be the case that $\alpha_{2}=C_{1}(te)=C(st)/2$. Hence,

$C_{2}(st)=C(st)/2,C_{2}(te)=0,C_{2}(x)=1/m,C_{2}(count)=C(count)$

Since $i^{3}$ decrements $x$ by 1 and also has a zero-test on $x$, it must be
the case that $\alpha_{3}=C_{2}(x)=1/m$. Hence,

$C_{3}(st)=C(st)/2,C_{3}(te)=1/m,C_{3}(x)=0,C_{3}(count)=C(count)+1/m$

Since $i^{4}$ decrements $te$ by 1 and also has a zero-test on $te$, it must
be the case that $\alpha_{4}=C_{3}(te)=1/m$. Hence,

$C_{4}(st)=C(st)/2,C_{4}(te)=0,C_{4}(x)=1/m,C_{4}(count)=C(count)+1/m$

Hence, the proof is complete.

###  B.4. Proof details of Theorem 5.5

Suppose $g(c_{init})$ can reach $(\overline{q_{f}},\mathbf{0})$ in
$\mathcal{C}_{1}$ in $2(m+1)$ steps by means of a run $\rho$. By applying the
Initialization lemma $m$ times and then using the rule from $in_{0}$ to
$q_{in}$ which does nothing, it follows that starting from $d_{init}$ we can
reach the configuration $D$ where $\mathsf{state}(D)=q_{in}$ and
$D(c_{0})=D(c_{1})=0,D(st)=1/2^{m},D(te)=0,D(x)=1/m$ and $D(count)=1$. Since
$\mathcal{C}$ contains all the rules of $\mathcal{C}_{1}$ and since
$g(c_{init})$ and $D$ agree on their states and the counter values of
$c_{0},c_{1},st$ and $te$, we can simply execute the run $\rho$ from the
configuration $D$ in $\mathcal{C}$ to reach $d_{fin}$.

Suppose $d_{init}$ can reach $d_{fin}$ in exactly $\ell:=4m+1+2(m+1)$ steps in
$\mathcal{C}$. Let $D_{0}:=d_{init}\xrightarrow{}D_{1}\xrightarrow{}D_{2}\dots
D_{\ell-1}\xrightarrow{}d_{fin}:=D_{\ell}$ be such a run. By construction of
the $[0,1]\mathchar 45\relax\mathsf{VASS}_{\mathsf{RL}}^{0?}$ ${\mathsf{cc}}$,
there must be exactly one index $j$ such that $\mathsf{state}(D_{j})=q_{in}$
and $\mathsf{state}(D_{j-1})=in_{0}$ and the rule fired between $D_{j-1}$ and
$D_{j}$ does nothing to the counters. By construction of $\mathcal{C}$, this
means that the steps from $D_{0}$ to $D_{j-1}$ are steps in the initialization
gadget and the steps from $D_{j-1}$ to $D_{\ell}$ are steps in
$\mathcal{C}_{1}$. Since no step in $\mathcal{C}_{1}$ affects the value of the
counter $count$ and since $d_{fin}(count)$ is 1, it follows that
$D_{j-1}(count)=1$. Since the steps from $D_{0}$ to $D_{j-1}$ are steps in the
initialization gadget and since
$\mathsf{state}(D_{0})=\mathsf{state}(D_{j-1})=in_{0}$, by repeated
applications of the Initialization lemma, it follows that $j-1$ must be $4m$
and the values of the counters in $D_{j-1}$ satisfy

$D_{j-1}(c_{0})=D_{j-1}(c_{1})=0,D_{j-1}(st)=1/2^{m},D_{j-1}(te)=0,D_{j-1}(x)=1/m,D_{j-1}(count)=1$

Since the counter values of $D_{j}$ and $D_{j-1}$ are the same, the same
equation holds if we replace $D_{j-1}$ with $D_{j}$. Notice that
$\mathsf{state}(D_{j})=q_{in},D_{j}(c_{0})=D_{j}(c_{1})=D_{j}(te)=0,D_{j}(st)=1/2^{m}$.
Since the run from $D_{j}$ to $d_{fin}$ uses only the rules from
$\mathcal{C}_{1}$, it follows that executing the same sequence of rules also
gives us a run from $g(c_{init})$ to $(\overline{q_{f}},\mathbf{0})$ in
$\mathcal{C}_{1}$ of length $\ell-j=\ell-4m-1=2(m+1)$.

##  Appendix C Proofs for Section 6

###  C.1. Proof details of Lemma 6.2

Let us fix a rule $r=(q,t,q^{\prime})$ in $\mathcal{C}$ with $t=(w,s)$.

For the soundness claim, suppose $C\xrightarrow{\alpha r}C^{\prime}$ in
$\mathcal{C}$. It follows that from $G(C)_{\zeta}$ we can fire $r^{b}$ to
reach a configuration $D$ whose counter values are the same as
$G(C^{\prime})_{\zeta}$. By assumption, $C^{\prime}(x)=0$ for every $x\in s$.
It follows that from $G(C^{\prime})_{\zeta}$ we can fire $r^{m}$ and then
$r^{e}$ to reach the configuration $G(C^{\prime})_{\zeta+2}$.

For the completeness part, suppose $G(C)_{\zeta}\xrightarrow{\alpha
r^{b}}D^{b}\xrightarrow{\beta r^{m}}D^{m}\xrightarrow{\gamma r^{e}}D^{\prime}$
for some $\alpha,\beta,\gamma,\zeta$ and $D^{b},D^{m},D^{\prime}$ such that
$D^{\prime}(ctrl)=\zeta+2$. Let $D=G(C)_{\zeta}$. By construction of $r^{b}$,
it follows that $D^{b}(c)=D(c)+\alpha\bar{w}$ for every counter $c$. By
definition of $D$ and $\bar{w}$, it follows that

(1) $D^{b}(c)\in[0,1]\text{ for every counter }c\neq ctrl.$

Further, since the value of $ctrl$ has increased by 2 between $g(C)_{\zeta}$
and $D^{\prime}$, by construction of the gadget, it follows that
$\beta=\gamma=1$. By construction of $r^{m}$, this means that
$D^{b}(\bar{x})=1$ for every $x\in S$ and so

(2) $D^{b}(x)=0\text{ for every }x\in S.$

Combining equations 1 and 2 and using the definition of the rules $r$ and
$r^{b}$, it follows that there exists $C^{\prime}$ such that
$C\xrightarrow{\alpha r}C^{\prime}$ in $\mathcal{C}$ and
$\mathsf{val}(D^{b})=\mathsf{val}(G(C^{\prime})_{\zeta})$. Notice that since
$\beta=\gamma=1$, by construction of $r^{m}$ and $r^{e}$, it follows that
$\mathsf{val}(D^{b})(c)=\mathsf{val}(D^{\prime})(c)$ for every $c\neq ctrl$.
Since $D^{\prime}(ctrl)=\zeta+2$, we have that
$\mathsf{val}(D^{\prime})=\mathsf{val}(G(C^{\prime}))_{\zeta+2}$. Further,
since $\mathsf{state}(D^{\prime})=\mathsf{state}(G(C^{\prime})_{\zeta+2})$, it
follows that $D^{\prime}=G(C^{\prime})_{\zeta+2}$.

###  C.2. Proof details of Lemma 6.3

Suppose $c_{init}$ can reach $c_{fin}$ in $\mathcal{C}$ in $m$ steps.
Repeatedly applying the soundness part of the control counter simulation lemma
(Lemma 6.2) to every step of this run, it follows that $G(c_{init})_{0}$ can
reach $G(c_{fin})_{2m}$ in $3m$ steps in $\mathcal{M}$.

Suppose $C_{0}:=G(c_{init})_{0}\xrightarrow{}C_{1}\xrightarrow{}C_{2}\dots
C_{3m-1}\xrightarrow{}C_{3m}:=G(c_{fin})_{2m}$ is a run in $\mathcal{M}$. By
construction of $\mathcal{M}$ it follows that for every $0\leq i\leq m-1$,
there exists a rule $r_{i}$ of $\mathcal{C}$ and fractions
$\alpha_{i},\beta_{i},\gamma_{i}$ such that
$C_{3i}\xrightarrow{\alpha_{i}r^{b}}C_{3i+1}\xrightarrow{\beta_{i}r^{m}}C_{3i+2}\xrightarrow{\gamma_{i}r^{e}}C_{3i+3}$.
By construction of $r^{b},r^{m}$ and $r^{e}$, we have
$C_{3i+3}(ctrl)=C_{3i}(ctrl)+\beta_{i}+\gamma_{i}$. Hence,
$2m=C_{3m}(ctrl)=C_{0}(ctrl)+\sum_{0\leq i\leq m-1}(\beta_{i}+\gamma_{i})$.
Since $C_{0}(ctrl)=0$ and since each $\beta_{i}$ and $\gamma_{i}$ is a
fraction, it follows that for every $i$, $\beta_{i}=\gamma_{i}=1$. Hence,
$C_{3i+3}(ctrl)=C_{3i}(ctrl)+2$. Repeatedly applying the completeness part of
the control counter simulation lemma (Lemma 6.2), it follows that there is a
run from $c_{init}$ to $c_{fin}$ using the sequence
$\alpha_{1}r_{1},\alpha_{2}r_{2},\dots,\alpha_{m}r_{m}$, thereby completing
the proof.

##  Appendix D Proof details for Theorem 7.2

In this section, we present the proof details behind Theorem 7.2. To prove
this, we first show that coverability in $\mathbb{Q}_{+}\mathchar
45\relax\mathsf{VASS}_{\mathsf{RL}}$ is $\mathsf{NEXPTIME}$-hard even for a
constant number of counters and even when all the numbers are encoded in
unary. We do this in four stages. The first two stages recall the chain of
reductions starting from Bounded-MPCP and observe some minute details about
those reductions. The next two stages exploit these details in order to prove
the desired hardness result.

### Stage 1: Hardness of structured instances of reachability in
$[0,1]\mathchar 45\relax\mathsf{VASS}_{\mathsf{RL}}^{0?}$.

We first prove that reachability in $[0,1]\mathchar
45\relax\mathsf{VASS}_{\mathsf{RL}}^{0?}$ is $\mathsf{NEXPTIME}$-hard even
under some special constraints on the instances. An instance
$\langle\mathcal{C},c_{init},c_{fin},m\rangle$ of the reachability problem for
$[0,1]\mathchar 45\relax\mathsf{VASS}_{\mathsf{RL}}^{0?}$ is said to be
_structured_ if all the _denominators_ of the initial and the final
configurations are powers of 2. We now show that reachability in
$[0,1]\mathchar 45\relax\mathsf{VASS}_{\mathsf{RL}}^{0?}$ is
$\mathsf{NEXPTIME}$-hard even for structured instances. To do this, we first
trace the chain of reductions starting from Bounded-PCP.

In (Aiswarya et al., 2022, Section 6.1), it was shown that Bounded-PCP is
$\mathsf{NEXPTIME}$-hard even when the bound $\ell$ is restricted to be a
power of 2. By slightly modifying the reduction given in the proof of Theorem
4.2 (by adding more nope instructions if necessary), we can then show that
reachability in $\mathsf{2CM}^{\cdot 2,+1}_{\mathsf{RL}}$ is
$\mathsf{NEXPTIME}$-hard even when the bound on the length is restricted to be
a power of 2. Examining the reduction from reachability in
$\mathsf{2CM}^{\cdot 2,+1}_{\mathsf{RL}}$ to reachability in $[0,1]\mathchar
45\relax\mathsf{VASS}_{\mathsf{RL}}^{0?}$ given in Section 5, we notice that
all the numerators of the initial and the final configurations constructed by
the reduction are all either 0 or 1 and all the denominators are either $1$ or
$m$, where $m$ is the bound on the length of the reachability in the given
$\mathsf{2CM}^{\cdot 2,+1}_{\mathsf{RL}}$. Hence, this immediately implies
that reachability in $[0,1]\mathchar 45\relax\mathsf{VASS}_{\mathsf{RL}}^{0?}$
is $\mathsf{NEXPTIME}$-hard for structured instances.

### Stage 2: Hardness of super-structured instances of coverability in
$\mathbb{Q}_{+}\mathchar 45\relax\mathsf{VASS}_{\mathsf{RL}}$.

Next we prove that coverability in $\mathbb{Q}_{+}\mathchar
45\relax\mathsf{VASS}_{\mathsf{RL}}$ is hard even with some special
constraints on its instances. An instance
$\langle\mathcal{M},c_{init},c_{fin},m\rangle$ of the coverability problem for
$\mathbb{Q}_{+}\mathchar 45\relax\mathsf{VASS}_{\mathsf{RL}}$ is said to be
_structured_ if all the _denominators_ of the initial and the final
configurations are powers of 2. It is said to be _super-structured_ if it is
structured and all the values of the initial and the final configurations are
_at most 1_. We now show that coverability in $\mathbb{Q}_{+}\mathchar
45\relax\mathsf{VASS}_{\mathsf{RL}}$ is $\mathsf{NEXPTIME}$-hard even when
restricted to super-structured instances.

Consider the reduction from reachability in $[0,1]\mathchar
45\relax\mathsf{VASS}_{\mathsf{RL}}^{0?}$ to coverability in
$\mathbb{Q}_{+}\mathchar 45\relax\mathsf{VASS}_{\mathsf{RL}}$ given in Section
6. If the given instance of reachability in $[0,1]\mathchar
45\relax\mathsf{VASS}_{\mathsf{RL}}^{0?}$ is structured, then the reduction
also outputs a structured instance of coverability in $\mathbb{Q}_{+}\mathchar
45\relax\mathsf{VASS}_{\mathsf{RL}}$. We now give a reduction from structured
instances of coverability in $\mathbb{Q}_{+}\mathchar
45\relax\mathsf{VASS}_{\mathsf{RL}}$ to super-structured instances of
coverability in $\mathbb{Q}_{+}\mathchar 45\relax\mathsf{VASS}_{\mathsf{RL}}$.

Let $\langle\mathcal{M},c_{init},c_{fin},m\rangle$ be a structured instance of
coverability in $\mathbb{Q}_{+}\mathchar 45\relax\mathsf{VASS}_{\mathsf{RL}}$.
Let $2^{k}$ be the smallest power of two which is strictly bigger than all the
numbers appearing in $c_{init},c_{fin}$ and $m$. (Notice that $2^{k}$ can be
at most twice the maximum number appearing in any one of these terms). To
$\mathcal{M}$, add two new counters $b$ and $\overline{b}$ and replace each
rule $r:=(q,t,q^{\prime})$ with the gadget in Figure 10.

$q$$r_{mid}$$q^{\prime}$$t,b{\footnotesize{\texttt{-\hskip
0.1pt-}}},\overline{b}{\footnotesize{\texttt{++}}}$$b{\footnotesize{\texttt{++}}},\overline{b}{\footnotesize{\texttt{-\hskip
0.1pt-}}}$ Figure 10. Gadget for the rule $r:=(q,t,q^{\prime})$. Assume that
the values of $b$ and $\overline{b}$ are $1/2^{k}$ and 0 to begin with
respectively. The first rule ($r^{b}$) from $q$ to $r_{mid}$ does everything
that $r$ does and in addition decrements $b$ and increments $\overline{b}$.
The second rule ($r^{e}$) from $r_{mid}$ to $q^{\prime}$ aims to bring the
values of $b$ and $\overline{b}$ to $1/2^{k}$ and 0 respectively.

Call the resulting $\mathbb{Q}_{+}\mathchar 45\relax\mathsf{VASS}$ as
$\mathcal{M}_{1}$. For any configuration $C$ of $\mathcal{M}$, let $H(C)$
denote the _set of configurations_ of $\mathcal{M}_{1}$ such that $D\in H(C)$
iff $\mathsf{state}(D)=\mathsf{state}(C),D(x)=C(x)/2^{k}$ for every counter
$x$ of $\mathcal{M}$ and $D(b)+D(\overline{b})=1/2^{k}$. Note that any two
configurations in $H(C)$ differ only by their values of $b$ and
$\overline{b}$. Further, fixing any one of these two values determines the
value of the other as well. For any $\zeta\leq 1/2^{k}$, let $H(C)_{\zeta}$
denote the unique configuration in $H(C)$ whose $b$ value is $\zeta$. The
following lemma is a simple consequence of the construction of the gadgets in
$\mathcal{M}_{1}$.

###### Lemma D.1 (Fractional Simulation Lemma).

Suppose $C$ is a configuration and $r$ is a rule of $\mathcal{M}$.

  * •

(Soundness): If $C\xrightarrow{\alpha r}C^{\prime}$ in $\mathcal{M}$, then for
any $\zeta\leq 1/2^{k}$,
$H(C)_{\zeta}\xrightarrow{\alpha/2^{k}r^{b},(1-\alpha)/2^{k}r^{e}}H(C^{\prime})_{\zeta}$.

  * •

(Completeness): If $H(C)_{\zeta}\xrightarrow{\alpha r^{b},\beta r^{e}}D$ for
some $\alpha,\beta,D$ and some $0<\zeta\leq 1/2^{k}$ then $\alpha,\beta\leq
1/2^{k}$ and there exists $C^{\prime},\zeta^{\prime}$ such that
$0<\zeta^{\prime}\leq 1/2^{k},D=H(C^{\prime})_{\zeta^{\prime}}$ and
$C\xrightarrow{(\alpha\cdot 2^{k})r}C^{\prime}$.

Because of the above lemma, we immediately get

###### Theorem D.2.

$c_{init}$ can cover $c_{fin}$ in $\mathcal{M}$ in exactly $m$ steps if and
only if $H(c_{init})_{1/2^{k}}$ can cover $H(c_{fin})_{1/2^{k}}$ in
$\mathcal{M}_{1}$ in exactly $2m$ steps.

Notice that
$\langle\mathcal{M}_{1},H(c_{init})_{1/2^{k}},H(c_{fin})_{1/2^{k}},2m\rangle$
is a super-structured instance of coverability in $\mathbb{Q}_{+}\mathchar
45\relax\mathsf{VASS}_{\mathsf{RL}}$, which completes the required claim.

### Stage 3: Hardness of coverability in $\mathbb{Q}_{+}\mathchar
45\relax\mathsf{VASS}_{\mathsf{RL}}$ with unary encodings using amplifiers.

In the next stage, assuming the existence of objects called _amplifiers_ , we
prove our main result, that the coverability problem for
$\mathbb{Q}_{+}\mathchar 45\relax\mathsf{VASS}_{\mathsf{RL}}$ is
$\mathsf{NEXPTIME}$-hard even for a constant number of counters and even when
all the numbers are encoded in unary. We proceed to first define the notion of
an amplifier.

Let $p_{1},p_{2},\dots,p_{m}$ be natural numbers, all of them encoded in
binary using exactly $n$ bits, and let $k$ be a number such that each
$p_{i}\leq 2^{k}$. Assume the following theorem.

###### Theorem D.3 ($\mathbb{Q}_{+}\mathchar 45\relax\mathsf{VASS}$ Amplifiers
Theorem).

In polynomial time in $n,m$ and $k$, we can construct a
$\mathbb{Q}_{+}\mathchar 45\relax\mathsf{VASS}$ $Amp(p_{1},\dots,p_{m},k)$ and
two configurations $c$ and $c^{\prime}$ satisfying the following properties:

  * •

$Amp(p_{1},\dots,p_{m},k)$ has $2m+5$ counters, which are called
$y,y_{1},\dots,y_{m+2},\overline{y_{1}},\dots,\overline{y_{m+2}}$.

  * •

The control flow graph of $Amp(p_{1},\dots,p_{m},k)$ is a path of length
exactly $3(2k+4nm)$ which begins at $\mathsf{state}(c)$ and ends at
$\mathsf{state}(c^{\prime})$.

  * •

Every value of $c$ and the value $c^{\prime}(y)$ is encoded in unary.

  * •

$c^{\prime}(y_{i})=p_{i}/2^{k}$ for every $i\leq m$,
$c^{\prime}(\overline{y_{i}})=1-c^{\prime}(y_{i})$ for every $i\leq m+2$.

  * •

There is exactly one run from $c$ which can reach a configuration $d$ such
that $d(y)\geq c^{\prime}(y)$. Further, this run is of length exactly
$3(2k+4nm)$ and the configuration reached at the end of this run is
$c^{\prime}$ itself.

Such a tuple $\langle Amp(p_{1},\dots,p_{m},k),c,c^{\prime}\rangle$ is called
a $\mathbb{Q}_{+}\mathchar 45\relax\mathsf{VASS}$ amplifier for
$(p_{1},\dots,p_{m},k)$.

Here the control flow graph of a $\mathbb{Q}_{+}\mathchar
45\relax\mathsf{VASS}$ $\mathcal{M}$ is the graph obtained by taking the set
of states of $\mathcal{M}$ as its vertices and connecting any two vertices by
an edge if there is a rule between them.

The reason behind calling such a $\mathbb{Q}_{+}\mathchar
45\relax\mathsf{VASS}$ an amplifier is that starting from a configuration
encoded in _unary_ , it is able to reach a configuration encoded in _binary_.

Assuming the above theorem, we now reduce coverability in
$\mathbb{Q}_{+}\mathchar 45\relax\mathsf{VASS}_{\mathsf{RL}}$ over super-
structured instances to coverability in $\mathbb{Q}_{+}\mathchar
45\relax\mathsf{VASS}_{\mathsf{RL}}$ with unary encodings, which will prove
the required $\mathsf{NEXPTIME}$-hardness result. In the next subsection, we
will prove the $\mathbb{Q}_{+}\mathchar 45\relax\mathsf{VASS}$ Amplifiers
theorem, which will complete our overall proof.

Let $\langle\mathcal{M},c_{init},c_{fin},\ell\rangle$ be a super-structured
instance of coverability in $\mathbb{Q}_{+}\mathchar
45\relax\mathsf{VASS}_{\mathsf{RL}}$ with counters $x_{1},\dots,x_{m}$. (Note
that $c_{init}$ and $c_{fin}$ are encoded in binary). Without loss of
generality, we can assume that there are no incoming rules (resp. outgoing
rules) to (resp. from) $\mathsf{state}(c_{init})$ (resp.
$\mathsf{state}(c_{fin})$). By definition of a super-structured instance, the
denominator of each value in $c_{init}$ and $c_{fin}$ is a power of 2. By
multiplying each numerator with a sufficient power of 2, we may assume that
the denominator of each value in the initial and final configurations is the
same $2^{k}$ for some number $k$. (Note that this is a polynomial-time
transformation). Let $c_{init}(x_{i})=\alpha_{i}/2^{k}$ and
$c_{fin}(x_{i})=\beta_{i}/2^{k}$ for each $i$. By padding with sufficient
zeros, we can assume that each $\alpha_{i}$ and $\beta_{i}$ is described the
same number of bits (say $n$). Hence, we have $2m$ numerators each of which is
less than $2^{k}$ and each of which are describable by exactly $n$ bits.

The essential idea behind the reduction is to simply plugin
$Amp(\alpha_{1},\dots,\alpha_{m},k)$ and $Amp(\beta_{1},\dots,\beta_{m},k)$
before and after $\mathcal{M}$. We now expand on this idea. By Theorem D.3, in
polynomial time in the size of the given super-structured instance we can
construct amplifiers $\langle\mathcal{M}_{d},d_{init},d_{fin}\rangle$ and
$\langle\mathcal{M}_{e},e_{init},e_{fin}\rangle$ for
$(\alpha_{1},\dots,\alpha_{m},k)$ and $(\beta_{1},\dots,\beta_{m},k)$
respectively. Let
$y,y_{1},\dots,y_{m+2},\overline{y_{1}},\dots,\overline{y_{m+2}}$ be the
counters of $\mathcal{M}_{d}$ and
$z,z_{1},\dots,z_{m+2},\overline{z_{1}},\dots,\overline{z_{m+2}}$ be the
counters of $\mathcal{M}_{e}$ respectively. Without loss of generality, we can
assume that the sets of counters
$\\{x_{1},\dots,x_{m}\\},\\{y,y_{1},\dots,\overline{y_{m+2}}\\},\\{z,z_{1},\dots,\overline{z_{m+2}}\\}$
are disjoint.

##### The construction.

Let $q_{1},q_{2},q_{3},q_{4},q_{5},q_{6}$ be the states of
$d_{init},d_{fin},c_{init},c_{fin},e_{init},e_{fin}$ respectively. We now
construct a $\mathbb{Q}_{+}\mathchar 45\relax\mathsf{VASS}$ $\mathcal{C}$ as
given in Figure 11. We use the following shorthand notation in that figure as
follows: Between the states $q_{2}$ and $q_{3}$ we have a rule labelled by
$T^{inc}(x,y,\overline{y})$. This is shorthand for $m+2$ rules of the form

$q_{2}\xrightarrow{x_{1}{\footnotesize{\texttt{++}}},y_{1}{\footnotesize{\texttt{-\hskip
0.1pt-}}},\overline{y_{1}}{\footnotesize{\texttt{++}}}}p_{1}\xrightarrow{x_{2}{\footnotesize{\texttt{++}}},y_{2}{\footnotesize{\texttt{-\hskip
0.1pt-}}},\overline{y_{2}}{\footnotesize{\texttt{++}}}}p_{2}\dots
p_{m-1}\xrightarrow{x_{m}{\footnotesize{\texttt{++}}},y_{m}{\footnotesize{\texttt{-\hskip
0.1pt-}}},\overline{y_{m}}{\footnotesize{\texttt{++}}}}p_{m}\xrightarrow{y_{m+1}{\footnotesize{\texttt{-\hskip
0.1pt-}}},\overline{y_{m+1}}{\footnotesize{\texttt{++}}}}p_{m+1}\xrightarrow{y_{m+2}{\footnotesize{\texttt{-\hskip
0.1pt-}}},\overline{y_{m+2}}{\footnotesize{\texttt{++}}}}q_{3}$

where $p_{1},\dots,p_{m+1}$ are new states. Similarly, from $q_{6}$ to $end$
we have a rule labelled by $T^{dec}(x,z,\overline{z})$. This is also shorthand
for $m+2$ rules of the same kind as before, obtained by introducing fresh
states $p_{1}^{\prime},\dots,p_{m+1}^{\prime}$ and the following rules,

$q_{6}\xrightarrow{x_{1}{\footnotesize{\texttt{-\hskip
0.1pt-}}},z_{1}{\footnotesize{\texttt{-\hskip
0.1pt-}}},\overline{z_{1}}{\footnotesize{\texttt{++}}}}p_{1}^{\prime}\xrightarrow{x_{2}{\footnotesize{\texttt{-\hskip
0.1pt-}}},z_{2}{\footnotesize{\texttt{-\hskip
0.1pt-}}},\overline{z_{2}}{\footnotesize{\texttt{++}}}}p_{2}^{\prime}\dots
p_{m-1}^{\prime}\xrightarrow{x_{m}{\footnotesize{\texttt{-\hskip
0.1pt-}}},z_{m}{\footnotesize{\texttt{-\hskip
0.1pt-}}},\overline{z_{m}}{\footnotesize{\texttt{++}}}}p_{m}^{\prime}\xrightarrow{z_{m+1}{\footnotesize{\texttt{-\hskip
0.1pt-}}},\overline{z_{m+1}}{\footnotesize{\texttt{++}}}}p_{m+1}^{\prime}\xrightarrow{z_{m+2}{\footnotesize{\texttt{-\hskip
0.1pt-}}},\overline{z_{m+2}}{\footnotesize{\texttt{++}}}}end$

Note that in the first set of rules the $x_{i}$’s were incremented, whereas in
the second set they are decremented.

$q_{1}$$\dots\dots$$q_{2}$$\mathcal{M}_{d}$$q_{3}$$\dots\dots$$q_{4}$$\mathcal{M}$$q_{5}$$\dots\dots$$q_{6}$$\mathcal{M}_{e}$$end$$T^{inc}(x,y,\overline{y})$$T^{dec}(x,z,\overline{z})$
Figure 11. Construction of the final $\mathbb{Q}_{+}\mathchar
45\relax\mathsf{VASS}$ $\mathcal{C}$.

Note that the set of counters of $\mathcal{C}$ is the union of the set of
counters of $\mathcal{M}_{d},\mathcal{M}$ and $\mathcal{M}_{e}$ which we will
respectively denote by $\mathbf{y},\mathbf{x},\mathbf{z}$ respectively.

#### Observations about $\mathcal{C}$

Before we state the initial and the final configurations of our reduction and
prove its correctness, let us observe some facts about the constructed
$\mathbb{Q}_{+}\mathchar 45\relax\mathsf{VASS}$ $\mathcal{C}$.

##### Fact 1:

Let $c$ be any configuration of $\mathcal{C}$ whose state is $q_{1}$ such that
$c(w)=d_{init}(w)$ for every counter $w\in\mathbf{y}$. Let $c^{\prime}$ be the
configuration of $\mathcal{C}$ whose state is $q_{2}$ and whose counter values
are the same as that of $c$, except that $c^{\prime}(w)=d_{fin}(w)$ for every
counter $w\in\mathbf{y}$. Then, there is a run from $c$ to $c^{\prime}$ of
length exactly $3(2k+4nm)$. Further, any run from $c$ to a configuration
$c^{\prime\prime}$ such that $c^{\prime\prime}(y)\geq c^{\prime}(y)$ must
necessarily visit $c^{\prime}$ after exactly $3(2k+4nm)$ steps.

##### Proof of Fact 1:

This is simply the assumption on the amplifier
$\langle\mathcal{M}_{d},d_{init},d_{fin}\rangle$ recast in terms of the
$\mathbb{Q}_{+}\mathchar 45\relax\mathsf{VASS}$ $\mathcal{C}$. By construction
of $\mathcal{C}$ and by the fact that
$\langle\mathcal{M}_{d},d_{init},d_{fin}\rangle$ is a $\mathbb{Q}_{+}\mathchar
45\relax\mathsf{VASS}$ amplifier, it follows that there is a run from $c$ to
$c^{\prime}$ of length exactly $3(2k+4nm)$ in $\mathcal{C}$. Further, suppose
there is a run from $c$ to some configuration $c^{\prime\prime}$ such that
$c^{\prime\prime}(y)\geq c^{\prime}(y)$. Since the counter $y$ is never
affected after leaving the state $q_{2}$ to fire the rules corresponding to
$T^{inc}(x,y,\overline{y})$, we can assume that the supposed run from $c$ to
$c^{\prime\prime}$ consists only of those rules belonging to $\mathcal{M}_{d}$
in $\mathcal{C}$. By definition of an amplifier, the required claim then
follows.

##### Fact 2:

Let $c$ be any configuration of $\mathcal{C}$ whose state is $q_{2}$ such that
$c(w)=d_{fin}(w)$ for every counter $w\in\mathbf{y}$. Let $c^{\prime}$ be the
configuration of $\mathcal{C}$ whose state is $q_{3}$ and whose counter values
are the same as that of $c$, except that $c^{\prime}(y_{i})=0$ and
$c^{\prime}(\overline{y_{i}})=1$ for every $1\leq i\leq m+2$ and
$c^{\prime}(x_{i})=c(x_{i})+\alpha_{i}/2^{k}$ for every $1\leq i\leq m$. Then,
there is a run from $c$ to $c^{\prime}$ of length exactly $m+2$. Further, any
run from $c$ to a configuration $c^{\prime\prime}$ such that
$c^{\prime\prime}(y_{i})\geq c^{\prime}(y_{i})$ and
$c^{\prime\prime}(\overline{y_{i}})\geq c^{\prime}(\overline{y_{i}})$ for
every $1\leq i\leq m+2$ must necessarily visit $c^{\prime}$ after exactly
$m+2$ steps.

##### Proof of Fact 2:

By construction of the rules of the gadget $T^{inc}(x,y,\overline{y})$, it
follows that there is a run from $c$ to $c^{\prime}$ of length exactly $m+2$.
Further, suppose there is a run from $c$ to some configuration
$c^{\prime\prime}$ such that $c^{\prime\prime}(y_{i})\geq 0$ and
$c^{\prime\prime}(\overline{y_{i}})\geq 1$ for every $1\leq i\leq m+2$. By
definition of an amplifier, it follows that the only outgoing rules from
$q_{2}$ in $\mathcal{C}$ are the edges corresponding to the rules in
$T^{inc}(x,y,\overline{y})$. By assumption on the configuration $c$, we have
$c(y_{i})=\alpha_{i}/2^{k}$ for every $1\leq i\leq m$ and
$c(\overline{y_{i}})=1-c(y_{i})$ for every $1\leq i\leq m+2$. Since the
counters $\\{y_{i},\overline{y_{i}}:1\leq i\leq m+2\\}$ are never affected
after the rules in $T^{inc}(x,y,\overline{y})$, we can assume that supposed
run from $c$ to $c^{\prime\prime}$ consists only of those rules in
$T^{inc}(x,y,\overline{y})$. By construction of the rules in
$T^{inc}(x,y,\overline{y})$ and by the definition of $c$ and $c^{\prime}$, it
follows that this run must necessarily visit $c^{\prime}$ after exactly $m+2$
steps.

##### Fact 3:

Let $c$ be any configuration of $\mathcal{C}$ whose state is $q_{5}$ such that
$c(w)=e_{init}(w)$ for every counter $w\in\mathbf{z}$. Let $c^{\prime}$ be the
configuration of $\mathcal{C}$ whose state is $q_{6}$ and whose counter values
are the same as that of $c$, except that $c^{\prime}(w)=e_{fin}(w)$ for every
counter $w\in\mathbf{z}$. Then there is a run from $c$ to $c^{\prime}$ of
length exactly $3(2k+4nm)$. Further, any run from $c$ to a configuration
$c^{\prime\prime}$ such that $c^{\prime\prime}(z)\geq c^{\prime}(z)$ must
necessarily visit $c^{\prime}$ after exactly $3(2k+4nm)$ steps.

##### Proof of Fact 3:

The proof is similar to the proof of Fact 1.

##### Fact 4:

Let $c$ be any configuration of $\mathcal{C}$ whose state is $q_{6}$ such that
$c(w)=e_{fin}(w)$ for every counter $w\in\mathbf{z}$. If $c(w)\geq c_{fin}(w)$
for every $w\in\mathbf{x}$, there is a run from $c$ to $c^{\prime}$ of length
exactly $m+2$ where $c^{\prime}$ is the configuration of $\mathcal{C}$ whose
state is $end$ and whose counter values are the same as that of $c$, except
that $c^{\prime}(z_{i})=0$ and $c^{\prime}(\overline{z_{i}})=1$ for every
$1\leq i\leq m+2$ and $c^{\prime}(x_{i})=c(x_{i})-\beta_{i}/2^{k}$ for every
$1\leq i\leq m$. Further, any run from $c$ to a configuration
$c^{\prime\prime}$ such that $c^{\prime\prime}(z_{i})\geq 0$ and
$c^{\prime\prime}(\overline{z_{i}})\geq 1$ for every $1\leq i\leq m+2$ must
necessarily mean that $c(w)\geq c_{fin}(w)$ for every $w\in\mathbf{x}$ and
also that the run must necessarily visit $c^{\prime}$ after exactly $m+2$
steps.

##### Proof of Fact 4:

The proof is similar to the proof of Fact 2.

#### Correctness of the reduction.

Now we prove the correctness of our reduction. Let $f_{init}$ be the
configuration of $\mathcal{C}$ whose state is $q_{1}$ such that
$f_{init}(w)=d_{init}(w)$ for every $w\in\mathbf{y}$,
$f_{init}(w)=e_{init}(w)$ for every $w\in\mathbf{z}$ and $f_{init}(w)=0$ for
every $w\in\mathbf{x}$. Let $f_{fin}$ be the configuration of $\mathcal{C}$
whose state is $end$ such that $f_{fin}(w)=0$ for every
$w\in\\{y_{1},\dots,y_{m+2},z_{1},\dots,z_{m+2}\\}$, $f_{fin}(w)=1$ for every
$w\in\\{\overline{y_{1}},\dots,\overline{y_{m+2}},\overline{z_{1}},\dots,\overline{z_{m+2}}\\}$,
$f_{fin}(y)=d_{fin}(y),f_{fin}(z)=e_{fin}(z)$ and $f_{fin}(w)=0$ for every
$w\in\mathbf{x}$. Note that by the assumption on the amplifiers, both
$f_{init}$ and $f_{fin}$ can be encoded in unary. Set
$\ell_{\mathcal{C}}=3(2k+4nm)+(m+2)+\ell+1+3(2k+4nm)+(m+2)$. We now claim
that,

###### Theorem D.4.

$f_{init}$ can cover $f_{fin}$ in $\mathcal{C}$ in $\ell_{\mathcal{C}}$ steps
in $\mathcal{C}$ iff $c_{init}$ can cover $c_{fin}$ in $\ell$ steps in
$\mathcal{M}$.

###### Proof.

Suppose $c_{init}$ can reach a configuration $c$ which covers $c_{fin}$ in
exactly $\ell$ steps in $\mathcal{M}$ by a run $\rho$. First let us define the
following configurations:

  * •

$f_{2}$ is the same configuration as $f_{init}$ except that its state is
$q_{2}$ and $f_{2}(w)=d_{fin}(w)$ for every $w\in\mathbf{y}$.

  * •

$f_{3}$ is the same configuration as $f_{2}$ except that its state is $q_{3}$
and $f_{3}(y_{i})=0,f_{3}(\overline{y_{i}})=1$ for every $1\leq i\leq m+2$ and
$f_{3}(x_{i})=c_{init}(x_{i})$ for every $1\leq i\leq m$.

  * •

$f_{4}$ is the same configuration as $f_{3}$ except that its state is $q_{4}$
and $f_{4}(x_{i})=c(x_{i})$ for every $1\leq i\leq m$.

  * •

$f_{5}$ is the same configuration as $f_{4}$ except that its state is $q_{5}$.

  * •

$f_{6}$ is the same configuration as $f_{5}$ except that its state is $q_{6}$
and $f_{6}(w)=e_{fin}(w)$ for every $w\in\mathbf{y}$.

  * •

$f_{7}$ is the same configuration as $f_{6}$ except that its state is $end$
and $f_{7}(z_{i})=0,f_{7}(\overline{z_{i}})=1$ for every $1\leq i\leq m+2$ and
$f_{7}(x_{i})=f_{6}(x_{i})-\beta_{i}/2^{k}$ for every $1\leq i\leq m$.

By Facts 1, 2, 3 and 4, we have that $f_{init}$ can reach $f_{2}$ in exactly
$3(2k+4nm)$ steps, $f_{2}$ can reach $f_{3}$ in exactly $m+2$ steps, $f_{5}$
can reach $f_{6}$ in exactly $3(2k+4nm)$ steps and $f_{6}$ can reach $f_{7}$
in exactly $m+2$ steps. Further, from the construction it is clear that
$f_{4}$ can reach $f_{5}$ in exactly one step and also that $f_{7}$ covers
$f_{fin}$. By assumption there is a run $\rho$ from $c_{init}$ to $c$ of
exactly $m$ steps in $\mathcal{M}$. By construction of $f_{3}$ and $f_{4}$ it
can be observed that the same run $\rho$ is also a run from $f_{3}$ to $f_{4}$
in $\mathcal{C}$. It then follows that we have a run from $f_{init}$ to
$f_{7}$ of length exactly $\ell_{C}$.

Suppose $f_{init}$ can reach a configuration $f$ which covers $f_{fin}$ in
exactly $\ell_{\mathcal{C}}$ steps in $\mathcal{C}$ by a run $\rho$. First let
us define the following configurations:

  * •

$f_{2}$ is the same configuration as $f_{init}$ except that its state is
$q_{2}$ and $f_{2}(w)=d_{fin}(w)$ for every $w\in\mathbf{y}$.

  * •

$f_{3}$ is the same configuration as $f_{2}$ except that its state is $q_{3}$
and $f_{3}(y_{i})=0,f_{3}(\overline{y_{i}})=1$ for every $1\leq i\leq m+2$ and
$f_{3}(x_{i})=c_{init}(x_{i})$ for every $1\leq i\leq m$.

  * •

$f_{4}$ is the same configuration as $f_{3}$ except that its state is $q_{4}$
and $f_{4}(x_{i})=f(x_{i})+\beta_{i}/2^{k}$ for every $1\leq i\leq m$.

  * •

$f_{5}$ is the same configuration as $f_{4}$ except that its state is $q_{5}$.

  * •

$f_{6}$ is the same configuration as $f_{5}$ except that its state is $q_{6}$
and $f_{6}(w)=e_{fin}(w)$ for every $w\in\mathbf{y}$.

By Facts 1 and 2, it must be the case that after $3(2k+4nm)$ steps of $\rho$,
$f_{2}$ is reached and after $m+2$ steps from there, $f_{3}$ is reached. Now
let us look at the first points in the run $\rho$ when the state $q_{4}$ is
reached and let us call the configuration at that point as $c_{4}$. By
assumption on $\mathcal{M}$, there are no outgoing rules from $q_{4}$ in
$\mathcal{M}$ and so the only way to move out of $q_{4}$ in $\mathcal{C}$ is
to take the rule to $q_{5}$ to reach a configuration $c_{5}$ whose counter
values are the same as that of $q_{4}$. By construction of $\mathcal{C}$, no
counter in $\mathbf{z}$ is affected before reaching the state $q_{5}$ and so
this means that $c_{5}(w)=f_{init}(w)=e_{init}(w)$ for any $w\in\mathbf{z}$.
Since $f(z)\geq f_{fin}(z)=e_{fin}(z)$ and since we have a run from $c_{5}$ to
$f$, by Fact 3, it must be the case that starting from $c_{5}$, after
$3(2k+4nm)$ steps of $\rho$, we reach a configuration $c_{6}$ which is the
same as $c_{5}$ except that its state is $q_{6}$ and $c_{6}(w)=e_{fin}(w)$ for
any $w\in\mathbf{z}$. By Fact 4, it must be the case that starting from
$c_{6}$, after $m+2$ steps of $\rho$, we reach a configuration $c_{7}$ whose
state is $end$ and whose counter values are the same as that of $c_{6}$,
except that $c_{7}(z_{i})=0$ and $c_{7}(\overline{z_{i}})=1$ for every $1\leq
i\leq m+2$ and $c_{7}(x_{i})=c_{6}(x_{i})-\beta_{i}/2^{k}$ for every $1\leq
i\leq m$. Since there are no outgoing rules from $end$ in $\mathcal{C}$, it
follows that $c_{7}=f$. This in turn implies that $c_{6}=f_{6},c_{5}=f_{5}$
and $c_{4}=f_{4}$. This further implies that the path from $f_{3}$ to $f_{4}$
in $\rho$ is a path of length exactly $\ell$ consisting only of those rules
from $\mathcal{M}$. By definition of $f_{3}$ and $f_{4}$, this run is also a
run of length exactly $\ell$ in $\mathcal{M}$ from the configuration
$c_{init}$ to the configuration $c$ whose state is $q_{4}$ and
$c(x_{i})=f(x_{i})+\beta_{i}/2^{k}$ for every $i$. Since $c$ covers $c_{fin}$,
it follows that there is a run of length exactly $\ell$ in $\mathcal{M}$ from
$c_{init}$ which covers $c_{fin}$. ∎

Finally, we make an observation on the number of counters that we have used
for the reduction. Inspecting the arguments given in Stages 1 and 2, we
already see that coverability in $\mathbb{Q}_{+}\mathchar
45\relax\mathsf{VASS}_{\mathsf{RL}}$ for super-structured instances is already
$\mathsf{NEXPTIME}$-hard for 15 counters. The reduction given in Stage 3 gives
us an instance of coverability in $\mathbb{Q}_{+}\mathchar
45\relax\mathsf{VASS}_{\mathsf{RL}}$ over unary encodings with $m+2(2m+5)$
counters, where $m$ is the number of counters in the given super-structured
instance of coverability in $\mathbb{Q}_{+}\mathchar
45\relax\mathsf{VASS}_{\mathsf{RL}}$. Assuming Theorem D.3, it then follows
that

###### Theorem D.5.

Coverability in $\mathbb{Q}_{+}\mathchar 45\relax\mathsf{VASS}_{\mathsf{RL}}$
over unary encodings is $\mathsf{NEXPTIME}$-hard, already over
$\mathbb{Q}_{+}\mathchar 45\relax\mathsf{VASS}$es of dimension 85.

Since the reduction from $\mathbb{Q}_{+}\mathchar
45\relax\mathsf{VASS}_{\mathsf{RL}}$ to $\mathbb{Q}_{+}\mathchar
45\relax\mathsf{PVASS}$ given in Subsection 6.1 preserves coverability and
produces a $\mathbb{Q}_{+}\mathchar 45\relax\mathsf{PVASS}$ of bounded stack-
height, we get Theorem 7.2.

### Stage 4: Constructing $\mathbb{Q}_{+}\mathchar 45\relax\mathsf{VASS}$
amplifiers.

All that remains is to prove Theorem D.3, i.e., construct
$\mathbb{Q}_{+}\mathchar 45\relax\mathsf{VASS}$ amplifiers. Let
$p_{1},p_{2},\dots,p_{m}$ be natural numbers, all of them encoded in binary
using exactly $n$ bits and let $k$ be a number such that each $p_{i}\leq
2^{k}$. Let $\mathbf{p}$ be the vector $(p_{1},\dots,p_{m})$. We want to
construct a $\mathbb{Q}_{+}\mathchar 45\relax\mathsf{VASS}$ amplifier for
$(\mathbf{p},k)$ in time polynomial in $n,m$ and $k$. We do this in the
following way. Instead of constructing a $\mathbb{Q}_{+}\mathchar
45\relax\mathsf{VASS}$ which is an amplifier for $(\mathbf{p},k)$, we first
construct a $[0,1]\mathchar 45\relax\mathsf{VASS}_{\mathsf{RL}}^{0?}$ which is
an amplifier for $(\mathbf{p},k)$. Then we apply the reduction from Section 6
on this $[0,1]\mathchar 45\relax\mathsf{VASS}_{\mathsf{RL}}^{0?}$ amplifier
and show that the resulting $\mathbb{Q}_{+}\mathchar 45\relax\mathsf{VASS}$ is
also an amplifier for $(\mathbf{p},k)$.

To do this, we first introduce gadgets which can do basic operations on
counters such as addition, doubling and halving. We have already seen all of
these gadgets as part of the reduction given in Section 5.

#### Gadgets for addition, doubling and halving.

Consider the three $[0,1]\mathchar 45\relax\mathsf{VASS}_{\mathsf{RL}}^{0?}$’s
given in Figures 12, 13, 14, which we call the addition, subtraction, doubling
and halving gadgets respectively. In these gadgets $x,st$ and $te$ are some
three counters. The addition and subtraction gadgets are parameterized by two
counters $x$ and $st$ and the doubling and halving gadgets are parameterized
by a single counter $x$. The addition and the doubling gadgets are the same as
the ones that appeared as gadgets for the $\mathbf{inc}$ and $\mathbf{double}$
rules respectively in Section 5. The halving gadget is a simplification of the
initialization gadget used in Section 5.

A configuration $C$ of any one of these gadgets $\mathcal{M}_{g}$ is said to
be _good_ if

  * •

$\mathcal{M}_{g}$ is the addition gadget and $C(x)+C(st)\leq 1$.

  * •

$\mathcal{M}_{g}$ is the doubling gadget and $2C(x)\leq 1$.

  * •

$\mathcal{M}_{g}$ is the halving gadget and $C$ is any configuration.

The following lemma is immediate from the construction of these gadgets.

###### Lemma D.6 (The gadget lemma).

Suppose $C$ is a good configuration of one of these gadgets $\mathcal{M}_{g}$
such that $\mathsf{state}(C)=q$ and $C(te)=0$. Then, there is exactly one run
of length two in any of these gadgets from $C$ which reaches a configuration
$C^{\prime}$ which is the same as $C$ except that
$\mathsf{state}(C^{\prime})=q^{\prime}$ and

  * •

$C^{\prime}(x)=C(x)+C(st)$ if $\mathcal{M}_{g}$ is the addition gadget.

  * •

$C^{\prime}(x)=2C(x)$ if $\mathcal{M}_{g}$ is the doubling gadget.

  * •

$C^{\prime}(x)=C(x)/2$ if $\mathcal{M}_{g}$ is the halving gadget.

$q$$add$$q^{\prime}$$x{\footnotesize{\texttt{++}}},te{\footnotesize{\texttt{++}}},st{\footnotesize{\texttt{-\hskip
0.1pt-}}};\
st=0?$$st{\footnotesize{\texttt{++}}},te{\footnotesize{\texttt{-\hskip
0.1pt-}}};\ te=0?$ Figure 12. The addition gadget $Add(x,st)$.
$q$$doub$$q^{\prime}$$x{\footnotesize{\texttt{-\hskip
0.1pt-}}},te{\footnotesize{\texttt{+=2}}};\
x=0?$$x{\footnotesize{\texttt{++}}},te{\footnotesize{\texttt{-\hskip
0.1pt-}}};\ te=0?$ Figure 13. The doubling gadget $Doub(x)$.
$q$$halve$$q^{\prime}$$x{\footnotesize{\texttt{-\hskip
0.1pt=2}}},te{\footnotesize{\texttt{++}}};\
x=0?$$x{\footnotesize{\texttt{++}}},te{\footnotesize{\texttt{-\hskip
0.1pt-}}};\ te=0?$ Figure 14. The halving gadget $Halve(x)$.

#### Constructing $[0,1]\mathchar 45\relax\mathsf{VASS}_{\mathsf{RL}}^{0?}$
amplifiers.

Given an $[0,1]\mathchar 45\relax\mathsf{VASS}_{\mathsf{RL}}^{0?}$
$\mathcal{M}$, its control flow graph is the graph obtained by taking the set
of states of $\mathcal{M}$ as its vertices and connecting any two vertices by
an edge if there is a rule between them. We now define the notion of an
$[0,1]\mathchar 45\relax\mathsf{VASS}_{\mathsf{RL}}^{0?}$ amplifier for the
tuple $(\mathbf{p},k)$.

###### Definition D.7 ($[0,1]\mathchar
45\relax\mathsf{VASS}_{\mathsf{RL}}^{0?}$ amplifier.).

An $[0,1]\mathchar 45\relax\mathsf{VASS}_{\mathsf{RL}}^{0?}$ amplifier for the
tuple $(\mathbf{p},k)$ is a triple
$\langle\mathcal{C},c_{init},c_{fin}\rangle$ such that $\mathcal{C}$ is an
$[0,1]\mathchar 45\relax\mathsf{VASS}_{\mathsf{RL}}^{0?}$ and
$c_{init},c_{fin}$ are two of its configurations satisfying the following
properties:

  * •

$\mathcal{C}$ has $m+2$ counters $x_{1},\dots,x_{m},st,te$.

  * •

The control flow graph of $\mathcal{C}$ is a path of length exactly $2k+4nm$.

  * •

$c_{init}$ is 0 on every counter, except on $st$ where it takes the value 1.

  * •

$c_{fin}(x_{i})=p_{i}/2^{k}$ for each $i$, $c_{fin}(st)=1/2^{k}$ and
$c_{fin}(te)=0$.

  * •

Starting from $c_{init}$ there is exactly one run of length $2k+4nm$. Further,
this run ends at $c_{fin}$.

We now show that

###### Theorem D.8.

In time polynomial in $n,m$ and $k$ we can construct a $[0,1]\mathchar
45\relax\mathsf{VASS}_{\mathsf{RL}}^{0?}$ amplifier for $(\mathbf{p},k)$.

###### Proof.

Before we proceed with the construction, we make a small remark on notation.
In the sequel, we will describe $[0,1]\mathchar
45\relax\mathsf{VASS}_{\mathsf{RL}}^{0?}$’s using statements of the form ”We
move from state $q$ to $q^{\prime}$ by adding the counter $st$ to the counter
$x$”. This statement simply means that we attach the addition gadget
$Add(x,st)$ in between the state $q$ and $q^{\prime}$. We employ a similar
notation for doubling and halving as well.

Now we move on the construction of the $[0,1]\mathchar
45\relax\mathsf{VASS}_{\mathsf{RL}}^{0?}$ amplifier. For the sake of
simplicity, let us first handle the case when $\mathbf{p}$ is just a single
number $p$. Hence, we want to construct an $[0,1]\mathchar
45\relax\mathsf{VASS}_{\mathsf{RL}}^{0?}$ with counters $x_{1},st$ and $te$.
Let the binary encoding of $p$ in least significant bit notation be
$b_{1},b_{2},\dots,b_{n}$.

We construct the $[0,1]\mathchar 45\relax\mathsf{VASS}_{\mathsf{RL}}^{0?}$ as
follows. First, we halve the value of $st$ for $k$ times, by introducing $k+1$
states $p_{0},p_{1},\dots,p_{k}$ and by moving from $p_{i}$ to $p_{i+1}$ by
halving the value of $st$. Note that since each halving operation actually
requires 2 rules, we can do this part by using exactly $2k$ rules. Hence, if
we initially began with value 1 in $st$, after executing these $k$ rules, we
would have reached the value $1/2^{k}$ in $st$. Then if the bit $b_{1}$ is 0
we move from $p_{k}$ to a state $q_{1}$ by adding the value of $st$ to $x_{1}$
two times and if the bit $b_{1}$ is 1, we move from $p_{k}$ to $q_{1}$ by
adding the value of $st$ to $x_{1}$ exactly once. Hence, if $b_{1}$ is 0 we
would have reached $q_{1}$ with the value $2/2^{k}$ in the counter $x_{1}$ and
otherwise we would have reached $q_{1}$ with the value $1/2^{k}$ in the
counter $x_{1}$. From here on, we introduce states $q_{2},q_{3},\dots,q_{n}$
and for each $1\leq i\leq n-1$, we move from $q_{i}$ to $q_{i+1}$ in the
following manner: If the bit $b_{i+1}$ is 0, we move from $q_{i}$ to $q_{i+1}$
by doubling the value of the counter $x_{1}$ and if the bit $b_{i+1}$ is 1, we
move from $q_{i}$ to $q_{i+1}$ by first doubling the value of the counter
$x_{1}$ and then adding the value of $st$ to $x_{1}$. By introducing
appropriate dummy rules which do nothing, we can be assured that moving from
$p_{k}$ to $q_{1}$ and moving from each $q_{i}$ to $q_{i+1}$ takes exactly 4
rules.

Note that the values of $c_{init}$ and $c_{fin}$ are fixed by the constraints
on the definition of the amplifiers and we just need to specify their states
in the $[0,1]\mathchar 45\relax\mathsf{VASS}_{\mathsf{RL}}^{0?}$. We set the
initial state to be $p_{0}$ and the final state to be $q_{n}$. By repeatedly
applying the Gadget lemma (Lemma D.6), we can then easily show that starting
from $c_{init}$ there is exactly one run of length $2k+4n$ and further that
this run ends at $c_{fin}$.

This construction can be generalized in a straightforward manner to the case
when $m>1$. Essentially, we do the same process as above, where we first halve
the counter $st$ for $k$ times to arrive at the value $1/2^{k}$ in $st$ (by
using $2k$ rules), then we set $x_{1}$ to $p_{1}/2^{k}$, $x_{2}$ to
$p_{2}/2^{k}$ and so on till $x_{m}$ is set to $p_{m}/2^{k}$, all of them by
the same procedure defined above (by using $4n$ rules for each $x_{i}$,
thereby resulting in $4nm$ rules totally).

Finally, note that the control flow graph of the constructed $[0,1]\mathchar
45\relax\mathsf{VASS}_{\mathsf{RL}}^{0?}$ is a path of length exactly
$2k+4nm$. ∎

#### Constructing $\mathbb{Q}_{+}\mathchar 45\relax\mathsf{VASS}$ amplifiers.

Now we construct $\mathbb{Q}_{+}\mathchar 45\relax\mathsf{VASS}$ amplifiers,
i.e., the original amplifiers that we wanted to construct. Let
$\langle\mathcal{C},c_{init},c_{fin}\rangle$ be a $[0,1]\mathchar
45\relax\mathsf{VASS}_{\mathsf{RL}}^{0?}$ amplifier for the tuple
$(\mathbf{p},k)$ where the counters of $\mathcal{C}$ are
$x_{1},\dots,x_{m},st,te$. Apply the reduction from Section 6 on the
$[0,1]\mathchar 45\relax\mathsf{VASS}_{\mathsf{RL}}^{0?}$ reachability
instance $\langle\mathcal{C},c_{init},c_{fin},2k+4nm\rangle$ to get a
$\mathbb{Q}_{+}\mathchar 45\relax\mathsf{VASS}_{\mathsf{RL}}$ instance
$\langle\mathcal{M},d_{init},d_{fin},3(2k+4nm)\rangle$. We claim that
$\langle\mathcal{M},d_{init},d_{fin}\rangle$ is a $\mathbb{Q}_{+}\mathchar
45\relax\mathsf{VASS}$ amplifier for $(\mathbf{p},k)$.

First, $\mathcal{M}$ has $2m+5$ counters
$x_{1},\dots,x_{m},st,te,\overline{x_{1}},\overline{x_{2}},\dots,\overline{x_{m}},\overline{st},\overline{te},ctrl$.
Next, since $c_{init}$ is encoded in unary so is $d_{init}$. Further,
$d_{fin}(x_{i})=c_{fin}(x_{i})=p_{i}/2^{k}$ and for every
$x\in\\{x_{1},\dots,x_{m},st,te\\}$, we have
$d_{fin}(\overline{x})=1-d_{fin}(x)$. Finally, $c_{fin}(ctrl)$ is simply
$2(2k+4nm)$ which can also be encoded in unary. Since $\mathcal{C}$ is an
amplifier, it follows that the control flow graph of $\mathcal{C}$ is a path
of length exactly $2k+4nm$. Inspecting the structure of $\mathcal{M}$, we
notice that the control flow graph of $\mathcal{M}$ is a path of length
exactly $3(2k+4nm)$ Hence, the first four requirements of being a
$\mathbb{Q}_{+}\mathchar 45\relax\mathsf{VASS}$ amplifier are satisfied.

Now we come to the fifth requirement. Since there is a run from $c_{init}$ to
$c_{fin}$ of length exactly $2k+4nm$, by the correctness of the reduction,
there is a run from $d_{init}$ to $d_{fin}$ of length exactly $3(2k+4nm)$.
Now, suppose there is some other run $\rho$ from $d_{init}$ to a configuration
$d$ such that $d(ctrl)\geq d_{fin}(ctrl)$. Inspecting the structure of
$\mathcal{M}$, we notice that the control flow graph of $\mathcal{M}$ is a
path of length exactly $3(2k+4nm)$ such that only every second and third rule
increases the counter $ctrl$ by one. Since $\rho$ ends in a configuration
whose $ctrl$ value is at least $2(2k+4nm)$, it follows that $\rho$ is a run of
length exactly $3(2k+4nm)$ and also that $d(ctrl)=d_{fin}(ctrl)=2(2k+4nm)$.

By slicing the run $\rho$ into rules of three each, applying the completeness
part of the control counter simulation lemma repeatedly and using the fact
that $\mathcal{C}$ is an amplifier, we can then show that $d=d_{fin}$, thereby
satisfying the fifth requirement of being a $\mathbb{Q}_{+}\mathchar
45\relax\mathsf{VASS}$ amplifier.

todos main.todos.ctrtodos todos0 todos