# Memory Enhanced Embedding Learning for
Cross-Modal Video-Text Retrieval

Rui Zhao<EMAIL_ADDRESS>University of Science and Technology of
China ,  Kecheng Zheng<EMAIL_ADDRESS>University of Science and
Technology of China ,  Zheng-Jun Zha<EMAIL_ADDRESS>University of
Science and Technology of China ,  Hongtao Xie<EMAIL_ADDRESS>University
of Science and Technology of China and  Jiebo Luo<EMAIL_ADDRESS>University of Rochester

###### Abstract.

Cross-modal video-text retrieval, a challenging task in the field of vision
and language, aims at retrieving corresponding instance giving sample from
either modality. Existing approaches for this task all focus on how to design
encoding model through a hard negative ranking loss, leaving two key problems
unaddressed during this procedure. First, in the training stage, only a mini-
batch of instance pairs is available in each iteration. Therefore, this kind
of hard negatives is locally mined inside a mini-batch while ignoring the
global negative samples among the dataset. Second, there are many text
descriptions for one video and each text only describes certain local features
of a video. Previous works for this task did not consider to fuse the multiply
texts corresponding to a video during the training. In this paper, to solve
the above two problems, we propose a novel memory enhanced embedding learning
(MEEL) method for video-text retrieval. To be specific, we construct two kinds
of memory banks respectively: cross-modal memory module and text center memory
module. The cross-modal memory module is employed to record the instance
embeddings of all the datasets for global negative mining. To avoid the fast
evolving of the embedding in the memory bank during training, we utilize a
momentum encoder to update the features by a moving-averaging strategy. The
text center memory module is designed to record the center information of the
multiple textual instances corresponding to a video, and aims at bridging
these textual instances together. Extensive experimental results on two
challenging benchmarks, $i.e.$, MSR-VTT and VATEX, demonstrate the
effectiveness of the proposed method.

††copyright: acmcopyright

##  1\. Introduction

Figure 1. Illustration of a given text query, positive video sample (with blue
rectangle), negative video samples in the current mini-batch (with green
rectangle), and negative video samples in memory bank (with yellow rectangle).
A video sample is represented by a key frame for illustration. The memory bank
memorizes informative and more diverse negative samples.

Recent years have witnessed encouraging progress of both video analysis and
natural language processing, while the cross-modal tasks (Zha et al., 2019b;
Liu et al., 2018, 2019d; Yang et al., 2019; Zha et al., 2020; Cai et al.,
2014; Liu et al., 2019b), such as video-text retrieval (Dong et al., 2018,
2019; Song and Soleymani, 2019; Li et al., 2019a; Chen et al., 2020; Mithun et
al., 2018; Liu et al., 2019a), video captioning (Gao et al., 2017), video
moment localization (Hendricks et al., 2017), and video question answering
(Zha et al., 2019a) etc., remain challenging due to the semantic gap between
different modalities. Cross-modal video-text retrieval (Huang et al., 2018)
aims at retrieving the target video (text) instances given text (video) query.
As compared to image-text retrieval, the video-text retrieval is more
challenging due to the temporal dynamics of video content and the matching
across different modalities.

Existing approaches for video-text retrieval mainly focus on learning a joint
feature embedding space for visual and textual modalities, where the cross-
modal similarity could be measured appropriately. They generally utilize a
two-branch network architecture to first encode visual and textual features
respectively and then learn a joint embedding space by designed loss functions
. The widely used loss is the bi-direction ranking loss on triplets of a video
(text) embedding, a positive text (video) embedding and a negative text
(video) embedding . It maximizes the similarity between a video (text)
embedding and the corresponding text (video) embedding as well as minimizes
the similarity to all other non-matching ones.

Although existing works have steadily improved the performance of video-text
retrieval, the retrieval results are still unsatisfactory. Existing approaches
update the network gradually over a series of mini-batches of training
triplets. The “receptive field” of the network is confined to the current
mini-bath at each iteration. That is, the network is fed with only the current
mini-batch and does not explicitly exploit the history information at previous
training iterations. It is necessary to endow the network with memory ability
towards exploiting history information and significantly enlarging its
“receptive field”. Moreover, as shown in Figure 2, a video clip is usually
described by multiple text descriptions, which are different but correlated.
Such kind of correlation is effective for text embedding, however not well
exploited in existing works.

Motivated by the above observations, in this paper, we propose a memory
enhanced embedding learning (MEEL) approach for cross-modal video-text
retrieval as shown in Figure 3. In particular, we introduce a video memory
bank and a text memory bank, which memorize the video embedding features and
text embedding features in a certain number of previous mini-batches,
respectively. To avoid the fast evolving of feature embedding in memory banks
during training, we utilize a momentum encoder to update the feature embedding
in memory banks, without the requirement of gradient back-propagation. The
video (text) features in memory bank are then used to help learn the text
(video) feature embedding of the current mini-batch by a contrastive loss.
Moreover, we use a text-center memory bank, which memorizes the

two types of memory banks, respectively: the first type is constructed for
global negative mining, which includes the knowledge beyond a mini-batch, as
shown in Figure 1. There are two memory banks for this type: video memory bank
and text memory bank, which record the instances’ embedding before the current
iteration and are updated in an enqueue-dequeue manner. While text memory bank
is utilized to store more text embedding for the global negative mining of
current videos mini-batch, the video memory bank is utilized to store more
videos embedding for the global negative mining of the current texts mini-
batch. To avoid the fast evolving of the embeddings in the memory bank during
training, we utilize a momentum encoder for the embedding enqueueing and this
type memory bank does not require gradient back-propagation. The second type
is constructed to record the center information of the multiple instances,
which includes the global knowledge across these instances and aims at
bridging the difference of them during the training. There is only one memory
bank for this type: text center memory bank, due to the one-to-multi property
between video and text. It is trained by gradient back-propagation. Each
memory bank results in an individual loss and a memory enhanced loss is
produced by the fusion of them. Both two types of memory bank can be trained
respectively and either of them can boost the video-text matching performance,
while fusion of them can bring further improvement because their functions are
absolutely different and can learn different knowledge during the training. We
conduct extensive experiments to evaluate MEEL on two challenging datasets and
achieve superior performance over the state-of-the-art approaches.

Figure 2. Illustration of the “one video to multiple texts” peculiarity
existing in cross-modal video-text retrieval task.

The main contributions of this paper are summarized as follows: 1) we
introduce memory bank modules into video-text retrieval and propose novel
memory enhanced embedding learning (MEEL) to incorporate complementary
knowledge during training; and 2) we construct two types of memory banks: one
type for global negative mining and another type for bridging the difference
among the multiple texts that belong to the same video.

Figure 3. Illustration of our proposed architecture. It consists of two memory
banks that store the embedding of videos and texts for global negative mining
and one text center memory bank that aims at bridging the difference between
the multiple texts of a video, leading to three individual losses that better
optimize the encoder model.

##  2\. RELATED WORK

Image-Text Retrieval. Image-text retrieval is similar to video-text retrieval,
which firstly encodes images and texts into a fix-dimensional embedding
vectors and aims at matching between the vectors. Most of the previous work
(Faghri et al., 2017; Huang et al., 2018; Karpathy and Fei-Fei, 2015; Lee et
al., 2018; Li et al., 2019b) construct joint latent space learning for the
matching of the embedding, which is optimized by a ranking loss that pushes
the positive image-text pairs to be closer than the negative pairs. Then the
distance or the similarity between any image and text pairs can be measured by
cosine similarity or Euclidean distance once the joint latent space is
constructed. Besides, there are also other work (Huang et al., 2017; Li et
al., 2017; Wang et al., 2016; Zhang and Lu, 2018; Wang et al., 2019a) explores
to turn the matching as a classification problem, which first make a fusion
between the embedding of image and text and then predict match or mismatch (+1
for match and -1 for mismatch) based on the fused multi-modal feature by a
logistic regression loss optimization. (Lee et al., 2018) proposed a stacked
cross attention to make alignment between words and image regions, but only
attending to either words or regions. (Wang et al., 2019a) further improves it
by making attending in both modalities symmetrically and exploiting message-
passing between two modalities. (Li et al., 2019b) propose an interpretable
reasoning model to generate visual representation that captures both objects
and their semantic relations.

Video-Text Retrieval. As mentioned before, the current dominant approaches for
video-text retrieval are to learn a joint embedding space to measure the
cross-modal similarity. (Yu et al., 2018) propose a joint sequence fusion
model for the sequential interaction between video and text. (Song and
Soleymani, 2019) considers the polysemous problem for videos and texts, which
computes multiple and diverse representations of an instance by combining
global context and locally-guided features. A recent work (Chen et al., 2020)
propose a Hierarchical Graph Reasoning model, which represents complicated
visual and text details into fine-grained global-local level. Hierarchical
textual embeddings, which can guide the learning of diverse and hierarchical
video representations, are generated by attention-based graph reasoning. We
can see that all of them focus on the feature representation or the
interaction of video and text. They are all trained by a simple triplet
ranking loss, which ignores some key properties of video-text retrieval. Our
work focus on the design of the training loss by considering two properties as
mentioned before, which shows to be more effective and results in better
embeddings for the matching of videos and texts.

Memory Augmented Scheme. Learning neural networks with memory augmented, which
can provide structural and addressable knowledge for the network, has been
explored in various tasks, such as question answering (Weston et al., 2014),
video understanding (Wu et al., 2019), few-shot learning (Santoro et al.,
2016), person re-identification (Zhong et al., 2019) and so on. There are two
kinds of memory: memory network and memory bank. Memory network (Weston et
al., 2014) is a differentiable module and can be read and written. Memory bank
is a non-parametric module and can be directly feed the feature of samples.
Inspired by these work, we introduce memory bank into video-text retrieval for
the complement of the two key properties. As far as we know, no study has
attempted to incorporate memory bank while designing the loss for video-text
retrieval.

##  3\. METHOD

In this section, we firstly present the overall architecture of our proposed
method as illustrated in Figure 3, and then introduce each component in the
following subsections.

###  3.1. Overall architecture

Let
$\boldsymbol{\mathcal{X}}=\\{\boldsymbol{x_{i}},\boldsymbol{t_{i}}\\}_{i=1}^{N}$
be a training set of $N$ video-text pairs. Given a query from either modality,
the goal of video-text retrieval is to identify the most relevant instances in
the other modality. Previous work for this task focus on the encoder model to
extract more discriminate feature representations supervised by a simple
triple ranking loss. In this paper, we seek to design a more effective loss.
To be specific, we introduce memory bank to augment the optimization of the
network by considering two key properties: cross-modal global negative mining
and one-to-multi relation between videos and texts. Just as shown in Figure 3,
our architecture additionally constructs three memory banks above any off-the-
shelf encoder, which consists of two cross-modal memory banks that
respectively store the embedding of videos and texts for the cross-modal
global negative mining and one text center memory that aims at bridging the
difference between the multiple texts of a video. All the memory banks are
randomly initialized. The former two cross-modal memory banks are updated by
enqueuing and dequeuing: enqueue the newest embeddings of current mini-batch
into the memory bank and dequeue the oldest mini-batch embeddings out of the
memory bank. Besides, to avoid the fast evolving of the embeddings in the
cross-modal memory bank, which may cause mismatch problem during the training,
we incorporate momentum encoder for both video and text inspired by (He et
al., 2019). The latter text center memory are updated by gradient back-
propagation.

###  3.2. Cross-Modal Memory Module

Triplet ranking loss is widely adopted in many retrieval task, such as person
re-identification (Hermans et al., 2017), image-text cross-modal retrieval
(Faghri et al., 2017), text-based person search (Liu et al., 2019c) and so on.
Previous work (Mithun et al., 2018; Dong et al., 2019; Liu et al., 2019a; Chen
et al., 2020) on video-text cross-modal retrieval also utilized this loss as
the learning objective. It first represents a video and text into an embedding
vector, and then a function $S$ is applied on them to calculate the similarity
between them, which is usually the cosine similarity:

(1) $\centering
s_{i,j}=\frac{\boldsymbol{v}\cdot\boldsymbol{t}}{\|\boldsymbol{v}\|\cdot\|\boldsymbol{t}\|},\@add@centering$

The triplet ranking loss can then be formulated as:

(2)
$\displaystyle\mathcal{L}_{tri}=max(0,\alpha-S(\boldsymbol{v},\boldsymbol{t})+S(\boldsymbol{v},\boldsymbol{t^{-}}))$
$\displaystyle+max(0,\alpha-S(\boldsymbol{v},\boldsymbol{t})+S(\boldsymbol{v^{-}},\boldsymbol{t})),$

where $\boldsymbol{v}\in\mathbb{R}^{d}$ and $\boldsymbol{t}\in\mathbb{R}^{d}$
respectively denote to the final embedding of video and text with embedding
dimension $d$, $\boldsymbol{t^{-}}$ denotes the hard negative text embedding
for $\boldsymbol{v}$ and $\boldsymbol{v^{-}}$ denote the hard negative video
embedding for $\boldsymbol{t}$ in a mini-batch.

