**footnotetext: These authors contributed equally to this work11institutetext:
Insititute of Medical Technologies and Intelligent Systems, Hamburg University
of Technology, Hamburg, Germany
11email: debayan.bhattacharya<EMAIL_ADDRESS>
22institutetext: Department of Otorhinolaryngology, Head and Neck Surgery and
Oncology 33institutetext: Clinic and Polyclinic for Diagnostic and
Interventional Radiology and Nuclear Medicine 44institutetext: Population
Health Research Department, University Heart and Vascular Center
55institutetext: Clinic and Polyclinic for Neurology
University Medical Center Hamburg-Eppendorf, Hamburg, Germany

# Supervised Contrastive Learning to Classify Paranasal Anomalies in the
Maxillary Sinus

Debayan Bhattacharya 1122 Benjamin Tobias Becker 22 Finn Behrendt 11 Marcel
Bengs 11 Dirk Beyersdorff 33 Dennis Eggert 22 Elina Petersen 44 Florian Jansen
22 Marvin Petersen 55 Bastian Cheng 55 Christian Betz 22 Alexander Schlaefer*
11 Anna Sophie Hoffmann* 22

###### Abstract

Using deep learning techniques, anomalies in the paranasal sinus system can be
detected automatically in MRI images and can be further analyzed and
classified based on their volume, shape and other parameters like local
contrast. However due to limited training data, traditional supervised
learning methods often fail to generalize. Existing deep learning methods in
paranasal anomaly classification have been used to diagnose at most one
anomaly. In our work, we consider three anomalies. Specifically, we employ a
3D CNN to separate maxillary sinus volumes without anomaly from maxillary
sinus volumes with anomaly. To learn robust representations from a small
labelled dataset, we propose a novel learning paradigm that combines
contrastive loss and cross-entropy loss. Particularly, we use a supervised
contrastive loss that encourages embeddings of maxillary sinus volumes with
and without anomaly to form two distinct clusters while the cross-entropy loss
encourages the 3D CNN to maintain its discriminative ability. We report that
optimising with both losses is advantageous over optimising with only one
loss. We also find that our training strategy leads to label efficiency. With
our method, a 3D CNN classifier achieves an AUROC of 0.85 $\pm$ 0.03 while a
3D CNN classifier optimised with cross-entropy loss achieves an AUROC of 0.66
$\pm$ 0.1. Our source code is available at
https://github.com/dawnofthedebayan/SupConCE_MICCAI_22.

###### Keywords:

Self-Supervised Learning Paranasal Pathology Nasal Pathology Magnetic
Resonance Images

##  1 Introduction

Paranasal sinus anamolies are common incidental findings reported in patients
who undergo diagnostic imaging of the head [21] for neuroradiological
assessment. Understanding the different opacifications of the paransal sinuses
is very useful, because the frequency of these findings represent clinical
challenges [5], and little is known about the incidence and significance of
these morphological changes in the general population. There have been
numerous studies on analysing the occurrence and progression of these
incidental findings
[19, 16, 18, 17, 2], but mostly in patients with sinunasal symptoms.

In our study, elderly people (45 - 74 years) received an MRI for neuro-
radiological assessment [7] in the city of Hamburg. The purpose of our study
is to find out what percentage of patients, who do not have sinunasal
symptoms, show findings in the paranasal sinus system in MRI images and if it
is possible to detect anomalies in the paranasal sinus system using deep
learning techniques and further analyze and classify based on their volume,
shape and other parameters like local contrast.

A three year retrospective study showed malignant tumors were misdiagnosed as
nasal polyps with a misdiagnosis rate of 5.63% while inverted papilloma were
misdiagnosed as nasal polyps with a rate of 8.45% [12]. As a first step, it
would be beneficial to separate MRI with any paranasal anomaly from normal MRI
using Computer Aided Diagnostics (CAD). This would allow the physicians to
closely inspect the MRIs containing paranasal anomaly with finer detail. This
can reduce chances of misdiagnosis while decreasing the workload of physicians
from having to see normal MRIs.

There have been works of paranasal sinus anomaly diagnosis using supervised
learning [10, 8, 11]. However, all these works have been used to classify at
most one anomaly. Our work considers three anomalies namely: (i) mucosal
thickening (ii) polyps and (iii) cysts. The anomalies are differently located
within the maxillary sinus and therefore we use a 3D volume of the maxillary
sinus as input to our 3D CNN. Additionally, existing works train on large
datasets to achieve good performance. However, labelling is a time consuming
task and in some scenarios it requires the supervision of Ears, Nose and
Throat (ENT) specialised radiologists who may not be immediately available. In
our case, we have a small dataset of 199 MRI volumes. To mitigate the
limitations of our small labelled dataset, we use contrastive learning [14] to
learn robust representations that does not overfit on the training set. In
contrastive learning, an encoder learns to map positive pairs close together
in the embedding space while pushing away negative pairs. In SimCLR [1], an
image is transformed twice through random transformations. The transformed
"views" of the image constitute a positive pair and every other image in the
mini-batch is used to construct negative pairs with the reference image. There
has been significant research in finding the best transformations as the
chosen transformations dictate the quality of learnt representation [1]. The
underlying assumption is that transformations augment the image while
preserving the semantic information. However, in our case two or more images
in the mini-batch can be semantically similar as they belong to the same
class. Particularly, a maxillary sinus of one patient can be semantically
similar to another patient’s maxillary sinus if both patients do not exhibit
any paranasal anomalies. Furthermore, they can be different as well due to the
anatomical variations of the maxillary sinus [19, 17]. Since our dataset
contains anomalies, it is also important that the classifier does not overfit
to a particular anomaly. Therefore, it is important for a classifier to learn
anatomically invariant representation of the maxillary sinus for volumes that
contain no anomaly and learn anomaly invariant representation of the maxillary
sinus for volumes exhibiting one of the three anomalies. This can reduce the
chances of overfitting on the training set. This motivates us to employ a
supervised contrastive learning approach [9] that brings embeddings of
maxillary sinus volumes without anomaly closer together while pushing away
embeddings of maxillary sinus with anomaly in the embedding space and vice
versa. Compared to the original method [9], we propose a training strategy
that simultaneously trains our 3D CNN using the supervised contrastive loss
and regular cross-entropy loss using two different projection networks. The
reasoning behind this is that minimizing the contrastive loss encourages the
3D CNN to learn representations that are robust to anatomical and anomaly
variations while the cross-entropy enforces the 3D CNN to preserve
discriminative ability.

In summary, our contributions are three-fold. First, we demonstrate the
feasibility of a deep learning approach to classify between normal and
anomalous maxillary sinuses. Second, we demonstrate through extensive
experiments that combining supervised contrastive loss and cross-entropy loss
is the better approach to improve the discriminative ability of the 3D CNN
classifier. Third, we empirically show that our method is the most label
efficient.

##  2 Method

Figure 1: (a) Our proposed method. The curved green and red lines represent
similar and dissimilar representations respectively. (b)-(c) Illustration of
the latent space embedding of normal and anomalous maxillary sinuses before
and after the encoder is trained respectively.

In global contrastive learning methods such as SimCLR [1], we learn a
parametric function $F_{\theta}:X\rightarrow\mathbb{R}^{D}$ where
$\mathbb{R}^{D}$ is a unit hypersphere. $F_{\theta}$ is trained to map
semantically similar samples closer together and semantically dissimilar
samples further apart through the InfoNCE loss [20]. The underlying assumption
here is that images in the mini-batch are semantically dissimilar. This is
untrue in our case as we have maxillary sinus volumes belonging to one of the
two classes and there are semantic similarities and dissimilarities in the
intra and inter class samples. Therefore, it is not possible to form
meaningful clusters from the global contrastive loss described in SimCLR [1].
Therefore, to incorporate the class priors, we sample volumes from the two
classes explicitly. Given an input mini-batch $B=\\{x_{1},x_{2},...,x_{N}\\}$
where $x_{i}$ represent the input 3D volume, a random transformation set $T$
is used to form a pair of augmented volumes. Instead of randomly sampling $N$
samples, we randomly sample $N/2$ maxillary sinus volumes without anomaly and
$N/2$ maxillary sinus volumes with anomaly from our dataset. Each of these
$N/2$ subsets undergo random transformation twice using $T$. Let us denote the
set containing all the augmented volumes of the $C$ classes as
$\mathbb{M}=\bigcup_{c=1}^{C}M_{c}$. In our case, $C=2$. Here, $M_{c}$ is the
subset of augmented volumes belonging to a single class and $|M_{c}|$ = $N$ is
its cardinality. Let $m_{i},i\in\mathbb{I}=\\{1,2,...,2N\\}$ represent the
augmented volumes in set $\mathbb{M}$ and $m_{k(i)}$ is its corresponding
volume augmented from the same volume in $B$. Furthermore, let $I_{c}$
represent indices of all the augmented volumes belonging to class $c$ such
that $\mathbb{I}=\bigcup_{c=1}^{C}I_{c}$. Using the above stated assumptions,
the InfoNCE loss that takes into consideration the class priors when making
positive and negative pairs can be written as:

