11institutetext: Department of Computer Science, Stony Brook University, NY,
USA 22institutetext: Department of Biomedical Informatics, Stony Brook
University, NY, USA 33institutetext: Amazon, WA, USA 44institutetext: Shanghai
Artificial Intelligence Laboratory

# Token Sparsification for Faster
Medical Image Segmentation

Lei Zhou Corresponding author, 11<EMAIL_ADDRESS>Huidong Liu 1133
Joseph Bae 22 Junjun He 44
Dimitris Samaras 11 Prateek Prasanna 22

###### Abstract

Can we use sparse tokens for dense prediction, e.g., segmentation? Although
token sparsification has been applied to Vision Transformers (ViT) to
accelerate classification, it is still unknown how to perform segmentation
from sparse tokens. To this end, we reformulate segmentation as a sparse
encoding $\rightarrow$ token completion $\rightarrow$ dense decoding (SCD)
pipeline. We first empirically show that naïvely applying existing approaches
from classification token pruning and masked image modeling (MIM) leads to
failure and inefficient training caused by inappropriate sampling algorithms
and the low quality of the restored dense features. In this paper, we propose
Soft-topK Token Pruning (STP) and Multi-layer Token Assembly (MTA) to address
these problems. In sparse encoding, STP predicts token importance scores with
a lightweight sub-network and samples the topK tokens. The intractable topK
gradients are approximated through a continuous perturbed score distribution.
In token completion, MTA restores a full token sequence by assembling both
sparse output tokens and pruned multi-layer intermediate ones. The last dense
decoding stage is compatible with existing segmentation decoders, e.g., UNETR.
Experiments show SCD pipelines equipped with STP and MTA are much faster than
baselines without token pruning in both training (up to 120% higher
throughput) and inference (up to 60.6% higher throughput) while maintaining
segmentation quality. Code is available here: https://github.com/cvlab-
stonybrook/TokenSparse-for-MedSeg

###### Keywords:

Token Pruning Multi-layer Token Assembly Medical Image Segmentation.

##  1 Introduction

Vision Transformers (ViT) [6] for dense prediction [29, 20] have achieved
impressive results in tasks including medical image segmentation [8]. In
general, high-resolution features [26] preserving details are always desirable
for precise segmentation. However, because of the quadratic computation
complexity in self-attention [25], doubling the resolution per dimension in a
3D volume can lead to an 8$\times$ longer sequence and hence 64$\times$ more
computation. This growing computing burden can quickly surpass limited
computation budgets. Considering ViT’s flexibility and great potential in
masked image modeling [9, 14], we explore acceleration algorithms based on the
standard ViT. Recently, token sparsification [21, 15, 16] has been proposed to
accelerate inference in ViT for classification by dropping less important
tokens. However, to the best of our knowledge, there are no ViT token
sparsification approaches for segmentation. This leads us to ask the question:
Can we use sparse tokens for dense prediction, e.g., segmentation?

To answer the question, we reformulate segmentation as a sparse encoding
$\rightarrow$ token completion $\rightarrow$ dense decoding (SCD) pipeline.
Unlike a standard dense encoding $\rightarrow$ dense decoding (DD) pipeline,
sparse encoding and token completion are required in SCD. Sparse encoding
requires learning a sparse token representation for speed and token completion
is needed to restore the full set of tokens for dense prediction. We first
examine a naïve realization of sparse encoding and token completion by
applying existing approaches. Specifically, we adapt sampling methods in
classification, e.g., EViT [15] and DynamicViT [21], to sparse encoding, and
masked image modeling (MIM) [9, 2] to token completion. However, we observe
significantly inferior results in this SCD pipeline (See Table 1). Next, we
provide more insight into the problems of existing methods.
Problems in Sparse Encoding. There are two steps in this step, i.e., token
score estimation and token sampling. We show that EViT’s token score
estimation is inappropriate for segmentation and DynamicViT’s token sampling
leads to training inefficiency: i) EViT [15] uses the attention weights
between spatial tokens and the [CLS] token to estimate scores. While this is
sound for classification since [CLS] is used for prediction, it is sub-optimal
for segmentation because [CLS] is deprecated in the segmentation decoder. ii)
DynamicViT [21] estimates token scores with a sub-network. DynamicViT frames
token sampling as a series of independent binary decisions to keep or drop
tokens. This does not guarantee a fixed number of sampled tokens for each
training input. To fit in batch training, DynamicViT keeps all tokens in
memory and masks self-attention entries, leading to training inefficiency.
Problems in Token Completion. Previous sparse token classification models [21,
15] do not require token completion. Thus, we borrow the design from MIM. MIM
reconstructs full tokens from a partial token sequence by padding it to full
length with learnable mask tokens and then hallucinating the masked regions
from their context. While MIM is useful for pre-training, it cannot accurately
restore detailed information, resulting in inferior segmentation results.

We propose Soft-topK Token Pruning (STP) and Multi-layer Token Assembly (MTA)
to implement sparse encoding and token completion. i) In sparse encoding, STP
predicts token importance scores with a sub-network, avoiding the limitation
of [CLS] in segmentation. STP then samples topK-scored tokens instead of
making binary decisions per token separately, accelerating training by
retaining only the sampled tokens in memory and computing. Motivated by subset
sampling [28, 12, 5], the intractable gradients of the topK operation are
approximated through a perturbed continuous score distribution. ii) In token
completion, the MTA restores a full token sequence by assembling both sparse
output tokens and pruned intermediate tokens from multiple layers. Compared to
MIM that fills the pruned positions with identical mask tokens, MTA produces
more informative, position-specific representations. For dense decoding, the
SCD pipeline is compatible with existing segmentation decoders, such as UNETR.

We evaluate our method on two relatively sparse 3D medical image segmentation
datasets, the CT Abdomen Multi-organ Segmentation (BTCV [11], N=30) dataset
and the MRI Brain Tumor Segmentation (MSD BraTS [1], N=484) dataset. On both
tasks, STP+MTA+UNETR matches the UNETR baseline while providing significant
computing savings with large token pruning ratios. On BraTS, STP+MTA+UNETR
accelerates segmentation inference/training throughput by 60.6%/120% and
achieves the same segmentation accuracy. On BTCV, STP+MTA+UNETR increases
inference/training throughput by 24.1%/97.36% while maintaining performance.
In summary, our contributions are:

  * •

To the best of our knowledge, we are the first to use token pruning/dropping
for ViT-based medical image segmentation.

  * •

Based on subset sampling, our proposed Soft-topK Token Pruning (STP) module
can be flexibly incorporated into a standard ViT to prune tokens with greater
efficiency while maintaining accuracy.

  * •

We propose Multi-layer Token Assembly (MTA) to recover a full set of tokens,
i.e., a dense representation, from a sparse set. MTA preserves high-detail
information for accurate segmentation.

  * •

We show that STP+MTA+UNETR maintains performance compared with UNETR with much
less computation on two 3D medical image datasets.

##  2 Methodology

Generally, a segmentation model consists of an encoder and a decoder. Our goal
is to accelerate the ViT segmentation encoder. To this end, we reformulate
segmentation as a sparse encoding $\rightarrow$ token completion $\rightarrow$
dense decoding (SCD) pipeline. Sparse encoding learns a sparse token
representation for acceleration; token completion restores the full tokens for
dense prediction; dense decoding predicts the segmentation mask from dense
features. We first recap Vision Transformers and then illustrate the three
components in the SCD pipeline.

Figure 1: Sparse Token Segmentation Pipeline. We reformulate segmentation as a
sparse encoding $\rightarrow$ token completion $\rightarrow$ dense decoding
pipeline. In sparse encoding, we design a Soft-topK Token Pruning (STP)
module. In the forward pass, STP performs topK sampling on perturbed scores.
In the backward pass, STP approximates the intractable gradient with a
continuous Gumbel Softmax estimation. In token completion, we propose Multi-
layer Token Assembly (MTA) to assemble both the output sparse tokens and the
pruned intermediate ones to restore the complete tokens. In dense decoding, we
avoid the intermediate sparse tokens by taking all inputs from the output of
MTA. In this simplified figure, we visualize token pruning as dropping the
last token. However, in practice pruned tokens are selected according to
predicted scores.

Preliminary: Vision Transformers. Vision Transformers treat an image/volume as
a sequence of tokens. In the case of 3D medical images, a 3D volume
$\mathbf{x}\in\mathbb{R}^{H\times W\times D\times C_{in}}$ is first reshaped
to a sequence of flattened patches
$\mathbf{x}_{p}\in\mathbb{R}^{N\times(P^{3}\times C_{in})}$ where $H\times
W\times D$ is the spatial size, $C_{in}$ is the input channel, $P\times
P\times P$ is the patch size, and $N=HWD/P^{3}$ is the sequence length, i.e.,
the number of patches. All the patches are then projected linearly to a
$C$-dimensional token space, with position embeddings added to the projected
patches. These patch tokens, together with a learnable prepended [CLS] token,
are denoted as $\mathbf{z}_{0}\in\mathbb{R}^{(1+N)\times C}$. $\mathbf{z}_{0}$
are further processed by $L$ Transformer blocks sequentially. Each block
consists of a multi-head self-attention (MSA) module and an MLP. We denote the
tokens output from the ${i}$th Transformer block as
$\mathbf{z}_{i}\in\mathbb{R}^{(1+N)\times C}$. For the segmentation task,
before feeding the output $\mathbf{z}_{L}$ of the encoder to the decoder, we
drop the [CLS] token and project the non-[CLS] token sequence
$\mathbf{z}_{L}^{[1:N]}\in\mathbb{R}^{N\times C}$ back to the original 3D
feature map $\mathbf{x}_{L}\in\mathbb{R}^{H/P\times W/P\times D/P\times C}$.

###  2.1 Sparse Encoding: Soft-topK Token Pruning (STP)

We build our sparse encoder on a ViT without modifying the self-attention
module. Instead, we propose a learnable plug-and-play Soft-topK Token Pruning
(STP) module. Compared to EViT & DynamicViT, our STP, as shown in the lower
half of Fig. 1, estimates token scores more effectively and can be trained
efficiently. STP can be inserted between two Transformer blocks
$\mathtt{TF}_{i}$ and $\mathtt{TF}_{i+1}$. Receiving as input the token
sequence $\mathbf{z}_{i}\in\mathbb{R}^{N_{i}\times C}$ from $\mathtt{TF}_{i}$,
STP prunes tokens with a ratio $r$ and passes the remaining tokens
$\mathbf{z}_{i}^{\prime}\in\mathbb{R}^{\lfloor(1-r)N_{i}\rceil\times C}$ to
$\mathtt{TF}_{i+1}$. In particular, STP consists of token-wise score
estimation and token sampling. To be concise, we change the notation of number
of tokens from $N_{i}$ to $n$.
Token Score Estimation. To decide which tokens to keep or prune, we introduce
a lightweight sub-network $s_{\theta}:\mathbb{R}^{n\times
C}\rightarrow\mathbb{R}^{n}$ to predict the token importance scores
$\mathbf{s}$, where $\theta$ are the network parameters. The architecture of
$s_{\theta}$ is designed to aggregate both the local and global features,
similarly to [21]. The global feature is simply obtained by average pooling
over all the tokens.

$\mathbf{s}=s_{\theta}(\mathbf{z})=\mathtt{Sigmoid}\bigg{(}\mathtt{MLP_{2}}\Big{(}[\mathbf{z},\mathtt{AvgPool}\big{(}\mathtt{MLP_{1}}(\mathbf{z})\big{)}]\Big{)}\bigg{)}$
(1)

Straight-through Gumbel Soft TopK Sampling. Given a token pruning ratio $r$,
STP needs to select $K=\lfloor(1-r)n\rceil$ tokens out of $n$ to keep. After
predicting the scores $\mathbf{s}$, we re-interpret each score value
$\mathbf{s}_{i}$ as the probability of the $i$-th token ranking in the topK.
We formulate this process as sampling a binary policy mask
$\mathbf{M}\in\\{0,1\\}^{n}$ from the predicted probabilities where
$\mathbf{M}$ is subject to $\mathtt{sum}(\mathbf{M})=K$. $\mathbf{M}_{i}=1$
indicates keeping the $i$-th token while $\mathbf{M}_{i}=0$ indicates pruning.
However, such discrete sampling is non-differentiable. To overcome the
problem, we relax the sampling of discrete topK masks to a continuous
approximation, the Gumbel-Softmax distribution:

$\underbrace{\mathbf{M}_{i}=\mathbbm{1}_{\text{topK}}(\mathrm{log}(s_{i})+g_{i})}_{\text{forward}}\xleftarrow{\text{approx}}\underbrace{\tilde{\mathbf{M}}_{i}=\frac{\mathrm{exp}((\mathrm{log}(s_{i})+g_{i})/\tau)}{\sum_{j=1}^{n}\mathrm{exp}((\mathrm{log}(s_{j})+g_{j})/\tau)}}_{\text{backward}}$
(2)

where $\mathbbm{1}_{\text{topK}}$ is an indicator function of whether the
input perturbed score is among the topK of all $n$ perturbed scores,
$\\{g\\}_{n}$ are i.i.d samples from the $\textrm{Gumbel}(0,1)$
distribution111$\mathrm{Gumbel}(0,1)$ samples are drawn by sampling
$-\mathrm{log}(-\mathrm{log}\;u)$ where $u\sim\mathrm{Uniform}(0,1)$. While
training, we forward STP to sample the topK tokens based on the discrete
$\mathbf{M}$ but backward with the gradient approximated by the continuous
$\tilde{\mathbf{M}}$. We call this Straight-through (ST) Gumbel Soft TopK
Sampling. During inference, we perform normal topK selection based on
predicted scores without Gumbel noise perturbation for deterministic
inference.

###  2.2 Token Completion: Multi-layer Token Assembly (MTA)

The output of the STP-ViT encoder is sparse. Thus, before passing the output
to the decoder, we need to first restore the complete tokens. A
straightforward solution can be obtained from Masked Image Modeling (MIM) [2,
9]. MIM reconstructs an image from random partial image patches. It first pads
the sparse token set with learnable [MASK] tokens up to its full length. Then
the padded tokens are forwarded through Transformer blocks to reconstruct the
masked regions. However, MIM is mostly utilized for pre-training which focuses
more on semantic hallucination rather than accurate detail restoration. Thus,
it is sub-optimal for segmentation tasks that require assigning labels to
pixels accurately.

We propose Multi-layer Token Assembly (MTA) to restore dense features by
assembling both the outputted sparse tokens and the pruned intermediate tokens
from multiple layers. Suppose we insert three STPs,
$\\{\mathit{STP}_{1},\mathit{STP}_{2},\mathit{STP}_{3}\\}$, after different
Transformer blocks in a ViT. We denote the token sets pruned by the three STPs
as $\\{\bar{\mathbf{z}}_{1},\bar{\mathbf{z}}_{2},\bar{\mathbf{z}}_{3}\\}$. We
concatenate these pruned tokens with the final output $\mathbf{z}_{L}$ and
rearrange them to their original spatial order. Then, we add three learnable
block tokens $\\{\mathtt{[BLK_{1}],[BLK_{2}],[BLK_{3}]}\\}$ to the
corresponding pruned tokens to indicate which block each token is pruned from.
Finally, we introduce sin-cos position embeddings $\mathbf{E}_{pos}$ to all
the tokens and forward them through Transformer blocks. The completion process
can be summarized as follows:

$\mathbf{z}_{\mathrm{compl}}=\mathtt{TF}(\mathtt{rearrange}(\big{[}\bar{\mathbf{z}}_{1}+\mathtt{[BLK_{1}]},\bar{\mathbf{z}}_{2}+\mathtt{[BLK_{2}]},\bar{\mathbf{z}}_{3}+\mathtt{[BLK_{3}]},\mathbf{z}_{L}\big{]})+\mathbf{E}_{pos})$
(3)

###  2.3 Dense Decoding & Optimization

As our goal is to design an acceleration method that is agnostic to decoder
designs, designing a new segmentation decoder is beyond the scope of this
paper. Thus, we couple the SCD pipeline with existing segmentation decoders.
However, certain segmentation decoders, e.g., UNETR, require inputs from
multiple layer outputs from the encoder, which causes problems because
intermediate features are still sparse. Motivated by recent research on the
non-hierarchical feature pyramid [13], we use the output
$\mathbf{z}_{\mathrm{compl}}$ of the completion network to replace all the
intermediate features required by the segmentation head, as shown in Fig. 1.

Unlike DynamicViT, we do not introduce additional loss functions for token
pruning. We optimize all segmentation models by segmentation loss. We adopt a
combination of cross entropy and Dice loss. Both loss weights are set to 1.

##  3 Experiments

###  3.1 Dataset Description

We evaluate on two benchmark 3D medical segmentation datasets with sparse
targets. The tasks are CT multi-organ and MRI Brain tumor segmentation.
CT Multi-organ Segmentation (BTCV). The BTCV [11] (Multi Atlas Labeling Beyond
The Cranial Vault) dataset consists of 30 subjects with abdominal CT scans
where 13 organs were annotated under the supervision of board-certified
radiologists. Each CT volume has $85\sim 198$ slices of $512\times 512$
pixels, with a voxel spatial resolution of ($0.54\times 0.98\times[2.5\sim
5.0]$ $mm^{3}$). For comparison convenience, we follow [4, 3] to split the 30
cases into 18 for training and 12 for validation. Hyper-parameters are
selected via 3-fold cross validation in the training set. We report the
average DSC (Dice Similarity Coefficient) and 95% Hausdorff Distance (HD95) on
8 abdominal organs (aorta, gallbladder, spleen, left kidney, right kidney,
liver, pancreas, spleen, stomach) to align with [4].
MRI Brain Tumor Segmentation (BraTS). The Medical Segmentation Decathlon (MSD)
[1] BraTS dataset has 484 multi-modal (FLAIR, T1w, T1-Gd and T2w) MRI scans.
The ground-truth segmentation labels include peritumoral edema, GD-enhancing
tumor and the necrotic/non-enhancing tumor core. The performance is measured
on three recombined regions, i.e., tumor core, whole tumor and enhancing
tumor. We randomly split the dataset into training (80%), validation (15%),
and test (5%) sets. We report average DSC and HD95.

###  3.2 Implementation Details

Our method is implemented in PyTorch [19] and MONAI [18] on a single NVIDIA
A100. Our encoder is based on a ViT-Base model. Three STP modules are inserted
after the 3rd, 6th, and 9th Transformer blocks in ViT-B. We follow UNETR [8]
on data processing. For BTCV, we clip the raw values between -958 and 326, and
re-scale the range between -1 and 1. For BraTS, we perform an instance-wise
normalization over the non-zero region per channel. For training, we set the
batch size to 2 and the initial learning rate to 1.3e-4. We use AdamW as the
optimizer and adopt layer-wise learning rate decay (ratio=0.75) to improve
training. For inference, we use a sliding window with an overlap of 50%.

###  3.3 Results

Naïve Combination of EViT/DynamicViT+MIM. We first test the straightforward
approach of applying EViT/DynamicViT to sparse encoding and MIM to token
completion. We use UNETR as the segmentation decoder. In Table 1,
EViT/DynamicViT + MIM fails to perform dense prediction for a very high
pruning ratio $r=0.9$ on BTCV. This justifies our efforts in this paper to
accelerate sparse token segmentation models while maintaining performance.

DSC(%) on BTCV (pruning ratio $r=0.9$) | sparse encoding
---|---
DynamicViT [21] | EViT [15] | STP (ours)
token completion | MIM [2, 9] | 24.35 (single run) | 18.64 (single run) | 44.71 (single run)
MTA (ours) | $80.24\pm 0.34$ | $78.62\pm 0.10$ | $82.18\pm 0.12$

Table 1: Performance of existing approaches on BTCV. We first examine the
performance of the naïve combination of existing approaches. For a large
pruning ratio $r=0.9$ on BTCV, MIM fails to perform segmentation effectively.
Even with our proposed MTA instead of MIM, EViT and DynamicViT still perform
worse than our STP. We report the mean and std on three random runs unless
otherwise stated. Please see Sec. 3 for more analysis.

Our Approach: STP+MTA. We evaluate the efficiency of our Soft-topK Token
Pruning (STP) and Multi-layer Token Assembly (MTA) on the BTCV and BraTS
datasets based on UNETR. We measure the efficiency by profiling the
throughput(image/s) and MAC number (Multiply–accumulate operations) for each
model variant. The throughput is measured on a NVIDIA A100 GPU with batch size
1. MACs are computed by measuring the forward complexity of a single image. We
present the results in Table 2. On BraTS, with an input size of $(128\times
128\times 128)$, our STP+MTA+UNETR ($r=0.75$) maintains performance while
significantly increasing inference throughput by 60.8%. On BTCV, with an input
size of $(96\times 96\times 96)$, STP+MTA+UNETR ($r=0.9$) can maintain
performance while the corresponding inference throughput increases by 24.1%.
Our method also increases training efficiency. The training throughput on BTCV
increases from 2.65 imgs/s to 5.23 imgs/s by 97.36%. The training throughput
on BraTS increases from 0.75 imgs/s to 1.65 imgs/s by 120%.

Method | MSD BraTS |  Encoder Throughput(img/s) |  Throughput (img/s) | MACs(G)
---|---|---|---|---
DSC$\uparrow$ | HD95$\downarrow$
UNETR | 75.44 | 8.89 | 7.10 | 4.85 | 824.38
STP+MTA+UNETR | 75.79 | 8.31 | 20.04 | 7.79 $(+60.6\%)$ | 428.28

Method | BTCV |  Encoder Throughput(img/s) |  Throughput (img/s) | MACs(G)
---|---|---|---|---
DSC$\uparrow$ | HD95$\downarrow$
UNETR | $80.78\pm 0.34$ | $\textbf{15.90}\pm 1.01$ | 30.30 | 16.18 | 273.45
STP+MTA+UNETR | $\textbf{82.18}\pm 0.12$ | $19.85\pm 1.12$ | 57.31 | 20.08 $(+24.1\%)$ | 146.63

Table 2: STP+MTA+UNETR vs. UNETR performance comparison. Based on the same ViT
scale and patch size, our proposed STP+MTA+UNETR can maintain performance
while significantly reducing computation by a large margin. We report the mean
and std of three random runs on BTCV. Please refer to Sec 3.3 for more details
on the experimental setting and analysis.

Sparse Encoding: STP vs. EViT/DynamicViT. EViT [15] and DynamicViT [21] were
initially designed for classification. Thus, we need to adapt EViT/DynamicViT
for comparison. To constrain the pruning ratio in DynamicViT, we add the ratio
loss function $\mathcal{L}_{ratio}$ with a weight of
$\mathcal{\lambda}_{ratio}=2$ following [21]. In EViT, we take the [CLS]
attention weights from the Transformer block as the token scores and use topK
for sampling. As shown in Table 4(a), our STP-ViT performs the best. The
inferiority of DynamicViT could be caused by i) mismatch between the training
(variable number of pruned tokens) and testing phases (fixed number of pruned
tokens) and ii) more hyper-parameters (e.g., $\mathcal{\lambda}_{ratio}$). The
performance drop in EViT indicates that the [CLS] attention scores are not
suitable for representing the true token importance in segmentation.
Token Completion: MTA vs. MIM. We implement a baseline inspired by MIM [2, 9].
As Table 4(b) shows, MIM-style completion fails ($44.71\%$) with a high
pruning ratio $r=0.9$. Our results suggest that pruned token reuse in MTA
plays an important role in a highly sparse token segmentation framework.
Token Pruning Ratio in STP. We ablate the pruning ratio in Table 3. STP is
robust to a wide range of pruning ratios $[0.25,0.9]$. Thus, our STP+MTA+UNETR
can adopt a high pruning ratio to reduce computation by a large margin.
Although our method achieves higher DSC on BTCV than UNETR, the HD95 is worse.
We speculate that HD95 is more sensitive to the boundary segmentation results
and that token pruning may lead to sub-optimal boundary prediction.

Pruning Ratio $r$ | BTCV | BraTS |  Encoder Throughput | Throughput | MACs(G)
---|---|---|---|---|---
DSC$\uparrow$ | HD95$\downarrow$ | DSC$\uparrow$ | HD95$\downarrow$
baseline | $80.78\pm 0.34$ | $15.90\pm 1.01$ | 75.44 | 8.89 | 7.10 | 4.85 | 824.38
0.25 | $81.56\pm 0.16$ | $19.65\pm 3.25$ | 75.50 | 7.98 | 11.77 | 6.12 | 631.75
0.50 | $81.81\pm 0.59$ | $\mathbf{15.78}\pm 1.01$ | 75.02 | 7.40 | 17.34 | 7.35 | 497.97
0.75 | $81.95\pm 0.18$ | $16.37\pm 5.41$ | 75.79 | 8.31 | 20.04 | 7.79 | 428.28
0.9 | $\mathbf{82.18}\pm 0.12$ | $19.85\pm 1.12$ | 75.32 | 8.04 | 21.63 | 8.04 | 404.14

Table 3: Ablation on the Pruning Ratio $r$. STP shows robustness to a wide
range of pruning ratios ($0.25\rightarrow 0.9$) in terms of DSC. Different
datasets have different optimal pruning ratios. Refer to Sec 2 for more
details. We report the mean and std of three random runs on BTCV unless
otherwise stated.

Encoder | DSC
---|---
DynamicViT | $80.24\pm 0.34$
EViT | $78.62\pm 0.10$
STP-ViT (Ours) | $\mathbf{82.18}\pm 0.12$

(a) Comparison with DynamicViT&EViT

Token Completion | DSC
---|---
MIM | 44.71 (single run)
MTA (ours) | $\mathbf{82.18}\pm 0.12$

(b) Token Completion Methods

Perturbation | DSC
---|---
No (ST TopK) | $81.67\pm 0.21$
Yes (ours) | $\mathbf{82.18}\pm 0.12$

(c) Gumbel Perturbation

$\tau$ | DSC
---|---
0.01 | $81.36\pm 0.15$
0.1 | $82.06\pm 0.22$
1 (ours) | $\mathbf{82.18}\pm 0.12$

(d) Temperature $\tau$ in STP

Table 4: Ablation studies on BTCV. In (a), we compare STP with DynamicViT and
EViT. STP achieves better performance. In (b), we compare our proposed MTA
with MIM where MIM performs much worse than MTA. In (c), we demonstrate that
Gumbel perturbation is beneficial. In (d), we ablate different $\tau$ values.
$\tau=0.1$ and $\tau=1$ perform similarly while $\tau=0.01$ performs worse. We
report the mean and std of three random runs unless otherwise stated.

Temperature $\tau$ in STP. We ablate temperature $\tau$ in Eq. 2 in Table
4(d). According to [10], a small temperature leads to a large variance of
gradients and vice versa. We tried three different $\tau$ values
$\\{0.01,0.1,1\\}$. Experiments show $\tau=0.1$ and $\tau=1$ perform similarly
while $\tau=0.01$ performs worse.
Noise Perturbation in STP. In Soft-topK Token Pruning (STP), we design a
straight-through (ST) Gumbel soft topK algorithm for sampling. STP forward
process can be split into three steps, i.e., score prediction, Gumbel
perturbation, and topK sampling. In Table 4(c), we ablate the Gumbel
perturbation on BTCV by evaluating a straight-through (ST) topK variant. Note
that we do not add Gumbel noise during inference, to ensure that the model
performs deterministically for inference. For the ST topK variant, we also
remove the Gumbel noise perturbation from the training phase. With a pruning
ratio $r=0.9$, results show that the Gumbel perturbation is beneficial. It is
worth noting that the ST topK variant without perturbation also achieves a
competitive result.

Framework | DSC$\uparrow$/HD95$\downarrow$ | Aorta | Gallbladder | Kidney(L) | Kidney(R) | Liver | Pancreas | Spleen | Stomach
---|---|---|---|---|---|---|---|---|---
V-Net [17] | 68.81/- | 75.34 | 51.87 | 77.10 | 80.75 | 87.84 | 40.05 | 80.56 | 56.98
DARR [7] | 69.77/- | 74.74 | 53.77 | 72.31 | 73.24 | 94.08 | 54.18 | 89.90 | 45.96
U-Net(R50) [22] | 74.68/36.87 | 84.18 | 62.84 | 79.19 | 71.29 | 93.35 | 48.23 | 84.41 | 73.92
AttnUNet(R50) [23] | 75.57/36.97 | 55.92 | 63.91 | 79.20 | 72.71 | 93.56 | 49.37 | 87.19 | 74.95
TransUNet [4] | 77.48/31.69 | 87.23 | 63.13 | 81.87 | 77.02 | 94.08 | 55.86 | 85.08 | 75.62
UNETR (PatchSize=16) | 78.83/25.59 | 85.46 | 70.88 | 83.03 | 82.02 | 95.83 | 50.99 | 88.26 | 72.74
UNETR (PatchSize=8) | 80.78/15.90 | 88.59 | 70.97 | 83.38 | 83.76 | 95.52 | 59.76 | 88.53 | 74.30
STP+MTA+UNETR (PatchSize=8) |  82.18/19.85 | 89.23 | 73.60 | 85.66 | 83.65 | 95.59 | 62.17 | 88.84 | 77.37

Table 5: Comparison with other methods on BTCV. Figure 2: Ground truth and
model outputs on BraTS (first two rows) and BTCV (last two rows). We visualize
the depth at which tokens are pruned under high (r=0.9) and low (r=0.25)
pruning ratios (red shading in columns 2 and 3). Tokens that are immediately
dropped are not shaded, whereas darker red shading indicates the pruning of
tokens in later layers.

Pruning Policy Visualization. We visualize the pruning policy for both brain
tumors and abdominal organs in Fig. 2 under two extreme pruning ratios, the
highest one at $r=0.9$ and the lowest at $r=0.25$. We use shades of red to
denote the depth at which tokens are pruned. Patches (tokens in ViT) with no
red overlap are pruned by the very first STP, whereas patches with the deepest
red color are kept in ViT until the last. In Fig 2, with $r=0.9$, most tokens
are dropped at a very early stage. Some tokens around the brain tumor,
especially at tumor boundaries, are never pruned. When the ratio decreases to
$r=0.25$, more patches are kept and still cluster around the target tumor
region.
Class-wise Comparison with Others on BTCV. We show class-wise results of
UNETR, STP+MTA+UNETR, and other methods in Table 5.

STP+MTA+UNETR shows improvement over a series of methods on BTCV. Note that
current SOTA methods [30, 27, 24] rely on either stronger priors (window
attention) or SSL pre-training. However, our goal is accelerating standard
ViT-based segmentation instead of purely pursuing increased performance.

##  4 Conclusion and Future Work

We introduced a ViT-based sparse token segmentation framework for medical
images. First, we proposed a Soft-topK Token Pruning (STP) module to prune
tokens in ViT. STP can speed up ViTs in both training and inference phases. To
produce a full set of tokens for dense prediction, we proposed Multi-layer
Token Assembly (MTA) that recovers a complete set of tokens by assembling both
output and intermediate tokens from multiple layers. In our 3D medical image
experiments STP+MTA+UNETR speeds up the UNETR baseline significantly while
maintaining segmentation performance. Accelerating the decoder, which also
plays a big role in the inference speed, is left for future work.

## Acknowledgement

The reported research was partly supported by NIH award $\\#$
1R21CA258493-01A1, NSF awards IIS-2212046 and IIS-2123920, and Stony Brook
OVPR seed grants. The content is solely the responsibility of the authors and
does not necessarily represent the official views of the National Institutes
of Health

## References

  * [1] Antonelli, M., Reinke, A., Bakas, S., Farahani, K., Landman, B.A., Litjens, G., Menze, B., Ronneberger, O., Summers, R.M., van Ginneken, B., et al.: The medical segmentation decathlon. arXiv preprint arXiv:2106.05735 (2021)
  * [2] Bao, H., Dong, L., Wei, F.: Beit: Bert pre-training of image transformers. arXiv preprint arXiv:2106.08254 (2021)
  * [3] Chen, J.N.: Transunet, https://github.com/Beckschen/TransUNet
  * [4] Chen, J., Lu, Y., Yu, Q., Luo, X., Adeli, E., Wang, Y., Lu, L., Yuille, A.L., Zhou, Y.: Transunet: Transformers make strong encoders for medical image segmentation. arXiv preprint arXiv:2102.04306 (2021)
  * [5] Cordonnier, J.B., Mahendran, A., Dosovitskiy, A., Weissenborn, D., Uszkoreit, J., Unterthiner, T.: Differentiable patch selection for image recognition. In: CVPR. pp. 2351–2360 (2021)
  * [6] Dosovitskiy, A., Beyer, L., Kolesnikov, A., Weissenborn, D., Zhai, X., Unterthiner, T., Dehghani, M., Minderer, M., Heigold, G., Gelly, S., et al.: An image is worth 16x16 words: Transformers for image recognition at scale. arXiv preprint arXiv:2010.11929 (2020)
  * [7] Fu, S., Lu, Y., Wang, Y., Zhou, Y., Shen, W., Fishman, E., Yuille, A.: Domain adaptive relational reasoning for 3d multi-organ segmentation. In: MICCAI. pp. 656–666. Springer (2020)
  * [8] Hatamizadeh, A., Tang, Y., Nath, V., Yang, D., Myronenko, A., Landman, B., Roth, H.R., Xu, D.: Unetr. In: WACV (2022)
  * [9] He, K., Chen, X., Xie, S., Li, Y., Dollár, P., Girshick, R.: Masked autoencoders are scalable vision learners. arXiv preprint arXiv:2111.06377 (2021)
  * [10] Jang, E., Gu, S., Poole, B.: Categorical reparameterization with gumbel-softmax. arXiv preprint arXiv:1611.01144 (2016)
  * [11] Landman, B., Xu, Z., Igelsias, J., Styner, M., Langerak, T., Klein, A.: MICCAI multi-atlas labeling beyond the cranial vault–workshop and challenge. In: Proc. MICCAI Multi-Atlas Labeling Beyond Cranial Vault—Workshop Challenge (2015)
  * [12] Li, J., Cotterell, R., Sachan, M.: Differentiable subset pruning of transformer heads. Transactions of the Association for Computational Linguistics 9, 1442–1459 (2021)
  * [13] Li, Y., Mao, H., Girshick, R., He, K.: Exploring plain vision transformer backbones for object detection. arXiv preprint arXiv:2203.16527 (2022)
  * [14] Li, Y., Xie, S., Chen, X., Dollar, P., He, K., Girshick, R.: Benchmarking detection transfer learning with vision transformers. arXiv preprint arXiv:2111.11429 (2021)
  * [15] Liang, Y., Chongjian, G., Tong, Z., Song, Y., Wang, J., Xie, P.: Evit: Expediting vision transformers via token reorganizations. In: ICLR (2021)
  * [16] Meng, L., Li, H., Chen, B.C., Lan, S., Wu, Z., Jiang, Y.G., Lim, S.N.: Adavit: Adaptive vits for efficient image recognition. arXiv preprint arXiv:2111.15668 (2021)
  * [17] Milletari, F., Navab, N., Ahmadi, S.A.: V-net: Fully convolutional neural networks for volumetric medical image segmentation. In: 3DV. pp. 565–571. IEEE (2016)
  * [18] MONAI Consortium: MONAI: Medical Open Network for AI (3 2020). https://doi.org/10.5281/zenodo.4323058, https://github.com/Project-MONAI/MONAI
  * [19] Paszke, A., Gross, S., Massa, F., Lerer, A., Bradbury, J., Chanan, G., Killeen, T., Lin, Z., Gimelshein, N., Antiga, L., et al.: Pytorch: An imperative style, high-performance deep learning library. NeurIPS 32 (2019)
  * [20] Ranftl, R., Bochkovskiy, A., Koltun, V.: Vision transformers for dense prediction. In: ICCV (2021)
  * [21] Rao, Y., Zhao, W., Liu, B., Lu, J., Zhou, J., Hsieh, C.J.: Dynamicvit: Efficient vision transformers with dynamic token sparsification. NeurIPS 34 (2021)
  * [22] Ronneberger, O., Fischer, P., Brox, T.: U-net: Convolutional networks for biomedical image segmentation. In: MICCAI. Springer (2015)
  * [23] Schlemper, J., Oktay, O., Schaap, M., Heinrich, M., Kainz, B., Glocker, B., Rueckert, D.: Attention gated networks: Learning to leverage salient regions in medical images. Medical image analysis 53, 197–207 (2019)
  * [24] Tang, Y., Yang, D., Li, W., Roth, H.R., Landman, B., Xu, D., Nath, V., Hatamizadeh, A.: Self-supervised pre-training of swin transformers for 3d medical image analysis. In: CVPR (2022)
  * [25] Vaswani, A., Shazeer, N., Parmar, N., Uszkoreit, J., Jones, L., Gomez, A.N., Kaiser, Ł., Polosukhin, I.: Attention is all you need. NeurIPS 30 (2017)
  * [26] Wang, J., Sun, K., Cheng, T., Jiang, B., Deng, C., Zhao, Y., Liu, D., Mu, Y., Tan, M., Wang, X., et al.: Deep high-resolution representation learning for visual recognition. IEEE transactions on PAMI 43(10), 3349–3364 (2020)
  * [27] Wu, Y., Liao, K., Chen, J., Chen, D.Z., Wang, J., Gao, H., Wu, J.: D-former: A u-shaped dilated transformer for 3d medical image segmentation. arXiv preprint arXiv:2201.00462 (2022)
  * [28] Xie, S.M., Ermon, S.: Reparameterizable subset sampling via continuous relaxations. arXiv preprint arXiv:1901.10517 (2019)
  * [29] Zheng, S., Lu, J., Zhao, H., Zhu, X., Luo, Z., Wang, Y., Fu, Y., Feng, J., Xiang, T., Torr, P.H., et al.: Rethinking semantic segmentation from a sequence-to-sequence perspective with transformers. In: CVPR (2021)
  * [30] Zhou, H.Y., Guo, J., Zhang, Y., Yu, L., Wang, L., Yu, Y.: nnformer: Interleaved transformer for volumetric segmentation. arXiv preprint arXiv:2109.03201 (2021)


#  Tight toughness, isolated toughness and binding number bounds for the
$\\{K_{2},C_{n}\\}$-factors

Xiaxia Guan, Tianlong Ma, Chao Shi
School of Mathematical Sciences
Xiamen University
P. R. China
Email<EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract

The $\\{K_{2},C_{n}\\}$-factor of a graph is a spanning subgraph whose each
component is either $K_{2}$ or $C_{n}$. In this paper, a sufficient condition
with regard to tight toughness, isolated toughness and binding number bounds
to guarantee the existence of the $\\{K_{2},C_{2i+1}|i\geq 2\\}$-factor for
any graph is obtained, which answers a problem due to Gao and Wang (J. Oper.
Res. Soc. China (2021), https://doi.org/10.1007/s40305-021-00357-6).
Keywords: Component factor; toughness; isolated toughness; binding number
AMS subject classification 2020: 05C42; 05C38.

##  1 Introduction

All graphs considered in this paper are simple, finite and undirected. Given a
graph $G$, let $V(G)$ and $E(G)$ denote the sets of vertices and edges of $G$,
respectively. For a subset $S\subseteq V(G)$, we use $G-S$ to denote the
subgraph of $G$ induced by the set $V(G)\setminus S$. Let $N_{G}(S)$ denote
the set of all neighbours of the vertices in $S$, and let $c(G-S)$ and
$iso(G-S)$ denote the numbers of components and isolated vertices in $G-S$,
respectively.

For a set of connected graphs $\mathcal{S}$, a spanning subgraph $F$ of $G$ is
called an _$\mathcal{S}$ -factor_ if each component of $F$ is isomorphic to a
member of $\mathcal{S}$. In particular an $\mathcal{S}$-factor is a $P_{\geq
k}$-factor if $\mathcal{S}=\\{P_{k},P_{k+1},\ldots\\}$, where $P_{k}$ is a
path with $k$ vertices. We refer the readers to book [12] for more details on
graph factors.

In [4], Chvátal defined the _toughness_ of a graph $G$, denoted by $t(G)$, as
follows: if $G$ is a completed graph, then $t(G)=+\infty$; otherwise

$t(G)=\min\left\\{\frac{|S|}{c(G-S)}\bigg{|}S\subseteq V(G),c(G-S)\geq
2\right\\}.$

Zhou et al. [16] showed that for a graph $G$ with $t(G)\geq\frac{2}{3}$, $G$
has a $P_{\geq 3}$-factor. Liu and Zhang [7] showed that for a graph $G$ with
$t(G)\geq 1$, $G$ has a $\\{K_{2},C_{2i+1}|i\geq 1\\}$-factor. The further
relationships between toughness and graph factors were studied in [2, 13].

To study fractional factors, a new parameter of a graph $G$, called _isolated
toughness_ and denoted by $I(G)$, is introduced by Yang et al. in [11], which
is defined as follows: if $G$ is a complete graph, then $I(G)=+\infty$;
otherwise,

$I(G)=\min\left\\{\frac{|S|}{iso(G-S)}\bigg{|}S\subseteq V(G),iso(G-S)\geq
2\right\\}.$

In [8], Kano et al. proved that if $I(G)\geq\frac{3}{2}$ for any graph $G$,
then $G$ admits a $P_{\geq 3}$-factor. The fractional Tutte $1$-factor theorem
[9] stated that a graph $G$ has a $\\{K_{2},C_{2i+1}|i\geq 1\\}$-factor if and
only if $iso(G-S)\leq|S|$ for any $S\subseteq V(G)$. It follows that $G$
admits a $\\{K_{2},C_{2i+1}|i\geq 1\\}$-factor if and only if $I(G)\geq 1$.

Further, a variant of isolated toughness was defined by Zhang and Liu [14],
denoted by $I^{\prime}(G)$: if $G$ is a completed graph, then
$I^{\prime}(G)=+\infty$; otherwise

$I^{\prime}(G)=\min\left\\{\frac{|S|}{iso(G-S)-1}\bigg{|}S\subseteq
V(G),iso(G-S)\geq 2\right\\}.$

Recently, Gao and Wang [3] proved that if $I^{\prime}(G)>2$ for any graph $G$,
then $G$ admits a $P_{\geq 3}$-factor. Similar to isolated toughness, by the
fractional Tutte $1$-factor theorem, we have that $G$ admits a
$\\{K_{2},C_{2i+1}|i\geq 1\\}$-factor if and only if $I^{\prime}(G)>1$.

In [10], Woodall defined the _binding number_ of $G$, denoted by $bind(G)$, as
follows:

$bind(G)=\min\left\\{\frac{|N_{G}(S)|}{|S|}\bigg{|}\emptyset\neq S\subseteq
V(G),N_{G}(S)\neq V(G)\right\\}.$

Binding number plays an important role in the research of graph factors. In
1971, Anderson [1] showed for a graph $G$ of even order with
$bind(G)\geq\frac{4}{3}$, $G$ has a $1$-factor. Later, Woodall [10] showed for
a graph $G$ with $bind(G)\geq\frac{3}{2}$, $G$ has a $2$-factor. Gao and Wang
[3] proved that if $bind(G)\geq\frac{5}{4}$ for any graph $G$, then $G$ admits
a $P_{\geq 3}$-factor. Moreover, they also proved that a graph $G$ admits a
$\\{K_{2},C_{2i+1}|i\geq 1\\}$-factor if and only if $bind(G)\geq 1$. We refer
to the papers [6, 15] for more details on binding number.

In [10], Woodall proved the relation $t(G)\geq bind(G)-1$ for any graph $G$.
For any graph $G$, let $S$ be a subset of vertices in $G$ such that
$I(G)=\frac{|S|}{iso(G-S)}$. Note that $iso(G-S)\leq c(G-S)$, and thus

$t(G)\leq\frac{|S|}{c(G-S)}\leq\frac{|S|}{iso(G-S)}=I(G).$

Let $Y$ be the set of the isolated vertices in $G-S$. Clearly, $iso(G-S)=|Y|$
and $N_{G}(Y)\subseteq S$. Then $|N_{G}(Y)|\leq|S|$. Therefore we have

$bind(G)\leq\frac{|N_{G}(Y)|}{|Y|}\leq\frac{|S|}{iso(G-S)}=I(G).$

The relation $I(G)<I^{\prime}(G)$ is trivial from the definitions. Thus we
have $t(G)\leq I(G)<I^{\prime}(G)$ and $bind(G)\leq I(G)<I^{\prime}(G)$. We
think that these relations are simple and immediate, but it is a surprise that
we can’t find it in the existing literature.

In [3], Gao and Wang also simply surveyed the important results on component
factors, and proposed the following problem.

######  Problem 1.1.

_[3]_ What is the tight toughness, isolated toughness and binding number
bounds for a graph $G$ to have a $\\{K_{2},C_{2i+1}|i\geq 2\\}$-factor?

In this paper, we give a sufficient condition with regard to tight toughness,
isolated toughness and binding number bounds to guarantee the existence of the
$\\{K_{2},C_{2i+1}|i\geq 2\\}$-factor for any graph, and then Problem 1.1 is
answered.

######  Theorem 1.2.

If a graph $G$ of order at least $5$ satisfies one of the following four
conditions:

(i) $t(G)\geq 1$;

(ii) $I(G)\geq 3$;

(iii) $I^{\prime}(G)>5$;

(iv) $bind(G)>\frac{4}{3}$,
then $G$ admits a $\\{K_{2},C_{2i+1}|i\geq 2\\}$-factor.

These bounds of toughness, isolated toughness and binding number our obtain
are sufficient to admit a $\\{K_{2},C_{2i+1}|i\geq 2\\}$-factor in any graph,
but not necessary, which can be easily checked by a path of even order. Note
that for a graph $G$, if $t(G)\geq 1$, our conclusion can be viewed as a
generalization of the result that $G$ has a $\\{K_{2},C_{2i+1}|i\geq
1\\}$-factor due to Liu and Zhang [7].

In particular, for the variant of isolated toughness, if we abandon several
graphs of small order, we have the following further result.

######  Theorem 1.3.

Let $G$ be a graph of order at least $16$ with $I^{\prime}(G)>\frac{7}{2}$.
Then $G$ admits a $\\{K_{2},C_{2i+1}|i\geq 2\\}$-factor.

In next section, we shall complete the proofs of Theorems 1.2 and 1.3.
Futhermore, some classes of graphs are constructed to demonstrate the
tightness for the bounds our obtain on the four parameters.

##  2 Proof of Theorem 1.2

In this section, we divide Theorem 1.2 into four lemmas to prove and
demonstrate the tightness for the bounds our obtain. We begin with a
characterization on $\\{K_{2},C_{2i+1}|i\geq 2\\}$-factors, which plays a
vital role in our forthcoming arguments.

We call a connected graph _triangular-cactus_ if its each block is a triangle.
Clearly, $K_{3}$ is a triangular-cactus. We usually also view $K_{1}$ as a
triangular-cactus. Let $c_{tc}(G)$ denote the number of triangular-cacti
components of $G$. In the following, we present the characterization on
$\\{K_{2},C_{2i+1}|i\geq 2\\}$-factors due to Cornuéjols and Pulleyblank [5].

######  Theorem 2.1.

_[5]_ A graph $G$ has a $\\{K_{2},C_{2i+1}|i\geq 2\\}$-factor if and only if
$c_{tc}(G-S)\leq|S|$ for any $S\subseteq V(G)$.

We now prove our main results in the following.

######  Lemma 2.2.

Let $G$ be a graph of order at least $5$. If $G$ admits no
$\\{K_{2},C_{2i+1}|i\geq 2\\}$-factors, then $t(G)<1$.

###### Proof.

By Theorem 2.1, there exists an $S\subseteq V(G)$ such that
$c_{tc}(G-S)\geq|S|+1$. Note that $c(G-S)\geq c_{tc}(G-S)\geq|S|+1$. If
$c(G-S)\geq 2$, then

$t(G)\leq\frac{|S|}{c(G-S)}\leq\frac{c(G-S)-1}{c(G-S)}<1.$

If $c(G-S)=1$, then $G$ is a triangular-cactus with at least $5$ vertices.
Clearly, there exists a cut vertex $v$ in $G$, that is, $c(G-\\{v\\})\geq 2$.
Thus

$t(G)\leq\frac{|\\{v\\}|}{c(G-\\{v\\})}\leq\frac{1}{2}.$

The proof is complete.

Remark 1.  Let us show that $t(G)<1$ is tight. Let $G_{m}$ be a graph obtained
from a completed graph $K$ of order $m-1$ by joining $m$ independent vertices
to each vertex of $K$ for $m\geq 3$. Note that $G_{m}$ has no
$\\{K_{2},C_{2i+1}|i\geq 2\\}$-factor as $c_{tc}(G_{m}-V(K))>|V(K)|$. If
$c(G_{m}-S)\geq 2$, then $V(K)\subseteq S$ and $c(G_{m}-S)=2m-1-|S|$, which
implies that $|S|\geq m-1$. Hence

$\frac{|S|}{c(G_{m}-S)}=\frac{|S|}{2m-1-|S|}=-1+\frac{2m-1}{2m-1-|S|}.$

Therefore, $t(G_{m})=\frac{m-1}{m}<1$, and
$\lim\limits_{m\to+\infty}t(G_{m})=1$.

######  Lemma 2.3.

Let $G$ be a graph without $\\{K_{2},C_{2i+1}|i\geq 2\\}$-factors. Then
$I(G)<3$.

###### Proof.

By Theorem 2.1, there exists an $S\subseteq V(G)$ such that
$c_{tc}(G-S)\geq|S|+1$. Let $a$ denote the number of $K_{1}$ in $G-S$. Let
$T_{1},T_{2},\ldots,T_{b}$ be the components with at least $3$ vertices in
$G-S$. So we rewrite $c_{tc}(G-S)=a+b\geq|S|+1$, and then $|S|\leq a+b-1$.
Take two neighbours of a vertex of degree $2$ in $T_{i}$ to form a set
$X_{i}$, and set $X=\bigcup\limits_{i=1}^{b}X_{i}$. Clearly,
$|X|=\sum\limits_{i=1}^{b}|X_{i}|=2b$ and
$\sum\limits_{i=1}^{b}iso(T_{i}-X_{i})=b$. Set $Y=S\cup X$. Then we have

$|Y|=|S|+|X|\leq a+b-1+2b=a+3b-1,$

and

$iso(G-Y)=a+b.$

Therefore,

$I(G)\leq\frac{|Y|}{iso(G-Y)}\leq\frac{a+3b-1}{a+b}=3+\frac{-2a-1}{a+b}<3.$

This completes the proof.

Remark 2.  Let us show that $I(G)<3$ is tight. Let $H_{m}$ be a graph obtained
from completed graph $K$ of order $m-1$ by joining each vertex of $m$ disjoint
$K_{3}$’s to each vertex of $K$ for $m\geq 3$. Note that $H_{m}$ has no
$\\{K_{2},C_{2i+1}|i\geq 2\\}$-factor as $c_{tc}(H_{m}-V(K))>|V(K)|$. Let
$S\subseteq V(H_{m})$ such that $iso(H_{m}-S)\geq 2$. Then $V(K)\subseteq S$.
So we have $iso(H_{m}-S)\leq m$ and $|S|\geq m-1+2iso(H_{m}-S)$. Hence

$\frac{|S|}{iso(H_{m}-S)}\geq\frac{m-1+2iso(H_{m}-S)}{iso(H_{m}-S)}\geq\frac{3m-1}{m}.$

In particular, if we take two vertices from each $K_{3}$ and $V(K)$ as the set
$S^{\prime}$, then
$\frac{|S^{\prime}|}{iso(H_{m}-S^{\prime})}=\frac{3m-1}{m}$. Therefore
$I(H_{m})=\frac{3m-1}{m}<3$, and $\lim\limits_{m\to+\infty}I(H_{m})=3$.

Fig. 1. Three exceptions in Lemma 2.4.

######  Lemma 2.4.

Let $G$ be a graph of order $n$ containing no $\\{K_{2},C_{2i+1}|i\geq
2\\}$-factors with $n\geq 5$. Then

(i) $I^{\prime}(G)\leq 5$;

(ii) $I^{\prime}(G)\leq 4$ if $G$ is not one of three graphs in Fig 1;

(iii) $I^{\prime}(G)\leq\frac{11}{3}$ if $n\notin\\{6,7,11\\}$;

(iv) $I^{\prime}(G)\leq\frac{7}{2}$ if $n\notin\\{6,7,11,15\\}$.

###### Proof.

By Theorem 2.1, there exists an $S\subseteq V(G)$ such that
$c_{tc}(G-S)\geq|S|+1$. Let $a$, $b$ and $c$ denote the number of $K_{1}$,
$K_{3}$ and triangular-cactus with at least $5$ vertices in $G-S$,
respectively, and let $T_{1},T_{2},\ldots,T_{c}$ be the components of
triangular-cactus with at least $5$ vertices. So we rewrite
$c_{tc}(G-S)=a+b+c\geq|S|+1$, and then $|S|\leq a+b+c-1$. We take two vertices
from every $K_{3}$ to form a set $R$ in $G-S$. Clearly, $|R|=2b$.

Suppose that $a+b+c=1$, and then we have $|S|=0$. Since $n\geq 5$, we have
$a=b=0$ and $c=1$, which implies that $G$ is a triangular-cactus. If $n=5$,
then there are two vertices $u$ and $v$ of degree $2$ from distinct two blocks
and $|N_{G}(u)\cup N_{G}(v)|=3$. Take $X=N_{G}(u)\cup N_{G}(v)$. Then

$I^{\prime}(G)\leq\frac{|X|}{iso(G-X)-1}=\frac{3}{2-1}=3.$

If $n\geq 6$, then there exist three vertices $u,v$ and $w$ of degree $2$ from
distinct three blocks. Take $X=N_{G}(u)\cup N_{G}(v)\cup N_{G}(w)$. Then
$|X|\leq 6$ and hence

$I^{\prime}(G)\leq\frac{|X|}{iso(G-X)-1}\leq\frac{6}{3-1}=3.$

Suppose that $a+b+c\geq 2$. Note that there exist two vertices $u_{i},v_{i}$
of degree $2$ from distinct blocks in $T_{i}$ for $i=1,2,\ldots,c$. Take
$X_{i}=N(u_{i})\cup N(v_{i})$ and $X=\bigcup\limits_{i=1}^{c}X_{i}$. Clearly
$|X|\leq 4c$ and $iso(G-X)\geq 2c$. Let $Y=S\cup R\cup X$. Then

$|Y|=|S|+|R|+|X|\leq a+b+c-1+2b+4c=a+3b+5c-1$

and $iso(G-Y)\geq a+b+2c\geq 2$. So we have

$\displaystyle I^{\prime}(G)$ $\displaystyle\leq\frac{|Y|}{iso(G-Y)-1}$
$\displaystyle\leq\frac{a+3b+5c-1}{a+b+2c-1}$
$\displaystyle=3+\frac{-2a-c+2}{a+b+2c-1}$ $\displaystyle\leq
3+\frac{-2a-c+2}{c+1}$ $\displaystyle=2+\frac{-2a+3}{c+1}$ (1)
$\displaystyle\leq 2+\frac{3}{c+1}$ (2) $\displaystyle\leq 5.$

Thus we complete the proof of (i).

If $a\geq 1$, then, by inequality (1), $I^{\prime}(G)\leq 3$. If $a=0$ and
$c\geq 1$, then, by inequality (2), $I^{\prime}(G)\leq\frac{7}{2}$. It remains
to consider the case $a=c=0$ and $b\geq 2$ to complete the proofs of (ii),
(iii) and (iv). It implies that $|S|\leq b-1$.

Suppose that $b=2$, so we have $|S|\leq 1$. If $|S|=0$, then $n=6$. We have

$I^{\prime}(G)\leq\frac{|R|}{iso(G-R)-1}=\frac{4}{2-1}=4.$

If $|S|=1$, then $n=7$. Let $S=\\{s\\}$. Since $G$ is not one of three graphs
in Fig 1, we can take two vertices $u$ and $v$ from two distinct $K_{3}$’s
such that they are not adjacent to $s$. Set $X=V(G)\setminus\\{s,u,v\\}$. Then

$I^{\prime}(G)\leq\frac{|X|}{i(G-X)-1}=\frac{4}{3-1}=2.$

Suppose that $b\geq 3$. Take $Y=S\cup R$. Then $|Y|=|S|+|R|$ and $iso(G-Y)=b$.
If $|S|\leq b-2$, then

$I^{\prime}(G)\leq\frac{|Y|}{iso(G-Y)-1}\leq\frac{3b-2}{b-1}=3+\frac{1}{b-1}\leq\frac{7}{2}.$

If $|S|=b-1$, then

$I^{\prime}(G)\leq\frac{|Y|}{iso(G-Y)-1}=\frac{3b-1}{b-1}=3+\frac{2}{b-1}.$

Clearly, $I^{\prime}(G)\leq 4$ when $b=3$ (i.e., $n=11$),
$I^{\prime}(G)\leq\frac{11}{3}$ when $b=4$ (i.e., $n=15$), and
$I^{\prime}(G)\leq\frac{7}{2}$ when $b\geq 5$. Therefore (ii), (iii) and (iv)
hold.

Remark 3.  Similar to Remark 2, we can obtain that
$I^{\prime}(H_{m})=\frac{3m-1}{m-1}$. Therefore, we have
$I^{\prime}(H_{2})=5$, $I^{\prime}(H_{3})=4$, $I^{\prime}(H_{4})=\frac{11}{3}$
and $I^{\prime}(H_{5})=\frac{7}{2}$. This implies that the bounds are tight in
Lemma 2.4.

Theorem 1.3 is an immediate result of Lemma 2.4 (iv). We consider the binding
number of a graph without $\\{K_{2},C_{2i+1}|i\geq 2\\}$-factor in the
following.

######  Lemma 2.5.

Let $G$ be a graph of order at least $5$. If $G$ admits no
$\\{K_{2},C_{2i+1}|i\geq 2\\}$-factors, then $bind(G)\leq\frac{4}{3}$.

###### Proof.

By Theorem 2.1, there exists an $S\subseteq V(G)$ such that
$c_{tc}(G-S)\geq|S|+1$. Let $A$, $B$ and $C$ denote the collections of
$K_{1}$, $K_{3}$ and triangular-cactus with at least $5$ vertices in $G-S$,
respectively, and let $|A|=a$, $|B|=b$, $|C|=c$. Let
$T_{1},T_{2},\ldots,T_{c}$ be the components of triangular-cactus with at
least $5$ vertices. So we rewrite $c_{tc}(G-S)=a+b+c\geq|S|+1\geq 1$, and then
$|S|\leq a+b+c-1$. Note that $|V(G)|\geq a+3b+5c+|S|$. If $a\neq 0$, we take
$Y=V(G)\setminus S$. Note that $N_{G}(Y)=V(G)\setminus A\neq V(G)$. Thus

$\displaystyle bind(G)$ $\displaystyle\leq\frac{|N_{G}(Y)|}{|Y|}$
$\displaystyle=\frac{|V(G)|-a}{|V(G)|-|S|}$
$\displaystyle=1+\frac{|S|-a}{|V(G)|-|S|}$ $\displaystyle\leq
1+\frac{b+c-1}{a+3b+5c}$ $\displaystyle<1+\frac{b+c}{3b+3c}$
$\displaystyle=\frac{4}{3}.$

We now divide two cases to complete the proof for $a=0$ in the following.

Case 1. $c=0$.

Note that $b\geq 2$ as $|V(G)|\geq 5$. Clearly $|S|\leq b-1$. Let $Y$ be a set
of all vertices from $b-1$ $K_{3}$’s in $B$. Clearly $|Y|=3(b-1)$. Note that
$N_{G}(Y)\subseteq Y\cup S\neq V(G)$, and then $|N_{G}(Y)|\leq 3(b-1)+|S|\leq
4(b-1)$. Thus

$bind(G)\leq\frac{|N_{G}(Y)|}{|Y|}\leq\frac{4(b-1)}{3(b-1)}=\frac{4}{3}.$

Case 2. $c\geq 1$.

Let $v$ be a vertex of degree $2$ in $T_{1}$. Then $|N_{T_{1}}(v)|=2$. Set
$Y=V(G)\setminus(S\cup N_{T_{1}}(v))$. Then $N_{G}(Y)\subseteq
V(G)\setminus\\{v\\}.$ Clearly $|Y|=|V(G)|-|S|-2$ and
$|N_{G}(Y)|\leq|V(G)|-1$. Then

$\displaystyle bind(G)$ $\displaystyle\leq\frac{|N_{G}(Y)|}{|Y|}$
$\displaystyle\leq\frac{|V(G)|-1}{|V(G)|-|S|-2}$
$\displaystyle=1+\frac{|S|+1}{|V(G)|-|S|-2}$ $\displaystyle\leq
1+\frac{|S|+1}{|V(B)|+|V(C)|-2}$ $\displaystyle\leq 1+\frac{b+c}{3b+5c-2}$
$\displaystyle\leq 1+\frac{b+c}{3b+3c}$ $\displaystyle=\frac{4}{3}.$

The proof is complete.

Remark 4.  Recall the graph $H_{m}$ defined in Remark 2. Let $Y\subseteq
V(H_{m})$ such that $N_{H_{m}}(Y)\neq V(H_{m})$. Then $|Y\cap V(K)|\leq 1$. If
$|Y\cap V(K)|=1$, then $|Y\cap(V(H_{m})\setminus V(K))|=0$ as
$N_{H_{m}}(Y)\neq V(H_{m})$. Therefore we have
$\frac{|N_{G}(Y)|}{|Y|}=\frac{|V(G)|-1}{1}>\frac{4}{3}$. If $|Y\cap V(K)|=0$,
let $m_{i}$ be the number of $K_{3}$’s such that $|Y\cap V(K_{3})|=i$ in
$H_{m}-V(K)$, where $i=1,2,3$. Clearly, $|Y|=m_{1}+2m_{2}+3m_{3}$ and
$|N_{H_{m}}(Y)|=m-1+2m_{1}+3m_{2}+3m_{3}$. Since $N_{H_{m}}(Y)\neq V(H_{m})$,
we have $m_{2}+m_{3}\leq m-1$. Then

$\displaystyle\frac{|N_{H_{m}}(Y)|}{|Y|}$
$\displaystyle=\frac{m-1+2m_{1}+3m_{2}+3m_{3}}{m_{1}+2m_{2}+3m_{3}}$
$\displaystyle=2+\frac{m-1-m_{2}-3m_{3}}{m_{1}+2m_{2}+3m_{3}}$
$\displaystyle\geq 2-\frac{2m_{3}}{m_{1}+2m_{2}+3m_{3}}$
$\displaystyle=\frac{4}{3}+\frac{2m_{1}+4m_{2}}{3(m_{1}+2m_{2}+3m_{3})}$
$\displaystyle\geq\frac{4}{3}.$

By Lemma 2.5, we have $bind(H_{m})=\frac{4}{3}$, which implies that the bound
is tight. In addition, we can also take a simple example to show the tightness
of our bound. Let $G$ denote a triangular-cactus with $5$ vertices. Obviously,
$G$ has no $\\{K_{2},C_{2i+1}|i\geq 2\\}$-factor and $bind(G)=\frac{4}{3}$.

## References

  * [1] I. Anderson, Perfect matchings of a graph, _J. Combin. Theory Ser. B_ 10 (1971) (3) 183-186.
  * [2] W. Gao, J. Guirao, Y. Chen, A toughness condition for fractional $(k,m)$-deleted graphs revisited, _Acta Math. Sin. (Engl. Ser.)_ 35 (2019) 1227-1237.
  * [3] W. Gao, W.F. Wang, Remarks on component factors, _J. Oper. Res. Soc. China_ (2021), https://doi.org/10.1007/s40305-021-00357-6.
  * [4] V. Chvátal, Tough graphs and Hamiltonian circuits, _Discrete Math._ 5 (1973) 215-228.
  * [5] G. Cornuéjols, W.R. Pulleyblank, Perfect triangle-free $2$-matchings, Combinatorial optimization, II (Proc. Conf. Univ. East Anglia, Norwich,1979), _Math. Program. Stud._ 13 (1980) 1-7.
  * [6] P. Katerinis, D.R. Woodall, Binding numbers of graphs and the existence of $k$-factors, _Q. J. Math., Oxf. II. Ser._ 38 (1987)(2) 221-228.
  * [7] C. Liu, L. Zhang, Toughness and the existence of fractional $k$-factors of graphs, _Discrete Math._ 308 (2008) 1741-1748.
  * [8] M. Kano, H. Lu, Q. Yu, Component factors with large components in graphs, _Appl. Math. Lett._ 23 (2010) 385-389.
  * [9] E. Scheinerman, D. Ullman, _Fractional Graph Theory: A Rational Approach to the Theory of Graphs_ , John Wiley, New York, 1997\.
  * [10] D. Woodall, The binding number of a graph and its Anderson number, _J. Combin. Theory Ser. B_ 15 (1973) 225-255.
  * [11] J. Yang, Y. Ma, G. Liu, Fractional $(g,f)$-factors in graphs, _Appl. Math. J. Chinese Univ. Ser. A_ 16 (2001) 385-390.
  * [12] Q. Yu, G. Liu, Graph Factors and Matching Extensions, Higher Education Press, Beijing, 2009, p.xii+353. Springer-Verlag, Berlin.
  * [13] Y. Yuan, R. Hao, Toughness condition for the existence of all fractional $(a,b,k)$-critical graphs, _Discrete Math._ 342 (2019) 2308-2314.
  * [14] L. Zhang, G. Liu, Fractional $k$-factor of graphs, _J. Syst. Sci. Math. Sci._ 21 (2001) 88-92.
  * [15] S. Zhou, Z. Sun, Binding number conditions for $P_{\geq 2}$-factor and $P_{\geq 3}$-factor uniform graphs, Discrete Math. 343 (3) (2020) 111715.
  * [16] S. Zhou, J. Wu, T. Zhang, The existence of $P_{\geq 3}$-factor covered graphs, _Discuss. Math. Graph Theory_ 37(4) (2017) 1055-1065.


$f(\varphi)\,\stackrel{{\scriptstyle\text{{def}}}}{{=}}\,\exists
x_{1}\ldots\exists
x_{n}.\,(f(\varphi,\textsf{VAR},1,\emptyset)\wedge\displaystyle{\bigwedge_{i\in[1,n]}}(y_{i}^{1}=x_{i}\wedge
x_{i}=0))$

By Claim 1, it follows that for each finite trace, $enc(w)\models\varphi$ if
and only if $w\models f(\varphi)$. This concludes the proof of Proposition
9.theorem.

###  9.3 Syntax and semantics of past HyperLTLC and proof of Theorem 3.16

In this section, we first define the syntax and semantics of past HyperLTLC,
the extension of HyperLTLC with past temporal modalities. Then, we provide a
proof of Theorem 3.16.

The syntax of past HyperLTLC quantifier-free formulas $\psi$ over AP and VAR
is as follows:

$\psi::=\top\ |\ p[x]\ |\ \neg\psi\ |\ \psi\wedge\psi\ |\ \textsf{X}\psi\ |\
\textsf{Y}\psi\ |\ \psi\textsf{U}\psi\ |\ \psi\textsf{S}\psi\ |\ \langle
C\rangle\psi$

where Y (“previous") and S (“since") are the standard past counterparts of the
temporal modalities X and U, respectively. Let $C$ be a context, $\Pi$ a
pointed-trace assignment, and $i\geq 0$ be an offset. The _$(C,i)$
-predecessor of $\Pi$_, denoted by $\Pi-_{C}i$, is defined as follows:

  * •

if there is $x\in{\textit{Dom}}(\Pi)\cap C$ such that $\Pi(x)=(\pi,h)$ and
$h<i$, then $\Pi-_{C}i=\textsf{und}$ (intuitively, und denotes the _undefined_
value);

  * •

otherwise, $\Pi-_{C}i$ is the pointed-trace assignment with domain
${\textit{Dom}}(\Pi)$ defined as follows. For each $x\in{\textit{Dom}}(\Pi)$,
where $\Pi(x)=(\pi,h)$: $[\Pi-_{C}i](x)=(\pi,h-i)$ if $x\in C$, and
$[\Pi-_{C}i](x)=\Pi(x)$ otherwise.

Intuitively, if the pointed-trace assignment $\Pi-_{C}i$ is defined, then the
positions of the pointed traces associated with the variables in $C$ move back
of $i$ steps, while the positions of the other pointed traces remain
unchanged. The semantics of the past temporal modalities is as follows:

$\begin{array}[]{ll}(\Pi,C)\models\textsf{Y}\psi&\Leftrightarrow\Pi-_{C}1\neq\textsf{und}\text{
and }(\Pi-_{C}1,C)\models\psi\\\
(\Pi,C)\models\psi_{1}\textsf{S}\psi_{2}&\Leftrightarrow\text{for some }i\geq
0\text{ such that
}\Pi-_{C}i\neq\textsf{und}:\,(\Pi-_{C}i,C)\models\psi_{2}\text{ and }\\\
&\,\,(\Pi-_{C}k,C)\models\psi_{1}\text{ for all }0\leq k<i\end{array}$

We write $\Pi\models\psi$ to mean that $(\Pi,\textsf{VAR})\models\psi$.
Moreover, for a trace $w$, we write $w\models\psi$ to mean that
$\Pi_{w}\models\psi$, where $\Pi_{w}$ is the initial pointed-trace assignment
associating to each trace variable occurring in $\psi$ the pointed trace
$(w,0)$.

Theorem 3.16 directly follows from the following two propositions.

######  Proposition 9.theorem.

Let $\varphi$ be a FO[$<$, $+$] sentence over AP. Then, one can construct in
polynomial time a HyperLTLC quantifier-free formula $f(\varphi)$ over AP such
that for each trace $w$, it holds that $w\models\varphi$ _if and only if_
$w\models f(\varphi)$.

######  Proof 9.theorem.

The proof is similar to that of Proposition 9.theorem but we use the past
temporal modalities for encoding the atomic formulas of the given FO[$<$, $+$]
sentence $\varphi$. In particular, given two variables $x$ and $y$, we exploit
the following past HyperLTLC quantifier-free formula $\psi_{=}(x,y)$ for
expressing that $x$ and $y$ refer to the same position:

$\begin{array}[]{ll}\psi_{=}(x,y)&\,\stackrel{{\scriptstyle\text{{def}}}}{{=}}\,({\textit{init}}(x)\wedge{\textit{init}}(y))\vee\\{x,y\\}\textsf{Y}(\,\top\,\textsf{S}\,({\textit{init}}(x)\wedge{\textit{init}}(y)))\vspace{0.2cm}\\\
{\textit{init}}(z)&\,\stackrel{{\scriptstyle\text{{def}}}}{{=}}\,\\{z\\}\,\neg\textsf{Y}(\displaystyle{\bigvee_{p\in\textsf{AP}}}(p[z]\vee\neg
p[z]))\quad\text{ for each }z\in\textsf{VAR}\end{array}$

The proof of the following proposition is a simplified version of that of
Proposition 9.theorem and we omit the details here.

######  Proposition 9.theorem.

Let $\varphi$ be a past HyperLTLC quantifier-free formula over AP. Then, one
can construct in polynomial time a FO[$<$, $+$] sentence $f(\varphi)$ over AP
such that for each trace $w$, it holds that $w\models f(\varphi)$ _if and only
if_ $w\models\varphi$.

###  9.4 Proof of Theorem 3.17

In this section, we provide a proof of Theorem 3.17.

######  Theorem 3.theorem.

Model-checking against the fragment ${\mathcal{U}}$ of HyperLTLC is
$\Sigma_{0}^{1}$-hard.

######  Proof 9.theorem.

The result is obtained by a polynomial time reduction from the halting problem
of non-deterministic Minsky $2$-counter machines [19], a well-known
$\Sigma_{0}^{1}$-complete problem [19].

Recall that the fragment ${\mathcal{U}}$ consists of two-variable quantifier
alternation-free formulas of the form $\exists x_{1}.\exists
x_{2}.\,\psi_{0}\wedge\\{x_{2}\\}\textsf{F}\\{x_{1},x_{2}\\}\psi$, where
$\psi_{0}$ and $\psi$ are quantifier-free HyperLTL formulas. Fix a Minsky
$2$-counter machine $M=\langle
Q,\Delta,\delta_{\textit{init}},\delta_{\textit{halt}}\rangle$. Note that $M$
is defined as at the end of Section 3.1 but the designated transition
$\delta_{\textit{rec}}$ is replaced with the halting transition
$\delta_{\textit{halt}}$. An halting computation of $M$ is a finite
computation of $M$ starting at the initial configuration and leading to a
configuration of the form $(\delta_{\textit{halt}},\nu)$ for some counter
valuation $\nu:\\{1,2\\}\rightarrow{\mathbb{N}}$. The halting problem consists
in checking the existence of an halting computation for the given machine $M$.
Without loss of generality, we assume that
$\delta_{\textit{init}}\neq\delta_{\textit{halt}}$. We construct a Kripke
structure $\mathcal{K}_{M}$ and a HyperLTLC formula $\varphi_{M}$ in the
fragment ${\mathcal{U}}$ such that there is an halting computation of $M$ iff
$\mathcal{L}(\mathcal{K}_{M})\models\varphi_{M}$ (i.e., $\mathcal{K}_{M}$ is a
model of $\varphi_{M}$).

We first provide a description of the reduction. Codes of $M$-configurations
(_segments_) are similar to the ones described in the proof of Theorem 3.7,
where the padding proposition allows to obtain codes of the same
$M$-configuration having arbitrary length. The finite Kripke structure
$\mathcal{K}_{M}$ ensures that its set of traces contains the _well-formed
traces_ $\pi$ of the form $s_{1}\ldots s_{n}\cdot\\{\bot\\}^{\omega}$, where
$s_{1},\ldots,s_{n}$ are segments, segment $s_{1}$ encodes the initial
configuration, segment $s_{n}$ encodes some halting configuration, and the
second segment $s_{2}$ is marked by a special proposition. Then the
${\mathcal{U}}$-formula ensures that both the two variables, say $x_{1}$ and
$x_{2}$, are bound to a well-formed trace $\pi=s_{1}\ldots
s_{n}\cdot\\{\bot\\}^{\omega}$ and $\pi$ is faithful to the evolution of $M$.
This last requirement is ensured by moving in the context $\\{x_{2}\\}$ the
position for the $x_{2}$-trace to the beginning of the second segment $s_{2}$,
and by requiring, by means of a lockstepwise traversal of the trace $\pi$ and
the suffix of $\pi$ starting from the beginning of the second segment $s_{2}$,
that all the segments have the same length. In this way, in this traversal,
the $(i+1)^{th}$-segment of $\pi$ along the $x_{2}$-trace matches the
$i^{th}$-segment along the $x_{1}$-trace, and one can ensure that the
configuration encoded by the $(i+1)^{th}$-segment is a $M$-successor of the
configuration encoded by the $i^{th}$-segment. Note that the existence of an
halting computation in $M$ entails the existence of a uniform upper bound on
the values of the counters along the computation. Thus, by exploiting the
padding proposition, one can ensure that in the encoding of such a computation
all the segments have the same length.

We now proceed with the technical details of the reduction. We exploit the set
AP of atomic propositions defined as
$\textsf{AP}\,\stackrel{{\scriptstyle\text{{def}}}}{{=}}\,\Delta\cup\\{c_{1},c_{2},\\#,\textit{beg},\textit{pad},\bot\\}$.
An $M$-configuration $(\delta,\nu)$ is encoded by the finite words over
$2^{\textsf{AP}}$ (called _segments_) of the form:

$\\{\textit{beg},\delta\\}P_{1}\ldots P_{m}\\{\textit{pad}\\}^{k}$

where $k\geq 1$, $m=\max(\nu(1),\nu(2))$, and for all $i\in[1,m]$, (i)
$\emptyset\neq P_{i}\subseteq\\{c_{1},c_{2}\\}$ and (ii) for all
$\ell\in\\{1,2\\}$, $c_{\ell}\in P_{i}$ iff $i\leq\nu(\ell)$. A _marked
segment_ is defined as a segment but the first position is additionally
labeled by the proposition $\\#$. A _well-formed_ trace of $M$ is a trace of
the form $s_{1}\ldots s_{n}\cdot\\{\bot\\}^{\omega}$ such that (i) $n>1$ and
$s_{1},\ldots,s_{n}$ are $n$ segments, (ii) $s_{1}$ encodes the initial
configuration, (iii) $s_{n}$ encodes some halting configuration, and (iv)
$s_{2}$ is a marked segment. Thus, halting computations of $M$ are encoded by
well-formed traces which, additionally, are faithful to the evolution of $M$.
The following result is straightforward.

Claim. One can construct in polynomial time a Kripke structure
$\mathcal{K}_{M}$ such that

  * •

$\mathcal{L}(\mathcal{K}_{M})$ contains all the well-formed traces.

  * •

For each $\pi\in\mathcal{L}(\mathcal{K}_{M})$, $\pi$ is well-formed iff $\pi$
visits a position labeled by $\bot$.

We construct a ${\mathcal{U}}$-formula $\varphi_{M}$ such that
$\mathcal{L}(\mathcal{K}_{M})\models\varphi_{M}$ iff there is a well-formed
trace which is faithful to the evolution of $M$. Hence, the result follows.
The ${\mathcal{U}}$-formula $\varphi_{M}$ is defined as follows:

$\varphi_{M}\,\stackrel{{\scriptstyle\text{{def}}}}{{=}}\,\exists
x_{1}.\exists
x_{2}.\displaystyle{\bigwedge_{p\in\textsf{AP}}}\textsf{G}(p[x_{1}]\leftrightarrow
p[x_{2}])\,\wedge\,\\{x_{2}\\}\textsf{F}\\{x_{1},x_{2}\\}\bigl{(}\\#[x_{2}]\,\wedge\,\textsf{F}\bot[x_{2}]\,\wedge\,\psi_{f}\,\bigr{)}$

where $\psi_{f}$ is a quantifier-free HyperLTL formula defined in the
following. Note that the first conjunct ensures that variables $x_{1}$ and
$x_{2}$ are bound to the same trace $\pi$ of $\mathcal{K}_{M}$, while by the
previous claim, the subformula $\textsf{F}\bot[x_{2}]$ in the second conjunct
ensures that the trace $\pi=s_{1}\ldots s_{n}\cdot\\{\bot\\}^{\omega}$ is
well-formed. Moreover, the position for the $x_{2}$-trace is moved to the
beginning of the second segment of $\pi$ in the context $\\{x_{2}\\}$ and
$\psi_{f}$ ensures by a lockstepwise traversal of the trace $\pi$ and the
suffix of $\pi$ starting from the beginning of the second segment that $\pi$
is faithful to the evolution of $M$. The quantifier-free HyperLTL formula
$\psi_{f}$ consists of two conjuncts enforcing the following requirements:

  * •

The segments $s_{1},\ldots,s_{n}$ have the same length. This ensures that in
the lockstepwise traversal of $\pi$ (bound to variable $x_{1}$) and
$s_{2}\ldots s_{n}\cdot\\{\bot\\}^{\omega}$ (bound to variable $x_{2}$), the
$(i+1)^{th}$-segment for the $x_{2}$-trace matches in the traversal the
$i^{th}$-segment for the $x_{1}$-trace for all $1\leq i<n$.

$\textsf{G}(\textit{beg}[x_{2}]\leftrightarrow\textit{beg}[x_{1}])$

  * •

The configuration encoded by the $(i+1)^{th}$-segment for the $x_{2}$-trace is
a $M$-successor of the configuration encoded by the $i^{th}$-segment for the
$x_{1}$-trace for all $1\leq i<n$.

$\displaystyle{\bigwedge_{\delta=(q,({\textit{op}},\ell),q^{\prime})\in\Delta}}\textsf{G}\Bigl{(}\bigl{(}\textit{beg}[x_{1}]\wedge\textit{beg}[x_{2}]\wedge\delta[x_{1}]\bigr{)}\,\longrightarrow\,\Bigl{(}\displaystyle{\bigvee_{\delta^{\prime}=(q^{\prime},({\textit{op}}^{\prime},\ell^{\prime}),q^{\prime\prime})\in\Delta}}\delta^{\prime}[x_{2}]\,\wedge\,$
$\hskip 71.13188pt\underbrace{\textsf{X}\bigl{(}(c_{3-\ell}[x_{1}]\wedge
c_{3-\ell}[x_{2}])\textsf{U}(\neg c_{3-\ell}[x_{1}]\wedge\neg
c_{3-\ell}[x_{2}])}_{\text{the value of counter $3-\ell$ does not
change}}\bigr{)}\,\wedge\,$ $\hskip
14.22636pt\underbrace{{\textit{op}}={\mathsf{inc}}\rightarrow\textsf{X}\bigl{(}(c_{\ell}[x_{1}]\wedge
c_{\ell}[x_{2}])\textsf{U}(\neg c_{\ell}[x_{1}]\wedge
c_{\ell}[x_{2}]\wedge\neg\textsf{X}c_{\ell}[x_{2}])}_{\text{increment of
counter $\ell$}}\bigr{)}\,\wedge\,$ $\hskip
14.22636pt\underbrace{{\textit{op}}={\mathsf{dec}}\rightarrow\textsf{X}\bigl{(}(c_{\ell}[x_{1}]\wedge
c_{\ell}[x_{2}])\textsf{U}(c_{\ell}[x_{1}]\wedge\neg
c_{\ell}[x_{2}]\wedge\neg\textsf{X}c_{\ell}[x_{1}])}_{\text{decrement of
counter $\ell$}}\bigr{)}\,\wedge\,$ $\hskip
71.13188pt\underbrace{{\textit{op}}={\mathsf{if\\_zero}}\rightarrow\textsf{X}(\neg
c_{\ell}[x_{1}]\wedge\neg c_{\ell}[x_{2}])}_{\text{zero test of counter
$\ell$}}\,\,\Bigr{)}\Bigr{)}$

By construction, if $\mathcal{L}(\mathcal{K}_{M})\models\varphi_{M}$, then
there exists a well-formed trace which is faithful to the evolution of $M$,
hence, there is an halting computation of $M$. Vice versa if there is an
halting computation $\rho$ of $M$, then there is a uniform bound on the
counter values along $\rho$. Hence, by construction, there exists a well-
formed trace $\pi$ whose segments have the same length which satisfies the
quantifier-free part of $\varphi_{M}$ with $x_{1}$ and $x_{2}$ bound to $\pi$.
By the previous claim, it follows that
$\mathcal{L}(\mathcal{K}_{M})\models\varphi_{M}$, and we are done.

###  9.5 Proof of Theorem 3.18

In this section, we provide a proof of Theorem 3.18. We show that a simple
HyperLTLC formula can be translated in polynomial time into an equivalent
FO[$<$,E] formula (see Appendix 10.1 for the definition of the syntax and
semantics of FO[$<$,E]). Thus, since model checking of FO[$<$,E] is decidable
[7], Theorem 3.18 directly follows.

######  Proposition 9.theorem.

Given a simple HyperLTLC formula, one can construct in polynomial time an
equivalent FO[$<$,E] formula.

######  Proof 9.theorem.

Let $\textsf{VAR}=\\{x_{1},\ldots,x_{n}\\}$ and ${\mathcal{F}}$ be the set of
quantifier-free HyperLTLC formulas over VAR of the form $C\psi$ such that $C$
is a context and $\psi$ is a quantifier-free HyperLTLC formula whose contexts
are all singletons, i.e. consisting of a single trace variable. Evidently,
each simple HyperLTLC quantifier-free formula $\varphi$ can be equivalently
rewritten as a Boolean combination of quantifier-free formulas in the fragment
${\mathcal{F}}$. Thus, it suffices to show that for each formula $C\psi$ in
the fragment ${\mathcal{F}}$, there exists a FO[$<$,E] formula $\psi^{\prime}$
with free variables $x_{1},\ldots,x_{n}$ such that for all sets $\mathcal{L}$
of traces and _initial_ pointed-trace assignments $\Pi$ over VAR and
$\mathcal{L}$, it holds that $\Pi\models C\psi$ iff
$\Pi\models_{\mathcal{L}}\psi^{\prime}$.

For each variable $x_{i}\in\textsf{VAR}$ and $\ell\in{\mathbb{N}}$, let
$y_{i}^{\ell}$ be a fresh copy of $x_{i}$. For a quantifier-free HyperLTLC
formula $\psi$ whose contexts are all singletons, a context $\emptyset\neq
C\subseteq\textsf{VAR}$, and $\ell\in{\mathbb{N}}$, we associate to the tuple
$(\psi,C,\ell)$, a FO[$<$,E] formula $f(\psi,C,\ell)$ with free variables
$y_{1}^{\ell},\ldots,y_{n}^{\ell}$. The mapping $f$ is inductively defined as
follows (recall that for each $p\in\textsf{AP}$, FO[$<$,E] provides the
monadic predicate $P_{p}$):

  * •

$f(p[x_{i}],C,\ell)\,\stackrel{{\scriptstyle\text{{def}}}}{{=}}\,P_{p}(y_{i}^{\ell})$.

  * •

$f(\neg\psi,C,\ell)\,\stackrel{{\scriptstyle\text{{def}}}}{{=}}\,\neg
f(\psi,C,\ell)$.

  * •

$f(\psi_{1}\wedge\psi_{2},C,\ell)\,\stackrel{{\scriptstyle\text{{def}}}}{{=}}\,f(\psi_{1},C,\ell)\wedge
f(\psi_{2},C,\ell)$.

  * •

$\begin{array}[]{l}f(\textsf{X}\psi,C,\ell)\,\stackrel{{\scriptstyle\text{{def}}}}{{=}}\,\exists
y_{1}^{\ell+1}.\,\ldots\exists
y_{n}^{\ell+1}.\,\bigl{(}\displaystyle{\bigwedge_{x_{i}\in
C}}y_{i}^{\ell+1}=y_{i}^{\ell}+1\,\wedge\,\displaystyle{\bigwedge_{x_{i}\notin
C}}y_{i}^{\ell+1}=y_{i}^{\ell}\,\wedge\,f(\psi,C,\ell+1)\bigr{)}\end{array}$

Note that for variables $x$ and $y$, the predicate $y=x+1$ can be expressed in
FO[$<$,E] as follows: $x<y\wedge\neg\exists z.\,x<z\wedge z<y$.

  * •

$\begin{array}[]{ll}f(\psi_{1}\textsf{U}\psi_{2},C,\ell)\,\stackrel{{\scriptstyle\text{{def}}}}{{=}}&\exists
y_{1}^{\ell+1}.\,\ldots\exists
y_{n}^{\ell+1}.\,\Bigl{(}\displaystyle{\bigwedge_{x_{i}\in C}}y_{i}^{\ell}\leq
y_{i}^{\ell+1}\,\wedge\,\displaystyle{\bigwedge_{x_{i}\notin
C}}y_{i}^{\ell+1}=y_{i}^{\ell}\,\wedge\,\theta_{E}(C,\ell+1)\,\wedge\vspace{0.1cm}\\\
&f(\psi_{2},C,\ell+1)\,\wedge\,\forall y_{1}^{\ell+2}.\,\ldots\forall
y_{n}^{\ell+2}.\,\bigl{[}\displaystyle{\bigwedge_{x_{i}\in
C}}(y_{i}^{\ell}\leq
y_{i}^{\ell+2}\,\wedge\,y_{i}^{\ell+2}<y_{i}^{\ell+1})\,\wedge\vspace{0.1cm}\\\
&\displaystyle{\bigwedge_{x_{i}\notin
C}}y_{i}^{\ell+2}=y_{i}^{\ell}\,\wedge\,\theta_{E}(C,\ell+2)\bigr{]}\longrightarrow
f(\psi_{1},C,\ell+2)\Bigr{)}\vspace{0.1cm}\\\
\theta_{E}(C,\ell)\,\stackrel{{\scriptstyle\text{{def}}}}{{=}}&\displaystyle{\bigwedge_{x_{i},x_{j}\in
C\mid x_{i}\neq x_{j}}}E(y_{i}^{\ell},y_{j}^{\ell})\end{array}$

Note that if $C$ is a singleton, then $\theta_{E}(C,\ell)$ is $\top$ (the
empty conjunction is $\top$).

  * •

$f(\\{x_{i}\\}\psi,C,\ell)\,\stackrel{{\scriptstyle\text{{def}}}}{{=}}\,f(\psi,\\{x_{i}\\},\ell)$.

By construction, we obtain the following result, where a pointed-trace
assignment $\Pi$ with domain VAR is _consistent with a context $C$_ if there
is a unique position $m$ such that for all $x_{i}\in C$, it holds that
$\Pi(x_{i})$ is of the form $(\pi,m)$ for some trace $\pi$.

Claim. Let $\psi$ be a quantifier-free HyperLTLC formula over VAR whose
contexts are all singletons, $C\subseteq\textsf{VAR}$ a context, and
$\ell\in{\mathbb{N}}$. Then, for each set $\mathcal{L}$ of traces and each
pointed-trace assignment $\Pi$ over VAR and $\mathcal{L}$ which is consistent
with the context $C$:

$\Pi\models\psi\text{ if and only if
}\Pi_{\ell}\models_{\mathcal{L}}f(\psi,C,\ell)$

where $\Pi_{\ell}$ is the pointed-trace assignment over
$\\{y_{1}^{\ell},\ldots,y_{n}^{\ell}\\}$ defined as:
$\Pi_{\ell}(y_{i}^{\ell})\,\stackrel{{\scriptstyle\text{{def}}}}{{=}}\,\Pi(x_{i})$.

Proof of the claim. By a straightforward induction on the structure of the
formula $\psi$, (i) we first prove that the result holds when $C$ is a
singleton, and then (ii) we generalize the result to the case where $C$ is not
a singleton. ∎

For a formula $C\psi$ in the fragment ${\mathcal{F}}$, let $\psi^{\prime}$ be
the FO[$<$,E] formula with free variables $x_{1}\ldots,x_{n}$ given by
$\exists y_{1}^{1}.\,\ldots\exists
y_{n}^{1}.\,(f(\psi,C,1)\wedge\displaystyle{\bigwedge_{x_{i}\in\textsf{VAR}}}y_{i}^{1}=x_{i})$.
By the previous claim, we obtain that for all sets $\mathcal{L}$ of traces and
_initial_ pointed-trace assignments $\Pi$ over VAR and $\mathcal{L}$, it holds
that $\Pi\models\psi$ iff $\Pi\models_{\mathcal{L}}\psi^{\prime}$, and we are
done.

##  10 Proofs from Section 4

###  10.1 Syntax and semantics of FO[$<$,E] and S1S[E]

We recall syntax and semantics of the logics FO[$<$,E] [14] and S1S[E] [7].
FO[$<$,E] [14] extends standard first-order logic FO[$<$] over infinite words
or traces with the equal-level binary predicate $E$. It is a first-order logic
with equality over the signature $\\{<,E\\}\cup\\{P_{a}\mid
a\in\textsf{AP}\\}$ for a given finite set AP of atomic propositions. S1S[E]
extends FO[$<$,E] by second-order quantification over monadic predicates.

Given a finite set AP of atomic propositions, a finite set
$V_{1}=\\{x,y,\ldots\\}$ of first-order variables, and a finite set
$V_{2}=\\{X,Y,\ldots\\}$ of second-order variables, the syntax of S1S[E]
formulas over AP, $V_{1}$, and $V_{2}$ is as follows:

$\varphi::=P_{a}(x)\ |\ x\in X\ |\ x<y\ |\ x=y\ |\ E(x,y)\ |\ \neg\varphi\ |\
\varphi\wedge\varphi\ |\ \exists x.\varphi|\ \exists X.\varphi$

where $a\in\textsf{AP}$, $x,y\in V_{1}$, and $X\in V_{2}$. A S1S[E] sentence
is a S1S[E] formula where each (first-order or second-order) variable occurs
in the scope of a quantifier. FO[$<$,E] corresponds to the fragment of S1S[E]
where the predicate $x\in X$ and the second-order quantifiers are disallowed.
Note that standard first-order logic FO[$<$] over traces and its monadic
second-order extension S1S syntactically correspond to the fragments of
FO[$<$,E] and S1S[E], respectively, where the equal-level predicate $E$ is
disallowed.

While S1S is interpreted over traces, S1S[E] is interpreted over sets of
traces. A set $\mathcal{L}$ of traces induces the relational structure with
domain $\mathcal{L}\times{\mathbb{N}}$ (i.e., the set of pointed traces
associated with $\mathcal{L}$), where (i) the binary predicate $<$ is
interpreted as the set of pairs of pointed traces in
$\mathcal{L}\times{\mathbb{N}}$ of the form $((\pi,i_{1}),(\pi,i_{2}))$ such
that $i_{1}<i_{2}$, and (ii) the equal-level predicate $E$ is interpreted as
the set of pairs of pointed traces in $\mathcal{L}\times{\mathbb{N}}$ of the
form $((\pi_{1},i),(\pi_{2},i))$. Hence, the predicate $<$ allows to compare
distinct timestamps along the same trace, while the equal-level predicate
allows to compare distinct traces at the same timestamp. The semantics of
S1S[E] is formally defined as follows. A _first-order valuation over
$\mathcal{L}$_ is a pointed-trace assignment $\Pi$ over $V_{1}$ and
$\mathcal{L}$, and a _second-order valuation over $\mathcal{L}$_ is a mapping
${\mathcal{V}}$ assigning to each second-order variable in $V_{2}$ a set of
pointed traces in $\mathcal{L}\times{\mathbb{N}}$. Given a S1S[E] formula
$\varphi$, the satisfaction relation
$\Pi,{\mathcal{V}}\models_{\mathcal{L}}\varphi$ is inductively defined as
follows (we omit the semantics for the Boolean connectives which is standard):

$\begin{array}[]{ll}\Pi,{\mathcal{V}}\models_{\mathcal{L}}P_{a}(x)&\Leftrightarrow\Pi(x)=(\pi,i)\text{
and }a\in\pi(i)\\\ \Pi,{\mathcal{V}}\models_{\mathcal{L}}x\in
X&\Leftrightarrow\Pi(x)\in{\mathcal{V}}(X)\\\
\Pi,{\mathcal{V}}\models_{\mathcal{L}}x<y&\Leftrightarrow\Pi(x)=(\pi_{1},i_{1}),\,\Pi(y)=(\pi_{2},i_{2}),\,\pi_{1}=\pi_{2},\,\text{
and }i_{1}<i_{2}\\\
\Pi,{\mathcal{V}}\models_{\mathcal{L}}x=y&\Leftrightarrow\Pi(x)=\Pi(y)\\\
\Pi,{\mathcal{V}}\models_{\mathcal{L}}E(x,y)&\Leftrightarrow\Pi(x)=(\pi_{1},i_{1}),\,\Pi(y)=(\pi_{2},i_{2}),\text{
and }i_{1}=i_{2}\\\ \Pi,{\mathcal{V}}\models_{\mathcal{L}}\exists
x.\varphi&\Leftrightarrow\Pi[x\mapsto(\pi,i)]\models_{\mathcal{L}}\varphi\text{
for some }(\pi,i)\in\mathcal{L}\times N\\\
\Pi,{\mathcal{V}}\models_{\mathcal{L}}\exists
X.\varphi&\Leftrightarrow{\mathcal{V}}[X\mapsto
A]\models_{\mathcal{L}}\varphi\text{ for some }A\subseteq\mathcal{L}\times
N\end{array}$

where ${\mathcal{V}}[X\mapsto A](X)=A$ and ${\mathcal{V}}[X\mapsto
A](Y)={\mathcal{V}}(Y)$ for $Y\neq X$. Note that if $\varphi$ is a sentence,
then the satisfaction relation $\Pi,{\mathcal{V}}\models_{\mathcal{L}}\varphi$
is independent of $\Pi$ and ${\mathcal{V}}$. We say that $\mathcal{L}$ is a
model of $\varphi$, written $\mathcal{L}\models\varphi$ if
$\Pi,{\mathcal{V}}\models_{\mathcal{L}}\varphi$ for some first-order valuation
$\Pi$ and second-order valuation ${\mathcal{V}}$ over $\mathcal{L}$.

###  10.2 Proof of Lemma 4.1

In this section, we provide a proof of Lemma 4.1 (see Appendix 10.1 for the
definition of the syntax and semantics of S1S[E] and S1S).

######  Lemma 4.theorem.

Let $k\geq 1$ and $\varphi$ be a S1S[E] sentence over AP. Then, one can
construct a S1S sentence $\varphi^{\prime}$ over $\textsf{AP}\times[1,k]$
whose set of models is the $k$-language of $\varphi$.

######  Proof 10.theorem.

Fix $k\geq 1$. Let $\psi$ be a S1S[E] formula over AP with first-order
variables $V_{1}=\\{x_{1},\ldots,x_{n}\\}$ and second-order variables
$V_{2}=\\{X_{1},\ldots,X_{m}\\}$ for some $n\geq 1$ and $m\geq 0$. For each
first-order variable $x_{i}$, we introduce $k$ fresh first-order variables
$y_{i,1},\ldots,y_{i,k}$. Moreover, for each second-order variable $X_{j}$, we
introduce $k$ fresh second-order variables $Y_{j,1},\ldots,Y_{j,k}$. Let
$V^{\prime}_{1}=\\{y_{1,1},\ldots,y_{1,k},\ldots,y_{n,1},\ldots,y_{n,k}\\}$
and
$V^{\prime}_{2}=\\{Y_{1,1},\ldots,Y_{1,k},\ldots,Y_{m,1},\ldots,Y_{m,k}\\}$.
Let $\mathcal{L}=\\{\pi_{1},\ldots,\pi_{k}\\}$ be a set of traces (over AP) of
cardinality $k$. Intuitively, for a first-order variable $x_{i}$ mapped to a
pointed trace $(\pi_{\ell},h)$, we use the variable $y_{i,\ell}$ in S1S for
keeping track of the position $h$ associated to the trace $\pi_{\ell}$ in
$\mathcal{L}$. Moreover, for a set $A\subseteq\mathcal{L}\times{\mathbb{N}}$
mapped to variable $X_{i}$, we use the second-order variables
$Y_{i,1},\ldots,Y_{i,k}$ for partitioning the set of timestamps in $A$ in
accordance to the first component of the pointed traces in $A$ (recall that
the second-order variables in S1S are mapped to sets of positions of the given
trace).

Let $g:V_{1}\mapsto[1,k]$ be a choice function associating to each first-order
variable $x_{i}$ an index $\ell\in[1,k]$. We associate to the S1S[E] formula
$\psi$ and the choice function $g$ an S1S formula $f(\psi,g)$ over
$\textsf{AP}\times[1,k]$, $V^{\prime}_{1}$, and $V^{\prime}_{2}$. The mapping
$f(\psi,g)$ is inductively defined as follows:

  * •

$f$ is homomorphic for the Boolean connectives.

  * •

$f(P_{a}(x_{i}),g)\,\stackrel{{\scriptstyle\text{{def}}}}{{=}}\,P_{(a,g(x_{i}))}(y_{i,g(x_{i})})$

  * •

$f(x_{i}\in
X_{j},g)\,\stackrel{{\scriptstyle\text{{def}}}}{{=}}\,y_{i,g(x_{i})}\in
Y_{j,g(x_{i})}$

  * •

$f(x_{i}<x_{j},g)\,\stackrel{{\scriptstyle\text{{def}}}}{{=}}\,\left\\{\begin{array}[]{ll}\neg\top&\text{
if }g(x_{i})\neq g(x_{j})\\\ y_{i,g(x_{i})}<y_{j,g(x_{j})}&\text{
otherwise}\end{array}\right.$

  * •

$f(x_{i}=x_{j},g)\,\stackrel{{\scriptstyle\text{{def}}}}{{=}}\,\left\\{\begin{array}[]{ll}\neg\top&\text{
if }g(x_{i})\neq g(x_{j})\\\ y_{i,g(x_{i})}=y_{j,g(x_{j})}&\text{
otherwise}\end{array}\right.$

  * •

$f(E(x_{i},x_{j}),g)\,\stackrel{{\scriptstyle\text{{def}}}}{{=}}\,y_{i,g(x_{i})}=y_{j,g(x_{j})}$

  * •

$f(\exists
x_{i}.\,\psi,g)\,\stackrel{{\scriptstyle\text{{def}}}}{{=}}\,\displaystyle{\bigvee_{\ell\in[1,k]}}\exists
y_{i,\ell}.\,f(\psi,g[x_{i}\mapsto\ell])$

  * •

$f(\exists
X_{i}.\,\psi,g)\,\stackrel{{\scriptstyle\text{{def}}}}{{=}}\,\exists
Y_{i,1}.\ldots\exists Y_{i,k}.f(\psi,g)$

where $g[x_{i}\mapsto\ell](x_{j})=\ell$ if $j=i$,
$g[x_{i}\mapsto\ell](x_{j})=g(x_{j})$ otherwise. Fix a well-formed trace $\nu$
over $\textsf{AP}\times[1,k]$ and let $\mathcal{L}(\nu)$ be the set of traces
over AP having cardinality $k$ associated with $\nu$. Then, $\mathcal{L}(\nu)$
can be written in the form $\mathcal{L}(\nu)=\\{\pi_{1},\ldots,\pi_{k}\\}$
where for each $\ell\in[1,k]$ and $i\geq 0$,
$\pi_{\ell}(i)=\\{p\in\textsf{AP}\mid(p,\ell)\in\nu(i)\\}$. Let
$g:V_{1}\mapsto[1,k]$ be a choice function, ${\mathcal{V}}_{1}$ be a first-
order S1S-valuation over $V^{\prime}_{1}$ (i.e., a function associating a
position $i\geq 0$ to each variable in $V^{\prime}_{1}$), and
${\mathcal{V}}_{2}$ be a second-order S1S-valuation over $V^{\prime}_{2}$ for
S1S (i.e., a function associating a subset of ${\mathbb{N}}$ to each variable
in $V^{\prime}_{2}$). We denote by $\Pi({\mathcal{V}}_{1},g)$ and
${\mathcal{V}}({\mathcal{V}}_{2})$ the first-order S1S[E]-valuation and the
second-order S1S[E]-valuation over $V_{1}$ and $V_{2}$, respectively, for the
set of traces $\mathcal{L}(\nu)$, defined as follows:

  * •

for each $x_{i}\in V_{1}$, let $g(x_{i})=\ell$: then
$\Pi({\mathcal{V}}_{1},g)(x_{i})\,\stackrel{{\scriptstyle\text{{def}}}}{{=}}\,(\pi_{\ell},{\mathcal{V}}_{1}(y_{i,\ell}))$;

  * •

for each $X_{i}\in V_{2}$,
${\mathcal{V}}({\mathcal{V}}_{2})(X_{i})\,\stackrel{{\scriptstyle\text{{def}}}}{{=}}\,\displaystyle{\bigcup_{1\leq\ell\leq
k}\\{\pi_{\ell}\\}\times{\mathcal{V}}_{2}(Y_{i,\ell})}$.

We first show the following.

Claim. ${\mathcal{V}}_{1},{\mathcal{V}}_{2}\models_{\nu}f(\psi,g)$ if and only
if
$\Pi({\mathcal{V}}_{1},g),{\mathcal{V}}({\mathcal{V}}_{2})\models_{\mathcal{L}(\nu)}\psi$.

Proof of the claim:  by induction on the structure of $\psi$. The case of
Boolean connectives directly follows from the induction hypothesis. For the
other cases, we proceed as follows:

  * •

$\psi=P_{a}(x_{i})$ for some $a\in\textsf{AP}$ and $i\in[1,n]$. Let
$g(x_{i})=\ell$ and ${\mathcal{V}}_{1}(y_{i,\ell})=h$. By construction,
$f(\psi,g)=P_{(a,\ell)}(y_{i,\ell})$ and
$\Pi({\mathcal{V}}_{1},g)(x_{i})=(\pi_{\ell},h)$. Moreover,
$a\in\pi_{\ell}(h)$ iff $(a,\ell)\in\nu(h)$. Hence, the result follows.

  * •

$\psi=x_{i}\in X_{j}$ for some $i\in[1,n]$ and $j\in[1,m]$. Let
$g(x_{i})=\ell$, ${\mathcal{V}}_{1}(y_{i,\ell})=h$, and
${\mathcal{V}}_{2}(Y_{j,\ell})=A\subseteq{\mathbb{N}}$. By construction,
$f(\psi,g)=y_{i,\ell}\in Y_{j,\ell}$,
$\Pi({\mathcal{V}}_{1},g)(x_{i})=(\pi_{\ell},h)$, and
${\mathcal{V}}({\mathcal{V}}_{2})(X_{j})\cap(\\{\pi_{\ell}\\}\times{\mathbb{N}})=\\{\pi_{\ell}\\}\times
A$. Hence,
$\Pi({\mathcal{V}}_{1},g)(x_{i})\in{\mathcal{V}}({\mathcal{V}}_{2})(X_{j})$
iff ${\mathcal{V}}_{1}(y_{i,\ell})\in{\mathcal{V}}_{2}(Y_{j,\ell})$, and the
result holds in this case as well.

  * •

$\psi=x_{i}<x_{j}$ for some $i,j\in[1,n]$. Let $g(x_{i})=\ell$,
$g(x_{j})=\ell^{\prime}$, ${\mathcal{V}}_{1}(y_{i,\ell})=h$, and
${\mathcal{V}}_{1}(y_{j,\ell^{\prime}})=h^{\prime}$. By construction,
$\Pi({\mathcal{V}}_{1},g)(x_{i})=(\pi_{\ell},h)$ and
$\Pi({\mathcal{V}}_{1},g)(x_{j})=(\pi_{\ell^{\prime}},h^{\prime})$. Moreover,
_either_ $\ell\neq\ell^{\prime}$ and $f(\psi,g)=\neg\top$, _or_
$\ell=\ell^{\prime}$ and $f(\psi,g)=y_{i,\ell}<y_{j,\ell}$. Thus, since
$\pi_{\ell}\neq\pi_{\ell^{\prime}}$ if $\ell\neq\ell^{\prime}$, the result
easily follows.

  * •

$\psi=x_{i}=x_{j}$ for some $i,j\in[1,n]$. This case is similar to the
previous one.

  * •

$\psi=E(x_{i},x_{j})$ for some $i,j\in[1,n]$. Let $g(x_{i})=\ell$,
$g(x_{j})=\ell^{\prime}$, ${\mathcal{V}}_{1}(y_{i,\ell})=h$, and
${\mathcal{V}}_{1}(y_{j,\ell^{\prime}})=h^{\prime}$. By construction,
$\Pi({\mathcal{V}}_{1},g)(x_{i})=(\pi_{\ell},h)$,
$\Pi({\mathcal{V}}_{1},g)(x_{j})=(\pi_{\ell^{\prime}},h^{\prime})$, and
$f(\psi,g)=y_{i,\ell}=y_{j,\ell^{\prime}}$. Hence, (i)
${\mathcal{V}}_{1},{\mathcal{V}}_{2}\models_{\nu}f(\psi,g)$ iff $h=h^{\prime}$
and (ii)
$\Pi({\mathcal{V}}_{1},g),{\mathcal{V}}({\mathcal{V}}_{2})\models_{\mathcal{L}(\nu)}\psi$
iff $h=h^{\prime}$, and the result follows.

  * •

$\psi=\exists x_{i}.\,\theta$ for some $i\in[1,n]$. First, assume that
${\mathcal{V}}_{1},{\mathcal{V}}_{2}\models_{\nu}f(\exists x_{i}.\,\theta,g)$.
By construction, there exists $\ell\in[1,k]$ such that
${\mathcal{V}}_{1},{\mathcal{V}}_{2}\models_{\nu}\exists
y_{i,\ell}.\,f(\theta,g[x_{i}\mapsto\ell])$. Hence, for some
$h\in{\mathbb{N}}$, ${\mathcal{V}}_{1}[y_{i,\ell}\mapsto
h],{\mathcal{V}}_{2}\models_{\nu}f(\theta,g[x_{i}\mapsto\ell])$. Let
${\mathcal{V}}^{\prime}_{1}={\mathcal{V}}_{1}[y_{i,\ell}\mapsto h]$ and
$g^{\prime}=g[x_{i}\mapsto\ell]$. By the induction hypothesis, we have that
$\Pi({\mathcal{V}}^{\prime}_{1},g^{\prime}),{\mathcal{V}}({\mathcal{V}}_{2})\models_{\mathcal{L}(\nu)}\theta$.
Since
$\Pi({\mathcal{V}}^{\prime}_{1},g^{\prime})=\Pi({\mathcal{V}}_{1},g)[x_{i}\mapsto(\pi_{\ell},h)]$,
we obtain that
$\Pi({\mathcal{V}}_{1},g)[x_{i}\mapsto(\pi_{\ell},h)],{\mathcal{V}}({\mathcal{V}}_{2})\models_{\mathcal{L}(\nu)}\theta$.
Hence,
$\Pi({\mathcal{V}}_{1},g),{\mathcal{V}}({\mathcal{V}}_{2})\models_{\mathcal{L}(\nu)}\exists
x_{i}.\,\theta$. The converse implication is similar.

  * •

$\psi=\exists X_{i}.\,\theta$ for some $i\in[1,m]$. First, assume that
${\mathcal{V}}_{1},{\mathcal{V}}_{2}\models_{\nu}f(\exists X_{i}.\,\theta,g)$.
By construction, for each $\ell\in[1,k]$, there exists a set
$A_{\ell}\subseteq{\mathbb{N}}$ such that
${\mathcal{V}}_{1},{\mathcal{V}}_{2}[Y_{i,1}\mapsto
A_{1},\ldots,Y_{i,k}\mapsto A_{k}]\models_{\nu}f(\theta,g)$. Let
${\mathcal{V}}^{\prime}_{2}={\mathcal{V}}_{2}[Y_{i,1}\mapsto
A_{1},\ldots,Y_{i,k}\mapsto A_{k}]$. By the induction hypothesis, we have that
$\Pi({\mathcal{V}}_{1},g),{\mathcal{V}}({\mathcal{V}}^{\prime}_{2})\models_{\mathcal{L}(\nu)}\theta$.
Let $A=\displaystyle{\bigcup_{\ell\in[1,k]}}\\{\pi_{\ell}\\}\times A_{i}$.
Since
${\mathcal{V}}({\mathcal{V}}^{\prime}_{2})={\mathcal{V}}({\mathcal{V}}_{2})[X_{i}\mapsto
A]$, we obtain that
$\Pi({\mathcal{V}}_{1},g),{\mathcal{V}}({\mathcal{V}}_{2})[X_{i}\mapsto
A]\models_{\mathcal{L}(\nu)}\theta$. Hence,
$\Pi({\mathcal{V}}_{1},g),{\mathcal{V}}({\mathcal{V}}_{2})\models_{\mathcal{L}(\nu)}\exists
X_{i}.\,\theta$. The converse implication is similar.

This concludes the proof of the claim.∎

Fix an arbitrary choice function $g_{0}:V_{1}\mapsto[1,k]$. For a S1S[E]
sentence $\varphi$ over AP, $V_{1},$ and $V_{2}$, let $\varphi^{\prime}$ be
the S1S sentence over $\textsf{AP}\times[1,k]$ given by

$\varphi^{\prime}:=f(\varphi,g_{0})\wedge\displaystyle{\bigwedge_{\ell,\ell^{\prime}\in[1,k]:\,\ell\neq\ell}\exists
z_{0}.\,\bigvee_{a\in\textsf{AP}}}(P_{(a,\ell)}(z_{0})\leftrightarrow\neg
P_{(a,\ell^{\prime})}(z_{0}))$

Note that the second conjunct captures the well-formed traces over
$\textsf{AP}\times[1,k]$. By the previous claim, it follows that the
$k$-language of $\varphi$ is the set of traces (over $\textsf{AP}\times[1,k]$)
satisfying $\varphi^{\prime}$. This concludes the proof of Lemma 4.1.