However, just as shown in Eq.(2), the triple ranking loss $\mathcal{L}_{tri}$
only considers the local negative samples in a mini-batch. However, there are
actually many other negative samples globally existing among the training set,
which is ignored by previous work. It’s too time-consuming if directly
comparing the samples with the whole training set at each iteration rather
than in a mini-batch as mentioned in (Mithun et al., 2018), which is not
suitable for piratical application.

While simply increase the training batch can make comparison with more
samples, the optimization may be difficult and the memory of GPU can also be
limited. Thus a suitable and effective strategy needs to be explored. In this
paper, we introduce memory bank for the cross-modal global negative mining. We
define two complimentary formulations of cross-modal memory below: Text-to-
Video and Video-to-Text.

Video-to-Text Cross-Modal Memory. To mine the global negative samples for
video, we construct a memory bank $\boldsymbol{M_{t}}\in\mathbb{R}^{K\times
d}$ in text side to store the previous text embeddings before current mini-
batch. Once given the video embedding $\boldsymbol{v}$ from mini-batch with
corresponding ground-truth texts set $\boldsymbol{T_{v}}$ and the text memory
bank $\boldsymbol{M_{t}}$, we incorporate a contrastive loss function named
InfoNCE (Oord et al., 2018) to optimize the encoder model:

(3)
$\mathcal{L}_{v2t}=-log{\frac{exp(\boldsymbol{v}\cdot\boldsymbol{k_{+}}/\tau)}{\sum\limits_{\begin{subarray}{c}i=0\\\
\boldsymbol{k_{i}}\notin\boldsymbol{T_{v}}\end{subarray}}^{K-1}exp(\boldsymbol{v}\cdot\boldsymbol{k_{i}}/\tau)}},$

where $\tau$ denotes a temperature hyper-parameter, $K$ denotes the length of
memory bank. $\boldsymbol{k_{+}}$ denotes the current positive text embedding
for $\boldsymbol{v}$, while $\boldsymbol{k_{i}}$ denotes the negative text
embedding. Note that, because of the one-to-multi relation between videos and
texts, there may be multiple ground-truth texts in text memory bank for
current video, we implement mask operation for these texts. Thus, the sum is
over one positive and other negative samples. This loss is intuitively a log
loss of softmax-based classifier that aims at classifying the positive
$(\boldsymbol{v},\boldsymbol{k+})$ pair against the remaining negative pairs.

Text-to-Video Cross-modal Memory. Same to video-to-text cross-modal memory, we
also construct a memory bank $\boldsymbol{M_{v}}\in\mathbb{R}^{K\times d}$ in
video side to mine the global negative samples for text. Given the embedding
$\boldsymbol{t}$ of a text from mini-batch with corresponding ground-truth
video set $\boldsymbol{V_{t}}$ and the text memory bank $\boldsymbol{M_{v}}$,
the contrastive loss between them can be formulated as:

(4)
$\mathcal{L}_{t2v}=-log{\frac{exp(\boldsymbol{t}\cdot\boldsymbol{k_{+}}/\tau)}{\sum\limits_{\begin{subarray}{c}i=0\\\
\boldsymbol{k_{i}}\notin\boldsymbol{T_{v}}\end{subarray}}^{K-1}exp(\boldsymbol{t}\cdot\boldsymbol{k_{i}}/\tau)}},$

where $\tau$ denotes a temperature hyper-parameter. $\boldsymbol{k_{+}}$
denotes the current positive video embedding for $\boldsymbol{t}$, while
$\boldsymbol{k_{i}}$ denotes the negative video embedding. Mask operation is
also adopted.

Momentum Encoder As mentioned before, if we directly feed the embedding of
current mini-batch into the memory bank, the embedding in the memory bank may
fast evolve during the training. To avoid this, we incorporate a momentum
encoder, as inspired by (He et al., 2019). Define the original encoder model
as $f_{q}$ and the momentum encoder as $f_{k}$. The model structure of $f_{q}$
and $f_{k}$ are completely same, while the only difference is the way of
parameters updating. The parameters updating of $f_{k}$ can be formulated as:

(5) $\theta_{k}\leftarrow m\theta_{k}+(1-m)\theta_{q},$

where $m\in[0,1)$ is a momentum hyper-parameter, $\theta_{k}$ is the parameter
of $f_{k}$ and $\theta_{q}$ is the parameter of $f_{q}$. Only the parameter
$\theta_{q}$ is updated by gradient back-propagation and the momentum update
in Eq.(5) makes the evolving of $\theta_{k}$ more smoothly than $\theta_{q}$.
In this way, though the embeddings in memory bank are encoded in different
mini-batch, the difference between them can be reduced by applying a large
momentum. Besides, in our experiments, testing by the embeddings of $f_{k}$
shows a better performance than $f_{q}$, which verifies the effectiveness of
the smoothing operation. Algorithm 1 provides the pseudo-code of the overall
cross-modal memory module with momentum encoder for video-text retrieval.

###  3.3. Text Center Memory Module

As mentioned before, due to the complexity of video content and the variance
of text description, a video can usually be retrieved by several different but
semantic related sentences. This kind of one-to-multi relation between video
and text are necessary to be considered. In order to bridge the difference
between the multiple texts belonging to a same video, we proposed to construct
a text center memory $\boldsymbol{M_{c}}\in\mathbb{R}^{H\times d}$, which
records the center information of these texts. We regard the texts that belong
to one video as one class and adopt intra-class variation minimization by:

(6)
$\mathcal{L}_{c}=\frac{1}{2}\sum_{i=1}^{B}\left\|\boldsymbol{t_{i}}-\boldsymbol{c_{y_{i}}}\right\|_{2}^{2},$

where $\boldsymbol{t_{i}}$ denotes the text embedding from mini-batch that
belongs to $y_{i}$th class and $\boldsymbol{c_{y_{i}}}$ is corresponding
center vector of $y_{i}$th class in $\boldsymbol{M_{c}}$. $B$ and $H$ are the
size of mini-batch and the text center memory.

Instead of updating the centers with respect to the entire training set, we
perform the update based on the mini-batch following to (Wen et al., 2016). In
each iteration, we compute the distance between the text embeddings of current
mini-batch and corresponding class center embedding in text center memory as
$\mathcal{L}_{c}$.

Algorithm 1 Pytorch Pseudocode for Cross-Modal Memory Module

# f_q, g_q: the original encoder network of video and text

# f_k, g_k: the momentum encoder network of video and text

# queue_v, queue_t: embedding memory bank of video and text

# m: momentum coefficient

# t: temperature coefficient

initializing: f_k.params=f_q.params, g_k.params=g_q.params

for (x_v, x_t) in dataloader do

v_q = f_q.forward(x_v)

t_q = g_q.forward(x_t)

v_k = f_k.forward(x_v).detach() # no gridient

t_k = g_k.forward(x_t).detach()

# logits for positive: Bx1

l_pos_v2t = bmm(v_q.view(B, 1, D), t_k.view(B, D, 1))

l_pos_t2v = bmm(t_q.view(B, 1, D), v_k.view(B, D, 1))

# logits for negative: BxK

l_neg_v2t = mm(v_q.view(B, D), queue_t.view(D, K))

l_neg_t2v = mm(t_q.view(B, D), queue_v.view(D, K))

# logits: Bx(1+K)

logits_v2t = concat([l_pos_v2t, l_neg_v2t], dim=1)

logits_t2v = concat([l_pos_t2v, l_neg_t2v], dim=1)

# constractive loss in Eq.(3) and Eq.(4)

labels = zeros(B)

loss_v2t = CrossEntropyLoss(logits_v2t / t, labels)

loss_t2v = CrossEntropyLoss(logits_t2v / t, labels)

loss=loss_tri+loss_v2t+loss_t2v # loss_tri denotes triplet loss

# SGD update

loss.backward()

Update(f_q.params, g_q.params)

# Momentum update

f_k.params = m * f_k.params + (1-m) * f_q.params

g_k.params = m * g_k.params + (1-m) * g_q.params

# Memory update

Enqueue(queue_v, v_k)

Dequeue(queue_v)

Enqueue(queue_t, t_k)

Dequeue(queue_t)

end for

###  3.4. Training and Testing

The final loss function that is used to train the whole model is the summation
of the triple ranking loss ($\mathcal{L}_{tri}$), video-side memory loss
($\mathcal{L}_{v2t}$), text-side memory loss ($\mathcal{L}_{t2v}$) and the
text center memory loss ($\mathcal{L}_{c}$):

(7)
$\mathcal{L}=\mathcal{L}_{tri}+\mathcal{L}_{v2t}+\mathcal{L}_{t2v}+\alpha\mathcal{L}_{c},$

where $\alpha$ is a scale weight to balance the influence of the loss term.
The additional memory can capture different external knowledge, which can
improve the optimization of the encoder model to obtain a more robust feature
representation with the joint supervision of $\mathcal{L}_{tri}$,
$\mathcal{L}_{v2t}$, $\mathcal{L}_{t2v}$ and $\mathcal{L}_{t2v}$.

During the testing time, given a text description or a video clip, its final
representation is extracted by its corresponding momentum encoder network.
Assume there are $p$ videos and $q$ texts in the whole test set, the distance
between all the video-text pairs are calculated by cosine similarity in
Eq.(1), which produce a distance matrix $D_{cos}\in\mathbb{R}^{p\times q}$.
The distance are then sorted and $Recall@1$ through $Recall@10$ are reported.

##  4\. EXPERIMENTS

Table 1. Overall performance comparison with the state-of-the-art methods on the MSR-VTT dataset. Higher $R@K$ and lower $MedR$, $MeanR$ is better. Sum of Recalls ($RSum$) indicates the overll performance. Method | Text-to-Video Retrieval | Video-to-Text Retrieval | Sum of Recalls
---|---|---|---
R@1 | R@5 | R@10 | MedR | MeanR | R@1 | R@5 | R@10 | MedR | MeanR
W2VV (Dong et al., 2018) | 1.8 | 7.0 | 10.9 | 193 | - | 9.2 | 25.4 | 25.4 | 24 | - | 90.3
VSE (Kiros et al., 2014) | 5.0 | 16.4 | 24.6 | 47 | 215.1 | 7.7 | 20.3 | 31.2 | 28 | 185.8 | 105.2
Mithun et al. (Huang et al., 2018) | 5.8 | 17.6 | 25.2 | 61 | 296.6 | 10.5 | 26.7 | 35.9 | 25 | 266.6 | 121.7
W2VViml (Dong et al., 2019) | 6.1 | 18.7 | 27.5 | 45 | - | 11.8 | 28.9 | 39.1 | 21 | - | 132.1
VSE++ (Faghri et al., 2017) | 5.7 | 17.1 | 24.8 | 65 | 300.8 | 10.2 | 25.4 | 35.1 | 25 | 228.1 | 118.3
DualEncoding (Dong et al., 2019) | 7.7 | 22.0 | 31.8 | 32 | - | 13.0 | 30.8 | 43.3 | 15 | - | 148.6
VSE++ with MEEL | 6.2 | 18.9 | 27.5 | 43 | 224.7 | 11.0 | 28.2 | 38.8 | 20 | 150.7 | 130.6
DualEncoding with MEEL | 8.3 | 24.1 | 34.4 | 26 | 165.6 | 15.5 | 35.4 | 46.2 | 12 | 99.4 | 163.9
Table 2. Performance comparision with the state-of-the-art methods on the VATEX dataset. Method | Text-to-Video Retrieval | Video-to-Text Retrieval | Sum of Recalls
---|---|---|---
R@1 | R@5 | R@10 | MedR | MeanR | R@1 | R@5 | R@10 | MedR | MeanR
VSE (Kiros et al., 2014) | 18.9 | 50.7 | 64.9 | 5 | 45.2 | 25.6 |  58.4 | 71.8 | 4 | 35.8 | 290.3
VSE++ (Faghri et al., 2017) | 21.1 | 53.5 | 66.2 | 5 | 50.1 | 30.2 | 61.2 | 74.8 | 3 | 33.9 | 307.0
DualEncoding (Dong et al., 2019) | 23.7 | 58.8 | 71.2 | 4 | 41.7 | 32.1 |  63.4 | 75.1 | 3 | 35.0 | 324.3
VSE++ with MEEL | 22.1 | 55.5 | 68.7 | 4 | 36.7 | 32.1 | 63.0 | 75.9 | 3 | 27.8 | 317.3
DualEncoding with MEEL | 25.4 | 61.6 | 73.4 | 4 | 36.5 | 35.5 | 66.2 | 76.4 | 3 | 30.5 | 338.6
Table 3. Ablation studies on the MSR-VTT dataset to investigate the additions of the three memory based loss. $\mathcal{L}_{tri}$ | $\mathcal{L}_{v2t}$ | $\mathcal{L}_{t2v}$ | $\mathcal{L}_{c}$ | Momentum | Text-to-Video Retrieval | Video-to-Text Retrieval | Sum of Recalls
---|---|---|---|---|---|---|---
R@1 | R@5 | R@10 | MedR | MeanR | R@1 | R@5 | R@10 | MedR | MeanR
$\surd$ |  |  |  |  | 7.7 | 22.0 | 31.8 | 32 | - | 13.0 | 30.8 | 43.3 | 15 | - | 148.6
$\surd$ | $\surd$ | $\surd$ |  |  | 8.1 | 23.4 | 32.8 | 32 | 206.4 | 13.9 | 32.3 | 44.5 | 15 | 120.5 | 155.0
$\surd$ | $\surd$ | $\surd$ |  | $\surd$ | 8.2 | 24.1 | 34.4 | 26 | 176.3 | 14.7 | 34.1 | 45.3 | 13 | 110.7 | 159.2
$\surd$ |  |  | $\surd$ |  | 7.8 | 23.2 | 33.3 | 27 | 178.0 | 14.5 | 33.8 | 44.6 | 14 | 102.0 | 157.2
$\surd$ | $\surd$ | $\surd$ | $\surd$ | $\surd$ | 8.3 | 24.1 | 34.4 | 26 | 165.6 | 15.5 | 35.4 | 46.2 | 12 | 99.4 | 163.9