$L_{simclr}=-\sum_{c=1}^{C}\frac{1}{|M_{c}|}\sum_{i\in
I_{c}}log\frac{e^{sim(Z_{i},Z_{k(i)})/\tau}}{e^{sim(Z_{i},Z_{k(i)})/\tau}+\sum_{j\in\mathbb{I}\setminus
I_{c}}e^{sim(Z_{i},Z_{j})/\tau}}$ (1)

where $\tau\in\mathbb{R}^{+}$ is the scalar temperature parameter,
$Z_{i}=F_{\theta}^{con}(m_{i})$ is the normalised feature vector such that
$F_{\theta}^{con}(.)=Proj_{1}(Enc(.))$, $k(i)$ is the index of the
corresponding volume in $\mathbb{M}$ augmented from the same volume in $B$ and
$sim(.)$ is the cosine similarity function. Although Eq. 1 only constructs
negative pairs such that the two volumes are from different classes, it still
constructs positive pairs by augmenting the same volume using the random
augmentation set $T$. As a result, we are reliant on the transformations to
learn meaningful representations. However, the transformations do not
guarantee anatomical and anomaly invariance as the encoder is not incentivised
to produce similar representations for volumes belonging to the same class in
the mini-batch. Therefore, we use a supervised contrastive loss [9] that
constructs arbitrary number of positive pairs where each volume in the pair is
from the same class but unique in the mini-batch. Formally, the supervised
contrastive loss can be described as shown below:

$L_{sc}=-\sum_{c=1}^{C}\frac{1}{|M_{c}|}\sum_{i\in I_{c}}log\frac{\sum_{j\in
I_{c}\setminus\\{i\\}}e^{sim(Z_{i},Z_{j})/\tau}}{\sum_{j\in
I_{c}\setminus\\{i\\}}e^{sim(Z_{i},Z_{j})/\tau}+\sum_{j\in\mathbb{I}\setminus
I_{c}}e^{sim(Z_{i},Z_{j})/\tau}}$ (2)

The main differences of eq. 2 compared to eq. 1 is that numerous positive
pairs are constructed in the numerator by matching every volume with every
other volume belonging to the same class in the mini-batch. In this case,
$|M_{c}|$ = $N/2$ as we do not use $T$ and $\mathbb{I}=\\{1,2,...,N\\}$. This
incentivises the encoder to give similar representations for volumes belonging
to the same class. This leads to learning anatomical and anomaly invariant
representations. Apart from using $L_{sc}$ we also use regular cross-entropy
loss to preserve the discrimintative ability of our 3D CNN. The cross-entropy
loss is formalised as follows:

$L_{ce}=-\frac{1}{N}\sum_{i\in\mathbb{I}}y_{i}log(F_{\theta}^{class}(m_{i}))$
(3)

Here, $F_{\theta}^{class}(.)$ can be decomposed into $Proj_{2}(Enc(.))$ and
$y_{i}$ is the class label of $m_{i}$ such that $y_{i}\in\\{0,1\\}$.
Therefore, our combined loss function is

$L_{ours}=L_{sc}+\lambda L_{ce}$ (4)

In our case, we set $\lambda=1$. In summary, we train models using only
$L_{ce}$ and set this as the baseline. We then train models using $L_{simclr}$
to show that transformation invariance does not help in our downstream
classification task. Next, we train our models using $L_{sc}$ to show the
benefit of clustering based on class priors and the importance of anatomical
and anomaly invariant representation learning. Finally, we train our models
using $L_{ours}$ to show that contrastive loss and cross-entropy loss improve
the discriminative ability of the models and overfit the least on the training
set.

###  2.1 Dataset

Figure 2: [LEFT] Pre-processing steps involve (a) Extraction of 3D sub-volumes
of left and right maxillary sinus from FLAIR MRI samples. (b) Flipping the
coronal plane slices of right maxillary sinus sub-volume to give it the
appearance of left maxillary sinus sub-volume. [RIGHT] FLAIR-MRI slices from
the sagittal , axial and coronal views illustrating the difference between
anomaly and normal class. The red circles denote anomalies and green circles
denote normal maxillary sinus. (c) Cyst observed in right maxillary sinus. (d)
Polyp observed in the left maxillary sinus (e) Cyst observed in left maxillary
sinus. (f) -(h) FLAIR-MRI slices with no pathology.

As part of the population study [7], MRI of the head and neck area of
participants based in the city of Hamburg, Germany were recorded. The MRIs
were recorded at University Medical Center Hamburg-Eppendorf. The age group of
the participants were between 45 and 74 years. Each participant had
T1-weighted and fluid attenuated inversion recovery (FLAIR) sequences stored
in the NIfTI***https://nifti.nimh.nih.gov/ format. FLAIR-MRIs were chosen as
the imaging modality as the incidental findings are more visible due to the
higher contrast relative to T1 weighted MRI. The labelled dataset consists of
199 FLAIR-MRI volumes of which 106 patients exhibit normal maxillary sinuses
and 93 patients have maxillary sinuses with anomaly in at least one maxillary
sinus. The diagnosis of the observed pathology in 199 FLAIR-MRIs was confirmed
by two ENT surgeons and one ENT specialised radiologist. The incidental
findings are categorised and defined as follows: (i) mucosal thickening (ii)
polyps (iii) cysts. The statistics of the pathology observed is reported in
the supplementary material. In this work, all the anomalies are grouped into a
single class called "anomaly" and all the normal maxillary sinuses are grouped
into a class called "normal". Altogether, there are 269 maxillary sinus
volumes without anomaly and 130 abnormal maxillary sinus volumes with anomaly.
Each MRI has a resolution of 173 x 319 x 319 voxels along the saggital,
coronal and axial directions respectively. The voxel size is 0.53 $mm$ x 0.75
$mm$ x 0.75 $mm$.

Preprocessing: We performed rigid registration by randomly selecting one
FLAIR-MRI sample as a fixed volume followed by resampling to a dimension of
128 x 128 x 128. Of the resampled volumes, we extracted two sub-volumes, one
for each maxillary sinus from a single patient. We made sure that the
extracted sub-volumes subsumed the maxillary sinus.

Since the maxillary sinus are symmetric, we horizontally flipped the coronal
planes of right maxillary sinus volumes to make it look like left maxillary
sinus volumes. The decision of which maxillary sinus to flip was arbitrary.
Ultimately, these sub-volumes were reshaped to a standard size of 32 x 32 x 32
voxels for the 3D CNN. Finally, all the maxillary sinus volumes were
normalised to the range of -1 to 1. Our preprocessing step is shown in Fig. 2.

Training, Validation and Test Split: We perform a nested stratified K-fold
with 5 inner and 5 outer folds. The inner fold was used to choose the best
hyperparameters. In summary, each experiment has 80 volumes in test set, 64
volumes in cross validation set and 255 samples in training set. The folds are
constructed by preserving the percentage of samples for the two classes.

##  3 Experiments and Discussion

###  3.1 Implementation Details

All of our experiments are implemented in PyTorch [15] and PyTorch Lightning
[4]. We use a batch size of 128 for all our experiments based on
hyperparameter tuning (See supplementary material). We use Adam Optimization
with a learning rate of 1e-4. Similar to Chen et al. [1], we fix $\tau=0.1$.
Our encoder $Enc(.)$ is the 3DResNet18 [6]. Our projection layer $Proj_{1}(.)$
is a fully connected layer with input dimension 512 and output dimension 128.
A ReLU activation is placed in between the layers. Projection layer
$Proj_{2}(.)$ is a linear fully connected layer with input and output
dimensions of 512 and 2 respectively. All our models are trained for 200
epochs.

###  3.2 Evaluation of learnt representations

Table 1: Evaluation of our representations

