# Towards Complex-query Referring Image Segmentation: A Novel Benchmark

Wei Ji Li Li Hao Fei Xiangyan Liu Xun Yang Juncheng Li Roger Zimmermann
National University of Singapore

###### Abstract

Referring Image Understanding (RIS) has been extensively studied over the past
decade, leading to the development of advanced algorithms. However, there has
been a lack of research investigating how existing algorithms should be
benchmarked with complex language queries, which include more informative
descriptions of surrounding objects and backgrounds (e.g., "the black car."
vs. "the black car is parking on the road and beside the bus."). Given the
significant improvement in the semantic understanding capability of large pre-
trained models, it is crucial to take a step further in RIS by incorporating
complex language that resembles real-world applications. To close this gap,
building upon the existing RefCOCO and Visual Genome datasets, we propose a
new RIS benchmark with complex queries, namely RIS-CQ. The RIS-CQ dataset is
of high quality and large scale, which challenges the existing RIS with
enriched, specific and informative queries, and enables a more realistic
scenario of RIS research. Besides, we present a nichetargeting method to
better task the RIS-CQ, called dual-modality graph alignment model (DuMoGa),
which outperforms a series of RIS methods.

##  1 Introduction

Correctly comprehending the subtle alignment (i.e., grounding) between
language and vision has long been the pivotal research in the intersecting
communities of computer vision and language processing [29, 28, 33]. Among a
range of vision-language grounding topics, Referring Image Segmentation (RIS)
has been proposed with the aim to ground a given language query onto a
specific region of an image, i.e., typically represented by a segmentation
map, as exemplified in Figure 1. By precisely bridging the semantics between
the images and texts, RIS plays a crucial role in various downstream cross-
modal applications, including image editing [2, 12], and language-based human-
robot interaction[25, 32].

Figure 1:  The comparison between the existing Referring Image Segmentation
(RIS) and the complex-query RIS proposed in this work.

Although attracting increasing research attention, the existing RIS
benchmarks, unfortunately, can be subject to the simplicity and naivety of the
language queries. Specifically, via data statistics of the current popular RIS
datasets, including RefCOCO and RefCOCO+ [30, 20], we find that _i)_ 85.3%
text queries have short forms (i.e., with length $\leq$ 5 words), and _ii)_
83.8% queries involve only one or two visual objects. We note that such
characteristics would inevitably lead to the key pitfalls that hamper the
utility and applicability of RIS task.

  * •

On the one hand, caused by the inequality between vision and language, i.e.,
language is abstract and succinct while vision always entails richer details,
simple short language queries with shallow object descriptions usually trigger
ambiguity for the visual coreference. The sample in Figure 1 shows the case.
More severely, in the existing RIS datasets, a significant majority of query
sentences suffer from such ambiguity. Intuitively, RIS models, being trained
on such overly simplistic data, would largely fail to disambiguate the image
referring and lead to suboptimal performance.

  * •

On the other hand, in real-world applications, individuals are more likely to
input detailed textual descriptions in complex forms, so as to accurately
locate the desired objects. Although the recent RIS methods [27, 31, 5]
achieve satisfactory performance on the in-house testing set, they can still
struggle when confronted with complex and informative queries. Our preliminary
experiment indicates that even the current top-performing RIS model, LAVT[27],
drops dramatically (74.46 vs. 10.84 in mIoU on two RIS datasets) when testing
on the complex query. In other words, being trained on existing RIS datasets
can lead to the failure of generalizing to the input queries from realistic
users in the wild.

The above observations imperatively motivate the exploration of _Referring
Image Segmentation with Complex Queries (RIS-CQ)_. In this work, we propose a
novel benchmark for RIS under such complex scenario. Specifically, we
construct a RIS-CQ dataset (cf. §2), which is of high quality and large scale.
Technically, we first extract the salient objects with their pertaining
relations (spatial, action, _etc._) from an image, and then generate
semantically detailed and meaningful descriptions for the referring objects
towards their surrounding objects, which serve as the complex-form queries.
Notedly, the recent large language models (LLMs), e.g., ChatGPT [19] have
revealed the great capability of human-level understanding of language
semantics. Thus we take advantage of the LLM to assist to generate large
amounts of complex queries while without sacrificing the labeling quality.
Finally, we obtain a novel RIS-CQ dataset with 118,287 images and 13.18 words
on average for each query.

The key to accurate RIS recognition in our scenario essentially lies in the
deep understanding of the underlying semantics of different modalities,
because of the intrinsic complex form of textual query and the sophisticated
visual content. To this end, we propose a novel dual-modality graph alignment
(dubbed DuMoGa) model (cf. §3) to benchmark the RIS-CQ task, where the input
sentence and image are represented with the semantic dependency graph [22] and
semantic scene graph [23], respectively. Meanwhile, the semantics of the two
modalities should be sufficiently interacted for deep comprehension of the
inputs. Correspondingly, two levels of cross-modal alignment learning are
carried out in DuMoGa to capture the intrinsic correspondence between the
input text and vision, including the structural alignment between two semantic
graphs and the feature alignment between two semantic representations. On the
RIS-CQ datasets our DuMoGa achieves 24.4 in mIoU, outperforming the current
state-of-the-art (SoTA) RIS method by more than 200%.

To sum up, this work contributes to the following three aspects. (1) We
construct a novel benchmark dataset, RIS-CQ, which challenges the existing RIS
with complex queries, and enables a more realistic scenario of RIS research.
(2) We present a strong-performing system (DuMoGa) to model the task, which
brings a new SoTA results on the RIS-CQ dataset. (3) Series of in-depth
analyses are shown based on our dataset and the systems, where some important
and interesting findings are presented and concluded to shed light on the
future exploration of this topic. All our data and resource will be made open
later to facilitate the follow-up research.

##  2 Constructing Complex Query for Referring Image Segmentation

###  2.1 Problem Definition

Given an image $\mathcal{I}$ and a set of textual queries (i.e., long-form
sentences with semantically complex expressions)
$\mathcal{Q}=\\{\mathbf{p}_{i}\\}_{i=1}^{M}$, RIS-CQ aims to predict a set of
segmentation masks $\mathcal{S}=\\{\mathbf{s}_{i}\\}_{i=1}^{M}$, where each
$\mathbf{s}_{i}$ correspond to each query $\mathbf{p}_{i}$ that localizes it
in the image. Note that $M$ is the number of referring expressions for a given
image $\mathcal{I}$, which is set as $M\in[1,10]$.

###  2.2 Dataset Construction

In this section, we elaborate on how to elicit complex and contextualized
queries from large language models (i.e., ChatGPT) by leveraging diverse
structured semantics in images (e.g., inter-object relations). First, we
extract holistic semantic relations for each image and then select more
significant objects that involve diverse interactions with other objects as
the candidate objects. Second, we utilize specially tailored prompts to guide
ChatGPT in generating complex queries for each candidate object based on rich
visual context. Finally, we manually filter out or revise problematic queries
(e.g., ambiguous references), to ensure the annotation quality.

#### Step-1: Relation extraction.

To begin with, we utilize an off-the-shelf scene graph generation model, VC-
Tree, to directly extract the objects present in the images along with their
relationships. These relationships are stored in the form of triplets, such as
<person, cup, holding>, which indicates that the person is holding the cup.
Additionally, during this step, we apply a simple filter to exclude objects
that have fewer than two relationships with other objects. We believe that
generating queries to describe these objects would be relatively
straightforward, increasing the probability of ambiguous references or
incorrect references.

#### Step-2: Complex query generation.

In this section, we devise a tailored set of prompts to efficiently leverage
the in-context learning capabilities of a large language model. For each
object and its corresponding relation triplets, we generate a descriptive text
query using the model. For instance, given a set of triplets associated with
the target object person, <person, cup, holding>, <person, wall, leaning on>,
<table, person, next to>, ChatGPT can provide us with the output "the person
is next to the table, holding the cup and leaning on the wall."

Specifically, we utilize the gpt-3.5-turbo model as our large language model,
with the API interface provided by OpenAI. To ensure stable outputs from the
model, we set the decoding temperature to 0. The relevant prompts used are
detailed in the appendix for reference. An additional noteworthy aspect is
that the presence of the large language model entirely liberates us from the
manual labor of annotating images for generating language queries. This
significantly reduces our workforce costs while ensuring the quality of
queries. Moreover, it facilitates the expansion of our dataset to the
magnitude of 100k.

Figure 2: Failure cases of Complex-query Referring Image Segmentation.

#### Step-3: Post-processing.

Finally, we manually filter out or revise queries with ambiguous references to
ensure a precise one-to-one correspondence between the queries and objects
within the image. After multiple iterations in constructing prompts, we have
successfully developed prompts that yield high-quality queries generated by
ChatGPT. However, it is important to note that since ChatGPT receives input
solely from the relation triplets generated by the scene graph model, it lacks
certain contextual information from the image. As a result, there may be
instances where the generated queries exhibit ambiguous references to the
objects being described. Unfortunately, these queries cannot be filtered out
automatically in our automated pipeline, necessitating manual intervention for
their removal.

###  2.3 Dataset Statistics

Figure 3 presents the statistical analysis of objects and predicates in the
RIS-CQ dataset, which consists of a total of 133 object classes and 56
relation classes. The language queries generated are solely based on the
objects depicted in Figure 3 along with their corresponding relations. The
objects and relations are categorized into 9 groups and 6 groups respectively,
with each group containing elements that exhibit certain correlations. The
group names represent abstract summaries of the shared attributes among the
elements within each group.

We analyze the failure cases of current models on RIS-CQ dataset. From Figure
2, we can summarize them into three types: misidentified referent, incorrect
object classification, and failure segmentation.

Figure 3: The distribution of object and relation categories, organized based
on the parent classes. Best viewed by zooming in.

###  2.4 Dataset Comparison

RefCOCO/ RefCOCO+/ RefCOCOg. RefCOCO [30], RefCOCO+ [30], and RefCOCOg [20]
are three visual grounding datasets with images and referred objects selected
from MS COCO [15]. The referred objects are selected from the MS COCO object
detection annotations and belong to 80 object classes. RefCOCO [30] has 19,994
images with 142,210 referring expressions for 50,000 object instances.
RefCOCO+ has 19,992 images with 141,564 referring expressions for 49,856
object instances. RefCOCOg has 25,799 images with 95,010 referring expressions
for 49,822 object instances.

#### Visual Genome.

Visual Genome (VG v1.4) [11] contains $108,077$ images with $21$ relationships
on average per image, which is split into $103,077$ training images and
$5,000$ testing images.

Table 1: Statistics of current Referring Image Understanding benchmarks. Dataset | RefCOCO | RefCOCO+ | RefCOCOg | Visual Genome | RIS-CQ
---|---|---|---|---|---
# Images | 19,994 | 19,992 | 26,711 | 108,077 | 118,287
# Text query | 142,209 | 141,564 | 85,474 | 5.4M | 285,781
Avg. query length | 3.61 | 3.53 | 8.43 | 5 | 13.18
Avg. object / query | 1.76 | 1.67 | 3.03 | - | 3.58
Annotation methods | Manual | Manual | Manual | Manual | Auto + Manual

#### RIS-CQ.

is our proposed referring image segmentation benchmark, which targets the
explanation of image contents. The image source for RIS-CQ is the union of VG
[11] and COCO [15] datasets. RIS-CQ challenges RIS models to understand the
rich object interactions in daily activities. As shown in Table 1, we
summarize the details of each dataset compared with our RIS-CQ dataset.

##  3 Proposed Method

Figure 4:  Our proposed DuMoGa framework, includes three procedures: Dual-
modality Graph Representation, Dual-modality Graph Alignment, and Prediction.
Best viewed by zooming in.

Unlike classic dense prediction models with complex design in RIS (e.g. LAVT
[27]), which take expensive computational power to make inferences, the graph
learning based architecture provides efficient training process and promising
results. To address the numerous descriptions of surrounding objects and
backgrounds within images, images are parsed into scene graphs, which are
treated as fine-grained image representations to analyze the relations of
these objects with a graph structure. On the other hand, following previous
dependency-based RE methods [6], we parse the queries into syntax dependency
trees, which can provide information for dual-modality graph alignment. As a
result, we propose a graph learning-based method named DuMoGa to align the
semantics in queries and the information in images, aiming at efficiently
locating the target instances. The whole structure of our proposed DuMoGa is
shown in Fig 4.