In this section, we conduct extensive experiments to evaluate the
effectiveness of our proposed MEEL. We apply MEEL above the state-of-the-art
methods on two challenging datasets (MSR-VTT (Xu et al., 2016) and VATEX (Wang
et al., 2019b)) for video-to-text retrieval and text-to-video retrieval, which
are widely used in other vision and language task such as video question
answering and video captioning. Moreover, ablation study is also shown.

###  4.1. Experimental Setup

Datasets. In this paper, we first conduct experiments on MSR-VTT and the newly
released VATEX dataset. MSR-VTT is the dominant dataset for video-text cross-
modal retrieval. It consists of 10000 video clips, each of which is annotated
with 20-sentence descriptions. All the sentences are utilized in our work.
Following the prior work (Mithun et al., 2018; Dong et al., 2019), we split
MSR-VTT into 6513 clips for training, 497 clips for validation and 2990 clips
for testing. The VATEX datasets contains 25,991 videos for training, 3000 for
validation and 6000 for testing. Since the annotations on testing set are
private, we regard the original validation set as new testing set and randomly
split 1500 videos from orginal training set as new validation set. The
remaining 24491 videos compose the new training set. While there are 10
sentence descriptions in English and Chinese respectively describing each
video, we only utilize the English part in our work.

Evaluation Metrics. There are two kinds of video-text retrieval task: 1)
sentence retrieval task requires identifying ground truth sentences given a
query video (V2T); 2) video retrieval task requires identifying ground truth
videos given a query sentences (T2V). We measure the retrieval performance for
both V2T and T2V task with the standard metrics commonly used in information
retrieval: Recall at $K$ ($R@K$), Median Rank ($MedR$) and Mean Rank
($MeanR$). $R@K$ is defined as the recall rate at the top $K$ results to the
query, where $K$ is usually set as $1,5,10$, where higher score indicates
better performance. $MedR$ and $MeanR$ are respectively the median and average
rank of ground truth samples in the retrieved ranking list, where lower score
achieves better performance. $Rsum$ is calculated by summing all the $R@K$ in
V2T and T2V to compare the overall performance.

Implementation Details. All the implementations are based on Pytorch framework
with NVIDIA 1080Ti gpu. We keep the settings of encoder model consistent with
prior work. For the video encoding, Resnet-152 pretrained on ImageNet (He et
al., 2016) is adopted to extract frame-wise video feature for MSR-VTT dataset,
while the officially provided I3D (Carreira and Zisserman, 2017) video feature
is utilized for VATEX dataset. For the text encoding, we set the word
embedding as 512 and initialize by word2vec (Mikolov et al., 2013) pretrained
on English tags of 30 million Flickr images following to (Dong et al., 2019).
SGD with Adam is adopted as the optimizer. The size of our video memory bank
and text memory $K$ and the temperature coefficient $\tau$ in Eq.(3) and
Eq.(4) are set to 2560 and 0.07 respectively. Momentum coefficient $m$ in
Eq.(5) is set to 0.99 and then decays to 0.999 after 2 epochs. $\alpha$ in
Eq.(6) is set to 0.005.

###  4.2. Comparison with the State of the Art

We compare our method with several recent state-of-the-art models on MSR-VTT
and VATEX datasets, including W2VV (Dong et al., 2016), VSE (Kiros et al.,
2014), VSE++ (Faghri et al., 2017), Mithun et al. (Mithun et al., 2018) and
DualEncoding (Dong et al., 2019). Note that, we apply our proposed MEEL on two
state-of-the-art methods DualEncoding and VSE++ to show its effectiveness.

Table 1 shows the overall I2T and T2I retrieval result of our method on MSR-
VTT testing set. Our proposed MEEL improves the state-of-the-art model
DualEncoding by a margin with respect to all the retrieval metric.
Specifically, DualEncoding with MEEL achieves the best $R@1$ result: 8.3 for
T2V and 15.5 for V2T, leading to 7.8% and 19.2% relative gains. The overall
performance reflected by the $RSum$ metric is also boosted with a margin
+15.3, which indicates that MEEL can optimize the encoder model better and
results in a discriminate feature representation. Note that, the external
memory requires only little extra GPU space and additional training time,
which can be easy insert to other model.

To further demonstrate the robustness of our approach, we further provide
quantitative results on VATEX dataset in Table 2. The difference is that video
feature of VATEX is extracted by I3D model, officially provided by (Wang et
al., 2019b). We can see that after applying MEEL on DualEncoding, the model
achieves consistent improvement across different dataset and feature, which
result in a relative 7.2% and 10.6% gains on $R@1$ metric and +14.3 marin on
the over performance $RSum$. This verifies that it’s beneficial to take global
negative mining and the one-to-multi-relation into consideration for video-
text retrieval task.

To verify the generalization ability of the proposed MEEL, we also apply it on
VSE++, which results in a consistent improvement on both datasets.

###  4.3. Ablation Studies

In order to demonstrate the effectiveness and contribution of each component
of our proposed MEEL, we apply it on DualEncoding and conduct a series of
ablation experiments on MSR-VTT dataset. We first evaluate the effect of the
cross-modal memory module, the text center memory module, the momentum encoder
and compare their performance for both video retrieval and sentence retrieval
task. Then we evaluate how $RSum$ is affected by the memory size of the cross-
modal memory module.

Impact of proposed component. Tables 3 summarizes the ablation results. We
first remove our center memory module and we can observe that the video-side
memory loss ($\mathcal{L}_{v2t}$) and the text-side memory loss
($\mathcal{L}_{t2v}$) together result in an improvement from 148.6 to 159.2
over $Rsum$ by a margin, which verifies that the global negative mining are
necessary for video-text retrieval. We also remove our cross-modal memory
module and only utilize the center memory module, which achieves an
improvement on $Rum$. These two comparisons show the importance to explore
external knowledge augmentation. Further more, the fusion of the two memory
module additionally achieve a promising result. Note that, we conduct late
fusion for the two memory module, which is better than early fusion in our
experiment.

Figure 4. Evaluation of the proposed cross-modal memory module with different
memory sizes.

Impact of momentum encoder. As mentioned in Section 3.2, to avoid the fast
evolving of the embedding in memory bank, we conduct an extra momentum encoder
for the cross-modal memory module. As a result, during the encoding, there are
two kinds of embedding: embedding with momentum encoder and embedding without
momentum encoder as illustrated in Figure 3. We compare the retrieval
performance of best model selected by these two kinds embedding as shown in
the second row and third row of Table 3. The improvement demonstrates the
effectiveness of momentum encoder.

Impact of memory size. To evaluate the impact of memory size $K$ of the
proposed cross-modal memory module, we remove the text center memory for
precise comparison. We set $K$ to be an integer multiple of the batch size.
The results are shown in Figure 4. From Figure 4, we can see that the
retrieval performance is not sensitive to $K$, while $K=2560$ yields the best
performance.

###  4.4. Qualitative Results

To better understand the contribution of our proposed MEEL, we compare some
visualization of retrieval results on MSR-VTT testing split, which are
respectively retrieved by the models trained with and without MEEL. Figure 5
illustrates the text-to-video retrieval examples. In the three visualization
examples, we can observe that: giving a query sentence, DualEncoding trained
without our MEEL can be always confused by some similar video, while the model
trained with MEEL can effectively find the correct video. This may contributes
to the global negative mining, which makes the model have the ability to
distinguish between similar videos that will make confusion. We provide the
video-to-text retrieval examples in Figure 6 as well, where similar phenomena
can be observed in the three giving example. Specifically, the model trained
with MEEL can give more correct sentences with a high rank, because we
consider to bridge the difference between these sentences. Thus the
effectiveness of our proposed MEEL is demonstrated through these examples.

##  5\. CONCLUSION

Figure 5. Top 3 text-to-video retrieval examples on MSR-VTT, where videos in
the left column are retrieved by DualEncoding with MEEL and videos in the
right column are retrieved without MEEL (red boxes are correct). Figure 6. Top
3 video-to-text retrieval examples on MSR-VTT, where texts in the left column
are retrieved by DualEncoding with MEEL and texts in the right column are
retrieved without MEEL (red sentences are correct).

In this paper, we proposed a novel memory enhanced embedding learning for
video-text retrieval, which considers two key properties existing in this
task: global negative mining and the one video paired with multiple texts.
Specifically, to unify these two problems in a framework, we fully incorporate
the memory module into two types: cross-modal memory module and text center
memory module. The cross-modal memory that stores more previous embeddings are
constructed for global negative mining, which consists of video-to-text memory
and text-to-video memory. The text center memory that stores the center
information of multiple texts belonging to one video are constructed to bridge
between these texts. We conduct extensive experiments on two datasets: MSR-VTT
and VATEX. The expermental results have demonstrated the effectiveness of our
proposed method.