Method | $L_{ce}$ | $L_{simclr}$ | $L_{sc}$ | Accuracy | F1(weighted) | AUROC | AUPRC
---|---|---|---|---|---|---|---
Scratch |  |  |  | $0.68\pm 0.03$ | $0.57\pm 0.04$ | $0.66\pm 0.10$ | $0.53\pm 0.12$
Scratch(with aug) |  |  |  | $0.69\pm 0.03$ | $0.58\pm 0.05$ | $0.68\pm 0.10$ | $0.56\pm 0.10$
SimCLR |  |  |  | $0.65\pm 0.03$ | $0.58\pm 0.04$ | $0.54\pm 0.09$ | $0.41\pm 0.09$
SupCon [9] |  |  |  | $0.72\pm 0.05$ | $0.70\pm 0.06$ | $0.73\pm 0.08$ | $0.61\pm 0.08$
Ours |  |  |  | $\textbf{0.80}\pm\textbf{0.02}$ | $\textbf{0.78}\pm\textbf{0.03}$ | $\textbf{0.85}\pm\textbf{0.03}$ | $\textbf{0.78}\pm\textbf{0.03}$

The metrics we have used to evaluate our representations are accuracy, F1
weighted, Area Under Receiver Operator Characteristics (AUROC) and Area Under
Precision Recall Curve (AUPRC). We chose F1 weighted and AUPRC as they give a
fair assessment of the performance of the models in the presence of class
imbalance. Our random transformation set $T$ consists of random affine, flip
and gaussian noise as these are semantic preserving transforms. For training
models with $L_{simclr}$, $L_{sc}$ and $L_{ours}$ we followed the training
strategy followed by Khosla et al [9]. The inference is performed using
$Proj_{2}(.)$ for all the experiments. We test for statistically significant
difference in our performance metrics using a permutation test with $nP$=
10000 samples and a significance level of $\alpha$ = 0.05 [3]. The difference
in the AUROC, AUPRC, F1 weighted and accuracy of our method is significant (p
< 0.05) compared to the other methods. From the results in Table 1 we observe
that the models trained with only $L_{ce}$ overfit and do not generalize well.
Models trained with $L_{sc}$ achieve a significant boost in all metrics
compared to models trained using $L_{ce}$ and $L_{simclr}$. We conjecture this
to be the case because the supervised contrastive loss clusters the maxillary
sinus volumes representations based on its class leading to invariant
representations and less overfitting. The absence of $L_{ce}$ causes the
clusters to be more spread out (See Fig. 3 SupCon). Our loss $L_{ours}$ shows
the best performance due to the increased discriminative ability of the
classifier which is reflected by the formation of compact clusters (See Fig. 3
Ours). SimCLR performs the worst as they fail to form meaningful clusters (See
Fig. 3 SimCLR).

###  3.3 Label Efficient Representation Learning

Figure 3: (UPPER LEFT) Precision Recall Curve. (UPPER RIGHT) Illustrating the
label efficiency of our method by plotting the AUPRC against the percentage of
training dataset (BOTTOM LEFT, MIDDLE, RIGHT) t-SNE [13] with perplexity = 30,
learning rate = 200, iterations=1000 used to visualise the representations
learnt by various contrastive losses. The red dots denote normal class and
purple dots denote anomaly class.

We evaluated the performance of models trained with the different loss
functions by supplying 60% and 80% of training samples. We excluded SimCLR
approach because it performed very poorly on 60% and 80% of training set. We
performed a five-fold cross validation experiment with the same training
strategy. The test set is the same for all the experiments. The AUPRC of the
models are displayed in the upper right graphic of fig. 3. We observe that
models trained using $L_{sc}$ outperform the baseline by a significant margin.
Even with limited data, both the losses ( $L_{sc}$ and $L_{ours}$) show
improved performance with the injection of more training data. We also observe
that $L_{ours}$ almost achieves AUPRC of 100% training set and it is also the
most label-efficient. These results reveal that our approach can reduce
labelling effort of physicians to an extent thereby allowing them to invest
more time in the diagnosis and evaluation of difficult clinical cases.

##  4 Conclusion

Previous works on population studies [19, 16, 18, 17, 2] have relied on manual
analysis by physicians. Our work is a first step towards bringing automation
in such studies. We show the benefit of contrastive loss in the classification
of anomalies in the maxillary sinus from limited labelled dataset.
Furthermore, we report the performance improvements relative to regular cross-
entropy. Specifically, clustering based on class priors is helpful to learn
representations that overfit less on the training set. We also show that a
combinination of cross-entropy loss and supervised contrative loss improve the
performance of the model. Finally, compared to other works that use deep
learning for paranasal inflammation study [8, 10, 11], ours is the first work
that tries to achieve label efficiency and thus attempts to reduce the
workload of physicians. A limitation of our work is that the classification
accuracy is still not satisfactory. As future work, we plan to label more MRIs
and even perform classification of the type of anomaly observed in the
maxillary sinus.