###  3.1 Dual-Modality Graph Representation

Semantic Scene Graph Generation for Vision. We employ a classic SGG model
(e.g. VCTree [23, 13]) to parse images into scene graphs. The whole process
can be formulated as:

$P_{r}\left(\mathcal{G}\ |\
\mathcal{I}\right)=P_{r}\left(\mathcal{S},\mathcal{O},\mathcal{R}\ |\
\mathcal{I}\right).$ (1)

An image $\mathcal{I}$ can be segmented into a set of masks $\mathcal{S}$.
Each mask is associated with an object with class label $\mathcal{O}$. A set
of relations $\mathcal{R}$ between objects are predicted. We construct the
node set $N_{i}=\left\\{O_{j}|j\in\left[1,n\right]\right\\}$ of the scene
graph, $O_{i}$ is the $i_{th}$ object detected in the image. $n$ represents
the number of detected object, and we set the maximum number of detected
object for each image to N. For the edge set
$E_{i}=\left\\{R_{a,b}=\left(I_{a},I_{b}\right)|a\in\left[1,n\right],b\in\left[0,n-1\right]\right\\}$,
$R_{a,b}$ denotes the $a_{th}$ object related with the $b_{th}$ object. As a
result, the scene graph can be formulated as follows:

$G_{i}=\left(N_{i},E_{i}\right).$ (2)

Syntax Dependency Graph for Text. We use the syntax dependency tree to explore
the dependency between words in the sentence. Following [22], we use ELMo to
obtain the dependency tree for the input text after which each word from the
text is connected by its governor and obtains its related dependency triple.
For the node set $N_{t}=\left\\{T_{j}|j\in\left[1,l\right]\right\\}$ of the
dependency tree, $T_{j}$ denotes the $j_{th}$ token in the sentence, and $l$
represents the total length of the sentence. For the edge set
$E_{t}=\left\\{G_{a,b}=\left(T_{a}^{*},T_{a}\right)|a\in\left[1,l\right]\right\\}$,$T_{a}^{*}$
denotes the governor of the $a_{th}$ token, and the graph representation for
the sentence can be formulated as follows:

$G_{t}=\left(N_{t},E_{t}\right).$ (3)

###  3.2 Dual-modality Alignment

To accurately locate the target instance using the query sentence, the gap
between visual and semantics needs to be bridged. Thus, we propose the graph
and feature alignment process to efficiently align visual and language
domains.

Graph Alignment. We approximate the node embedding matrix $\widetilde{P}$ by
factorizing a similarity matrix of the node identities, and align nodes
between the above two graphs by greedily matching the most similar embeddings
from the other graph.

Following [35], we combine $N_{i}$ and $N_{t}$, and count both in and out
degrees of k-top neighbors for each node. Then we compute the similarity
between every two nodes, getting a $n\times n$ similarity matrix
$\widetilde{P}$. After that we subsets $P_{1}$ and $P_{2}$ from
$\widetilde{P}$. The $P_{1}$ and $P_{2}$ denote separate representations for
nodes in $G_{i}$ and $G_{t}$.

${\widetilde{P}}_{1},{\widetilde{P}}_{2}=D\left(N\left(\widetilde{P}\right)\right),$
(4)

where $D$ denotes the dividing operation of $P$ by the number of nodes in
$N_{i}$ and $N_{t}$ in order, and $N$ is normalization operation. When
finishing graph structure alignment, we calculate the similarity between node
i from ${\widetilde{P}}_{1}$ and node j from ${\widetilde{P}}_{2}$ using the
formula below:

$a_{ij}=exp(-\left\|{\widetilde{P}}_{1}[i]-{\widetilde{P}}_{2}[j]\right\|_{2}^{2}).$
(5)

With the similarities between nodes, the two graphs are transformed into a
similarity map $\alpha$, which can be formulated as:

$\alpha=\left(a_{ij}\right)_{|V_{1}|\times|V_{2}|},$ (6)

where $a_{ij}$ represents the structural similarity between the $i_{th}$ word
of the input text and the $j_{th}$ object of the input image.

Feature Alignment. Though graph structure is efficient, the information within
is not enough for the task. We take the advantage of visual features from
images and word embeddings from sentences to promise a fine-grained searching
space. Specifically, for each image $I$, we get its visual feature $F_{i}$
from backbone model (e.g. ResNet-50 [7]). For each sentence $Q$, we get its
semantic embedding $F_{l}$ using BERT [3]. We treat $F_{i}$ as the query while
$F_{l}$ is treated as the key and value, completing the attention process
below:

$R^{a}=\text{Softmax}\left(\frac{qk^{T}}{\sqrt{d}}\right)v,$ (7)

where d denotes the dimension of $F_{l}$.

Feature Fusion and Prediction. After obtaining the results from graph
alignment and feature alignment processes, we fuse them to make the final
prediction.

$R^{f}=MLP\left([R^{a};\alpha F_{l}]\right),\quad
s=j^{*}=\mathop{\mathrm{Argmax}}_{1\leq j\leq
N}(R^{f}_{1},...R^{f}_{j},...,R_{N}^{f})\,,$ (8)

Where $[;]$ denotes concatenation, and we use the MLPs to project the feature
to N dimension. $s$ denotes the output of the referring objects from the input
with the largest probability.

###  3.3 Training Loss

For the N detected objects in the image, we match their masks with the ground
truth mask and obtain the $g_{th}$ object that share the most intersection
over union with the ground truth. To maximize the probability on the $g_{th}$
dimension of $R^{f}$, we employ a cross-entropy loss function below:

$L={\textstyle\sum_{i=1}^{N}}[-K^{i}log(R_{i}^{f})-(1-K^{i})log(1-R_{i}^{f})].$
(9)

K represents a one-hot vector with all zeros except for the $g_{th}$
dimension, and $K^{i}$ denotes the $i_{th}$ dimension of K. As a result, the
probability on the $g_{th}$ dimension of $R^{f}$ is maximized.

##  4 Experiment

###  4.1 Experimental Settings

We employ a VCTree [23] with ResNet-50 [7] as its backbone for scene graph
generation and visual feature extraction. The maximum detected object in one
image is set to 10. Specifically, the feature dimension for each of the
detected object is 1024. For the query sentence, we append the [CLS] and [SEP]
tokens to the beginning and end of the sentence respectively. Then a pre-
trained BERT is used to generate sentence embedding and the dimension is set
to 768. For our DuMoGa model, it is trained with Adamw optimizer, where we set
the base learning rate at 2e-5 and the batch size at 64.

Table 2: Comparison with state-of-the-art methods in terms of overall IoU on three benchmark datasets. GA represents Graph Alignment, FA represents Feature Alignment, and Full represents Graph Alignment + Feature Alignment. Method | Backbone Model | Refer Image Segmentation
---|---|---
mIoU |<EMAIL_ADDRESS>|<EMAIL_ADDRESS>|<EMAIL_ADDRESS>|<EMAIL_ADDRESS>|<EMAIL_ADDRESS>
MAttNet [31] | ResNet-101 | 8.00 | 9.61 | 7.90 | 6.15 | 5.51 | 4.58
VPD [34] | U-Net | 24.0 | 29.5 | 27.5 | 23.8 | 21.5 | 19.3
LAVT [4] | SWIN-B | 21.2 | 26.6 | 21.6 | 17.1 | 13.7 | 10.9
UNINEXT [26] | ResNet-50 | 19.8 | 22.3 | 21.8 | 21.0 | 19.9 | 19.2
DuMoGa (GA) | ResNet-50 | 15.0 | 19.5 | 18.3 | 16.7 | 14.4 | 11.7
DuMoGa (FA) | ResNet-50 | 16.4 | 21.1 | 19.4 | 17.8 | 15.5 | 13.4
DuMoGa (FULL) | ResNet-50 | 24.4 | 31.8 | 29.7 | 26.8 | 23.1 | 19.3
Figure 5: Visualization result of our proposed DuMoGa model on RIS-CQ dataset.
It is noteworthy that invalid prediction for LAVT was observed in the case of
sample (b).

###  4.2 Evaluation Metrics

For the Referring Image Segmentation task, we follow previous works [16, 21]
and adopt Precision@$X$ and IoU to verify the effectiveness. The IoU
calculates intersection regions over union regions of the predicted
segmentation mask and the ground truth. The Precision@$X$ measures the
percentage of test images with an IoU score higher than the threshold
$X\in\\{0.3,0.4,0.5,0.6,0.7\\}$, which focuses on the location ability of the
method.

###  4.3 Performance Comparison

Table 3 shows the performance comparison with other SoTA methods on the RIS-CQ
dataset, which includes the following models:

LAVT [27] is a Transformer-based framework for referring image segmentation.
Unlike traditional approaches that fuse cross-modal information after feature
extraction, LAVT incorporates language-aware visual encoding directly into the
model architecture;

VPD [34] proposed a new framework that exploits the semantic information of a
pre-trained text-to-image diffusion model in visual perception tasks;

UNINEXT [26] reformulates diverse instance perception tasks into a unified
object discovery and retrieval paradigm and can flexibly perceive different
types of objects by simply changing the input prompts;

MAttNet [31] is a two-stage method that first extracts multiple instances by
using an instance segmentation network Mask RCNN [8], then utilizes language
features to select the target from the extracted instances. Due to the space
limitation, we only list selected SoTA methods, more details can be found in
Supplementary Materials.

As shown in Table 3, our method achieves remarkably superior performance on
RIS-CQ dataset compared with other SoTA methods. Also our DuMoGa model is
based on ResNet-50 [7], which is not so strong as Swin-B [17], DuMoGa achieves
over 100% to 200% performance gain in all metrics compared with LAVT [4] on
RIS-CQ dataset. With stronger backbone models, the performance of our DuMoGa
model can be further improved.

We also provide the visualization of the output of our DuMoGa model in Figure
5. Compared with LAVT [4], our DuMoGa can accurately locate the referring
object based on the comprehensive understanding of visual-textual data, rather
than response to partial words in the query (such as the stop sign in Figure 5
(a)).

###  4.4 In-depth Analysis

Q1: How to control the annotation quality? The annotation process for the RIS-
CQ dataset spanned over a period of 6 months and involved the collaboration of
5 undergraduate students. To ensure the production of high-quality
annotations, the annotators were supervised and adhered to specific
principles. Firstly, all annotators underwent rigorous training before
commencing the actual annotation process. Secondly, separate annotators were
assigned for query and object selection annotations. Annotators responsible
for object selection were instructed to review the quality of queries,
ensuring that unclear or poor queries were either rectified or eliminated.
This approach simulated the evaluation process, guaranteeing the
reasonableness of the queries while avoiding subjective annotations. Lastly,
guidelines were provided for the maximal lengths of language queries,
specifying limits of over 20 words for queries and over 5 for
objects/background labels. We provide more details in the Supplementary
Materials.

Q2: What is the necessity of complex query? On the one hand, current RIS
models are sensitive to language queries. Even input two different queries
which refer to the same object but contain information in different
granularities, current RIS models will output different regions. So we need to
construct a new RIS dataset with complex queries to validate the robustness of
the proposed RIS models. On the other hand, it is not the final path to
general RIS model if restricted to train models with downstream annotated
benchmark datasets, such as RefCOCO with limited object classes and short
query length. It’s time to make a further step to real applications by
combining with large pre-trained models and propose a novel and informative
RIS dataset with more relations among objects.

##  5 What To Do Next?

With the emergence of large pre-trained models (such as GPT-4 [1] and SAM
[10]), the semantic understanding ability of dealing with multi-modal data has
been rapidly enhanced. Then, utilizing large pre-trained models is an
irresistible trend due to their superiority in open-vocabulary scenarios. In
the next step, we can develop lightweight RIS modules (based on the Graph
Alignment and Feature Alignment modules in our DuMoGa model) to adapt large
pre-trained models in a plug-and-play manner. Besides, on the basis of our
proposed RIS-CQ dataset, we can explore more scenarios in real applications,
such as referring object understanding in video and audio modality. And
evaluate the robustness of proposed RIS models even with none or multiple
referring objects according to the complex queries.

##  6 Related Work