## References

  * (1)
  * Cai et al. (2014) Junjie Cai, Zheng-Jun Zha, Meng Wang, Shiliang Zhang, and Qi Tian. 2014.  An attribute-assisted reranking model for web image search.  _IEEE transactions on image processing_ 24, 1 (2014), 261–272.
  * Carreira and Zisserman (2017) Joao Carreira and Andrew Zisserman. 2017.  Quo vadis, action recognition? a new model and the kinetics dataset. In _proceedings of the IEEE Conference on Computer Vision and Pattern Recognition_. 6299–6308.
  * Chen et al. (2020) Shizhe Chen, Yida Zhao, Qin Jin, and Qi Wu. 2020\.  Fine-grained Video-Text Retrieval with Hierarchical Graph Reasoning.  _arXiv preprint arXiv:2003.00392_ (2020).
  * Dong et al. (2016) Jianfeng Dong, Xirong Li, and Cees GM Snoek. 2016.  Word2visualvec: Image and video to sentence matching by visual feature prediction.  _arXiv preprint arXiv:1604.06838_ (2016).
  * Dong et al. (2018) Jianfeng Dong, Xirong Li, and Cees GM Snoek. 2018.  Predicting visual features from text for image and video caption retrieval.  _IEEE Transactions on Multimedia_ 20, 12 (2018), 3377–3388.
  * Dong et al. (2019) Jianfeng Dong, Xirong Li, Chaoxi Xu, Shouling Ji, Yuan He, Gang Yang, and Xun Wang. 2019.  Dual encoding for zero-example video retrieval. In _Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition_. 9346–9355.
  * Faghri et al. (2017) Fartash Faghri, David J Fleet, Jamie Ryan Kiros, and Sanja Fidler. 2017.  Vse++: Improving visual-semantic embeddings with hard negatives.  _arXiv preprint arXiv:1707.05612_ (2017).
  * Gao et al. (2017) Lianli Gao, Zhao Guo, Hanwang Zhang, Xing Xu, and Heng Tao Shen. 2017.  Video Captioning With Attention-Based LSTM and Semantic Consistency.  _IEEE Transactions on Multimedia_ 19, 9 (2017), 2045–2055.
  * He et al. (2019) Kaiming He, Haoqi Fan, Yuxin Wu, Saining Xie, and Ross Girshick. 2019.  Momentum contrast for unsupervised visual representation learning.  _arXiv preprint arXiv:1911.05722_ (2019).
  * He et al. (2016) Kaiming He, Xiangyu Zhang, Shaoqing Ren, and Jian Sun. 2016\.  Deep residual learning for image recognition. In _Proceedings of the IEEE conference on computer vision and pattern recognition_. 770–778.
  * Hendricks et al. (2017) Lisa Anne Hendricks, Oliver Wang, Eli Shechtman, Josef Sivic, Trevor Darrell, and Bryan C Russell. 2017.  Localizing Moments in Video with Natural Language.  (2017), 5804–5813.
  * Hermans et al. (2017) Alexander Hermans, Lucas Beyer, and Bastian Leibe. 2017\.  In defense of the triplet loss for person re-identification.  _arXiv preprint arXiv:1703.07737_ (2017).
  * Huang et al. (2017) Yan Huang, Wei Wang, and Liang Wang. 2017.  Instance-aware image and sentence matching with selective multimodal lstm. In _Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition_. 2310–2318.
  * Huang et al. (2018) Yan Huang, Qi Wu, Chunfeng Song, and Liang Wang. 2018\.  Learning semantic concepts and order for image and sentence matching. In _Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition_. 6163–6171.
  * Karpathy and Fei-Fei (2015) Andrej Karpathy and Li Fei-Fei. 2015.  Deep visual-semantic alignments for generating image descriptions. In _Proceedings of the IEEE conference on computer vision and pattern recognition_. 3128–3137.
  * Kiros et al. (2014) Ryan Kiros, Ruslan Salakhutdinov, and Richard S Zemel. 2014\.  Unifying visual-semantic embeddings with multimodal neural language models.  _arXiv preprint arXiv:1411.2539_ (2014).
  * Lee et al. (2018) Kuang-Huei Lee, Xi Chen, Gang Hua, Houdong Hu, and Xiaodong He. 2018.  Stacked cross attention for image-text matching. In _Proceedings of the European Conference on Computer Vision (ECCV)_. 201–216.
  * Li et al. (2019b) Kunpeng Li, Yulun Zhang, Kai Li, Yuanyuan Li, and Yun Fu. 2019b.  Visual semantic reasoning for image-text matching. In _Proceedings of the IEEE International Conference on Computer Vision_. 4654–4662.
  * Li et al. (2017) Shuang Li, Tong Xiao, Hongsheng Li, Wei Yang, and Xiaogang Wang. 2017.  Identity-aware textual-visual matching with latent co-attention. In _Proceedings of the IEEE International Conference on Computer Vision_. 1890–1899.
  * Li et al. (2019a) Xirong Li, Chaoxi Xu, Gang Yang, Zhineng Chen, and Jianfeng Dong. 2019a.  W2VV++ Fully Deep Learning for Ad-hoc Video Search. In _Proceedings of the 27th ACM International Conference on Multimedia_. 1786–1794.
  * Liu et al. (2018) Daqing Liu, Zheng-Jun Zha, Hanwang Zhang, Yongdong Zhang, and Feng Wu. 2018.  Context-aware visual policy network for sequence-level image captioning. In _Proceedings of the 26th ACM international conference on Multimedia_. 1416–1424.
  * Liu et al. (2019d) Daqing Liu, Hanwang Zhang, Feng Wu, and Zheng-Jun Zha. 2019d.  Learning to assemble neural module tree networks for visual grounding. In _Proceedings of the IEEE International Conference on Computer Vision_. 4673–4682.
  * Liu et al. (2019c) Jiawei Liu, Zheng-Jun Zha, Richang Hong, Meng Wang, and Yongdong Zhang. 2019c.  Deep Adversarial Graph Attention Convolution Network for Text-Based Person Search. In _Proceedings of the 27th ACM International Conference on Multimedia_. 665–673.
  * Liu et al. (2019b) Xuejing Liu, Liang Li, Shuhui Wang, Zheng-Jun Zha, Dechao Meng, and Qingming Huang. 2019b.  Adaptive reconstruction network for weakly supervised referring expression grounding. In _Proceedings of the IEEE International Conference on Computer Vision_. 2611–2620.
  * Liu et al. (2019a) Yang Liu, Samuel Albanie, Arsha Nagrani, and Andrew Zisserman. 2019a.  Use what you have: Video retrieval using representations from collaborative experts.  _arXiv preprint arXiv:1907.13487_ (2019).
  * Mikolov et al. (2013) Tomas Mikolov, Kai Chen, Greg Corrado, and Jeffrey Dean. 2013\.  Efficient estimation of word representations in vector space.  _arXiv preprint arXiv:1301.3781_ (2013).
  * Mithun et al. (2018) Niluthpol Chowdhury Mithun, Juncheng Li, Florian Metze, and Amit K Roy-Chowdhury. 2018.  Learning joint embedding with multimodal cues for cross-modal video-text retrieval. In _Proceedings of the 2018 ACM on International Conference on Multimedia Retrieval_. 19–27.
  * Oord et al. (2018) Aaron van den Oord, Yazhe Li, and Oriol Vinyals. 2018.  Representation learning with contrastive predictive coding.  _arXiv preprint arXiv:1807.03748_ (2018).
  * Santoro et al. (2016) Adam Santoro, Sergey Bartunov, Matthew Botvinick, Daan Wierstra, and Timothy Lillicrap. 2016\.  Meta-learning with memory-augmented neural networks. In _International conference on machine learning_. 1842–1850.
  * Song and Soleymani (2019) Yale Song and Mohammad Soleymani. 2019.  Polysemous visual-semantic embedding for cross-modal retrieval. In _Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition_. 1979–1988.
  * Wang et al. (2016) Liwei Wang, Yin Li, and Svetlana Lazebnik. 2016.  Learning deep structure-preserving image-text embeddings. In _Proceedings of the IEEE conference on computer vision and pattern recognition_. 5005–5013.
  * Wang et al. (2019b) Xin Wang, Jiawei Wu, Junkun Chen, Lei Li, Yuan-Fang Wang, and William Yang Wang. 2019b.  VATEX: A large-scale, high-quality multilingual dataset for video-and-language research. In _Proceedings of the IEEE International Conference on Computer Vision_. 4581–4591.
  * Wang et al. (2019a) Zihao Wang, Xihui Liu, Hongsheng Li, Lu Sheng, Junjie Yan, Xiaogang Wang, and Jing Shao. 2019a.  CAMP: Cross-Modal Adaptive Message Passing for Text-Image Retrieval. In _Proceedings of the IEEE International Conference on Computer Vision_. 5764–5773.
  * Wen et al. (2016) Yandong Wen, Kaipeng Zhang, Zhifeng Li, and Yu Qiao. 2016\.  A discriminative feature learning approach for deep face recognition. In _European conference on computer vision_. Springer, 499–515.
  * Weston et al. (2014) Jason Weston, Sumit Chopra, and Antoine Bordes. 2014\.  Memory networks.  _arXiv preprint arXiv:1410.3916_ (2014).
  * Wu et al. (2019) Chao-Yuan Wu, Christoph Feichtenhofer, Haoqi Fan, Kaiming He, Philipp Krahenbuhl, and Ross Girshick. 2019\.  Long-term feature banks for detailed video understanding. In _Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition_. 284–293.
  * Xu et al. (2016) Jun Xu, Tao Mei, Ting Yao, and Yong Rui. 2016\.  Msr-vtt: A large video description dataset for bridging video and language. In _Proceedings of the IEEE conference on computer vision and pattern recognition_. 5288–5296.
  * Yang et al. (2019) Tianhao Yang, Zheng-Jun Zha, and Hanwang Zhang. 2019\.  Making history matter: History-advantage sequence training for visual dialog. In _Proceedings of the IEEE International Conference on Computer Vision_. 2561–2569.
  * Yu et al. (2018) Youngjae Yu, Jongseok Kim, and Gunhee Kim. 2018.  A joint sequence fusion model for video question answering and retrieval. In _Proceedings of the European Conference on Computer Vision (ECCV)_. 471–487.
  * Zha et al. (2019a) Zhengjun Zha, Jiawei Liu, Tianhao Yang, and Yongdong Zhang. 2019a.  Spatiotemporal-Textual Co-Attention Network for Video Question Answering.  _ACM Transactions on Multimedia Computing, Communications, and Applications_ 15, 2 (2019), 53.
  * Zha et al. (2019b) Zheng-Jun Zha, Daqing Liu, Hanwang Zhang, Yongdong Zhang, and Feng Wu. 2019b.  Context-aware visual policy network for fine-grained image captioning.  _IEEE transactions on pattern analysis and machine intelligence_ (2019).
  * Zha et al. (2020) Zheng-Jun Zha, Jiawei Liu, Di Chen, and Feng Wu. 2020\.  Adversarial attribute-text embedding for person search with natural language query.  _IEEE Transactions on Multimedia_ (2020).
  * Zhang and Lu (2018) Ying Zhang and Huchuan Lu. 2018.  Deep cross-modal projection learning for image-text matching. In _Proceedings of the European Conference on Computer Vision (ECCV)_. 686–701.
  * Zhong et al. (2019) Zhun Zhong, Liang Zheng, Zhiming Luo, Shaozi Li, and Yi Yang. 2019.  Invariance matters: Exemplar memory for domain adaptive person re-identification. In _Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition_. 598–607.


University of Warsaw, Polandhttps://orcid.org/0000-0001-8674-4470 Supported by
the ERC project ‘Lipa’ within the EU Horizon 2020 research and innovation
programme (No. 683080). Sławomir Lasota [300]Theory of computation Concurrency
[500]Theory of computation Verification by model checking [500]Theory of
computation Logic and verification Petra Berenbrink and Benjamin Monmege 2
39th International Symposium on Theoretical Aspects of Computer Science (STACS
2022) STACS 2022 STACS 2022 March 15–18, 2022 Marseille, France 219 35

# Improved Ackermannian lower bound for the Petri nets reachability problem

Sławomir Lasota

###### Abstract

Petri nets, equivalently presentable as vector addition systems with states,
are an established model of concurrency with widespread applications. The
reachability problem, where we ask whether from a given initial configuration
there exists a sequence of valid execution steps reaching a given final
configuration, is the central algorithmic problem for this model. The
complexity of the problem has remained, until recently, one of the hardest
open questions in verification of concurrent systems. A first upper bound has
been provided only in 2015 by Leroux and Schmitz, then refined by the same
authors to non-primitive recursive Ackermannian upper bound in 2019. The
exponential space lower bound, shown by Lipton already in 1976, remained the
only known for over 40 years until a breakthrough non-elementary lower bound
by Czerwiński, Lasota, Lazic, Leroux and Mazowiecki in 2019. Finally, a
matching Ackermannian lower bound announced this year by Czerwiński and
Orlikowski, and independently by Leroux, established the complexity of the
problem.

Our primary contribution is an improvement of the former construction, making
it conceptually simpler and more direct. On the way we improve the lower bound
for vector addition systems with states in fixed dimension (or, equivalently,
Petri nets with fixed number of places): while Czerwiński and Orlikowski prove
$\mathcal{F}_{k}$-hardness (hardness for $k$th level in Grzegorczyk Hierarchy)
in dimension $6k$, our simplified construction yields
$\mathcal{F}_{k}$-hardness already in dimension $3k+2$.

###### keywords:

Petri nets, reachability problem, vector addition systems

###### category:

##  1 Introduction

Petri nets [Petri62] are an established model of concurrency with extensive
and diverse applications in various fields, including modelling and analysis
of hardware [BurnsKY00, LerouxAG15], software [GermanS92, BouajjaniE13, KKW14]
and database [BojanczykDMSS11] systems, as well as chemical [AngeliLS11],
biological [BaldanCMS10] and business [Aalst15, LiDV17] processes (the
references on applications are illustrative). The model admits various
alternative but essentially equivalent presentations, most notably _vector
addition systems_ (VAS) [KarpM69], and _vector addition systems with states_
(VASS) [Greibach78a, Sec.5], [HopcroftP79]. The central algorithmic question
for this model is the _reachability problem_ that asks whether from a given
initial configuration there exists a sequence of valid execution steps
reaching a given final configuration. Each of the alternative presentations
admits its own formulation of the reachability problem, all of them being
equivalent due to straightforward polynomial-time translations that preserve
reachability, see e.g. Schmitz’s survey [Schmitz16siglog, Section 2.1]. For
instance, in terms of VAS, the problem is stated as follows: given a finite
set $T$ of integer vectors in $d$-dimensional space and two $d$-dimensional
vectors $\mathbf{v}$ and $\mathbf{w}$ of nonnegative integers, does there
exist a walk from $\mathbf{v}$ to $\mathbf{w}$ such that it stays within the
nonnegative orthant, and every step modifies the current position by adding
some vector from $T$? The model of VASS is a natural extension of VAS with
finite control, where $\mathbf{v}$ is additionally equipped with an initial
control state, $\mathbf{w}$ with a final one, and each vector in $T$ is
additionally equipped with a source-target pair of control states.

We recall, following [Schmitz16siglog, stoc19, jacm, CLO21], that importance
of the Petri nets reachability problem is widespread, as many diverse problems
from formal languages [Crespi-ReghizziM77], logic [Kanovich95, DemriFP16,
DeckerHLT14, ColcombetM14], concurrent systems [GantyM12, EsparzaGLM17],
process calculi [Meyer09], linear algebra [HL18] and other areas (the
references are again illustrative) are known to admit reductions from the VASS
reachability problem; for more such problems and a wider discussion, we refer
to [Schmitz16siglog].

### Brief history of the problem

The complexity of the Petri nets reachability problem has remained unsettled
over the past half century. Concerning the decidability status, after an
incomplete proof by Sacerdote and Tenney in 1970s [SacerdoteT77], decidability
of the problem was established by Mayr [Mayr81, Mayr84] in 1981, whose proof
was then simplified by Kosaraju [Kosaraju82], and then further refined by
Lambert in the 1990s [Lambert92]. A different approach, based on inductive
invariants, has emerged from a series of papers by Leroux a decade ago
[Leroux10, Leroux11, Leroux12].