## References

  * [1] Chen, T., Kornblith, S., Norouzi, M., Hinton, G.: A simple framework for contrastive learning of visual representations, https://arxiv.org/pdf/2002.05709
  * [2] Cooke, L.D., Hadley, D.M.: Mri of the paranasal sinuses: incidental abnormalities and their relationship to symptoms. The Journal of laryngology and otology 105(4), 278–281 (1991). https://doi.org/10.1017/s0022215100115609
  * [3] Efron, B., Tibshirani, R.: An introduction to the bootstrap, Monographs on statistics and applied probability, vol. 57. Chapman & Hall, Boca Raton, Fla., [nachdr.] edn. (1998)
  * [4] Falcon et al., W.: Pytorch lightning. GitHub. Note: https://github.com/PyTorchLightning/pytorch-lightning 3 (2019)
  * [5] Hansen, A.G., Helvik, A.S., Nordgård, S., Bugten, V., Stovner, L.J., Håberg, A.K., Gårseth, M., Eggesbø, H.B.: Incidental findings in mri of the paranasal sinuses in adults: a population-based study (hunt mri). BMC ear, nose, and throat disorders 14(1), 13 (2014). https://doi.org/10.1186/1472-6815-14-13
  * [6] Hara, K., Kataoka, H., Satoh, Y.: Learning spatio-temporal features with 3d residual networks for action recognition, http://arxiv.org/pdf/1708.07632v1
  * [7] Jagodzinski, A., Johansen, C., Koch-Gromus, U., Aarabi, G., Adam, G., Anders, S., Augustin, M., der Kellen, R.B., Beikler, T., Behrendt, C.A., Betz, C.S., Bokemeyer, C., Borof, K., Briken, P., Busch, C.J., Büchel, C., Brassen, S., Debus, E.S., Eggers, L., Fiehler, J., Gallinat, J., Gellißen, S., Gerloff, C., Girdauskas, E., Gosau, M., Graefen, M., Härter, M., Harth, V., Heidemann, C., Heydecke, G., Huber, T.B., Hussein, Y., Kampf, M.O., von dem Knesebeck, O., Konnopka, A., König, H.H., Kromer, R., Kubisch, C., Kühn, S., Loges, S., Löwe, B., Lund, G., Meyer, C., Nagel, L., Nienhaus, A., Pantel, K., Petersen, E., Püschel, K., Reichenspurner, H., Sauter, G., Scherer, M., Scherschel, K., Schiffner, U., Schnabel, R.B., Schulz, H., Smeets, R., Sokalskis, V., Spitzer, M.S., Terschüren, C., Thederan, I., Thoma, T., Thomalla, G., Waschki, B., Wegscheider, K., Wenzel, J.P., Wiese, S., Zyriax, B.C., Zeller, T., Blankenberg, S.: Rationale and design of the hamburg city health study. European Journal of Epidemiology 35(2), 169–181 (Feb 2020). https://doi.org/10.1007/s10654-019-00577-4, https://doi.org/10.1007/s10654-019-00577-4
  * [8] Jeon, Y., Lee, K., Sunwoo, L., Choi, D., Oh, D.Y., Lee, K.J., Kim, Y., Kim, J.W., Cho, S.J., Baik, S.H., Yoo, R.E., Bae, Y.J., Choi, B.S., Jung, C., Kim, J.H.: Deep learning for diagnosis of paranasal sinusitis using multi-view radiographs. Diagnostics (Basel, Switzerland) 11(2) (2021). https://doi.org/10.3390/diagnostics11020250
  * [9] Khosla, P., Teterwak, P., Wang, C., Sarna, A., Tian, Y., Isola, P., Maschinot, A., Liu, C., Krishnan, D.: Supervised contrastive learning, https://arxiv.org/pdf/2004.11362
  * [10] Kim, Y., Lee, K.J., Sunwoo, L., Choi, D., Nam, C.M., Cho, J., Kim, J., Bae, Y.J., Yoo, R.E., Choi, B.S., Jung, C., Kim, J.H.: Deep learning in diagnosis of maxillary sinusitis using conventional radiography. Investigative radiology 54(1), 7–15 (2019). https://doi.org/10.1097/RLI.0000000000000503
  * [11] Liu, G.S., Yang, A., Kim, D., Hojel, A., Voevodsky, D., Wang, J., Tong, C.C.L., Ungerer, H., Palmer, J.N., Kohanski, M.A., Nayak, J.V., Hwang, P.H., Adappa, N.D., Patel, Z.M.: Deep learning classification of inverted papilloma malignant transformation using 3d convolutional neural networks and magnetic resonance imaging. International forum of allergy & rhinology (2022). https://doi.org/10.1002/alr.22958
  * [12] Ma, Z., Yang, X.: Research on misdiagnosis of space occupying lesions in unilateral nasal sinus. Lin chuang er bi yan hou tou jing wai ke za zhi = Journal of clinical otorhinolaryngology, head, and neck surgery 26(2), 59–61 (2012). https://doi.org/10.13201/j.issn.1001-1781.2012.02.005
  * [13] van der Maaten, L., Hinton, G.: Visualizing data using t-sne. Journal of Machine Learning Research 9(86), 2579–2605 (2008), http://jmlr.org/papers/v9/vandermaaten08a.html
  * [14] van den Oord, A., Li, Y., Vinyals, O.: Representation learning with contrastive predictive coding. CoRR abs/1807.03748 (2018), http://arxiv.org/abs/1807.03748
  * [15] Paszke, A., Gross, S., Massa, F., Lerer, A., Bradbury, J., Chanan, G., Killeen, T., Lin, Z., Gimelshein, N., Antiga, L., Desmaison, A., Köpf, A., Yang, E., DeVito, Z., Raison, M., Tejani, A., Chilamkurthy, S., Steiner, B., Fang, L., Bai, J., Chintala, S.: Pytorch: An imperative style, high-performance deep learning library, https://arxiv.org/pdf/1912.01703
  * [16] Rak, K.M., Newell, J.D., Yakes, W.F., Damiano, M.A., Luethke, J.M.: Paranasal sinuses on mr images of the brain: significance of mucosal thickening. AJR. American journal of roentgenology 156(2), 381–384 (1991). https://doi.org/10.2214/ajr.156.2.1898819
  * [17] Rege, I.C.C., Sousa, T.O., Leles, C.R., Mendonça, E.F.: Occurrence of maxillary sinus abnormalities detected by cone beam ct in asymptomatic patients. BMC oral health 12, 30 (2012). https://doi.org/10.1186/1472-6831-12-30
  * [18] Stenner, M., Rudack, C.: Diseases of the nose and paranasal sinuses in child. GMS current topics in otorhinolaryngology, head and neck surgery 13, Doc10 (2014). https://doi.org/10.3205/cto000113
  * [19] Tarp, B., Fiirgaard, B., Christensen, T., Jensen, J.J., Black, F.T.: The prevalence and significance of incidental paranasal sinus abnormalities on mri. Rhinology 38(1), 33–38 (2000)
  * [20] den van Oord, A., Li, Y., Vinyals, O.: Representation learning with contrastive predictive coding, https://arxiv.org/pdf/1807.03748
  * [21] Wilson, R., Kuan Kok, H., Fortescue-Webb, D., Doody, O., Buckley, O., Torreggiani, W.C.: Prevalence and seasonal variation of incidental mri paranasal inflammatory changes in an asymptomatic irish population. Irish medical journal 110(9), 641 (2017)


# Word maps, polynomial maps and image ratios

Saikat Panja<EMAIL_ADDRESS>Harish-Chandra Research Institute- Main
Building, Chhatnag Rd, Jhusi, Uttar Pradesh 211019, India

###### Abstract.

If $A$ is a finite group (or a finite ring) and $\omega$ is a word map (or a
polynomial map), we define the quantity $|\omega(A)|/|A|$ as the _image ratio
of $\omega$ on $A$_ and will be denoted by $\mu(\omega,A)$. In this article,
we investigate the set $\mathrm{R}(\omega)=\\{\mu(\omega,A):A\text{ is a
finite group}\\}$, and also consider the case of rings. Specifically, we
demonstrate the existence of word maps (and polynomial maps) whose set of
image ratios is dense in $[0,1]$ for groups (and rings).

###### Key words and phrases:

word maps, polynomial maps, finite groups, finite rings

###### 2020 Mathematics Subject Classification:

20G40, 20P05, 16R10, 16S50

The author is supported by a PDF-Math fellowship from the Harish-Chandra
Research Institute

##  1\. Introduction

Let $\mathbf{C}$ be the category of finite groups or algebras. An element
$\omega$ from a finitely generated free group or free polynomial ring will be
referred to as _word_. For $A\in\mathbf{C}$, and a word $\omega$ on $n$
generators, $\omega$ induces a set-theoretic map

(1.1) $\displaystyle\widetilde{\omega}:A^{n}\longrightarrow A,$

by means of evaluation. The image will be denoted by $\omega(A)$, by abuse of
notation. In the case of groups, these are known as _word maps_ and in the
case of algebras they are known as _polynomial maps_ , however, we will stick
with the term word map throughout the article. After the settlement of Ore’s
conjecture in [11], there has been a growing interest in the direction of word
maps in groups. The study of the polynomial maps was revamped after a somewhat
positive solution in [8] to a very old conjecture by L’vov and Kaplansky in
the case of a quadratically closed field $F$ and $\mathfrak{gl}_{2}(F)$, the
full matrix ring of $2\times 2$ matrices with entries from $F$. These results
incorporate results from the theory of algebraic groups, representation theory
of groups, _etc._ to handle the problems in group theory whereas results from
algebraic geometry, arithmetic properties of polynomial equations in
associative algebras _etc._ are being used to obtain results in case of
algebras. An interesting related problem in the theory of word maps (and
polynomial maps) is a _Waring-type_ problem which asks given a group/algebra
and a group $G$. There are several results in different directions and of
different kinds. We mention a few of them; in a series of three papers [12],
[21] and [10] it was proved that for any finite nonabelian simple group $G$ of
sufficiently high order and a word $\omega$, it satisfies $\omega(G)^{2}=G$.
After [8] appeared there has been results on $3\times 3$ full matrix ring over
algebraically closed fields (see [7]), on upper-triangular matrices in [4],
[15], for matrix ring over reals or quaternions in [17] and on more general
algebras in [2], [3]. There are several generalizations of these concepts as
well, for example, word maps with constants (see [5]) or polynomial maps with
constants (see [16]). Given that the literature in this area has grown so
much, it is not possible to include all of them, hence we suggest the readers
to the articles [20] for the group theoretic aspect and [6] for the ring
theoretic aspects.

When $A$ in Eq. 1.1 is finite, it makes sense to talk about the quantity
$|\omega(A)|/|A|$. For a fixed $A$ and $\omega$, this will be referred to as
_image ratio of $\omega$ on $A$_ and to be denoted by $\mu(\omega,A)$. Clearly
this ratio satisfies $\dfrac{1}{|A|}\leq\mu(\omega,A)\leq 1$. We are
interested in studying the set

$\displaystyle\mathrm{R}_{\mathbf{C}}(\omega)=\\{\mu(\omega,A):A\in\mathbf{C}\\}.$

More precisely we are interested in the limit points of the set
$\mathrm{R}_{\mathbf{C}}(\omega)$. Note that this definition can easily be
adapted to the category where we have a notion of measure and all objects have
finite measure, for example, the category of compact groups. In this article
when considering algebras we will restrict ourselves to the category of finite
$\mathbb{F}_{q}$-algebras, where $\mathbb{F}_{q}$ is a finite field of
cardinality $q$. In Section 2 we examine a few words and their possible limit
points. Furthermore, we show that if $\mathbf{C}$ is the category of finite
groups then there exist power maps corresponding to $M\geq 2$, such that
$\overline{\mathrm{R}_{\mathbf{C}}(\omega)}=[0,1]$, see Theorem 2.2. Although
the case for finite rings will follow from this, we mention them in Section 3
separately. An analogous result to Theorem 2.2, is stated without proof in
this section, see Theorem 3.1.

##  2\. Image ratios of power maps in finite groups