Referring image segmentation aims to segment a target region (e.g., object or
stuff) in an image by understanding a given natural linguistic expression,
which was first introduced by [9]. Early works [16, 14, 21] first extracted
visual and linguistic features by CNN and LSTM, respectively, and directly
concatenated two modalities to obtain final segmentation results by an FCN
[18]. In MAttNet [31], Yu et al. proposed a two-stage method that first
extracts instances using Mask R-CNN [8], and then adopts linguistic features
to choose the target from those instances. Then, a series of works are
proposed to adopt the attention mechanism. EFNet [5] designs a co-attention
mechanism to use language to refine the multi-modal features progressively,
which can promote the consistency of the cross-modal information
representation. Some recent works leverage transformer [24] to deal with the
RES task with satisfying performance. VLT [4] employs a transformer to build a
network with an encoder-decoder attention mechanism for enhancing the global
context information. All these methods are trained with RIS datasets with
simple queries.

##  7 Conclusion

In this paper, we propose a novel benchmark dataset for Referring Image
Segmentation with Complex Queries (RIS-CQ). The RIS-CQ dataset is of high
quality and large scale, which challenges the existing RIS with complex,
specific and informative language queries, and enables a more realistic
scenario of RIS research. Besides, we propose a novel SoTA framework to task
the RIS-CQ dataset, called dual-modality graph alignment model (DuMoGa), which
effectively captures the intrinsic correspondence of the semantics of the two
modalities. Experimental results and analyses demonstrate the necessity of our
proposed dataset and the model.

## References

  * Bubeck et al. [2023] Sébastien Bubeck, Varun Chandrasekaran, Ronen Eldan, Johannes Gehrke, Eric Horvitz, Ece Kamar, Peter Lee, Yin Tat Lee, Yuanzhi Li, Scott Lundberg, et al.  Sparks of artificial general intelligence: Early experiments with gpt-4.  _arXiv preprint arXiv:2303.12712_ , 2023.
  * Chen et al. [2018] Jianbo Chen, Yelong Shen, Jianfeng Gao, Jingjing Liu, and Xiaodong Liu.  Language-based image editing with recurrent attentive models.  In _CVPR_ , pages 8721–8729, 2018.
  * Devlin et al. [2019] Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova.  BERT: Pre-training of deep bidirectional transformers for language understanding.  In _NAACL_ , pages 4171–4186, June 2019.
  * Ding et al. [2021] Henghui Ding, Chang Liu, Suchen Wang, and Xudong Jiang.  Vision-language transformer and query generation for referring segmentation.  In _ICCV_ , pages 16321–16330, 2021.
  * Feng et al. [2021] Guang Feng, Zhiwei Hu, Lihe Zhang, and Huchuan Lu.  Encoder fusion network with co-attention embedding for referring image segmentation.  In _CVPR_ , pages 15506–15515, 2021.
  * Guo et al. [2019] Zhijiang Guo, Yan Zhang, and Wei Lu.  Attention guided graph convolutional networks for relation extraction.  In _ACL_ , pages 241–251, 2019.
  * He et al. [2016] Kaiming He, Xiangyu Zhang, Shaoqing Ren, and Jian Sun.  Deep residual learning for image recognition.  In _CVPR_ , pages 770–778, 2016.
  * He et al. [2017] Kaiming He, Georgia Gkioxari, Piotr Dollár, and Ross Girshick.  Mask r-cnn.  In _ICCV_ , pages 2961–2969, 2017.
  * Hu et al. [2016] Ronghang Hu, Marcus Rohrbach, and Trevor Darrell.  Segmentation from natural language expressions.  In _ECCV_ , pages 108–124, 2016.
  * Kirillov et al. [2023] Alexander Kirillov, Eric Mintun, Nikhila Ravi, Hanzi Mao, Chloe Rolland, Laura Gustafson, Tete Xiao, Spencer Whitehead, Alexander C Berg, Wan-Yen Lo, et al.  Segment anything.  _arXiv preprint arXiv:2304.02643_ , 2023.
  * Krishna et al. [2017] Ranjay Krishna, Yuke Zhu, Oliver Groth, Justin Johnson, Kenji Hata, Joshua Kravitz, Stephanie Chen, Yannis Kalantidis, Li-Jia Li, David A Shamma, et al.  Visual genome: Connecting language and vision using crowdsourced dense image annotations.  _IJCV_ , 123(1):32–73, 2017.
  * Li et al. [2020] Bowen Li, Xiaojuan Qi, Thomas Lukasiewicz, and Philip HS Torr.  Manigan: Text-guided image manipulation.  In _CVPR_ , pages 7880–7889, 2020.
  * Li et al. [2023] Li Li, Wei Ji, Yiming Wu, Mengze Li, You Qin, Lina Wei, and Roger Zimmermann.  Panoptic scene graph generation with semantics-prototype learning, 2023.
  * Li et al. [2018] Ruiyu Li, Kaican Li, Yi-Chun Kuo, Michelle Shu, Xiaojuan Qi, Xiaoyong Shen, and Jiaya Jia.  Referring image segmentation via recurrent refinement networks.  In _ICCV_ , pages 5745–5753, 2018.
  * Lin et al. [2014] Tsung-Yi Lin, Michael Maire, Serge Belongie, James Hays, Pietro Perona, Deva Ramanan, Piotr Dollár, and C Lawrence Zitnick.  Microsoft coco: Common objects in context.  In _ECCV_ , pages 740–755, 2014.
  * Liu et al. [2017] Chenxi Liu, Zhe Lin, Xiaohui Shen, Jimei Yang, Xin Lu, and Alan Yuille.  Recurrent multimodal interaction for referring image segmentation.  In _ICCV_ , pages 1271–1280, 2017.
  * Liu et al. [2021] Ze Liu, Yutong Lin, Yue Cao, Han Hu, Yixuan Wei, Zheng Zhang, Stephen Lin, and Baining Guo.  Swin transformer: Hierarchical vision transformer using shifted windows.  In _ICCV_ , pages 10012–10022, 2021.
  * Long et al. [2015] Jonathan Long, Evan Shelhamer, and Trevor Darrell.  Fully convolutional networks for semantic segmentation.  In _ICCV_ , pages 3431–3440, 2015.
  * Lund and Wang [2023] Brady D Lund and Ting Wang.  Chatting about chatgpt: how may ai and gpt impact academia and libraries?  _Library Hi Tech News_ , 40(3):26–29, 2023.
  * Mao et al. [2016] Junhua Mao, Jonathan Huang, Alexander Toshev, Oana Camburu, Alan L Yuille, and Kevin Murphy.  Generation and comprehension of unambiguous object descriptions.  In _CVPR_ , pages 11–20, 2016.
  * Margffoy-Tuay et al. [2018] Edgar Margffoy-Tuay, Juan C Pérez, Emilio Botero, and Pablo Arbeláez.  Dynamic multimodal instance segmentation guided by natural language queries.  In _ECCV_ , pages 630–645, 2018.
  * Peters et al. [2018] Matthew E. Peters, Mark Neumann, Mohit Iyyer, Matt Gardner, Christopher Clark, Kenton Lee, and Luke Zettlemoyer.  Deep contextualized word representations.  In _ACL_ , pages 2227–2237, 2018.
  * Tang et al. [2019] Kaihua Tang, Hanwang Zhang, Baoyuan Wu, Wenhan Luo, and Wei Liu.  Learning to compose dynamic tree structures for visual contexts.  In _CVPR_ , pages 6619–6628, 2019.
  * Vaswani et al. [2017] Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Łukasz Kaiser, and Illia Polosukhin.  Attention is all you need.  2017\.
  * Wang et al. [2019] Xin Wang, Qiuyuan Huang, Asli Celikyilmaz, Jianfeng Gao, Dinghan Shen, Yuan-Fang Wang, William Yang Wang, and Lei Zhang.  Reinforced cross-modal matching and self-supervised imitation learning for vision-language navigation.  In _CVPR_ , pages 6629–6638, 2019.
  * Yan et al. [2023] Bin Yan, Yi Jiang, Jiannan Wu, Dong Wang, Zehuan Yuan, Ping Luo, and Huchuan Lu.  Universal instance perception as object discovery and retrieval.  In _CVPR_ , 2023.
  * Yang et al. [2022] Zhao Yang, Jiaqi Wang, Yansong Tang, Kai Chen, Hengshuang Zhao, and Philip HS Torr.  Lavt: Language-aware vision transformer for referring image segmentation.  In _CVPR_ , pages 18155–18165, 2022.
  * Yang et al. [2019] Zhengyuan Yang, Boqing Gong, Liwei Wang, Wenbing Huang, Dong Yu, and Jiebo Luo.  A fast and accurate one-stage approach to visual grounding.  In _ICCV_ , pages 4683–4693, 2019.
  * Yang et al. [2020] Zhengyuan Yang, Tianlang Chen, Liwei Wang, and Jiebo Luo.  Improving one-stage visual grounding by recursive sub-query construction.  In _ECCV_ , pages 387–404, 2020.
  * Yu et al. [2016] Licheng Yu, Patrick Poirson, Shan Yang, Alexander C Berg, and Tamara L Berg.  Modeling context in referring expressions.  In _ECCV_ , pages 69–85, 2016.
  * Yu et al. [2018] Licheng Yu, Zhe Lin, Xiaohui Shen, Jimei Yang, Xin Lu, Mohit Bansal, and Tamara L Berg.  Mattnet: Modular attention network for referring expression comprehension.  In _CVPR_ , pages 1307–1315, 2018.
  * Zhang et al. [2020] Chao Zhang, Zichao Yang, Xiaodong He, and Li Deng.  Multimodal intelligence: Representation learning, information fusion, and applications.  _IEEE Journal of Selected Topics in Signal Processing_ , 14(3):478–493, 2020.
  * Zhao et al. [2022] Heng Zhao, Joey Tianyi Zhou, and Yew-Soon Ong.  Word2pix: Word to pixel cross-attention transformer in visual grounding.  _TNNLS_ , 2022.
  * Zhao et al. [2023] Wenliang Zhao, Yongming Rao, Zuyan Liu, Benlin Liu, Jie Zhou, and Jiwen Lu.  Unleashing text-to-image diffusion models for visual perception.  _ICCV_ , 2023.
  * Zheng et al. [2021] Changmeng Zheng, Junhao Feng, Ze Fu, Yi Cai, Qing Li, and Tao Wang.  Multimodal relation extraction with efficient graph alignment.  In _ACM MM_ , page 5298–5306, 2021.

##  Appendix A Performance Comparison

Table 3 shows the performance comparison with other SoTA methods on the RIS-CQ
dataset, which includes the following models:

LAVT [27] is a Transformer-based framework for referring image segmentation.
Unlike traditional approaches that fuse cross-modal information after feature
extraction, LAVT incorporates language-aware visual encoding directly into the
model architecture;

VPD [34] proposed a new framework that exploits the semantic information of a
pre-trained text-to-image diffusion model in visual perception tasks;

UNINEXT [26] reformulates diverse instance perception tasks into a unified
object discovery and retrieval paradigm and can flexibly perceive different
types of objects by simply changing the input prompts;

MAttNet [31] is a two-stage method that first extracts multiple instances by
using an instance segmentation network Mask RCNN [8], then utilizes language
features to select the target from the extracted instances.

As shown in Table 3, our method achieves remarkably superior performance on
CIU-CQ dataset compared with other SoTA methods. Also our DuMoGa model is
based on ResNet-50 [7] and ResNet-101, which are not as strong as Swin-B [17],
DuMoGa achieves over 100% to 200% performance gain in all metrics compared
with LAVT [4] on RIS-CQ dataset. With stronger backbone models, the
performance of our DuMoGa model can be further improved.