Concerning upper complexity bounds, the first such bound has been shown only
in 2015 by Leroux and Schmitz [LerouxS15], consequently improved to the
Ackermannian upper bound [LS].

Concerning lower complexity bounds, Lipton’s landmark exponential space lower
bound from 70ies [lipton76] has remained the state of the art for over 40
years until a breakthrough non-elementary lower bound by Czerwiński, Lasota,
Lazic, Leroux and Mazowiecki in 2019 [stoc19] (see also [jacm]): hardness of
the reachability problem for the class Tower of all decision problems that are
solvable in time or space bounded by a tower of exponentials whose height is
an elementary function of input size. A further refinement of Tower-hardness,
in terms of fine-grained complexity classes closed under polynomial-time
reductions, has been reported by Czerwiński, Lasota and Orlikowski [CLO21].
Finally, a matching Ackermannian lower bound has been announced recently,
independently by Czerwiński and Orlikowski [CO], and by Leroux [L] (the two
constructions underlying the proofs seem to be significantly different). These
results finally close the long standing complexity gap, and yield Ackermann-
completness of the Petri nets reachability problem. The techniques used in
[CO] and [L] substantially differ.

### Our contribution

We provide an improvement of the construction of [CO]. As our main
contribution, we make the construction conceptually simpler and more direct
(the idea of improvement is discussed at the end of Section 2, and the central
ingredient of our construction is presented in Section 4). Moreover, on the
way we improve the parametric lower bound with respect to the dimension of
vector addition systems with states (or, equivalently, the number of places of
Petri nets111We remark that a Petri net corresponding to a VASS of dimension
$d$ has $d+3$ places, due to $3$ extra places for encoding the control states
of VASS [HopcroftP79]. Likewise, a VAS corresponding to a VASS of dimension
$d$ has dimension $d+3$.). For formulating the result we refer to the
complexity classes $\mathcal{F}_{\alpha}$ corresponding to the Grzegorczyk
hierarchy of fast-growing functions [lob1970hierarchies, Schmitz16toct],
indexed by ordinals $\alpha=0,1,2,\ldots,\omega$; for instance, the class
$\mathcal{F}_{3}$ is Tower (class of all decision problems that are solvable
in time or space bounded by a tower of exponentials, closed under elementary
reductions) and $\mathcal{F}_{\omega}$ is Ackermann (class of all decision
problems that are solvable in time or space bounded by the Ackermann function,
closed under primitive-recursive reductions). Results of [CO, L] can be stated
in parametric terms as follows: the former shows $\mathcal{F}_{k}$-hardness of
the reachability problem for VASS in dimension $6k$, while the latter one
shows $\mathcal{F}_{k}$-hardness for VASS in dimension $4k+5$. Our simplified
construction yields a better lower bound: $\mathcal{F}_{k}$-hardness already
in dimension $3k+2$. This improvement is a step towards establishing the tight
dimension-parametric complexity of the problem, as the best known upper bound
is $\mathcal{F}_{k}$-membership in dimension $k-4$ [LS]. As a next step, an
improvement of the construction of [L] to dimension $2k+4$ has been recently
reported in [L-arxiv].

##  2 The reachability problem

In this section we define the reachability problem and explain our
contribution. Following [stoc19, jacm, CLO21, CO, L], we work with a
convenient presentation of VASS as counter programs without zero tests, where
the dimension of a VASS corresponds to the number of counters of a program.

### Counter programs

A _counter program_ (or simply a _program_) is a sequence of (line-numbered)
commands, each of which is of one of the following types:

> $\mathsf{x}\,\,+\\!\\!=\,1$ | (increment counter $\mathsf{x}$)
> ---|---
> $\mathsf{x}\,\,-\\!\\!=\,1$ | (decrement counter $\mathsf{x}$)
> goto $L$ or $L^{\prime}$ | (nondeterministically jump to either line $L$ or line $L^{\prime}$)
> zero? $\mathsf{x}$ | (zero test: continue if counter $\mathsf{x}$ equals $0$)

Counters are only allowed to have nonnegative values. We are particularly
interested in counter programs _without zero tests_ , i.e., ones that use no
zero test command. Whenever we use zero tests in the sequel, it is always in
view of faithfully simulating them by programs without zero tests.

> Convention: In the sequel, unless specified explicitly, counter programs are
> implicitly assumed to be without zero tests.

######  Example 2.1.

We write $\mathsf{x}\,\,+\\!\\!=\,m$ (resp. $\mathsf{x}\,\,-\\!\\!=\,m$) as a
shorthand for for $m$ consecutive increments (resp. decrements) of
$\mathsf{x}$. As an illustration, consider the program with three counters
$\mathsf{C}=\\{\mathsf{x},\mathsf{y},\mathsf{z}\\}$ (on the left), and its
more readable presentation using a syntactic sugar loop (on the right):

1:goto 2 or 6

2:$\mathsf{x}\,\,-\\!\\!=\,1$

3:$\mathsf{y}\,\,+\\!\\!=\,1$

4:$\mathsf{z}\,\,+\\!\\!=\,2$

5:goto 1 or 1

6:$\mathsf{z}\,\,+\\!\\!=\,1$

1:loop

2: $\mathsf{x}\,\,-\\!\\!=\,1$

3: $\mathsf{y}\,\,+\\!\\!=\,1$

4: $\mathsf{z}\,\,+\\!\\!=\,2$

5:$\mathsf{z}\,\,+\\!\\!=\,1$

The program repeats the block of commands in lines 2–4 some number of times
chosen nondeterministically (possibly zero, although not infinite because
$\mathsf{x}$ is decreasing, and hence its initial value bounds the number of
iterations) and then increments $\mathsf{z}$. In the sequel we conveniently
use loop construct instead of explicit goto commands. (A dummy command is
implicitly added after a loop in case it appears at the very end of a
program.)

We emphasise that counters are only permitted to have nonnegative values. In
the program above, that is why the decrement in line 2 works also as a non-
zero test.

Consider a program with counters $\mathsf{C}$. By $\mathbb{N}^{{\mathsf{C}}}$
we denote the set of all valuations of counters. Given an initial valuation of
counters, a _run_ (or _execution_) of a counter program is a finite sequence
of executions of commands, as expected. A run which has successfully finished
we call _complete_ ; otherwise, the run is _partial_. Observe that, due to a
decrement that would cause a counter to become negative, a partial run may
fail to continue because it is blocked from further execution. Moreover, due
to nondeterminism of goto, a program may have various runs from the same
initial valuation.

Two programs $\mathcal{P},\mathcal{Q}$ may be _composed_ by concatenating
them, written $\mathcal{P}\ \mathcal{Q}$. We silently assume the appropriate
re-numbering of lines referred to by goto command in $\mathcal{Q}$.

### The reachability problem

Given a subset $R\subseteq\mathbb{N}^{{\mathsf{C}}}$ of valuations, by a run
_from $R$_ we mean any run whose initial valuation belongs to $R$. A complete
run is called _$\mathsf{X}$ -zeroing_, for a subset
$\mathsf{X}\subseteq\mathsf{C}$ of counters, if it ends with $\mathsf{x}=0$
for all $\mathsf{x}\in\mathsf{X}$. When $\mathsf{X}=\\{\mathsf{x}\\}$ and/or
$R=\\{r\\}$ are a singleton we write simply “$\mathsf{x}$-zeroing” and/or
“from $r$”. For instance, the program from Example 2.1 has exactly one
$\mathsf{x}$-zeroing run from the valuation $\mathsf{x}=10$,
$\mathsf{y}=\mathsf{z}=0$, where the final values of counters are
$\mathsf{x}=0$, $\mathsf{y}=10$, $\mathsf{z}=21$.

By ${\bf 0}$ we denote the valuation where all counters are 0. Following
[stoc19, jacm, CLO21, CO, L], we investigate the complexity of the following
variant of the reachability problem (with a partially specified final
valuation of counters):

######  Problem 1.

Reachability problem A program $\mathcal{P}$ without zero tests, and a subset
$\mathsf{X}$ of its counters Does $\mathcal{P}$ have an $\mathsf{X}$-zeroing
run from the zero valuation ${\bf 0}$

Since counter programs without zero tests can be seen as presentations of
VASS, the above decision problem translates to a variant of the reachability
problem for the latter model, where all components of the initial vector are
0, and the specified components of the final vector are required to be 0. This
variant polynomially reduces to the classical one where all components of the
final vector are fully specified (say, required to be 0), and the reduction
preserves dimension. According to the encoding of VASS as Petri nets, the
problem translates to the _submarking reachability_ problem for the latter
model, where all places (except for those encoding the control states) are
initially empty, and the specified places are required to be finally empty.
Finally, the submarking reachability problem is polynomially equivalent to a
variant where the final content of all places is fully specified.

### Fast-growing hierarchy

For a positive integer $k$, let
$\mathbb{N}_{k}=\\{k,2k,3k,\ldots\\}\subseteq\mathbb{N}$ denote positive
multiplicities of $k$. We define the complexity classes $\mathcal{F}_{i}$
corresponding to the $i$th level in the Grzegorczyk Hierarchy [Schmitz16toct,
Sect. 2.3, 4.1]. The standard family of approximations
$\mathbf{A}_{i}:\mathbb{N}_{1}\to\mathbb{N}_{1}$ of Ackermann function, for
$i\in\mathbb{N}_{1}$, can be defined as follows:

$\mathbf{A}_{1}(n)=2n,\qquad\mathbf{A}_{i+1}(n)=\underbrace{\mathbf{A}_{i}\circ\mathbf{A}_{i}\circ\ldots\circ\mathbf{A}_{i}}_{n}(1)=\mathbf{A}_{i}^{n}(1).$

In particular, $\mathbf{A}_{2}(n)=2^{n}$ and $\mathbf{A}_{i}(1)=2$ for all
$i\in\mathbb{N}_{1}$. Using functions $\mathbf{A}_{i}$, we define the
complexity classes $\mathcal{F}_{i}$, indexed by $i\in\mathbb{N}_{1}$, of
problems solvable in deterministic time $\mathbf{A}_{i}(p(n))$, where
$p:\mathbb{N}_{1}\to\mathbb{N}_{1}$ ranges over functions computable in
deterministic time $\mathbf{A}_{i-1}^{m}(n)$, for some $m\in\mathbb{N}_{1}$:

$\mathcal{F}_{i}=\bigcup_{p\in\mathcal{FF}_{i-1}}\text{\sc
DTime}(\mathbf{A}_{i}(p(n))),\qquad\text{ where
}\mathcal{FF}_{i}=\bigcup_{m\in\mathbb{N}_{1}}\text{\sc
FDTime}(\mathbf{A}_{i}^{m}(n)).$

Intuitively speaking, the class $\mathcal{F}_{i}$ contains all problems
solvable in time $\mathbf{A}_{i}(n)$, and is closed under reductions
computable in time of lower order $\mathbf{A}_{i-1}^{m}(n)$, for some fixed
$m\in\mathbb{N}_{1}$. In particular, $\mathcal{F}_{3}=\textsc{Tower}$
(problems solvable in a tower of exponentials of time or space, whose height
is an elementary function of input size). The classes $\mathcal{F}_{k}$ are
robust with respect to the choice of fast-growing function hierarchy (see
[Schmitz16toct, Sect.4.1]). For $k\geq 3$, instead of deterministic time, one
could equivalently take nondeterministic time, or space.

### Dimension-parametric lower bound

As the main result we prove $\mathcal{F}_{k}$-hardness for programs with the
fixed number $3k+2$ of counters:

######  Theorem 2.2.

Let $k\geq 3$. The reachabilty problem for programs with $3k+2$ counters is
$\mathcal{F}_{k}$-hard.

The proof is in Section 6. The result can be compared to
$\mathcal{F}_{k}$-hardness shown in [CO] for $6k$ counters, and in [L] for
$4k+5$ counters. Like the cited results, Theorem 2.2 implies Ackermann-
hardness for unrestricted number of counters which, together with Ackermann
upper bound of [LS], yields Ackermann-completness of the reachability problem.

### Idea of simplification

Czerwiński and Orlikowski [CO] use the _ratio technique_ introduced previously
in [stoc19]. Speaking slightly informally, suppose some three counters
$\mathsf{b},\mathsf{c},\mathsf{d}$ satisfy initially

$\displaystyle\mathsf{b}=B,\qquad\mathsf{c}>0,\qquad\mathsf{d}=\mathsf{b}\cdot\mathsf{c},$
(1)

for some fixed positive integer $B\in\mathbb{N}$. Furthermore, suppose that
the initial values of $\mathsf{c}$ and $\mathsf{d}$ may be arbitrary, in a
nondeterministic way, as long as they satisfy the latter equality in (1); they
are hence unbounded. Under these assumptions, the ratio technique of [stoc19]
allows one to correctly simulate unboundedly many zero tests (in fact, the
number of simulated zero tests corresponds to the initial value of
$\mathsf{c}$ which may be arbitrarily large) on counters bounded by $B$, at
the price of using some auxiliary counters.