Let $F_{n}$ denote the free group on $n$ generators. If
$\omega\in[F_{n},F_{n}]$ is of the form

$\displaystyle\omega=\prod\limits_{i=1}^{t}x_{m_{i}}^{s_{i}},$

then for each $x_{j}$ the total power of $x_{j}$ in $\omega$ is $0$. Hence
$\mu(\omega,\mathbb{Z}/n\mathbb{Z})=\dfrac{1}{n}$, which tends to $0$ if
$n\rightarrow\infty$. This shows that if $\omega\in[F_{n},F_{n}]$, then
$0\in\overline{\mathrm{R}(\omega)}$.

If we take $\omega\in F_{n}\setminus[F_{n},F_{n}]$ then there exist integers
$a_{1},a_{2},\ldots,a_{n}\geq 0$ and $\omega^{\prime}\in[F_{n},F_{n}]$ such
that

$\omega=x_{1}^{a_{1}}x_{2}^{a_{2}}\ldots x_{n}^{a_{n}}\omega^{\prime}.$

If $\mathrm{g.c.d.}(a_{1},a_{2}\ldots,a_{n})=a>1$ then
$\mu(\omega,(\mathbb{Z}/k\mathbb{Z})^{t})=\dfrac{1}{k^{t}}$, which proves that
in this case also $0\in\overline{\mathrm{R}(\omega)}$. We now work with a
special family of words known as Engel words. These are words of
$[F_{2},F_{2}]$, defined inductively as follows;

$\displaystyle e_{1}$ $\displaystyle=[x,y]=xyx^{-1}y^{-1},$ $\displaystyle
e_{i}$ $\displaystyle=[e_{i-1},y],\text{for all }i>1.$

It follows from [1, Theorem A] that for $i\in\mathbb{N}$ there exists
$q_{0}(i)$ such that for all prime power $q\geq q_{0}(i)$ the $i$-th Engel
word $e_{i}$ satisfies
$e_{i}(\mathrm{SL}_{2}(q))=\mathrm{SL}_{2}(q)\setminus\\{\mathrm{Id}_{2}\\}$.
Hence we get

######  Remark 2.1.

For $i\geq 1$ the $i$-th Engel word satisfies
$0,1\in\overline{\mathrm{R}(e_{i})}$.

Now we examine the power maps which are induced by elements of $F_{1}$ and
given by $\theta_{M}:G\longrightarrow G$, given by $\theta_{M}(x)=x^{M}$.
These maps are interesting in their own right; they produce one of the
examples of words $\omega$ such that a finite non-abelian simple group $G$ may
have $\omega(G)^{2}\neq G$. This is why the results of [10] are optimal. These
maps have been studied for several groups, notably in a series of papers for
several finite groups of Lie type, see [9], [18] and [19]. They have
interesting applications as well, for example, see [14], [13]. Let $p$ be a
prime. Consider the group $\mathrm{GL}_{2}(q)$, where $q=p^{r}$ for some
$r>0$. Also, assume $M$ is a positive integer such that $p|M$ and
$(q^{2}-1,M)=1$. We wish to find $\mu(x^{M},\mathrm{GL}_{2}(q))$ in this case.
It is well-known that the conjugacy classes of $\mathrm{GL}_{2}(q)$ are given
by the representatives

$\displaystyle\left\\{\begin{pmatrix}\lambda&0\\\
0&\lambda\end{pmatrix}:\lambda\in\mathbb{F}_{q}^{\times}\right\\},$
$\displaystyle\left\\{\begin{pmatrix}\lambda&0\\\
0&\mu\end{pmatrix}:\lambda,\mu\in\mathbb{F}_{q}^{\times},\lambda\neq\mu\right\\},,$
$\displaystyle\left\\{\begin{pmatrix}\lambda&1\\\
0&\lambda\end{pmatrix}:\lambda\in\mathbb{F}_{q}^{\times}\right\\},$
$\displaystyle\left\\{\begin{pmatrix}0&\beta\\\
1&-\alpha\end{pmatrix}:\begin{subarray}{c}\alpha,\beta\in\mathbb{F}_{q},\\\
t^{2}-t\alpha+\beta\text{ is }\\\ \text{irreducible in
}\mathbb{F}_{q}[t]\end{subarray}\right\\}.$

While considering the map
$\theta_{M}:\mathrm{GL}_{2}(q)\longrightarrow\mathrm{GL}_{2}(q)$ given by
$\theta_{M}(g)=g^{M}$, we get that the conjugacy class of elements of the form
$\begin{pmatrix}\lambda&1\\\ 0&\lambda\end{pmatrix}$ do not survive. Hence we
get that

$\displaystyle|\theta_{M}\left(\mathrm{GL}_{2}(q)\right)|=(q^{2}-1)(q^{2}-q)-(q-1)(q^{2}-1),$

which in turn implies that $\mu(x^{M},\mathrm{GL}_{2}(q))=1-\dfrac{1}{q}$.
Hence combined with the previous result we get that if $M$ is a power of a
prime $p$, both $1$ and $0$ are limit points of $\mathrm{R}(\theta_{M})$ in
$[0,1]$ where $\omega=x^{M}$. We claim that this is the case for any $M$,
whenever $6\nmid M$, in particular for odd $M$ or even $M$ with $3\nmid M$.

Assume $6\nmid M$ and $M=p_{1}^{t_{1}}p_{2}^{t_{2}}\ldots p_{m}^{t_{m}}$ be a
prime factorization of $M$ into distinct primes satisfying
$p_{1}<p_{2}<\ldots<p_{m}$. Then $p_{1}^{2}\not\equiv 1\pmod{p_{i}}$ for all
$2\leq i\leq m$. Let $b_{i}>1$ be the least positive integer satisfying

$\displaystyle p_{1}^{2b_{i}}\equiv 1\pmod{p_{i}},$

for all $2\leq i\leq m$. Hence $p_{i}|p_{1}^{2t}-1$ for all $2\leq i\leq m$ if
and only if $t$ is divisible by the
$b=\mathrm{l.c.m.}(b_{2},b_{3},\ldots,b_{m})>1$. This implies that there exist
infinitely many $r$, say $r_{1},r_{2},\ldots$ such that
$(p_{1}^{2r_{s}}-1,M)=1$. We use these $r_{i}$’s and note that
$\mu(x^{M},\mathrm{GL}_{2}(p_{1}^{r_{i}}))=1-\dfrac{1}{p_{1}^{r_{i}}}$ which
tends to $1$ as $i\rightarrow\infty$. Thus we have proved that if $M\geq 2$ is
an integer such that $6\nmid M$, then $0,1\in\overline{\mathrm{R}(x^{M})}$. We
prove a more general statement below;

######  Theorem 2.2.

Let $M=2^{a}$ for an integer $a\geq 1$. Then
$\overline{\mathrm{R}(x^{M})}=[0,1]$.

###### Proof.

For two finite groups $H$ and $K$ and any word map $\omega$ we have

$\mu(\omega,H\times K)=\mu(\omega,H)\times\mu(\omega,K).$

From previous discussion, we know that there are groups $H_{i}$ such that
$\mu(x^{M},H_{i})=1-\dfrac{1}{2^{i}}$. Also considering the groups
$H_{j}=(\mathbb{Z}/2M\mathbb{Z})^{j}$, the $j$-fold direct product of the
cyclic groups, for all integer $j\geq 1$ we get that
$\mu(x^{M},H_{j})=\dfrac{1}{2^{j}}$. The rest of the proof relies on the
following partitions of intervals;

$\displaystyle(0,1)=\bigcup\limits_{t\geq
0}\left[\dfrac{1}{2^{t+1}},\dfrac{1}{2^{t}}\right),\,\left[\dfrac{1}{2},1\right)=\bigcup\limits_{t\geq
1}\left[1-\dfrac{1}{2^{t}},1-\dfrac{1}{2^{t+1}}\right).$

Fix an element $c\in(0,1)$. Then there exists $m\geq 1$ such that
$\dfrac{1}{2}\leq d=2^{m}c<1$. Hence there exists $n_{1}$ such that

$\displaystyle u_{1}=1-\dfrac{1}{2^{n_{1}}}\leq
d<1-\dfrac{1}{2^{n_{1}+1}}=v_{1},$

which implies

$\displaystyle\dfrac{1}{2}\leq\dfrac{u_{1}}{v_{1}}\leq\dfrac{d}{v_{1}}<1.$