Table 3: Comparison with state-of-the-art methods in terms of overall IoU on three benchmark datasets. GA represents Graph Alignment, FA represents Feature Alignment, and Full represents Graph Alignment + Feature Alignment. Method | Backbone Model | Refer Image Understanding
---|---|---
mIoU |<EMAIL_ADDRESS>|<EMAIL_ADDRESS>|<EMAIL_ADDRESS>|<EMAIL_ADDRESS>|<EMAIL_ADDRESS>
MAttNet | ResNet-101 | 8.00 | 9.61 | 7.90 | 6.15 | 5.51 | 4.58
LAVT | SWIN-B | 21.2 | 26.6 | 21.6 | 17.1 | 13.7 | 10.9
VPD | U-Net | 24.0 | 29.5 | 27.5 | 23.8 | 21.5 | 19.3
UNINEXT | ResNet-50 | 19.8 | 22.3 | 21.8 | 21.0 | 19.9 | 19.2
DuMoGa (GA) | ResNet-50 | 15.0 | 19.5 | 18.3 | 16.7 | 14.4 | 11.7
DuMoGa (FA) | ResNet-50 | 16.4 | 21.1 | 19.4 | 17.8 | 15.5 | 13.4
DuMoGa (FULL) | ResNet-50 | 24.4 | 31.8 | 29.7 | 26.8 | 23.1 | 19.3
DuMoGa (GA) | ResNet-101 | 16.8 | 21.8 | 21.2 | 19.0 | 16.3 | 13.4
DuMoGa (FA) | ResNet-101 | 17.5 | 21.6 | 20.3 | 18.7 | 16.9 | 14.7
DuMoGa (FULL) | ResNet-101 | 25.3 | 32.4 | 30.4 | 28.0 | 25.2 | 20.5

The DuMoGa framework is meticulously designed with a plug-and-play approach,
aiming to address the process of efficient dual-modality alignment. The
framework offers flexibility by allowing the substitution of the VCTree [23]
method, employed for scene graph generation, and the visual backbone, which is
responsible for extracting visual feature representations, with alternative
methodologies and backbone architectures. This adaptability makes the DuMoGa
framework compatible with a wide range of approaches, thereby accommodating
the evolving landscape of research in the field. By leveraging different
backbone models, as demonstrated in Table 1, the DuMoGa framework exhibits its
versatility. Through the utilization of more sophisticated feature extraction
techniques, such as employing ResNet-101 instead of ResNet-50, the DuMoGa
framework achieves superior performance across various evaluation metrics on
the RIU dataset. This empirical evidence underscores the efficacy of
incorporating more fine-grained feature extraction methods within the DuMoGa
framework.

In essence, our DuMoGa framework exhibits excellent adaptability in an era
characterized by the emergence of diverse feature extraction methods. For
instance, the SAM-series of works [10] have showcased remarkable prowess in
instance segmentation tasks, yielding exceptional performance. Leveraging the
advantages of the SAM models, they can serve as robust backbone models for the
DuMoGa framework. This integration not only enhances the quality of generated
scene graphs but also improves the extraction of visual features, leading to
more accurate and comprehensive inference results. The integration of SAM into
the DuMoGa framework represents a significant advancement in the field,
showcasing the potential for synergistic collaboration between different
methods. It demonstrates how the adaptability and extensibility of the DuMoGa
framework facilitate the integration of state-of-the-art techniques,
ultimately leading to improved performance and promising avenues for further
research in the community.

Effectiveness of each component in our DuMoGa method. As shown in Table 3, we
list three variants of our DuMoGa model. DuMoGa (GA), DuMoGa (FA), and DuMoGa
(Full) represent DuMoGa with only graph alignment, DuMoGa with only feature
alignment, and DuMoGa with graph alignment + feature alignment, respectively.
To evaluate the effectiveness of graph alignment process, we train a DuMoGa
(GA) only considers the information contained in scene graphs and semantic
tree graphs, which only have a few MLPs to complete the task. The same
evaluation process for our feature alignment process, we only use the visual
feature extracted from the SGG model and the sentence embedding from BERT.
These two simple models still outperform traditional RIS methods by a great
margin. The reasons is that as the complexity of query sentence increasing,
traditional methods may be mislead by the sophisticated logic and finally get
low performances, however, the parsed dependency tree graph is likely to
shares higher similarity with the generated scene graph for its richer
information within. As a result, our method easily achieves better
performance.

##  Appendix B Referring Query Generation