As our technical contribution, we improve and simplify the ratio technique.
The core idea underlying our simplification is, intuitively speaking, to swap
the roles of counters $\mathsf{b}$ and $\mathsf{c}$: we observe that the
above-defined assumption (1) allows us to correctly simulate exactly $B/2$
zero tests (for $B$ even) on unbounded counters (in fact, on counters bounded
by the initial value of $\mathsf{c}$ which may be arbitrarily large), without
any auxiliary counters. This novel approach is presented in detail in Section
4.

##  3 Multipliers

Following the lines of [stoc19, jacm, CO], we rely on a concept of
_multiplier_.

### Sets computed by programs

Consider a program $\mathcal{P}$ with counters $\mathsf{C}$, a set of counters
$\mathsf{X}\subseteq\mathsf{C}$ and $R\subseteq\mathbb{N}^{{\mathsf{C}}}$. We
define the set _$\mathsf{X}$ -computed by $\mathcal{P}$ from $R$_ as the set
of all valuations of counters at the end of all $\mathsf{X}$-zeroing (and
hence forcedly complete) runs of $\mathcal{P}$ from $R$. Formally, denoting by
$\textsc{Runs}_{\mathcal{P}}(R,\mathsf{X})$ the set of all
$\mathsf{X}$-zeroing runs of $\mathcal{P}$ from $R$, and by
$\textsc{fin}(\pi)$ the final counter valuation of a complete run $\pi$ of
$\mathcal{P}$, the set $\mathsf{X}$-computed by $\mathcal{P}$ from $R$ is

$\text{\sc Comp}_{\mathcal{P}}(R,\mathsf{X})\ =\
\\{\textsc{fin}(\pi)\mid\pi\in\textsc{Runs}_{\mathcal{P}}(R,\mathsf{X})\\}.$

We omit $\mathsf{X}$ when it is irrelevant. As before, when
$\mathsf{X}=\\{\mathsf{x}\\}$ and/or $R=\\{r\\}$ are a singleton we write
simply ’$\mathsf{x}$-computed’ and/or ’from $r$’.

######  Example 3.1.

The program in Example 2.1 above, $\mathsf{x}$-computes from the set of all
valuations satisfying $\mathsf{y}=\mathsf{z}=0$ (no constraint for
$\mathsf{x}$), the set of all valuations satisfying $\mathsf{x}=0$ (trivially)
and $\mathsf{z}=2\mathsf{y}+1$.

Likewise, for a fixed integer $m\in\mathbb{N}$ and a program $\mathcal{P}$
with zero tests, we define the set $\mathsf{X}$-computed by $\mathcal{P}$ from
$R$ _using $m$ zero tests_, by restricting the above definition to runs
$\pi\in\textsc{Runs}_{\mathcal{P}}(R,\mathsf{X})$ that do exactly $m$ zero
tests. This finer variant of the definition will be used in the next section.

### Multipliers

Let $\mathsf{b},\mathsf{c},\mathsf{d}\in\mathsf{C}$ be some three
distinguished counters, and $B\in\mathbb{N}_{4}$. We define the subset
$\succeq/(B,\mathsf{b},\mathsf{c},\mathsf{d},\mathsf{C})\subseteq\mathbb{N}^{{\mathsf{C}}}$,
called informally the _ratio of $B$_, consisting of all valuations that
satisfy the three conditions (1) and assign 0 to all other counters
$\mathsf{x}\in\mathsf{C}\setminus\\{\mathsf{b},\mathsf{c},\mathsf{d}\\}$.

######  Definition 3.2.

A program $\mathcal{M}$ (with no zero tests) with counters $\mathsf{C}$ that
$\mathsf{z}$-computes from the zero valuation ${\bf 0}$ the set
$\geq/(B,\mathsf{b},\mathsf{c},\mathsf{d},\mathsf{C})$, for some four of its
counters $\mathsf{z},\mathsf{b},\mathsf{c},\mathsf{d}\in\mathsf{C}$, we call
$B$-multiplier. In formula: $\text{\sc Comp}_{\mathcal{M}}({\bf
0},\mathsf{z})=\geq/(B,\mathsf{b},\mathsf{c},\mathsf{d},\mathsf{C})$.

######  Example 3.3.

As a simple example, for every fixed $B\in\mathbb{N}_{4}$, the following
program is a $B$-multiplier of size $\mathcal{O}(B)$ (several commands are
written in one line to save space). Counter $\mathsf{z}$ is not used at all.

Program $\mathcal{M}_{B}(\mathsf{b},\mathsf{c},\mathsf{d})$:

1:$\mathsf{b}\,\,+\\!\\!=\,B$ $\mathsf{d}\,\,+\\!\\!=\,B$
$\mathsf{c}\,\,+\\!\\!=\,1$

2:loop

3: $\mathsf{d}\,\,+\\!\\!=\,B$ $\mathsf{c}\,\,+\\!\\!=\,1$

Directly from the definition we derive the following fundamental property of
multipliers, to be used in the proofs in Sections 5 and 6:

######  Claim 2.

Let $\mathcal{M}$ be a $B$-multiplier with counters $\mathsf{C}$ as in
Definition 3.2, let $\mathcal{P}$ be a counter program with counters
$\mathsf{C}\setminus\\{\mathsf{z}\\}$, and let
$\mathsf{Y}\subseteq\mathsf{C}$. Then the set $\mathsf{Y}$-computed by
$\mathcal{P}$ from $\geq/(B,\mathsf{b},\mathsf{c},\mathsf{d},\mathsf{C})$ is
equal to the set $(\\{\mathsf{z}\\}\cup\mathsf{Y})$-computed by the composed
program $\mathcal{M}\ \mathcal{P}$ from ${\bf 0}$:

$\text{\sc
Comp}_{\mathcal{P}}(\geq/(B,\mathsf{b},\mathsf{c},\mathsf{d},\mathsf{C}),\mathsf{Y})\
=\ \text{\sc Comp}_{\mathcal{M}\,\mathcal{P}}({\bf
0},\\{\mathsf{z}\\}\cup\mathsf{Y}).$

######  Proof 3.4.

The claim is a special case of the following general composition rule: for two
programs $\mathcal{P}$ and $\mathcal{Q}$, if $\text{\sc
Comp}_{\mathcal{P}}(A,\mathsf{X})=B$ and $\mathcal{Q}$ does not use counters
$\mathsf{X}$, then $\text{\sc
Comp}_{\mathcal{P}\,\mathcal{Q}}(A,\mathsf{X}\cup\mathsf{Y})=\text{\sc
Comp}_{\mathcal{Q}}(B,\mathsf{Y})$. Indeed, under the above assumptions
$(\mathsf{X}\cup\mathsf{Y})$-zeroing runs of $\mathcal{P}\ \mathcal{Q}$ from
$A$ are in mutual correspondence with $\mathsf{Y}$-zeroing runs of
$\mathcal{Q}$ from $B$.

### Computing multipliers

For technical convenience we prefer to rely on the following family of
functions $\mathbf{F}_{i}:\mathbb{N}_{4}\to\mathbb{N}_{4}$, indexed by
$i\in\mathbb{N}_{1}$, closely related to functions $\mathbf{A}_{i}$ (cf. Claim
3 below):

$\displaystyle\mathbf{F}_{1}(n)=2n,\qquad\mathbf{F}_{i+1}=\widetilde{\mathbf{F}_{i}}\quad\text{where
}\quad\widetilde{F}(n)=\underbrace{F\circ F\circ\ldots\circ F}_{n/4}(4).$ (2)

By induction on $i$ one easily shows that $\mathbf{F}_{i}$ is a linear re-
scaling of $\mathbf{A}_{i}$:

######  Claim 3.

$\mathbf{F}_{i}(4\cdot n)=4\cdot\mathbf{A}_{i}(n)$, for
$i,n\in\mathbb{N}_{1}$.

######  Proof 3.5.

As $\mathbf{F}_{1}(n)=2n$ and $\mathbf{A}_{1}(n)=2n$, the claim holds for
$i=1$. Assuming the claim for $i\in\mathbb{N}_{1}$, by $n$-fold application
thereof we derive the required equality for $i+1$:

$\mathbf{F}_{i+1}(4\cdot n)\ =\
\underbrace{\mathbf{F}_{i}\circ\ldots\circ\mathbf{F}_{i}}_{n}(4)\ =\
4\cdot\underbrace{\mathbf{A}_{i}\circ\ldots\circ\mathbf{A}_{i}}_{n}(1)\ =\
4\cdot\mathbf{A}_{i+1}(n).$

As a technical core of the proof of Theorem 2.2, combining our simplification
with the lines of [CO], we provide an effective construction of
$B$-multipliers with $3k+2$ counters, where $B=\mathbf{F}_{k}(n)$, of size
polynomial in $k$ and $n$.

######  Theorem 3.6.

Given $k\in\mathbb{N}_{1}$ and $n\in\mathbb{N}_{4}$ one can compute, in time
polynomial in $k$ and $n$, an $\mathbf{F}_{k}(n)$-multiplier with $3k+2$
counters.

The proof is in Section 5.

##  4 Bounded number of zero tests

In this section we provide a novel construction that enables simulating a
bounded number $m$ of zero tests (cf. Lemma 4.2) at the cost of introducing
additional 3 counters initialised to the ratio of $B=2(m+1)$. This
construction is a core ingredient of the proofs of Theorems 2.2 and 3.6.

Whenever analysing a single run of a program, we denote by
$\overline{\mathsf{x}}$ the initial value of a counter $\mathsf{x}$, and by
$\underline{\mathsf{x}}$ the final value thereof.

### Maximal iteration

In the sequel we intensively use loops of the following form that,
intuitively, flush the value from counter $\mathsf{f}$ to $\mathsf{e}$,
decreasing simultaneously counter $\mathsf{d}$ (and possibly execute some
further commands):

(3)

Assuming $\overline{\mathsf{d}}\geq\overline{\mathsf{f}}$, we observe that the
amount $\overline{\mathsf{d}}-\underline{\mathsf{d}}$ by which $\mathsf{d}$ is
decreased as an effect of execution (we use the word _execution_ as a synonym
to _complete run_) of the above loop may be any value between $0$ and
$\overline{\mathsf{f}}$. Furthermore, assuming
$\overline{\mathsf{d}}\geq\overline{\mathsf{e}}+\overline{\mathsf{f}}$, the
equality
$\overline{\mathsf{d}}-\underline{\mathsf{d}}=\overline{\mathsf{e}}+\overline{\mathsf{f}}$
holds if and only if

$\displaystyle\overline{\mathsf{e}}=0=\underline{\mathsf{f}}.$ (4)

This simple observation will play a crucial role in the sequel, and deserves a
definition:

######  Definition 4.1.

Whenever an execution of a loop of the form (3) satisfies the two equalities
(4) we call this execution maximally iterated.

### The construction

Let $\mathcal{P}$ be a counter program with counters $\mathsf{C}$, and assume
that $\mathcal{P}$ uses zero tests only on two its counters
$\mathsf{x},\mathsf{y}\in\mathsf{C}$ (the construction easily extends to
programs with an arbitrary number of zero-tested counters). We add to
$\mathcal{P}$ three fresh counters $\mathsf{b},\mathsf{c},\mathsf{d}$ (let
$\mathsf{C^{*}\\!}=\mathsf{C}\cup\\{\mathsf{b},\mathsf{c},\mathsf{d}\\}$), and
transform $\mathcal{P}$ into a program $\mathcal{P}^{*}\\!$ _without zero
tests_ that, assuming its initial valuation of counters belongs to
$=/(2(m+1),\mathsf{b},\mathsf{c},\mathsf{d},\mathsf{C^{*}\\!})$ for some
$m\in\mathbb{N}$, simulates correctly $m$ zero tests (jointly) on counters
$\mathsf{x},\mathsf{y}$, as long as their sum is bounded by the initial value
of $\mathsf{c}$ (cf. Lemma 4.2).

The transformation proceeds in three steps. First, we accompany every
increment (decrement) on $\mathsf{x}$ with a decrement (increment) of
$\mathsf{c}$, and likewise we do for $\mathsf{y}$:

> command | replaced by
> ---|---
> $\mathsf{x}\,\,+\\!\\!=\,1$ |  $\mathsf{x}\,\,+\\!\\!=\,1$ $\mathsf{c}\,\,-\\!\\!=\,1$
> $\mathsf{x}\,\,-\\!\\!=\,1$ |  $\mathsf{x}\,\,-\\!\\!=\,1$ $\mathsf{c}\,\,+\\!\\!=\,1$
> command | replaced by
> ---|---
> $\mathsf{y}\,\,+\\!\\!=\,1$ |  $\mathsf{y}\,\,+\\!\\!=\,1$ $\mathsf{c}\,\,-\\!\\!=\,1$
> $\mathsf{y}\,\,-\\!\\!=\,1$ |  $\mathsf{y}\,\,-\\!\\!=\,1$ $\mathsf{c}\,\,+\\!\\!=\,1$