Then there exists $n_{2}$ such that
$u_{2}=1-\dfrac{1}{2^{n_{2}}}\leq\dfrac{d}{v_{1}}<1-\dfrac{1}{2^{n_{2}+1}}=v_{2}$
and so on. This process produces three sequences; (1) a sequence $\\{n_{i}\\}$
of natural numbers, (2) and two sequences $\\{u_{i}\\}$ and $\\{v_{i}\\}$ of
rationals. It can be shown that (1) the sequence $\\{n_{i}\\}$ is non-
decreasing and (2) the sequence $\\{u_{i}\\}$ is non-decreasing and has
infinitely many distinct terms. Since the sequence $\\{u_{i}\\}$ is bounded
above by $1$ it follows that it converses to $1$ and hence

$\displaystyle\lim\limits_{i\longrightarrow\infty}\dfrac{d}{v_{1}v_{2}\ldots
v_{i-1}}=1,$

and thus $\dfrac{v_{1}v_{2}\ldots v_{i-1}}{2^{m}}\longrightarrow c$ as
$i\longrightarrow\infty$. It is clear that using the groups $G_{i}$ and
$H_{j}$ each of the term

$\displaystyle\dfrac{1}{2^{m_{0}}}\left(1-\dfrac{1}{2^{m_{1}}}\right)\ldots\left(1-\dfrac{1}{2^{m_{k}}}\right)$

are achievable for $m_{j}\geq 1$ and $k\geq 0$. This finishes the proof. ∎

##  3\. Image ratios of power maps in finite rings

A similar treatment applies to polynomial maps as well and hence we keep this
section very short by just producing one map with a dense set of image ratios.
We will show that the squaring map corresponding to the polynomial
$\omega=x^{t}\in\mathbb{F}_{q}[t]$ satisfies
$\overline{\mathrm{R}(\omega)}=[0,1]$, when the category is taken to be of
finite algebras over a finite field of cardinality $2$. We work with the full
matrix ring $\mathfrak{gl}_{2}(2^{r})$. From the theory of Jordan canonical
form it follows that the conjugacy classes of this ring fall into the
following classes;

$\displaystyle\left\\{\begin{pmatrix}\lambda&0\\\
0&\lambda\end{pmatrix}:\lambda\in\mathbb{F}_{2^{r}}\right\\},$
$\displaystyle\left\\{\begin{pmatrix}\lambda&0\\\
0&\mu\end{pmatrix}:\lambda,\mu\in\mathbb{F}_{2^{r}},\lambda\neq\mu\right\\},,$
$\displaystyle\left\\{\begin{pmatrix}\lambda&1\\\
0&\lambda\end{pmatrix}:\lambda\in\mathbb{F}_{2^{r}}\right\\},$
$\displaystyle\left\\{\begin{pmatrix}0&\beta\\\
1&-\alpha\end{pmatrix}:\begin{subarray}{c}\alpha,\beta\in\mathbb{F}_{2^{r}},\\\
t^{2}-t\alpha+\beta\text{ is }\\\ \text{irreducible in
}\mathbb{F}_{2^{r}}[t]\end{subarray}\right\\}.$

Considering the squaring map on $\mathfrak{gl}_{2}(2^{r})$, we note that all
but the elements of the form $\begin{pmatrix}\lambda&1\\\
0&\lambda\end{pmatrix}$ appear in the image. Hence considering the conjugacy
class sizes, we get that

$\displaystyle\mu(x^{2},\mathfrak{gl}_{2}(2^{r}))=1-\dfrac{1}{2^{r}}.$

Since $\mu(x^{2},(\mathbb{Z}/4\mathbb{Z})^{n})=\dfrac{1}{2^{n}}$, it follows
from the arguments of Section 2 that $\overline{\mathrm{R}(\omega)}=[0,1]$ and
we tally that in the following theorem at this end.

######  Theorem 3.1.

Let $M=2^{a}$ for some integer $a\geq 2$. When considered $x^{M}$ as a
polynomial map for the category of $\mathbb{F}_{2}$-algebras, we have
$\overline{\mathrm{R}(x^{M})}=[0,1]$.

## References

  * [1] Tatiana Bandman, Shelly Garion and Fritz Grunewald  “On the surjectivity of Engel words on ${\rm PSL}(2,q)$”  In _Groups Geom. Dyn._ 6.3, 2012, pp. 409–439
  * [2] Matej Brešar  “Commutators and images of noncommutative polynomials”  In _Adv. Math._ 374, 2020, pp. 10734621
  * [3] Matej Brešar and Peter Šemrl  “The Waring problem for matrix algebras”  In _Israel J. Math._ 253.1, 2023, pp. 381–405
  * [4] Ivan Gonzales Gargate and Thiago Castilho Mello  “Images of multilinear polynomials on $n$ $\times$ $n$ upper triangular matrices over infinite fields”  In _Israel J. Math._ 252.1, 2022, pp. 337–354
  * [5] Nikolai Gordeev, Boris Kunyavskiuı and Eugene Plotkin  “Word maps, word maps with constants and representation varieties of one-relator groups”  In _J. Algebra_ 500, 2018, pp. 390–424
  * [6] Alexei Kanel-Belov, Sergey Malev, Louis Rowen and Roman Yavich  “Evaluations of noncommutative polynomials on algebras: methods and problems, and the L’vov-Kaplansky conjecture”  In _SIGMA Symmetry Integrability Geom. Methods Appl._ 16, 2020, pp. Paper No. 07161
  * [7] Alexey Kanel-Belov, Sergey Malev and Louis Rowen  “The images of multilinear polynomials evaluated on $3\times 3$ matrices”  In _Proc. Amer. Math. Soc._ 144.1, 2016, pp. 7–19
  * [8] Alexey Kanel-Belov, Sergey Malev and Louis Rowen  “The images of non-commutative polynomials evaluated on $2\times 2$ matrices”  In _Proc. Amer. Math. Soc._ 140.2, 2012, pp. 465–478
  * [9] Rijubrata Kundu and Anupam Singh  “Generating functions for the powers in GL(n, q)”  In _Israel J. Math._ 259.2, 2024, pp. 887–936
  * [10] Michael Larsen, Aner Shalev and Pham Huu Tiep  “The Waring problem for finite simple groups”  In _Ann. of Math. (2)_ 174.3, 2011, pp. 1885–1950
  * [11] Martin W. Liebeck, E.. O’Brien, Aner Shalev and Pham Huu Tiep  “The Ore conjecture”  In _J. Eur. Math. Soc. (JEMS)_ 12.4, 2010, pp. 939–1008
  * [12] Martin W. Liebeck and Aner Shalev  “Diameters of finite simple groups: sharp bounds and applications”  In _Ann. of Math. (2)_ 154.2, 2001, pp. 383–406
  * [13] Saikat Panja  “Fibers of the square map in some finite groups of Lie type and an application”, 2024  arXiv:2403.17096 [math.GR]
  * [14] Saikat Panja  “Roots of identity in finite groups of Lie type”, 2023  arXiv:2401.00202 [math.GR]
  * [15] Saikat Panja and Sachchidanand Prasad  “The image of polynomials and Waring type problems on upper triangular matrix algebras”  In _J. Algebra_ 631, 2023, pp. 148–193
  * [16] Saikat Panja, Prachi Saini and Anupam Singh  “Images of polynomial maps with constants”, 2023  arXiv:2312.13865 [math.GR]
  * [17] Saikat Panja, Prachi Saini and Anupam Singh  “Surjectivity of polynomial maps on Matrices”, 2024  arXiv:2305.19731 [math.GR]
  * [18] Saikat Panja and Anupam Singh  “Powers in finite orthogonal and symplectic groups: A generating function approach”, 2022  arXiv:2202.11513 [math.GR]
  * [19] Saikat Panja and Anupam Singh  “Powers in finite unitary groups”, 2023  arXiv:2304.13735 [math.GR]
  * [20] Aner Shalev  “Some results and problems in the theory of word maps”  In _Erdös centennial_ 25, Bolyai Soc. Math. Stud.  János Bolyai Math. Soc., Budapest, 2013, pp. 611–649
  * [21] Aner Shalev  “Word maps, conjugacy classes, and a noncommutative Waring-type theorem”  In _Ann. of Math. (2)_ 170.3, 2009, pp. 1383–1416


# STV+AGR: Towards Practical Verification of Strategic Ability Using Assume-
Guarantee Reasoning

Damian Kurpiewski  Institute of Computer Science, Polish Academy of Sciences,
Warsaw, Poland  Faculty of Mathematics and Computer Science, Nicolaus
Copernicus University, Toruń, Poland  Łukasz Mikulski  Faculty of Mathematics
and Computer Science, Nicolaus Copernicus University, Toruń, Poland  Institute
of Computer Science, Polish Academy of Sciences, Warsaw, Poland  Wojciech
Jamroga  Institute of Computer Science, Polish Academy of Sciences, Warsaw,
Poland  Interdisciplinary Centre for Security, Reliability and Trust, SnT,
University of Luxembourg, Luxembourg

###### Abstract

We present a substantially expanded version of our tool STV for strategy
synthesis and verification of strategic abilities. The new version provides a
web interface and support for assume-guarantee verification of multi-agent
systems.

##  1 Introduction

Model checking of multi-agent systems (MAS) allows for formal (and, ideally,
automated) verification of their relevant properties. Algorithms and tools for
model checking of _strategic abilities_ [1, 28, 9, 25] have been in
development for over 20 years [2, 10, 6, 13, 7, 21, 8, 4, 3, 15, 20].
Unfortunately, the problem is hard, especially in the realistic case of agents
with imperfect information [28, 5, 12].

In this paper, we propose a new extension of our experimental tool STV [19,
20] that facilitates compositional model checking of strategic properties in
asynchronous MAS through assume-guarantee reasoning (AGR) [26, 11]. The
extension is based on the preliminary results in [24], itself an adaptation of
the AGR framework for liveness specifications from [22, 23].

##  2 Application Domain

Many important properties of MAS refer to _strategic abilities_ of agents and
teams. For example, the $\mathbf{ATL_{\mathrm{}}^{*}}$ formula
$\langle\\!\langle{taxi}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathrm{G}\neg\mathsf{{fatality}}$
says that the autonomous cab can drive in such a way that no one gets ever
killed, and
$\langle\\!\langle{taxi,passg}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathrm{F}\,\mathsf{{destination}}$
expresses that the cab and the passenger have a joint strategy to arrive at
the destination, no matter what the other agents do. Another intuitive set of
strategic requirements is provided by properties of secure voting systems [27,
29]. As shown by case studies [16, 14, 18] practical verification of such
properties is still infeasible due to state-space and strategy-space
explosion. STV+AGR addresses the specification and verification of such
properties, as well as a user-friendly creation of models to be verified.

##  3 Simple Voting Scenario

$?,?$start$T,?$$F,?$$?,T$$?,F$$F,T$$T,F$$T,T$$F,F$$?\times?$$\forall\times\lnot?$$\forall\times\lnot?$$\lnot?\times\forall$$\lnot?\times\forall$$\forall\times?$$?\times\forall$$\forall\times?$$?\times\forall$$\forall\times\lnot?$$\forall\times\lnot?$$\forall\times\lnot?$$\forall\times\lnot?$$\lnot?\times\forall$$\lnot?\times\forall$$\lnot?\times\forall$$\lnot?\times\forall$$\forall\times\forall$$\forall\times\forall$$\forall\times\forall$$\forall\times\forall$
---

$?,?,?$start$1,?,?$$2,?,?$$1,1,?$$1,!,?$$2,!,?$$2,2,?$$1,1,T$$1,1,F$$1,!,F$$1,!,T$$2,!,T$$2,!,F$$2,2,F$$2,2,T$$\forall$$\forall$$\forall$$\forall$$\forall$$\forall$$T$$F$$F$$T$$T$$F$$F$$T$$?$$?$$?$$?$$\forall$$\forall$$\forall$$\forall$$\forall$$\forall$$\forall$$\forall$
---

Figure 1: Two modules: a coercer[2] (up) and a voter (down)

To present the capabilities of STV+AGR, we designed an asynchronous version of
the Simple Voting scenario [15]. The model consists of two types of agents,
presented in Figure 1, and described below.

Voter. Every voter agent has three local variables:

  * •

$vote_{i}$: the vote being cast ($?,1$, or $2$);

  * •

$reported_{i}$: the vote value presented to the coercer ($?,1,2$ or $!$),
where $!$ means that the voter decided not to share her vote with the coercer;

  * •

$pstatus_{i}$: the punishment status ($?,T$ or $F$).

Each voter $i$ can also see the value of the $pun_{i}$ variable of the
coercer.

The voter first casts her vote, then decides whether to share its value with
the coercer. Finally, she waits for the coercer’s decision to punish her or to
refrain from punishment.

Coercer. The coercer[k] has one local variable for each of $k$ voters:

  * •

$pun_{i}$: whether the voter $i$ was punished or not ($?,T$ or $F$).

Moreover, he can observe the value of $reported_{i}$ for each voter $i$.

The coercer has two available actions per voter: to punish the voter or to
refrain from punishment.

##  4 Formal Background

Modules. The main part of the input is given by a set of asynchronous modules
inspired by [23], where local states are labelled with valuations of state
variables. The transitions are valuations of input variables controlled by the
other modules. The multi-agent system is defined by a composition of its
modules.

Strategies. A strategy is a conditional plan that specifies what the agent(s)
are going to do in every possible situation. Here, we consider the case of
_imperfect information memoryless strategies_ , represented by functions from
the agent’s local states (or, equivalently, its epistemic indistinguishability
classes) to its available actions. The _outcome_ of a strategy from state $q$
consists of all the infinite paths starting from $q$ and consistent with the
strategy.

Logic. Given a model $M$ and a state $q$ in the model, the
$\mathbf{1\\!ATL_{-X}^{*}}$ [17] formula
$\langle\\!\langle{a}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\varphi$ holds in
the pointed model $(M,q)$ iff there exists a strategy for agent $a$ that makes
$\varphi$ true on all the outcome paths starting from any state
indistinguishable from $q$. The semantics of coalitional abilities is
analogous, for joint strategies of coalitions.

Assume-guarantee reasoning. The main idea is to cope with the state-space
explosion by decomposing the goal $\varphi$ of coalition $C$ into local goals
$\varphi_{i},i\in C$, and verify them one by one against abstractions of each
agent’s environment. An abstraction for $i$ is obtained by defining a single
module, called the _assumption_ , which _guarantees_ that all the paths
present in the original system have their counterparts in the composition of
module $i$ and its associated assumption. Moreover, we use a distance between
modules, based on shared synchronization actions, so that only “close” agents
are taken into account when preparing the assumption for $i$. This way, one
can deduce the existence of a joint strategy to obtain $\varphi$ from the
existence of individual strategies that achieve local goals $\varphi_{i}$.

Automated generation of assumptions. The main difficulty in using assume-
guarantee reasoning is how to define the right assumptions for the relevant
modules. To this end, we propose an automated procedure that generates the
assumptions, based on the subset of modules that are “close” the given module
$M_{i}$. The abstraction is obtained by composing all the “close” modules,
abstracting away their state labels and variables except for the ones that are
input to $M_{i}$, as well as removing all their input variables which are not
state variables of $M_{i}$.

##  5 Technology

STV+AGR does _explicit-state model checking_. That is, the global states and
transitions of the model are represented explicitly in the memory of the
verification process. The tool includes the following new functionalities.

User-defined input. The user can load and parse the input specification from a
text file that defines the groups of modules. The modules are local automata
representing the agents. The groups define the partition for the assume-
guarantee verification. Each group that describes the part of the coalition
must also define the formula to be verified.

Web-based graphical interface. The generated models and the verification
results are visualised in the intuitive web-based graphical interface. The GUI
is implemented in Typescript and uses the Angular framework.

V Monolithic model checking Assume-guarantee verification #st #tr DFS Apprx
#st #tr DFS Apprx 2 529 2216 <0.1 <0.1/Yes 161 528 <0.1 <0.1/Yes 3 12167
127558 <0.1 0.8/Yes 1127 7830 <0.1 <0.1/Yes 4 2.79e5 6.73e6 memout 7889 1.08e5
<0.1 0.8/Yes 5 memout 5.52e4 1.45e6 <0.1 11/Yes

Table 1: Results of assume-guarantee verification the asynchronous variant of
Simple Voting (times given in seconds)