Figure 6 depicts the procedural flow of generating referring queries using the
outputs of a scene graph model. Initially, we engage in a dialogue with
ChatGPT using Prompt A as the opening prompt. Prompt A serves the purpose of
clarifying the task we seek ChatGPT’s assistance with and outlining the
associated requirements. Additionally, examples are provided to harness the
powerful in-context learning capabilities of ChatGPT, aiming to achieve
reasoned inferences that align with our specified needs. Subsequently, we
instruct ChatGPT, following Prompt A, regarding the object we intend to
describe and its relevant relations to other objects. This enables ChatGPT to
generate descriptions of the designated objects as per the instructions
outlined in the prompt. It is noteworthy that, to alleviate the inferential
burden on ChatGPT, the triplets generated by the scene graph model (e.g.,
<person, book, holding>) are directly transformed into complete sentences
(e.g., "the person is holding the book"). Moreover, to differentiate between
objects of the same category, numerical suffixes such as "person2" or "cow3"
are assigned. This facilitates relatively precise object descriptions
leveraging relations, thereby significantly reducing the need for labor-
intensive manual annotation of specific object attributes. Finally, we perform
a rewrite on the initial answer generated by ChatGPT in Answer B, removing the
numeric suffix corresponding to the object (e.g., "<person1 is next to
person2" becomes "the person is next to another person," and "<the floor has
person1, person2, and person3 standing on it" becomes "the floor has multiple
people standing on it").

Figure 6: An example of generating descriptions for a specified object based
on the relations between objects provided by a scene graph model using
ChatGPT.

##  Appendix C Potential Impact and Limitations

Potential Impact. Referring Image Segmentation can track people in the scene
and understand their relations with the surrounding objects via language
description, it has the potential to be used to violate people’s privacy. The
possible application to the surveillance system can also bring negative
societal impacts.

Limitation. In this paper, we explore referring image segmentation with
complex queries for only one object. However, referring multiple objects with
complex language queries is also an important task in real applications, which
we will leave as future work.


# STANDARD MODEL SOFT QCD AT ATLAS AND CMS

D. CAFORIO  on behalf of the ATLAS and CMS Collaborations  II. Physikalisches
Institut, Justus-Liebig-Universität, Heinrich-Buff-Ring 16,
35392 Giessen, Germany

###### Abstract

Recent results in soft QCD at LHC by the ATLAS, CMS and TOTEM Collaborations
are presented. Special focus is reserved to studies in diffractive and forward
physics, and to the underlying event, with comparison with previous results
and highlighting novel techniques.

##  1 Diffractive and forward physics

###  1.1 Hard color-singlet exchange in dijet event

In 2$\rightarrow$2 parton scattering, in the high-energy limit of QCD the
fixed-order perturbation theory approach is no longer valid. In dijet
production, the expected dynamics described by the Balitsky-Fadin-Kuraev-
Lipatov (BFKL) evolution equation is reached in configurations where the two
jets are separated by a large rapidity interval.

Events in proton-proton (pp) collisions with two jets separated by a large
pseudorapidity ($\eta$) interval devoid of particle activity, known as
Mueller-Tang jets or jet-gap-jet events, have been recently studied [1] by the
CMS Collaboration [2]. The pseudorapidity gap is indicative of an underlying
t-channel hard color-singlet exchange. In the BFKL framework, hard color-
singlet exchange is described by t-channel two-gluon ladder exchange between
the interacting partons, where the color charge carried by the exchanged
gluons cancel, leading to a suppression of particle production between the
final-state jets.

Soft rescattering effects between partons and the proton remnants can induce
the production of particles in the $\eta$ interval that would otherwise be
devoid of particles, resulting in a reduction of the number of events
identified as having a jet-gap-jet signature. Soft rescattering effects can be
suppressed in processes where one or both of the colliding protons remain
intact after the interaction, such as in single- or central-diffractive dijet
processes or in dijet photoproduction, and can be used to better separate
events with a central gap between the jets. Jet-gap-jet events with an intact
proton were also studied, using the TOTEM detector [3].

Occasionally charged particles are emitted at large angles with respect to the
jet boundary into the $\eta$ region that should be devoid of particles: color-
singlet exchange events appear as an excess of events over the expected
charged particle multiplicity contribution from color-exchange dijet events at
the lowest charged particle multiplicity. The fraction of color-singlet
exchange dijet events $f_{CSE}=\frac{N^{F}-N^{F}_{non-CSE}}{N}$ is defined as
the difference between the number of dijets events ($N^{F}$) and the number of
dijet events with no underlying color-singlet exchange ($N^{F}_{non-CSE}$),
both at lowest multiplicity, over the total number of dijet events ($N$).

The left plot on Figure 1 shows that there is no significant difference
between 13 TeV and 7 TeV results, in contrast to the trend found at lower
energies, an indication that the rapidity gap survival probability stops
decreasing at the center-of-mass energies probed at the LHC.

Figure 1: (Left) Fraction of color-singlet exchange dijet events, $f_{CSE}$,
measured as a function of $p_{T}^{jet2}$ by the D0 and CDF Collaborations at
$\sqrt{s}$ = 0.63 (red open symbols) and 1.8 TeV (green open symbols), by the
CMS Collaboration at 7 TeV (magenta open symbols), and the present results at
13 TeV (filled circles). (Right) Fraction of color-singlet exchange dijet
events, $f_{CSE}$, measured as a function of $\Delta\eta_{jj}$ in pp
collisions at $\sqrt{s}$ = 13 TeV. The red solid curve corresponds to
theoretical predictions based on the RMK model with gap survival probability
of $\mid S\mid^{2}<$ = 10%. The EEIM model predictions with MPI-only
contributions and $\mid S\mid^{2}<$ = 1.2% or MPI+SCI are represented by the
purple dashed and orange dotted curves, respectively. The bands around the
curves represent the associated theoretical uncertainties. [1]

The right plot on Figure 1 shows that the implementation by Ekstedt, Enberg,
Ingelman and Motyka gives a fair description of the data within the
uncertainties only when considering survival probability effects based on MPI
and their soft color interaction model. This is the first time that jet-gap-
jet events were studied in association with an intact proton: the fraction of
color-singlet exchange dijet events is almost three times larger than that for
inclusive dijet production in dijets with similar kinematics, and this can be
interpreted in terms of a lower spectator parton activity in events with
intact protons, which decreases the likelihood of the central gap signature.

###  1.2 Observation of forward proton scattering in association with lepton
pairs produced via photon fusion

Electromagnetic fields sourced by protons at the Large Hadron Collider (LHC)
are sufficiently intense to exceed the Schwinger limit of $10^{18}$ V m-1 and
produce lepton pairs via photon fusion. The ATLAS Collaboration [4] recently
released a paper [5] reporting the observation of forward proton scattering in
association with lepton pairs produced via photon fusion. The scattered
protons are detected by the ATLAS Forward Proton spectrometer (AFP [6] [7]),
whereas the leptons are reconstructed by the central ATLAS detector. The
dominant sources of background, estimated using a data-driven method, come
from the Drell-Yan mechanism and by protons that are outside the AFP
acceptance or were not reconstructed in AFP.

The measured fiducial cross sections in the $ee$ and $\mu\mu$ channels are
$\sigma^{fid}_{ee+p}=11.0\pm 2.6$ (stat) $\pm 1.2$ (syst) $\pm 0.3$ (lumi) fb
and $\sigma^{fid}_{\mu\mu+p}=7.2\pm 1.6$ (stat) $\pm 0.9$ (syst) $\pm 0.2$
(lumi) fb, respectively. Table 1 shows a comparison between these results and
the proton soft survival models, where these factors are poorly constrained,
especially at high $\gamma\gamma$ invariant masses that are important for new
physics searches, because existing probes indirectly deduce dissociation rates
using only central-detector information.

Table 1: Fiducial cross sections from the combined HERWIG and LPAIR predictions with $S_{surv}=1$ and $S_{surv}$ estimated using Refs. [8] [9]. SUPERCHIC 4 predictions include fully kinematically dependent $S_{surv}$. [5] $\sigma_{HERWIG+LPAIR}\times S_{surv}$ |  $\sigma^{fid}_{ee+p}$ (fb) |  $\sigma^{fid}_{\mu\mu+p}$ (fb)
---|---|---
$S_{surv}=1$ | 15.5$\pm$1.2 | 13.5$\pm$1.1
$S_{surv}$ using Refs. [8] [9] | 10.9$\pm$0.8 | 9.4$\pm$0.7
SUPERCHIC 4 | 12.2$\pm$0.9 | 10.4$\pm$0.7
Measurement | 11.0$\pm$2.9 | 7.2$\pm$1.8

###  1.3 Measurement of differential cross sections for single diffractive
dissociation in $\sqrt{s}$ = 8 TeV pp collisions using the ATLAS ALFA
spectrometer

Cross sections related to diffractive dissociation have been measured using
early LHC data by exploiting the large rapidity gap signature that is
kinematically expected. These measurements are not able to distinguish fully
between the single diffractive process, its double dissociation analogue in
which both protons dissociate, and the tail of non-diffractive contributions
in which large rapidity gaps occur. The ATLAS Collaboration recently released
a measurement of the single diffractive cross-section at 8 TeV [10] with the
ALFA forward proton spectrometer [11]. In this process, the intact proton is
scattered through a very small angle of typically a few tens of $\mu$rad, and
is measured in the ALFA forward spectrometer, whereas the dissociated proton
is measured in the tracking detector. The interest in this measurement is that
the double diffractive and non diffractive contributions are suppressed and it
allows to measure the cross-section differentially in terms of the squared
four-momentum transfer $t$, the fractional energy loss of the intact proton
$\xi$ and the visible rapidity gap $\Delta\eta$. Background arises mostly from
central diffraction events. As shown in Table 2, the generators describe the
shape but overestimate the cross section, especially Herwig7.

Table 2: The SD cross section within the fiducial region (4.0 $<\log_{10}\xi\leq$ 1.6 and 0.016 $<\mid t\mid\leq$ 0.43 GeV2) and extrapolated across all $t$ using the measured slope parameter $B$. The systematic and statistical uncertainties are combined for data. The MC statistical uncertainties are negligible. [10] Distribution |  $\sigma^{fiducial(\xi,t)}_{SD}$ [mb] |  $\sigma^{t-extrap}_{SD}$ [mb]
---|---|---
Data | 1.59$\pm$0.13 | 1.88$\pm$0.15
Pythia8 A2 (Schuler-Sjöstrand) | 3.69 | 4.35
Pythia8 A3 (Donnachie-Landshoff) | 2.52 | 2.98
Herwig7 | 4.96 | 6.11

##  2 The underlying event

###  2.1 Underlying Event in top pairs

Another typical soft QCD phenomenon is the underlying event. The underlying
event model in $t\bar{t}$ events has been tested up to a scale of two times
the top quark mass in a study performed by the CMS Collaboration [12], and
measurements in categories of dilepton invariant mass indicate that it should
be valid at even higher scales. These measurements are also relevant as a
direct probe of color reconnection, which is needed to confine the initial QCD
color charge of the $t$ quark into color-neutral states. The main contribution
to the underlying event comes from the color exchanges between the beam
particles and is modeled in terms of multiparton interactions, color
reconnection and beam-beam remnants, tuned to minimum bias and Drell-Yan data.
The main background arises from $tW$ and Drell-Yan processes. In $t\bar{t}$
events the contribution of the underlying event is typically order of 20
charged particles with transverse momentum of about 2 GeV. The majority of the
distributions analyzed indicate a fair agreement between the data and
PowegPythia8, and disfavor the setups in which multiparton interactions and
color reconnection are switched off, or in which the strong coupling parameter
is increased. They also disfavor default configurations in PowegHerwig and
Sherpa. The value of the strong coupling parameter at the mass of $Z$ boson
$\alpha^{FSR}_{S}(M_{Z})=0.120\pm 0.006$ is consistent with the data, and the
corresponding uncertainties translate to a variation of the renormalization
scale by a factor of $\sqrt{2}$.

###  2.2 Underlying Event in $Z\rightarrow\mu^{+}\mu^{-}$

ATLAS recently released a paper [13] studying the underlying event in events
containing a $Z$ boson decaying into a muon pair. Charged-particle
multiplicities and transverse momentum are measured in regions of the azimuth
defined relative to the $Z$ boson direction. The absence of QCD final-state
radiation allows the study of different kinematic regions with varying
transverse momenta of the $Z$ boson. All tested generators show significant
deviations from the data, but predict the mean values better when focusing on
the MPI-sensitive regions.

Copyright 2021 CERN for the benefit of the ATLAS and CMS Collaborations. CC-
BY-4.0 license.

## References

## References

  * [1] [CMS and TOTEM Collaborations] “Hard color-singlet exchange in dijet events in proton-proton collisions at $\sqrt{s}$ = 13 TeV”, arxiv.org/pdf/2102.06945.pdf.
  * [2] [CMS Collaboration] “The CMS experiment at the CERN LHC”, JINST 3, S08004 (2008), doi:10.1088/1748-0221/3/08/S08004.
  * [3] [TOTEM Collaboration] “The TOTEM experiment at the CERN Large Hadron Collider”, JINST 3, S08007 (2008), doi:10.1088/1748-0221/3/08/s08007.
  * [4] [ATLAS Collaboration] “The ATLAS Experiment at the CERN Large Hadron Collider”, JINST 3, S08003 (2008), doi:10.1088/1748-0221/3/08/S08003.
  * [5] [ATLAS Collaboration] “Observation and Measurement of Forward Proton Scattering in Association with Lepton Pairs Produced via the Photon Fusion Mechanism at ATLAS”, Phys. Rev. Lett. 125, 261801 (2020).
  * [6] [ATLAS Collaboration] “Technical Design Report for the ATLAS Forward Proton Detector”, CERN Tech. Report No. CERN-LHCC-2015-009, ATLAS-TDR-024, 2015, https://cds.cern.ch/record/2017378.
  * [7] [ATLAS Collaboration] “Proton tagging with the one arm AFP detector”, CERN Report No. ATL-PHYS-PUB-2017-012, 2017, https://cds.cern.ch/record/2273274.
  * [8] L. A. Harland-Lang, V. A. Khoze, and M. G. Ryskin “The photon PDF in events with rapidity gaps”, Eur. Phys. J. C 76, 255 (2016).
  * [9] M. Dyndal and L. Schoeffel “The role of finite-size effects on the spectrum of equivalent photons in proton-proton collisions at the LHC”, Phys. Lett. B 741, 66 (2015).
  * [10] [ATLAS Collaboration] “Measurement of differential cross sections for single diffractive dissociation in $\sqrt{s}$ = 8 TeV pp collisions using the ATLAS ALFA spectrometer”, JHEP 02, 042 (2020).
  * [11] S. Abdel Khalek et al “The ALFA Roman Pot Detectors of ATLAS”, JINST 11, P11013 (2016), arxiv.org/pdf/1609.00249.pdf.
  * [12] A. M. Sirunyan et al “Study of the underlying event in top quark pair production in pp collisions at 13 TeV”, Eur. Phys. J. C 79, 123 (2019).
  * [13] [ATLAS Collaboration] “Measurement of distributions sensitive to the underlying event in inclusive Z boson production in pp collisions at $\sqrt{s}$ = 13 TeV with the ATLAS detector”, Eur. Phys. J. C 79, 666 (2019).


BatteryMonitor component, which regularly checks the battery level; and the
Interface, which updates the GRA when the rover needs to recharge.

Despite this system not being implemented in ROS, we are able to apply our
calculus to it because it is built from components that act similarly to a ROS
nodes. We take Fig. 9 as our system model (which maps to Step 1 of our
approach in §3) and apply our calculus to the ReasoningAgent and
Battery_Interface.

First, we apply the calculus to the subcomponents of the ReasoningAgent.
Because the output of the GRA is the input of both ComputePlan2Charging and
the ComputePlan2Destination, we use the branching output rule, R2:

$\small{\begin{array}[]{l}\forall\overline{i_{GRA}},\overline{o_{GRA}}\cdot\mathcal{A}_{GRA}(\overline{i_{GRA}})\
\Rightarrow\ \lozenge\mathcal{G}_{GRA}(\overline{o_{GRA}})\\\
\forall\overline{i_{CPC}},\overline{o_{CPC}}\cdot\mathcal{A}_{CPC}(\overline{i_{CPC}})\
\Rightarrow\ \lozenge\mathcal{G}_{CPC}(\overline{o_{CPC}})\\\
\forall\overline{i_{CPD}},\overline{o_{CPD}}\cdot\mathcal{A}_{CPD}(\overline{i_{CPD}})\
\Rightarrow\ \lozenge\mathcal{G}_{CPD}(\overline{o_{CPD}})\\\
\overline{o_{GRA}}=\overline{i_{CPC}}\cup\overline{i_{CPD}}\\\ \vdash\
\left(\begin{array}[]{l}\forall\overline{o_{GRA}},\overline{i_{CPC}}\cdot\mathcal{G}_{GRA}(\overline{o_{GRA}})\
\Rightarrow\ \mathcal{A}_{CPC}(\overline{i_{CPC}})\land\\\
\forall\overline{o_{GRA}},\overline{i_{CPD}}\cdot\mathcal{G}_{GRA}(\overline{o_{GRA}})\
\Rightarrow\ \mathcal{A}_{CPC}(\overline{i_{CPC}})\end{array}\right)\\\
\hline\cr\bigg{(}\forall\overline{i_{GRA}},\overline{o_{CPC}},\overline{o_{CPD}}\cdot\mathcal{A}_{GRA}(\overline{i_{GRA}})\
\Rightarrow\
\lozenge\mathcal{G}_{CPC}(\overline{o_{CPC}})\land\lozenge\mathcal{G}_{CPD}(\overline{o_{CPD}})\bigg{)}\end{array}}$

Intuitively this means that, when the assumptions of the GRA component hold,
then eventually the guarantees of the ComputePlan2Charging ($CPC$) and the
ComputePlan2Destination ($CPD$) hold. This also captures the requirement for
this system that all plans are valid and free from obstacles [28].

Similarly we can use the union of inputs rule, R3, to link the three
components that provide input to the Interface ($I$): the ComputePlan2Charging
($CPC$), the ComputePlan2Destination ($CPD$), and the BatteryMonitor ($BM$).

Using R3, we can derive the following:

$\small{\begin{array}[]{l}\forall\overline{i_{CPC}},\overline{o_{CPC}}\cdot\mathcal{A}_{CPC}(\overline{i_{CPC}})\
\Rightarrow\ \lozenge\mathcal{G}_{CPC}(\overline{o_{CPC}})\\\
\forall\overline{i_{CPD}},\overline{o_{CPD}}\cdot\mathcal{A}_{CPD}(\overline{i_{CPD}})\
\Rightarrow\ \lozenge\mathcal{G}_{CPD}(\overline{o_{CPD}})\\\
\forall\overline{i_{BM}},\overline{o_{BM}}\cdot\mathcal{A}_{BM}(\overline{i_{BM}})\
\Rightarrow\ \lozenge\mathcal{G}_{BM}(\overline{o_{BM}})\\\
\forall\overline{i_{I}},\overline{o_{I}}\cdot\mathcal{A}_{I}(\overline{i_{I}})\
\Rightarrow\ \lozenge\mathcal{G}_{I}(\overline{o_{I}})\\\
\overline{i_{I}}=\overline{o_{CPC}}\cup\overline{o_{CPD}}\cup\overline{o_{BM}}\\\
\vdash\
\forall\overline{i_{I}},\overline{o_{CPC}},\overline{o_{CPD}},\overline{o_{BM}}\cdot\mathcal{G}_{CPC}(\overline{o_{CPC}})\land\mathcal{G}_{CPD}(\overline{o_{CPD}})\land\mathcal{G}_{BM}(\overline{o_{BM}})\Rightarrow\
\mathcal{A}_{I}(\overline{i_{I}})\\\
\hline\cr\bigg{(}\forall\overline{i_{CPC}},\overline{i_{CPD},\overline{i_{BM}},\overline{o_{I}}},\cdot\mathcal{A}_{CPC}(\overline{i_{CPC}})\land\mathcal{A}_{CPD}(\overline{i_{CPD}})\land\mathcal{A}_{BM}(\overline{i_{BM}})\Rightarrow\
\lozenge\mathcal{G}_{I}(\overline{o_{I}})\bigg{)}\end{array}}$

Thus we can deduce that when the plan-computing components
(ComputePlan2Charging and ComputePlan2Destination) and the BatteryMonitor are
functioning correctly, then eventually the Interface’s guarantee is preserved.
This means that battery usage is computed correctly and that the rover stays
in the charger location until it has fully recharged.

Both, this previous approach and the derivations above are able to derive that
the rover produces obstacle-free plans. The approach in [28] was able to
verify that the rover never runs out of battery but our rules above only
allowed us to show that the rover recharges fully when required. These
properties are fairly closely related. The reason that we could deduce the
property that the rover never runs out of battery was down to the way that the
approach using CoCoSim works. There, we had to specify top-level requirements
including that the rover never runs out of battery and essentially show that
the component-level contracts imply this. Our current approach is more
flexible and does not require system-level properties in the same way, rather
it derives the properties for the system from the component-level contracts.
This has benefits, especially in the domain of autonomous systems where there
might be, previously unknown, emergent properties.

This subsection has illustrated how our contract-based compositional
verification approach can be applied in the case of non-ROS systems to derive
system-level contracts. We used the rover’s AADL model (Fig. 9) as our system
model, which maps to Step 1 in our approach (§3). Here, we did not need to
abstract the model to make it more manageable, but this may be needed for more
complicated models. Then we use FOL to write and reason about contracts, which
maps to Steps 2 and 3 of our approach. Heterogeneous verification (mapping to
Step 4a) is still possible here, guided by the FOL contracts. Automatically
generating runtime monitors (Step 4b) is not possible here, because that part
of our approach relies on information in the RCL contracts that is specific to
ROS. However, generating runtime monitors in a suitable generic framework that
can be applicable to non-ROS systems is a useful avenue of future work.

##  6 Conclusions and Future Work

This paper contributes a compositional approach to the development of
verifiable modular robotic systems, which focusses on systems that use the
Robot Operating System (ROS)– though parts of it are applicable to non-ROS
systems. Each module (or ROS node) is specified using an assume–guarantee
contract, written in First-Order Logic (FOL), that guide its verification. We
also present a calculus for composing these contracts, which caters for
sequences, joins, and branches in the system’s architecture. Each node can be
verified using the most suitable method; some may be amenable to formal
verification, while others may not. The verification is driven by the
contracts, which specify the minimal set of properties that the verification
must be able to show hold for that node (to an appropriate level of confidence
for the node, and the system’s regulatory environment).

As a safety net, we automatically synthesise formal monitors to verify the
contracts’ guarantee(s) at runtime. The runtime verification is handled by
ROSMonitoring [55], an existing tool for runtime verification of ROS systems.
Supporting this approach is the ROS Contract Language (RCL), a novel Domain
Specific Language (DSL) for writing FOL contracts for ROS systems; and Vanda,
which is a novel prototype tool that parses RCL and synthesises the runtime
monitors.

In our case study (§4) we introduce contracts to an existing system, then use
formal and non-formal verification techniques. Our case study is designed to
simply illustrate the core concepts of our approach: FOL contracts, combined
with a calculus, guiding the most suitable verification method for each node.

The benefit of letting the contract guide the verification is that it is
effective even if the specification language used to verify a node does not
directly implement FOL. For example, the verification of the Agent node
(§4.4.3) used program model checking of properties written in Linear-time
Temporal Logic (LTL) (which is inherently similar to FOL) enriched with
Belief-Desire-Intention (BDI) concepts [66]. However, the other nodes were
verified using a variety of techniques, both formal and non-formal. The
verification of the Radiation Sensor (§4.4.4) uses Hoare Logic, so the
contract’s FOL properties are easy to represent. The final two nodes were
verified using testing/experimental approaches, so the contracts are a guide
for the properties to be checked.

Our approach to the case study was to write contracts for, and verify the
nodes of, a pre-existing robotic system. However, if we reverse this workflow,
the RCL contracts could form a contract-based development approach for
building new robotic systems. Used in this way, the contracts would link the
system’s requirements to its low-level design. RCL could be used to specify
the assumptions and guarantees of the proposed system’s nodes, and how their
inputs and outputs connect the nodes together. Once this version of the design
was checked using the calculus, the ROS topic information could be added.
These completed contracts could be used to drive a low-level software design,
as the starting point for an implementation. Interesting future work could
involve extending Vanda to produce message type definitions and skeleton code
for ROS nodes, based on the specification in the RCL contracts.

For other future work, we will apply our approach to a larger and more complex
system, expanding the calculus to cater to other arrangements of nodes where
needed. We also aim to explore more sophisticated contracts involving real-
time constraints and, potentially, uncertainty. One area where Vanda could be
improved to aid the specification of the contracts is to add support for
calculating assumptions when composing contracts, similarly to the approach in
[73]. Finally, we intend to explore the level of confidence we can have in a
system that has been verified using a mixture of methods; particularly how
confidence can be calculated for more complex systems with loops in the
information flow.

## References

  * [1] H. Hastie, K. Lohan, M. Chantler, D. A. Robb, S. Ramamoorthy, R. Petrick, S. Vijayakumar, D. Lane, The ORCA Hub: Explainable offshore robotics through intelligent interfaces, in: Explainable Robotic Systems Workshop, ACM Human-Robot Interaction conference,, 2018, p. 2.
URL https://arxiv.org/abs/1803.02100

  * [2] R. Bogue, Robots in the Nuclear Industry: A review of technologies and applications, Industrial Robot: An International Journal 38 (2) (2011) 113–118.  doi:10.1108/01439911111106327.
  * [3] J. M. Aitken, S. M. Veres, A. Shaukat, Y. Gao, E. Cucco, L. A. Dennis, M. Fisher, J. A. Kuo, T. Robinson, P. E. Mort, Autonomous Nuclear Waste Management, IEEE Intelligent Systems 33 (6) (2018) 47–55.  doi:10.1109/MIS.2018.111144814.
  * [4] B. H. Wilcox, Robotic vehicles for planetary exploration, Applied Intelligence 2 (2) (1992) 181–193.  doi:10.1007/BF00058762.
  * [5] A. Flores-Abad, O. Ma, K. Pham, S. Ulrich, A review of space robotics technologies for on-orbit servicing, Progress in Aerospace Sciences 68 (2014) 1–26.  doi:10.1016/j.paerosci.2014.03.002.
  * [6] M. Quigley, K. Conley, B. Gerkey, J. Faust, T. Foote, J. Leibs, R. Wheeler, A. Ng, ROS: an open-source Robot Operating System, in: Workshop on Open Source Software, IEEE, 2009.
  * [7] M. Foughali, Formal Verification of the Functional Layer of Robotic and Autonomous Systems, Theses, Institut national des sciences appliquées de Toulouse (Dec. 2018).
URL https://hal.laas.fr/tel-02080063

  * [8] S. Fleury, M. Herrb, R. Chatila, GenoM: A Tool for the Specification and the Implementation of Operating Modules in a Distributed Robot Architecture, in: International Conference on Intelligent Robots and Systems, IEEE, 1997, pp. 842–849.  doi:10.1109/IROS.1997.655108.
  * [9] R. Halder, J. Proença, N. Macedo, A. Santos, Formal Verification of ROS-Based Robotic Applications Using Timed-Automata, in: Workshop on Formal Methods in Software Engineering, IEEE, 2017.  doi:10.1109/FormaliSE.2017.9.
  * [10] M. Luckcuck, M. Farrell, L. A. Dennis, C. Dixon, M. Fisher, Formal Specification and Verification of Autonomous Robotic Systems: A Survey, ACM Computing Surveys 52 (5) (2019) 1–41.  doi:10.1145/3342355.
  * [11] E. M. Clarke, O. Grumberg, D. Peled, Model checking, MIT press, 1999.
  * [12] M. Leucker, C. Schallhart, A brief account of runtime verification, J. Log. Algebraic Methods Program. 78 (5) (2009) 293–303.  doi:10.1016/j.jlap.2008.08.004.
  * [13] Y. Bertot, P. Castéran, Interactive Theorem Proving and Program Development: Coq’Art: the Calculus of Inductive Constructions, Springer, 2013\.  doi:10.1007/978-3-662-07964-5.
  * [14] M. Farrell, M. Luckcuck, M. Fisher, Robotics and Integrated Formal Methods: Necessity Meets Opportunity, in: Integrated Formal Methods, Vol. 11023 of LNCS, Springer, 2018, pp. 161–171.  doi:10.1007/978-3-319-98938-9_10.
  * [15] C. B. Jones, Tentative Steps Toward a Development Method for Interfering Programs, ACM Trans. on Programming Languages and Systems 5 (4) (1983) 596–619.
  * [16] B. Meyer, Applying "Design by Contract", Computer 25 (10) (1992) 40–51.  doi:10.1109/2.161279.
  * [17] M. Fisher, An Introduction to Practical Formal Methods Using Temporal Logic, John Wiley & Sons, 2011.  doi:10.1002/9781119991472.
  * [18] R. C. Cardoso, L. A. Dennis, M. Farrell, M. Fisher, M. Luckcuck, Towards Compositional Verification for Modular Robotic Systems, in: Proc. Second Workshop on Formal Methods for Autonomous Systems (FMAS2020), Vol. 329, Electronic Proceedings in Theoretical Computer Science, 2020, pp. 15–22.
URL http://arxiv.org/abs/2012.01648v1

  * [19] R. C. Cardoso, M. Farrell, M. Luckcuck, A. Ferrando, M. Fisher, Heterogeneous Verification of an Autonomous Curiosity Rover, in: Proc. NASA Formal Methods, Vol. 12229 of LNCS, Springer, 2020, pp. 353–360.  doi:10.1007/978-3-030-55754-6_20.
  * [20] N. Rouquette, I. Incer, A. Pinto, Early design exploration of space system scenarios using assume-guarantee contracts, in: International Conference on Space Mission Challenges for Information Technology, IEEE, 2023, pp. 15–24.
  * [21] M. Caporuscio, P. Inverardi, P. Pelliccione, Compositional verification of middleware-based software architecture descriptions, in: Proceedings. 26th International Conference on Software Engineering, IEEE, 2004, pp. 221–230.
  * [22] A. Benveniste, B. Caillaud, D. Nickovic, R. Passerone, J.-b. Raclet, P. Reinkemeier, A. Sangiovanni-vincentelli, W. Damm, T. Henzinger, K. G. Larsen, Contracts for Systems Design, Tech. Rep. RR-8147, INRIA (2012).
URL https://hal.inria.fr/hal-00757488v1

  * [23] J. Li, P. Nuzzo, A. Sangiovanni-Vincentelli, Y. Xi, D. Li, Stochastic contracts for cyber-physical system design under probabilistic requirements, in: International Conference on Formal Methods and Models for System Design, no. ii, ACM Press, New York, USA, 2017, pp. 5–14.  doi:10.1145/3127041.3127045.
  * [24] A. Cimatti, M. Dorigatti, S. Tonetta, Ocra: A tool for checking the refinement of temporal contracts, in: International Conference on Automated Software Engineering (ASE), IEEE, 2013, pp. 702–705.  doi:10.1109/ASE.2013.6693137.
  * [25] D. Cofer, A. Gacek, S. Miller, M. W. Whalen, B. LaValley, L. Sha, Compositional verification of architectural models, in: NASA Formal Methods Symposium, Vol. 7226 of LNCS, Springer, 2012, pp. 126–140.  doi:10.1007/978-3-642-28891-3_13.
  * [26] A. Champion, A. Gurfinkel, T. Kahsai, C. Tinelli, Cocospec: A mode-aware contract language for reactive systems, in: Software Engineering and Formal Methods, Vol. 9763 of LNCS, Springer, 2016, pp. 347–366.  doi:10.1007/978-3-319-41591-8_24.
  * [27] A. Champion, A. Mebsout, C. Sticksel, C. Tinelli, The kind 2 model checker, in: Proc. Computer Aided Verification, Vol. 9780 of LNCS, Springer, 2016, pp. 510–517.  doi:10.1007/978-3-319-41540-6_29.
  * [28] H. Bourbouh, M. Farrell, A. Mavridou, I. Sljivo, G. Brat, L. A. Dennis, M. Fisher, Integrating formal verification and assurance: An inspection rover case study, in: NASA Formal Methods Symposium, Vol. 12673 of LNCS, Springer, 2021, pp. 53–71.  doi:10.1007/978-3-030-76384-8_4.
  * [29] M. Broy, A Logical Approach to Systems Engineering Artifacts: Semantic Relationships and Dependencies beyond Traceability – from requirements to functional and architectural views, Software and System Modeling 17 (2) (2018) 365–393.  doi:10.1007/s10270-017-0619-4.
  * [30] I. Ruchkin, J. Sunshine, G. Iraci, B. Schmerl, D. Garlan, IPL: An integration property language for multi-model cyber-physical systems, in: Formal Methods, Vol. 10951 of LNCS, Springer, 2018, pp. 165–184.  doi:10.1007/978-3-319-95582-7_10.
  * [31] L. Baresi, C. Ghezzi, L. Mottola, Loupe: Verifying publish-subscribe architectures with a magnifying lens, IEEE Transactions on Software Engineering 37 (2) (2010) 228–246.
  * [32] A. Basu, M. Gallien, C. Lesire, T. Nguyen, S. Bensalem, F. Ingrand, J. Sifakis, Incremental component-based construction and verification of a robotic system, in: M. Ghallab, C. D. Spyropoulos, N. Fakotakis, N. M. Avouris (Eds.), ECAI 2008 - 18th European Conference on Artificial Intelligence, Patras, Greece, July 21-25, 2008, Proceedings, Vol. 178 of Frontiers in Artificial Intelligence and Applications, IOS Press, 2008, pp. 631–635.  doi:10.3233/978-1-58603-891-5-631.
URL https://doi.org/10.3233/978-1-58603-891-5-631

  * [33] S. Spellini, M. Lora, F. Fummi, S. Chattopadhyay, Compositional design of multi-robot systems control software on ros, ACM Trans. Embed. Comput. Syst. 18 (5s) (oct 2019).  doi:10.1145/3358197.
URL https://doi.org/10.1145/3358197

  * [34] A. Desai, S. Qadeer, S. A. Seshia, Programming safe robotics systems: Challenges and advances, in: Proc. 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), Vol. 11245 of LNCS, Springer, Berlin, Heidelberg, 2018, p. 103–119.  doi:10.1007/978-3-030-03421-4_8.
  * [35] S. Adam, M. Larsen, K. Jensen, U. Schultz, Rule-based dynamic safety monitoring for mobile robots, Journal of Software Engineering for Robotics 7 (2016) 120–141.  doi:10.6092/JOSER_2016_07_01_P120.
  * [36] S. García, P. Pelliccione, C. Menghi, T. Berger, T. Bures, Promise: High-level mission specification for multiple robots, in: Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering: Companion Proceedings, ICSE ’20, Association for Computing Machinery, New York, NY, USA, 2020, p. 5–8.  doi:10.1145/3377812.3382143.