In the resulting program $\mathcal{\overline{P}}$ counters $\mathsf{x}$,
$\mathsf{y}$ are, intuitively speaking, put on a shared ’budget’ $\mathsf{c}$.
Assuming $\mathsf{x}$ and $\mathsf{y}$ initially 0, this clearly enforces
$\mathsf{x}+\mathsf{y}$ to not exceed the initial value of $\mathsf{c}$, and
the sum $s=\mathsf{c}+\mathsf{x}+\mathsf{y}$ to remain invariant.

As the second step, we replace in $\mathcal{\overline{P}}$ every zero?
$\mathsf{x}$ command by the following macro:

$\text{\sc Zero?}\,\mathsf{x}$:

1:loop

2: $\mathsf{y}\,\,-\\!\\!=\,1$ $\mathsf{x}\,\,+\\!\\!=\,1$
$\mathsf{d}\,\,-\\!\\!=\,1$

3:loop

4: $\mathsf{c}\,\,-\\!\\!=\,1$ $\mathsf{y}\,\,+\\!\\!=\,1$
$\mathsf{d}\,\,-\\!\\!=\,1$

5:loop

6: $\mathsf{y}\,\,-\\!\\!=\,1$ $\mathsf{c}\,\,+\\!\\!=\,1$
$\mathsf{d}\,\,-\\!\\!=\,1$

7:loop

8: $\mathsf{x}\,\,-\\!\\!=\,1$ $\mathsf{y}\,\,+\\!\\!=\,1$
$\mathsf{d}\,\,-\\!\\!=\,1$

9:$\mathsf{b}\,\,-\\!\\!=\,2$

Likewise we replace every zero? $\mathsf{y}$ command by an analogous macro
$\text{\sc Zero?}\,\mathsf{y}$ obtained from $\text{\sc Zero?}\,\mathsf{x}$ by
swapping $\mathsf{x}$ and $\mathsf{y}$. This yields the program
$\mathcal{\widehat{P}}$ without zero tests. We note that each of the two Zero?
macros preserves the sum $s=\mathsf{c}+\mathsf{x}+\mathsf{y}$, and decrements
the counter $\mathsf{b}$ by $2$. Furthermore, each of the two Zero? macros
decrements $\mathsf{d}$ by at most $2s$ (cf. Claim 4 below), and hence the
macros preserve the inequality $d\geq\mathsf{b}\cdot s$ (recall that
$\mathsf{d}=\mathsf{b}\cdot s$ holds initially).

As the final step we adjoint at the end of $\mathcal{\widehat{P}}$ the
following program Set-$\mathsf{c}$-to-zero, thus obtaining the transformed
program $\mathcal{P}^{*}\\!$:

Set-$\mathsf{c}$-to-zero:

1:loop

2: $\mathsf{c}\,\,-\\!\\!=\,1$ $\mathsf{d}\,\,-\\!\\!=\,2$

3:$\text{\sc Zero?}\,\mathsf{c}$

The macro $\text{\sc Zero?}\,\mathsf{c}$ is obtained from $\text{\sc
Zero?}\,\mathsf{x}$ by swapping $\mathsf{x}$ and $\mathsf{c}$. We note that an
execution of Set-$\mathsf{c}$-to-zero may decrease the sum
$\mathsf{c}+\mathsf{x}+\mathsf{y}$ (but $\text{\sc Zero?}\,\mathsf{c}$
preserves it).

### Correctness

Recall that $\mathcal{\widehat{P}}$ preserves the sum
$\mathsf{c}+\mathsf{x}+\mathsf{y}$; we denote by $s$ the value of this sum. An
execution of $\text{\sc Zero?}\,\mathsf{x}$ is called _maximally iterated_ if
all four loops are so. Observe that every such execution is forcedly _correct_
, i.e. satisfies:

$\displaystyle\overline{\mathsf{x}}=\underline{\mathsf{x}}=0,\qquad\overline{\mathsf{y}}=\underline{\mathsf{y}},\qquad\overline{\mathsf{c}}=\underline{\mathsf{c}}.$
(5)

(Likewise in case of $\text{\sc Zero?}\,\mathsf{y}$ and $\text{\sc
Zero?}\,\mathsf{c}$.) The idea behind $\text{\sc Zero?}\,\mathsf{x}$ is to
flush from $\mathsf{y}$ to a zero-tested counter $\mathsf{x}$ and back, but
also flush from $\mathsf{c}$ to $\mathsf{y}$ and back, in an appropriately
nested way that guarantees that the amount
$\overline{\mathsf{d}}-\underline{\mathsf{d}}$ by which $\mathsf{d}$ is
decreased equals $2s$ exactly in maximally iterated executions:

######  Claim 4.

Consider an execution of $\text{\sc Zero?}\,\mathsf{x}$ (resp. $\text{\sc
Zero?}\,\mathsf{y}$) macro, assuming $\overline{\mathsf{d}}\geq 2s$. Then
$0\leq\overline{\mathsf{d}}-\underline{\mathsf{d}}\leq 2s$. Furthermore, the
equality $\overline{\mathsf{d}}-\underline{\mathsf{d}}=2s$ holds if and only
if the execution is maximally iterated.

Consider an execution of $\text{\sc Zero?}\,\mathsf{x}$, assuming
$\overline{\mathsf{d}}\geq 2s$, and let $\dot{\mathsf{y}}$ denote the value of
$\mathsf{y}$ at the exit from the first loop. The amount by which $\mathsf{d}$
is decreased in the two loops in lines 1–2 and 7–8 is at most

$\Delta_{1}=2(\overline{\mathsf{y}}-\dot{\mathsf{y}})+\overline{\mathsf{x}}.$

Furthermore, the amount by which $\mathsf{d}$ is decreased in the two loops in
lines 3–6 is at most

$\Delta_{2}=2\overline{\mathsf{c}}+\dot{\mathsf{y}}.$

The sum $\Delta_{1}+\Delta_{2}$ clearly satisfies $\Delta_{1}+\Delta_{2}\leq
2s=2(\overline{\mathsf{c}}+\overline{\mathsf{x}}+\overline{\mathsf{y}})$. It
equals $2s$ if and only if $\Delta_{1}=2\overline{\mathsf{y}}$ and
$\Delta_{2}=2\overline{\mathsf{c}}$, i.e., exactly when all four loops are
maximally iterated. In consequence, as $\mathsf{b}$ is decreased by $2$, if
the invariant $\mathsf{d}=\mathsf{b}\cdot s$ is preserved by an execution of
$\text{\sc Zero?}\,\mathsf{x}$ (resp. $\text{\sc Zero?}\,\mathsf{y}$) then the
zero test is forcedly correct. Furthermore notice that once the invariant is
violated, i.e., $\mathsf{d}>\mathsf{b}\cdot s$, due to the first part of Claim
4 the invariant can not be recovered later. These observations lead to the
correctness claim stated in Lemma 4.2.

In the proof of Lemma 4.2 we will also need the following corollary of Claim
4, where $s$ denotes, as before, the sum $\mathsf{c}+\mathsf{x}+\mathsf{y}$ at
the start of $\text{\sc Set-$\mathsf{c}$-to-zero}(\mathsf{c})$:

######  Claim 5.

Consider an execution of $\text{\sc Set-$\mathsf{c}$-to-zero}(\mathsf{c})$,
assuming $\overline{\mathsf{d}}\geq 2s$. Then
$0\leq\overline{\mathsf{d}}-\underline{\mathsf{d}}\leq 2s$. Furthermore, the
equality $\overline{\mathsf{d}}-\underline{\mathsf{d}}=2s$ holds if and only
if the $\text{\sc Zero?}\,\mathsf{c}$ macro is maximally iterated.

Consider an execution of $\text{\sc Set-$\mathsf{c}$-to-zero}(\mathsf{c})$ and
denote by $\dot{s}$ the value of $\mathsf{c}+\mathsf{x}+\mathsf{y}$ just
before entering $\text{\sc Zero?}\,\mathsf{c}$. Thus $\mathsf{d}$ decrease by
$2(s-\dot{s})$ before entering $\text{\sc Zero?}\,\mathsf{c}$. Moreover, due
to Claim 4, the macro $\text{\sc Zero?}\,\mathsf{c}$ decreases $\mathsf{d}$ by
at most $2\dot{s}$, and furthermore the macro decreases $\mathsf{d}$ by
exactly $2\dot{s}$ if and only if it is maximally iterated. These observations
imply the claim.

Recall that
$\mathsf{C^{*}\\!}=\mathsf{C}\cup\\{\mathsf{b},\mathsf{c},\mathsf{d}\\}$. We
define the _$\mathsf{C^{*}\\!}$ -extension_ of a counter valuation
$v\in\mathbb{N}^{{\mathsf{C}}}$ as the extension of $v$ where
$\mathsf{b},\mathsf{c}$ and $\mathsf{d}$ are all set to $0$. The
$\mathsf{C^{*}\\!}$-extension of a set $R\subseteq\mathbb{N}^{{\mathsf{C}}}$
is defined as the set of $\mathsf{C^{*}\\!}$-extensions of all valuations in
$R$.

######  Lemma 4.2.

The following sets are equal (as subsets of
$\mathbb{N}^{{\mathsf{C^{*}\\!}}}$):

  * •

the $\mathsf{C^{*}\\!}$-extension of the set computed by $\mathcal{P}$ from
${\bf 0}$ using $m$ zero tests.

  * •

the set $\mathsf{d}$-computed by $\mathcal{P}^{*}\\!$ from
$=/(2(m+1),\mathsf{b},\mathsf{c},\mathsf{d},\mathsf{C^{*}\\!})$.

######  Proof 4.3.

For the inclusion of the former set in the latter, we show that for each
complete run $\pi$ of $\mathcal{P}$ from ${\bf 0}$ that does $m$ zero tests on
$\mathsf{x},\mathsf{y}$, there is a corresponding $\mathsf{d}$-zeroing run of
$\mathcal{P}^{*}\\!$ from
$=/(2(m+1),\mathsf{b},\mathsf{c},\mathsf{d},\mathsf{C^{*}\\!})$, for any
initial value $\overline{\mathsf{c}}$ at least as large as the maximal value
of the sum $\mathsf{x}+\mathsf{y}$ along $\pi$. The run iterates maximally
$\text{\sc Zero?}\,\mathsf{x}$ and $\text{\sc Zero?}\,\mathsf{y}$ macros,
decrements $\mathsf{c}$ to $0$ in line 2 in $\text{\sc Set-$\mathsf{c}$-to-
zero}(\mathsf{c})$, and then iterates maximally $\text{\sc
Zero?}\,\mathsf{c}$. Thus the final counter valuation of the run is the
$\mathsf{C^{*}\\!}$-extension of the final counter valuation of $\pi$.

For the converse direction, consider a $\mathsf{d}$-zeroing run $\pi$ of
$\mathcal{P}^{*}\\!$ from
$=/(2(m+1),\mathsf{b},\mathsf{c},\mathsf{d},\mathsf{C^{*}\\!})$. The initial
counter valuation satisfies the equalities $\mathsf{b}=2(m+1)$ and
$\mathsf{d}=2(m+1)\cdot s$. Each execution of $\text{\sc Zero?}\,\mathsf{x}$
or $\text{\sc Zero?}\,\mathsf{y}$ or $\text{\sc Set-$\mathsf{c}$-to-
zero}(\mathsf{c})$ decreases $\mathsf{b}$ by $2$, and $\mathsf{d}$ by at most
$2s$ (by the first part of Claims 4 and Claim 5). Therefore, since
$\mathsf{b}$ and $\mathsf{d}$ are not affected elsewhere and
$\underline{\mathsf{d}}=0$ finally, we deduce:

######  Claim 6.

Each execution of $\text{\sc Zero?}\,\mathsf{x}$, $\text{\sc
Zero?}\,\mathsf{y}$ or $\text{\sc Zero?}\,\mathsf{c}$ in $\pi$ decreases
$\mathsf{d}$ by _exactly_ $2s$.

######  Claim 7.

There are exactly $m$ executions of $\text{\sc Zero?}\,\mathsf{x}$ or
$\text{\sc Zero?}\,\mathsf{y}$ in $\pi$.

######  Claim 8.

Finally, $\underline{\mathsf{b}}=0$.

By Claim 6 and the second part of Claim 4 we derive:

######  Claim 9.

Each execution of $\text{\sc Zero?}\,\mathsf{x}$ in $\pi$ is correct, i.e.
satisfies the equalities (5). Likewise for $\text{\sc Zero?}\,\mathsf{y}$.

Analogously, by Claim 6 and the second part of Claim 5 we derive:

######  Claim 10.

Finally, $\underline{\mathsf{c}}=0$.

Due to Claims 7 and 9, once we project away from $\pi$ the counters
$\mathsf{b},\mathsf{c},\mathsf{d}$, we obtain a complete run of $\mathcal{P}$
from ${\bf 0}$ that does exactly $m$ zero tests, as required. Finally, due to
Claims 8 and 10, the $\mathsf{C^{*}\\!}$-extension of the final counter
valuation of the obtained run is exactly the final counter valuation of $\pi$.

##  5 Computing a large multiplier (Proof of Theorem 3.6)