Evaluation. The assumption-guarantee scheme has been evaluated on the
asynchronous variant of Simple Voting, using formula
$\varphi\equiv\langle\\!\langle{\mathit{Voter}_{1}}\rangle\\!\rangle_{{}_{\\!\mathit{}}}\mathrm{G}(\lnot\mathsf{{pstatus_{1}}}\lor\mathsf{{voted_{1}}}=1)$.
Note that the coalition consisted of only one agent, which made the
decomposition of the formula trivial. The results are presented in Table 1.
The first column describes the configuration of the benchmark, i.e., the
number of voters. Then, we report the performance of model checking algorithms
that operate on the explicit model of the whole system vs. assume-guarantee
verification. _DFS_ is a straightforward implementation of depth-first
strategy synthesis. _Apprx_ refers to the method of fixpoint-approximation
[15]; besides the time, we also report if the approximation was conclusive.

##  6 Usage

The tool is available at stv.cs-htiew.com. The video demonstration of the tool
is available at youtu.be/1DrmSRK1fBA. Example specifications can be found at
stv-docs.cs-htiew.com. The current version of STV+AGR allows to:

  * •

Generate and display the composition of a set of modules into the model of a
multi-agent system;

  * •

Generate and display the automatic assumption, given a module and a distance
bound;

  * •

Provide local specifications for modules, and compute the global specification
as their conjunction;

  * •

Verify a $\mathbf{1\\!ATL_{-X}^{*}}$ formula for a given system (using the
verification methods available in the STV package);

  * •

Verify a $\mathbf{1\\!ATL_{-X}^{*}}$ formula for a composition of a module and
its automatic assumption (using the methods in STV);

  * •

Verify a $\mathbf{1\\!ATL_{-X}^{*}}$ formula for a composition of a module and
a user-defined assumption (using the methods in STV);

  * •

Display the verification result, including the relevant truth values and the
winning strategy (if one exists).

##  7 Conclusions

Much complexity of model checking for strategic abilities is due to the size
of the model. STV+AGR addresses the challenge by implementing a compositional
model checking scheme, called assume-guarantee verification. No less
importantly, our tool supports user-friendly modelling of MAS, and automated
generation of abstractions that are used as assumptions in the scheme.

## Acknowledgement

The authors thank Witold Pazderski and Yan Kim for assistance with the web
interface. The work was supported by NCBR Poland and FNR Luxembourg under the
PolLux/FNR-CORE project STV (POLLUX-VII/1/2019), as well as the CHIST-ERA
grant CHIST-ERA-19-XAI-010 by NCN Poland (2020/02/Y/ST6/00064).

## References

  * [1] R. Alur, T.A. Henzinger, and O. Kupferman.  Alternating-time Temporal Logic.  J. of the ACM, 49:672–713, 2002.
  * [2] R. Alur, T.A. Henzinger, F.Y.C. Mang, S. Qadeer, S. Rajamani, and S. Tasiran.  MOCHA: Modularity in model checking.  In Proc. of CAV’98, volume 1427 of LNCS, pages 521–525. Springer, 1998.
  * [3] F. Belardinelli, A. Lomuscio, A. Murano, and S. Rubin.  Verification of broadcasting multi-agent systems against an epistemic strategy logic.  In Proc. of IJCAI’17, pages 91–97, 2017.
  * [4] F. Belardinelli, A. Lomuscio, A. Murano, and S. Rubin.  Verification of multi-agent systems with imperfect information and public actions.  In Proc. of AAMAS’17, pages 1268–1276, 2017.
  * [5] N. Bulling, J. Dix, and W. Jamroga.  Model checking logics of strategic ability: Complexity.  In Specification and Verification of Multi-Agent Systems, pages 125–159. Springer, 2010.
  * [6] S. Busard, C. Pecheur, H. Qu, and F. Raimondi.  Improving the model checking of strategies under partial observability and fairness constraints.  In Formal Methods and Software Engineering, volume 8829 of LNCS, pages 27–42. Springer, 2014.
  * [7] P. Cermák, A. Lomuscio, F. Mogavero, and A. Murano.  MCMAS-SLK: A model checker for the verification of strategy logic specifications.  In Proc. of CAV’14, volume 8559 of LNCS, pages 525–532. Springer, 2014.
  * [8] P. Cermák, A. Lomuscio, and A. Murano.  Verifying and synthesising multi-agent systems against one-goal strategy logic specifications.  In Proc. of AAAI’15, pages 2038–2044, 2015.
  * [9] K. Chatterjee, T.A. Henzinger, and N. Piterman.  Strategy Logic.  Inf. and Comp., 208(6):677–693, 2010.
  * [10] T. Chen, V. Forejt, M. Kwiatkowska, D. Parker, and A. Simaitis.  PRISM-games: A model checker for stochastic multi-player games.  In Proc. of TACAS’13, volume 7795 of LNCS, pages 185–191. Springer, 2013.
  * [11] E.M. Clarke, D.E. Long, and K.L. McMillan.  Compositional model checking.  In Proc. of LICS’89, pages 353–362. IEEE Comput. Soc. Press, 1989.
  * [12] C. Dima and F.L. Tiplea.  Model-checking ATL under imperfect information and perfect recall semantics is undecidable.  CoRR, abs/1102.4225, 2011.
  * [13] X. Huang and R. van der Meyden.  Symbolic model checking epistemic strategy logic.  In Proc. of AAAI’14, pages 1426–1432, 2014.
  * [14] W. Jamroga, Y. Kim, D. Kurpiewski, and P.Y.A. Ryan.  Towards model checking of voting protocols in uppaal.  In Proc. of E-Vote-ID’20, volume 12455 of LNCS, pages 129–146. Springer, 2020.
  * [15] W. Jamroga, . Knapik, D. Kurpiewski, and Ł. Mikulski.  Approximate verification of strategic abilities under imperfect information.  Artif. Int., 277, 2019.
  * [16] W. Jamroga, M. Knapik, and D. Kurpiewski.  Model checking the SELENE e-voting protocol in multi-agent logics.  In Proc. of E-Vote-ID’18, volume 11143 of LNCS, pages 100–116. Springer, 2018.
  * [17] W. Jamroga, W. Penczek, T. Sidoruk, P. Dembinski, and A.W. Mazurkiewicz.  Towards partial order reductions for strategic ability.  J. Artif. Intell. Res., 68:817–850, 2020.
  * [18] Wojciech Jamroga, Damian Kurpiewski, and Vadim Malvone.  Natural strategic abilities in voting protocols.  In Proc. of STAST’20, 2021.  To appear.
  * [19] D. Kurpiewski, W. Jamroga, and M. Knapik.  STV: Model checking for strategies under imperfect information.  In Proceedings of the 18th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2019, pages 2372–2374. IFAAMAS, 2019.
  * [20] D. Kurpiewski, W. Pazderski, W. Jamroga, and Y. Kim.  STV+Reductions: Towards practical verification of strategic ability using model reductions.  In Proc. of AAMAS’21, pages 1770–1772. ACM, 2021.
  * [21] A. Lomuscio, H. Qu, and F. Raimondi.  MCMAS: An open-source model checker for the verification of multi-agent systems.  Int. J. Soft. Tools Tech. Trans., 19(1):9–30, 2017.
  * [22] A. Lomuscio, B. Strulo, N.G. Walker, and P. Wu.  Assume-guarantee reasoning with local specifications.  In Proc. of ICFEM’10, volume 6447 of LNCS, pages 204–219. Springer, 2010.
  * [23] A. Lomuscio, B. Strulo, N.G. Walker, and P. Wu.  Assume-guarantee reasoning with local specifications.  Int. J. Found. Comput. Sci., 24(4):419–444, 2013.
  * [24] Ł. Mikulski, W. Jamroga, and D. Kurpiewski.  Towards assume-guarantee verification of strategic ability.  In Proc. of AAMAS’22.  to appear.
  * [25] F. Mogavero, A. Murano, G. Perelli, and M.Y. Vardi.  Reasoning about strategies: On the model-checking problem.  ACM Trans. Comp. Log., 15(4):1–42, 2014.
  * [26] A. Pnueli.  In transition from global to modular temporal reasoning about programs.  In Logics and Models of Concurrent Systems, volume 13 of NATO ASI Series, pages 123–144. Springer, 1984.
  * [27] P.Y.A. Ryan.  The computer ate my vote.  In Formal Methods: State of the Art and New Directions, pages 147–184. Springer, 2010.
  * [28] P.Y. Schobbens.  Alternating-time logic with imperfect recall.  Electr. Not. Theor. Comput. Sci., 85(2):82–93, 2004.
  * [29] M. Tabatabaei, W. Jamroga, and Peter Y. A. Ryan.  Expressing receipt-freeness and coercion-resistance in logics of strategic ability: Preliminary attempt.  In Proc. of PrAISe@ECAI’16, pages 1:1–1:8. ACM, 2016.