URL https://doi.org/10.1145/3377812.3382143

  * [37] R. Carvalho, A. Cunha, N. Macedo, A. Santos, Verification of system-wide safety properties of ros applications, in: 2020 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), IEEE, 2020, pp. 7249–7254.  doi:10.1109/IROS45743.2020.9341085.
  * [38] N. Macedo, J. Brunel, D. Chemouil, A. Cunha, D. Kuperberg, Lightweight specification and analysis of dynamic systems with rich configurations, in: Proc. 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, Association for Computing Machinery, New York, NY, USA, 2016, p. 373–383.  doi:10.1145/2950290.2950318.
  * [39] A. Santos, A. Cunha, N. Macedo, C. Lourenço, A framework for quality assessment of ros repositories, in: 2016 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), 2016, pp. 4491–4496.  doi:10.1109/IROS.2016.7759661.
  * [40] A. Desai, S. Ghosh, S. A. Seshia, N. Shankar, A. Tiwari, Soter: A runtime assurance framework for programming safe robotics systems, in: 2019 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), 2019, pp. 138–150.  doi:10.1109/DSN.2019.00027.
  * [41] B. Wesselink, K. de Vos, I. Kuertev, M. Reniers, E. Torta, RoboSC: a domain-specific language for supervisory controller synthesis of ROS applications, in: 2023 IEEE International Conference on Robotics and Automation (ICRA), IEEE, 2023.  doi:10.1109/icra48891.2023.10161436.
URL https://doi.org/10.1109/icra48891.2023.10161436

  * [42] A. Miyazawa, P. Ribeiro, W. Li, A. Cavalcanti, J. Timmis, J. Woodcock, Robochart: Modelling and verification of the functional behaviour of robotic applications, Softw. Syst. Model. 18 (5) (2019) 3097–3149.  doi:10.1007/s10270-018-00710-z.
URL https://doi.org/10.1007/s10270-018-00710-z

  * [43] M. Farrell, N. Mavrakis, A. Ferrando, C. Dixon, Y. Gao, Formal modelling and runtime verification of autonomous grasping for active debris removal, Frontiers in Robotics and AI 8 (2021).  doi:10.3389/frobt.2021.639282.
  * [44] I. Gavran, R. Majumdar, I. Saha, Antlab: A multi-robot task server, ACM Trans. Embed. Comput. Syst. 16 (5s) (sep 2017).  doi:10.1145/3126513.
URL https://doi.org/10.1145/3126513

  * [45] M. Huth, M. Ryan, Logic in Computer Science: Modelling and reasoning about systems, Cambridge University Press, 2004.
  * [46] K. Ueda, Guarded horn clauses, in: Proceedings of the 4th Conference on Logic Programming, Vol. 221 of LNCS, Springer, 1985, pp. 168–179.  doi:10.1007/3-540-16479-0\\_17.
URL https://doi.org/10.1007/3-540-16479-0_17

  * [47] S. Gregory, Parallel logic programming in PARLOG - the language and its implementation, Addison-Wesley, 1987.
  * [48] A. Pnueli, The Temporal Logic of Programs, in: Foundations of Computer Science, IEEE, 1977, pp. 46–57.  doi:10.1109/SFCS.1977.32.
  * [49] K. A. Elkader, O. Grumberg, C. S. Păsăreanu, S. Shoham, Automated circular assume-guarantee reasoning, in: Formal Methods, Vol. 9109 of LNCS, Springer, 2015, pp. 23–39.  doi:10.1007/978-3-319-19249-9_3.
  * [50] B. Banieqbal, H. Barringer, Temporal Logic with Fixed Points, in: Temporal Logic in Specification, Vol. 398 of LNCS, Springer, 1987, pp. 62–74.  doi:10.1007/3-540-51803-7_22.
  * [51] X. Huang, D. Kroening, W. Ruan, J. Sharp, Y. Sun, E. Thamo, M. Wu, X. Yi, A survey of safety and trustworthiness of deep neural networks: Verification, testing, adversarial attack and defence, and interpretability, Computer Science Review 37 (2020) 100270.  doi:10.1016/j.cosrev.2020.100270.
  * [52] M. Luckcuck, M. Fisher, L. Dennis, S. Frost, A. White, D. Styles, Principles for the Development and Assurance of Autonomous Systems for Safe Use in Hazardous Environments (Jun. 2021).  doi:10.5281/zenodo.5012322.
URL https://doi.org/10.5281/zenodo.5012322

  * [53] M. Luckcuck, Using formal methods for autonomous systems: Five recipes for formal verification, Proceedings of the Institution of Mechanical Engineers, Part O: Journal of Risk and Reliability 0 (0) (2021) 1748006X2110349.  doi:10.1177/1748006X211034970.
  * [54] K. Y. Rozier, Specification: The biggest bottleneck in formal methods and autonomy, in: Working Conference on Verified Software: Theories, Tools, and Experiments, Vol. 9971 of LNCS, Springer, 2016, pp. 8–26.  doi:10.1007/978-3-319-48869-1_2.
  * [55] A. Ferrando, R. C. Cardoso, M. Fisher, D. Ancona, L. Franceschini, V. Mascardi, ROSMonitoring: A runtime verification framework for ROS, in: Towards Autonomous Robotic Systems, Vol. 12228 of LNCS, Springer, 2020, pp. 387–399.  doi:10.1007/978-3-030-63486-5_40.
  * [56] D. Ancona, L. Franceschini, A. Ferrando, V. Mascardi, RML: Theory and Practice of a Domain Specific Language for Runtime Verification, Science of Computer Programming 205 (2021) 102610.  doi:10.1016/j.scico.2021.102610.
  * [57] T. Wright, A. West, M. Licata, N. Hawes, B. Lennox, Simulating ionising radiation in gazebo for robotic nuclear inspection challenges, Robotics 10 (3) (2021).  doi:10.3390/robotics10030086.
URL https://www.mdpi.com/2218-6581/10/3/86

  * [58] L. A. Dennis, Gwendolen semantics: 2017, Tech. Rep. ULCS-17-001, University of Liverpool, Department of Computer Science (2017).
URL https://intranet.csc.liv.ac.uk/research/techreports/tr2017/ulcs-17-001.pdf

  * [59] L. Carlone, F. Dellaert, Duality-based verification techniques for 2d slam, in: 2015 IEEE international conference on robotics and automation (ICRA), IEEE, 2015, pp. 4589–4596.  doi:10.1109/ICRA.2015.7139835.
  * [60] L. Carlone, D. M. Rosen, G. Calafiore, J. J. Leonard, F. Dellaert, Lagrangian duality in 3d slam: Verification techniques and optimal solutions, in: 2015 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), IEEE, 2015, pp. 125–132.  doi:10.1109/IROS.2015.7353364.
  * [61] J. Briales, J. Gonzalez-Jimenez, Fast global optimality verification in 3d slam, in: 2016 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), IEEE, 2016, pp. 4630–4636.  doi:10.1109/IROS.2016.7759681.
  * [62] Y. Hasegawa, Y. Fujimoto, Experimental verification of path planning with slam, IEEJ Journal of Industry Applications 5 (3) (2016) 253–260.  doi:10.1541/ieejjia.5.253.
  * [63] F. Duchoň, J. Hažík, J. Rodina, M. Tölgyessy, M. Dekan, A. Sojka, Verification of slam methods implemented in ros, Journal of Multidisciplinary Engineering Science and Technology (JMEST) 6 (2019).  doi:10.22223/tr.2016-1/2011.
  * [64] R. Sivỳ, D. Perduková, Verification of slam methods on ros platform, Transactions of the VŠB-Technical University of Ostrava, Mechanical Series 62 (2016) 59–66.  doi:10.22223/tr.2016-1/2011.
  * [65] L. A. Dennis, B. Farwer, Gwendolen: A BDI Language for Verifiable Agents, in: Workshop on Logic and the Simulation of Interaction and Reasoning, AISB, 2008, pp. 16–23.
  * [66] L. A. Dennis, M. Fisher, M. P. Webster, R. H. Bordini, Model checking agent programming languages, Automated Software Engineering 19 (1) (2012) 5–63.  doi:10.1007/s10515-011-0088-x.
  * [67] W. Visser, K. Havelund, G. Brat, S.-J. Park, F. Lerda, Model Checking Programs, Automated Software Engineering 10 (2) (2002) 3–11.  doi:10.5555/786768.786967.
  * [68] A. S. Rao, M. Georgeff, BDI Agents: From Theory to Practice, in: International Conference on Multi-Agent Systems, AAAI, 1995, pp. 312–319.
  * [69] C. A. R. Hoare, An axiomatic basis for computer programming, Comms. of the ACM 12 (10) (1969) 576–580.  doi:10.1145/363235.363259.
  * [70] K. R. M. Leino, Dafny: An automatic program verifier for functional correctness, in: Logic for Programming Artificial Intelligence and Reasoning, Vol. 6355 of LNCS, Springer, 2010, pp. 348–370.  doi:10.1007/978-3-642-17511-4_20.
  * [71] M. Barnett, B.-Y. E. Chang, R. DeLine, B. Jacobs, K. R. M. Leino, Boogie: A Modular Reusable Verifier for Object-Oriented Programs, in: Formal Methods for Components and Objects, Vol. 4111 of LNCS, Springer, 2005, pp. 364–387.  doi:10.1007/11804192_17.
  * [72] L. De Moura, N. Bjørner, Z3: An efficient smt solver, in: Tools and Algorithms for the Construction and Analysis of Systems, Vol. 4963 of LNCS, Springer, 2008, pp. 337–340.  doi:10.1007/978-3-540-78800-3_24.
  * [73] J. M. Cobleigh, D. Giannakopoulou, C. S. Pasareanu, Learning Assumptions for Compositional Verification, in: Tools and Algorithms for the Construction and Analysis of Systems, Vol. 2619 of LNCS, Springer, 2003, pp. 331–346.  doi:10.1007/3-540-36577-X_24.

##  Appendix A Remote Inspection Contracts

This appendix contains the full listing of the RCL context and the contracts
of all four nodes from our case study in §4.

Context

$\begin{array}[]{rl}WayP:&\mathbb{R}\times\mathbb{R}\rightarrow\mathbb{N}\\\
RadStat:&\\{red,orange,green\\}\\\
CommandSet:&\\{move(\mathbb{R},\mathbb{R}),inspect(\mathbb{N})\\}\\\
PositionType:&\mathbb{R}\times\mathbb{R}\rightarrow\mathbb{B}\\\
AtType:&\mathbb{R}\times\mathbb{R}\rightarrow\mathbb{B}\\\
InspectedType:&\mathbb{N}\rightarrow\mathbb{B}\\\
SensorsType:&\emptyset\end{array}$

Agent

$\begin{array}[]{rl}inputs&(wayP:WayP,at:AtType,radiationStatus:RadStat,\\\
&inspected:InspectedType)\\\ outputs&(command:CommandSet)\\\
topics&(gazebo\\_radiation\\_plugins/Command~{}command\\\ &\qquad
matches:~{}out.command,\\\
&gazebo\\_radiation\\_plugins/Inspection~{}inspected\\\ &\qquad
matches:~{}in.inspected,\\\
&gazebo\\_radiation\\_plugins/At~{}at~{}matches:~{}in.at,\\\
&int16~{}wayP~{}matches:~{}in.wayP,\\\
&string~{}radiationStatus~{}matches:~{}in.radiationStatus)\\\
assume&(in.radiationStatus\in\\{red,orange,green\\})\\\ guarantee&(\forall
x^{\prime},y^{\prime}\in REAL,i\in NATURAL\cdot
in.at(x^{\prime},y^{\prime})=TRUE\\\ &\land
in.wayP(x^{\prime},y^{\prime})=i\land in.inspected(i)=TRUE\\\ &\land
in.radiationStatus\notin\\{red,orange\\}\\\ &\implies\exists x,y\in
REAL\cdot(in.wayP(x,y)=i+1\\\ &\lor(\forall
x^{\prime\prime},y^{\prime\prime}\in REAL\cdot
in.wayP(x^{\prime\prime},y^{\prime\prime})\neq i+1\\\ &\land
in.wayP(x,y)=0))\land out.command=move(x,y)\\\ guarantee&(\forall
x^{\prime},y^{\prime}\in REAL,i\in NATURAL\cdot
in.at(x^{\prime},y^{\prime})=TRUE\\\ &\land
in.wayP(x^{\prime},y^{\prime})=i\land in.inspected(i)=FALSE\\\ &\implies
out.command=inspect(i)\\\ guarantee&(\forall x^{\prime},y^{\prime}\in
REAL,i\in NATURAL\cdot\\\ &in.radiationStatus\in\\{red,orange\\}\\\
&\lor\neg\exists x,y\in REAL\cdot in.wayP(x,y)=i+1\implies\exists
x^{\prime\prime},y^{\prime\prime}\in REAL\\\ &\cdot
in.wayP(x^{\prime\prime},y^{\prime\prime})=0\land
out.command=move(x^{\prime\prime},y^{\prime\prime})\end{array}$

Localisation

$\begin{array}[]{rl}inputs&(sensors:SensorsType)\\\
outputs&(position:PositionType)\\\
topics&(geometry\\_msgs/PoseWithCovarianceStamped~{}amcl\\_pose\\\ &\qquad
matches:~{}out.position)\\\ assume&(TRUE)\\\ guarantee&(\exists!~{}x,y\in
REAL\cdot out.position(x,y))\end{array}$

Navigation

$\begin{array}[]{rl}inputs&(position:PositionType,command:CommandSet)\\\
outputs&(at:AtType)\\\
topics&(gazebo\\_radiation\\_plugins/Command~{}command\\\ &\qquad
matches:~{}in.command,\\\ &int16~{}currentLoc~{}matches:~{}in.position,\\\
&gazebo\\_radiation\\_plugins/At~{}at~{}matches:~{}out.at)\\\
assume&(\exists!~{}x,y\in REAL\cdot in.position(x,y)=TRUE)\\\
guarantee&(\forall x,y\in REAL\cdot in.command=move(x,y)\\\ &\land
in.position(x,y)=TRUE\iff out.at(x,y)=TRUE)\end{array}$

RadiationSensor

$\begin{array}[]{rl}inputs&(r:REAL,command:CommandSet)\\\
outputs&(radiationStatus:RadStat,inspected:InspectedType)\\\
topics&(gazebo\\_radiation\\_plugins/Simulated\\_Radiation\\_Msg~{}r\\\
&\qquad matches:~{}r,\\\ &gazebo\\_radiation\\_plugins/Command~{}command\\\
&\qquad matches:~{}in.command,\\\
&gazebo\\_radiation\\_plugins/Inspection~{}inspected\\\ &\qquad
matches:~{}inspected,\\\
&string~{}radiationStatus~{}matches:~{}out.radiationStatus)\\\ assume&(0\leq
in.r)\\\ guarantee&(\forall i\in NATURAL\cdot in.command=inspect(i)\implies\\\
&(out.inspected(i)=TRUE\\\ &\land 0\leq in.r\land in.r<120\implies
out.radiationStatus=green\\\ &\land 120\leq in.r\land in.r<250\implies
out.radiationStatus=orange\\\ &\land 250\leq in.r\implies
out.radiationStatus=red)\end{array}$

##  Appendix B Hoare Proofs

This appendix contains the full Hoare Logic Proofs used in §4.4.4

###  B.1 Proof 1

$\\{radiation\\_at(i)<10\\}$

⬇

1input $\coloneqq$ radiation_at(i)

$\\{input<10\\}$ \- Assignment Axiom

⬇

1IF (input < 10) THEN

$\quad\quad\\{input<10\land input<10\\}$

$\quad\quad\\{input<10\land green=green\\}$ \- strengthening

⬇

1 output $\coloneqq$ green

$\quad\quad\\{input<10\land output=green\\}$ \- Assignment Axiom

$\quad\quad\\{output=green\\}$ \- weakening

⬇

1 ELSE

$\quad\quad\\{input<10\land input\geq 10\\}$

$\quad\quad\\{\bot\\}$ \- strengthening

⬇

1 IF (input < 20) THEN

$\quad\quad\quad\quad\\{\bot\land input<20\\}$

$\quad\quad\quad\quad\\{\bot\\}$ \- strengthening

⬇

1 output $\coloneqq$ orange

$\quad\quad\quad\quad\\{\bot\\}$ \- Assignment axiom

⬇

1 ELSE

$\quad\quad\quad\quad\\{\bot\land input\geq 20\\}$

$\quad\quad\quad\quad\\{\bot\\}$ \- strengthening

⬇

1 output $\coloneqq$ red

$\quad\quad\quad\quad\\{\bot\\}$ \- Assignment axiom

$\quad\quad\quad\quad\\{output=green\\}$ \- weakening

$\quad\quad\\{output=green\\}$ – Conditional Rule

$\\{output=green\\}$ – Conditional Rule

###  B.2 Proof 2

$\\{10\leq radiation\\_at(i)<20\\}$

⬇

1input $\coloneqq$ radiation_at(i)

$\\{10\leq input<20\\}$ \- Assignment Axiom

⬇

1IF (input < 10) THEN

$\quad\quad\\{10\leq input<20\land input<10\\}$

$\quad\quad\\{\bot\\}$ \- strengthening

⬇

1 output $\coloneqq$ green

$\quad\quad\\{\bot\\}$ \- Assignment Axiom

$\quad\quad\\{output=orange\\}$ \- weakening

⬇

1 ELSE

$\quad\quad\\{10\leq input<20\land input\geq 10\\}$

$\quad\quad\\{10\leq input<20\\}$ \- strengthening

⬇

1 IF (input < 20) THEN

$\quad\quad\quad\quad\\{10\leq input<20\land input<20\\}$

$\quad\quad\quad\quad\\{10\leq input<20\land orange=orange\\}$ \-
strengthening

⬇

1 output $\coloneqq$ orange

$\quad\quad\quad\quad\\{10\leq input<20\land output=orange\\}$ \- Assignment
axiom

$\quad\quad\quad\quad\\{output=orange\\}$ \- weakening

⬇

1 ELSE

$\quad\quad\quad\quad\\{10\leq input<20\land input\geq 20\\}$

$\quad\quad\quad\quad\\{\bot\\}$ \- strengthening

⬇

1 output $\coloneqq$ red

$\quad\quad\quad\quad\\{\bot\\}$ \- Assignment axiom

$\quad\quad\quad\quad\\{output=orange\\}$ \- weakening

$\quad\quad\\{output=orange\\}$ – Conditional Rule

$\\{output=orange\\}$ – Conditional Rule

###  B.3 Proof 3

$\\{radiation\\_at(i)\geq 20\\}$

⬇

1input $\coloneqq$ radiation_at(i)

$\\{input\geq 20\\}$ \- Assignment Axiom

⬇

1IF (input < 10) THEN

$\quad\quad\\{input\geq 20\land input<10\\}$

$\quad\quad\\{\bot\\}$ \- strengthening

⬇

1 output $\coloneqq$ green

$\quad\quad\\{\bot\\}$ \- Assignment Axiom

$\quad\quad\\{output=red\\}$ \- weakening

⬇

1 ELSE

$\quad\quad\\{input\geq 20\land input\geq 10\\}$

$\quad\quad\\{input\geq 20\\}$ \- strengthening

⬇

1 IF (input < 20) THEN

$\quad\quad\quad\quad\\{input\geq 20\land input<20\\}$

$\quad\quad\quad\quad\\{\bot\\}$ \- strengthening

⬇

1 output $\coloneqq$ orange

$\quad\quad\quad\quad\\{\bot\\}$ \- Assignment axiom

$\quad\quad\quad\quad\\{output=red\\}$ \- weakening

⬇

1 ELSE

$\quad\quad\quad\quad\\{input\geq 20\land input\geq 20\\}$

$\quad\quad\quad\quad\\{input\geq 20\land red=red\\}$ \- strengthening

⬇

1 output $\coloneqq$ red

$\quad\quad\quad\quad\\{input\geq 20\land output=red\\}$ \- Assignment axiom

$\quad\quad\quad\quad\\{output=red\\}$ \- weakening

$\quad\quad\\{output=red\\}$ – Conditional Rule

$\\{output=red\\}$ – Conditional Rule

###  B.4 Proof 4

$\\{True\\}$

$\\{radiation\\_at(i)=radiation\\_at(i)\\}$ \- strengthening

⬇

1input $\coloneqq$ radiation_at(i)

$\\{input=radiation\\_at(i)\\}$ \- Assignment Axiom

⬇

1IF (input < 10) THEN

$\quad\quad\\{input=radiation\\_at(i)\land input<10\\}$

⬇

1 output $\coloneqq$ green

$\quad\quad\\{input=radiation\\_at(i)\land input<10\\}$ \- Assignment Axiom

$\quad\quad\\{input=radiation\\_at(i)\\}$ \- weakening

⬇

1 ELSE

$\quad\quad\\{input=radiation\\_at(i)\land input\geq 10\\}$

$\quad\quad\\{input=radiation\\_at(i)\\}$ \- strengthening

⬇

1 IF (input < 20) THEN

$\quad\quad\quad\quad\\{input=radiation\\_at(i)\land input<20\\}$

⬇

1 output $\coloneqq$ orange

$\quad\quad\quad\quad\\{input=radiation\\_at(i)\land input<20\\}$ \-
Assignment axiom

$\quad\quad\quad\quad\\{input=radiation\\_at(i)\\}$ \- weakening

⬇

1 ELSE

$\quad\quad\quad\quad\\{input=radiation\\_at(i)\land input\geq 20\\}$

⬇

1 output $\coloneqq$ red

$\quad\quad\quad\quad\\{input=radiation\\_at(i)\land input\geq 20\\}$ \-
Assignment axiom

$\quad\quad\quad\quad\\{input=radiation\\_at(i)\\}$ \- weakening

$\quad\quad\\{input=radiation\\_at(i)\\}$ – Conditional Rule

$\\{input=radiation\\_at(i)\\}$ – Conditional Rule