The proof proceeds by combining the concept of amplifier lifting of [CO] with
the program transformation of Section 4.

### Amplifiers

Let $F:\mathbb{N}_{4}\to\mathbb{N}_{4}$ be a monotone function satisfying
$F(n)\geq n$ for $n\in\mathbb{N}_{4}$. Informally speaking, an _$F$
-amplifier_ is a program without zero tests that computes the ratio of $F(B)$
from the ratio of $B$, for every $B\in\mathbb{N}_{4}$.

######  Definition 5.1.

Consider a program $\mathcal{P}$ with counters $\mathsf{C}$ without zero tests
and distinguished three _input counters_
$\mathsf{b},\mathsf{c},\mathsf{d}\in\mathsf{C}$ and three _output counters_
$\mathsf{b}^{\prime},\mathsf{c}^{\prime},\mathsf{d}^{\prime}\in\mathsf{C}$.
The program is called $F$-amplifier if for every $B\in\mathbb{N}_{4}$, it
$\mathsf{d}$-computes from $=/(B,\mathsf{b},\mathsf{c},\mathsf{d},\mathsf{C})$
the set
$\geq/(F(B),\mathsf{b}^{\prime},\mathsf{c}^{\prime},\mathsf{d}^{\prime},\mathsf{C})$.

We note that no condition is imposed on $\mathsf{d}$-zeroing runs from counter
valuations not belonging to any set
$\geq/(B,\mathsf{b},\mathsf{c},\mathsf{d},\mathsf{C})$. As an example,
consider the following program $\mathcal{L}_{\ell}$, for
$\ell\in\mathbb{N}_{1}$, with input counters
$\mathsf{b},\mathsf{c},\mathsf{d}$ and output counters
$\mathsf{b}^{\prime},\mathsf{c}^{\prime},\mathsf{d}^{\prime}$:

Program
$\mathcal{L}_{\ell}(\mathsf{b},\mathsf{c},\mathsf{d},\mathsf{b}^{\prime},\mathsf{c}^{\prime},\mathsf{d}^{\prime})$:

1:loop

2: loop

3: $\mathsf{c}\,\,-\\!\\!=\,1$ $\mathsf{c}^{\prime}\,\,+\\!\\!=\,1$
$\mathsf{d}\,\,-\\!\\!=\,1$ $\mathsf{d}^{\prime}\,\,+\\!\\!=\,\ell$

4: loop

5: $\mathsf{c}^{\prime}\,\,-\\!\\!=\,1$ $\mathsf{c}\,\,+\\!\\!=\,1$
$\mathsf{d}\,\,-\\!\\!=\,1$ $\mathsf{d}^{\prime}\,\,+\\!\\!=\,\ell$

6: $\mathsf{b}\,\,-\\!\\!=\,2$ $\mathsf{b}^{\prime}\,\,+\\!\\!=\,2\ell$

7:loop

8: $\mathsf{c}\,\,-\\!\\!=\,1$ $\mathsf{c}^{\prime}\,\,+\\!\\!=\,1$
$\mathsf{d}\,\,-\\!\\!=\,2$ $\mathsf{d}^{\prime}\,\,+\\!\\!=\,2\ell$

9:$\mathsf{b}\,\,-\\!\\!=\,2$ $\mathsf{b}^{\prime}\,\,+\\!\\!=\,2\ell$

######  Claim 11.

The above program is an $L_{\ell}$-amplifier, where
$L_{\ell}:\mathbb{N}_{4}\to\mathbb{N}_{4}=(x\mapsto\ell\cdot x)$.

[Proof sketch] Writing counter valuations as vectors
$(\mathsf{b},\mathsf{c},\mathsf{d},\mathsf{b}^{\prime},\mathsf{c}^{\prime},\mathsf{d}^{\prime})$,
one shows that the program $\mathsf{d}$-computes, from the set containing just
one counter valuation $(B,c,d,0,0,0)$, the set containing one counter
valuation $(0,0,0,\ell\cdot B,c,\ell\cdot d)$. Indeed, as $\mathsf{d}=0$
finally, each of the two inner loops in lines 2–5, as well as the last loop in
lines 7–8, is forcedly maximally iterated. Putting $\ell=1$ we get an
identity-amplifier
$\mathcal{L}_{1}(\mathsf{b},\mathsf{c},\mathsf{d},\mathsf{b}^{\prime},\mathsf{c}^{\prime},\mathsf{d}^{\prime})$.

### Amplifier lifting

Recall the definition (2) of functions $\mathbf{F}_{i}$; in particular
$\mathbf{F}_{1}=L_{2}$. Let $\mathcal{P}$ be a program with counters
$\mathsf{C}$, without zero tests, with distinguished input counters
$\mathsf{b}_{1},\mathsf{c}_{1},\mathsf{d}_{1}\in\mathsf{C}$ and output
counters $\mathsf{b}_{2},\mathsf{c}_{2},\mathsf{d}_{2}\in\mathsf{C}$. We
describe a transformation of the program $\mathcal{P}$ to a program
$\widetilde{\mathcal{P}}$, also without zero tests, such that assuming that
$\mathcal{P}$ is an $F$-amplifier for some function
$F:\mathbb{N}_{4}\to\mathbb{N}_{4}$, the program $\widetilde{\mathcal{P}}$ is
an $\widetilde{F}$-amplifier. The program $\widetilde{\mathcal{P}}$ uses,
except for the counters of $\mathcal{P}$, three fresh counters
$\mathsf{b},\mathsf{c},\mathsf{d}$. Thus counters of $\widetilde{\mathcal{P}}$
are $\mathsf{C^{*}\\!}=\mathsf{C}\cup\\{\mathsf{b},\mathsf{c},\mathsf{d}\\}$.
We let input counters of $\widetilde{\mathcal{P}}$ be
$\mathsf{b},\mathsf{c},\mathsf{d}$, and its output counters be
$\mathsf{b}_{2},\mathsf{c}_{2},\mathsf{d}_{2}$.

In the transformation we use the identity-amplifier
$\mathcal{L}=\mathcal{L}_{1}(\mathsf{b}_{2},\mathsf{c}_{2},\mathsf{d}_{2},\mathsf{b}_{1},\mathsf{c}_{1},\mathsf{d}_{1})$
with input counters $\mathsf{b}_{2},\mathsf{c}_{2},\mathsf{d}_{2}$ and output
counters $\mathsf{b}_{1},\mathsf{c}_{1},\mathsf{d}_{1}$, and the
$4$-multiplier
$\mathcal{M}=\mathcal{M}_{4}(\mathsf{b}_{1},\mathsf{c}_{1},\mathsf{d}_{1})$ of
Example 3.3, both without zero tests. For defining the program
$\widetilde{\mathcal{P}}$ we apply the transformation of Section 4 (with
counters $\mathsf{d}_{1}$ and $\mathsf{d}_{2}$ in place of $\mathsf{x}$ and
$\mathsf{y}$) to the following program $\mathcal{Q}$ built using
$\mathcal{P}$, $\mathcal{L}$ and $\mathcal{M}$:

Program $\mathcal{Q}$:

1:$\mathcal{M}$

2:loop

3: $\mathcal{P}$

4: zero? $\mathsf{d}_{1}$

5: $\mathcal{L}$

6: zero? $\mathsf{d}_{2}$

7:$\mathcal{P}$

8:zero? $\mathsf{d}_{1}$

Program $\widetilde{\mathcal{P}}$:

1:$\mathcal{\overline{M}}$

2:loop

3: $\mathcal{\overline{P}}$

4: $\text{\sc Zero?}\,\mathsf{d}_{1}$

5: $\overline{\mathcal{L}}$

6: $\text{\sc Zero?}\,\mathsf{d}_{2}$

7:$\mathcal{\overline{P}}$

8:$\text{\sc Zero?}\,\mathsf{d}_{1}$

9:Set-$\mathsf{c}$-to-zero

Formally, $\widetilde{\mathcal{P}}=\mathcal{Q}^{*}\\!$. Intuitively speaking,
the program $\mathcal{Q}$ directly implements the computation of
$\widetilde{F}$ according to the definition: with $2\ell+1$ zero tests it
computes, from ${\bf 0}$, the ratio of $F^{\ell+1}(4)$. Note that counters of
$\mathcal{Q}$ are $\mathsf{C}$ while counters of $\widetilde{\mathcal{P}}$ are
$C^{*}\\!$. Lemma 5.2 states the crucial amplifier-lifting property of the
program transformation $\mathcal{P}\mapsto\widetilde{\mathcal{P}}$.

######  Lemma 5.2.

If $\mathcal{P}$ is an $F$-amplifier, then $\widetilde{\mathcal{P}}$ is an
$\widetilde{F}$-amplifier.

######  Proof 5.3.

Let $\mathcal{P}$ be an $F$-amplifier. Thus for every $B\in\mathbb{N}_{4}$,
$\text{\sc
Comp}_{\mathcal{P}}(=/(B,\mathsf{b}_{1},\mathsf{c}_{1},\mathsf{d}_{1},\mathsf{C}),\mathsf{d}_{1})=\geq/(F(B),\mathsf{b}_{2},\mathsf{c}_{2},\mathsf{d}_{2},\mathsf{C})$.
The program $\mathcal{L}$, being an identity-amplifier,
$\mathsf{d}_{2}$-computes from
$=/(B,\mathsf{b}_{2},\mathsf{c}_{2},\mathsf{d}_{2},\mathsf{C})$ the set
$\geq/(B,\mathsf{b}_{1},\mathsf{c}_{1},\mathsf{d}_{1},\mathsf{C})$. Let
$B=4(\ell+1)\in\mathbb{N}_{4}$ for an arbitrary $\ell\in\mathbb{N}$. As
$\mathcal{P}$ is an $F$-amplifier and $\mathcal{L}$ is an identity-amplifier,
we deduce:

######  Claim 12.

$\mathcal{Q}$ computes from ${\bf 0}$ using $2\ell+1$ zero tests the set
$\geq/(F^{\ell+1}(4),\mathsf{b}_{2},\mathsf{c}_{2},\mathsf{d}_{2},\mathsf{C})$.

As $\widetilde{\mathcal{P}}=\mathcal{Q}^{*}\\!$, by Lemma 4.2 we deduce:

######  Claim 13.

$\text{\sc
Comp}_{\widetilde{\mathcal{P}}}(\geq/(4(\ell+1),\mathsf{b},\mathsf{c},\mathsf{d},\mathsf{{C^{*}\\!}}),\mathsf{d})=\geq/(F^{\ell+1}(4),\mathsf{b}_{2},\mathsf{c}_{2},\mathsf{d}_{2},\mathsf{C})$.

As $B\in\mathbb{N}_{4}$ was chosen arbitrarily and
$\widetilde{F}(B)=F^{\ell+1}(4)$, the last claim says that
$\widetilde{\mathcal{P}}$ is an $\widetilde{F}$-amplifier.

######  Remark 5.4.

The program $\mathcal{P}$ appears twice in the body of
$\widetilde{\mathcal{P}}$. This doubling can be easily avoided by re-
structuring the loop using explicit goto commands. In this way, the size of
$\widetilde{\mathcal{P}}$ becomes larger than the size of $\mathcal{P}$ only
by a constant.

######  Proof 5.5 (Proof of Theorem 3.6).

We rely on Lemma 5.2. Given $k\in\mathbb{N}_{1}$ and $n\in\mathbb{N}_{4}$ we
compute, in time linear in $k$, the $\mathbf{F}_{k}$-amplifier
$\mathcal{A}_{k}$ with $3k+3$ counters $\mathsf{C}$, by $(k-1)$-fold
application of the amplifier lifting transformation
$\mathcal{P}\mapsto\widetilde{\mathcal{P}}$ described above, starting from the
$\mathbf{F}_{1}$-amplifier $\mathcal{L}_{2}$ of Claim 11. The construction is
linear in $k$ due to Remark 5.4. Let
$\mathsf{b},\mathsf{c},\mathsf{d}\in\mathsf{C}$ be input counters of
$\mathcal{A}_{k}$. Relying on Claim 2 in Section 3, the
$\mathbf{F}_{k}(n)$-multiplier is obtained by pre-composing $\mathcal{A}_{k}$
with an $n$-multiplier (e.g.
$\mathcal{M}_{n}(\mathsf{b},\mathsf{c},\mathsf{d})$ from Section 2) that
outputs the set $\geq/(n,\mathsf{b},\mathsf{c},\mathsf{d},\mathsf{C})$. The
whole construction is thus linear in $n$.

Finally we observe that the counter $\mathsf{b}$ is bounded by $n$ and hence
can be eliminated: we encode its values in control locations, by cloning the
program into $n+1$ copies, where $i$th (for $i=0,\ldots,n$) copy corresponds
to the value $\mathsf{b}=i$. The resulting program has $3k+2$ counters.

##  6 Hardness of the reachability problem (Proof of Theorem 2.2)

Relying on Lemma 4.2 and Theorem 3.6, we prove in this section Theorem 2.2.
Fix $k\geq 3$. The proof proceeds by a polynomial-time reduction from the
following $\mathcal{F}_{k}$-hard problem: