#  Learning under Label Noise through Few-Shot Human-in-the-Loop Refinement

Aaqib Saeed1111Correspondence<EMAIL_ADDRESS>Dimitris Spathis2,3, Jungwoo
Oh4, Edward Choi4, Ali Etemad5
1Eindhoven University of Technology, 2Nokia Bell Labs, 3University of
Cambridge, 4KAIST, 5Queen’s University

###### Abstract

Wearable technologies enable continuous monitoring of various health metrics,
such as physical activity, heart rate, sleep, and stress levels. A key
challenge with wearable data is obtaining quality labels. Unlike modalities
like video where the videos themselves can be effectively used to label
objects or events, wearable data do not contain obvious cues about the
physical manifestation of the users and usually require rich metadata. As a
result, label noise can become an increasingly thorny issue when labeling such
data. In this paper, we propose a novel solution to address noisy label
learning, entitled Few-Shot Human-in-the-Loop Refinement (FHLR). Our method
initially learns a seed model using weak labels. Next, it fine-tunes the seed
model using a handful of expert corrections. Finally, it achieves better
generalizability and robustness by merging the seed and fine-tuned models via
weighted parameter averaging. We evaluate our approach on four challenging
tasks and datasets, and compare it against eight competitive baselines
designed to deal with noisy labels. We show that FHLR achieves significantly
better performance when learning from noisy labels and achieves state-of-the-
art by a large margin, with up to $19\%$ accuracy improvement under symmetric
and asymmetric noise. Notably, we find that FHLR is particularly robust to
increased label noise, unlike prior works that suffer from severe performance
degradation. Our work not only achieves better generalization in high-stakes
health sensing benchmarks but also sheds light on how noise affects commonly-
used models.

##  1 Introduction

The increasing adoption of wearable technology has enabled continuous
monitoring of various health metrics, such as physical activity, heart rate,
sleep, and stress levels. This has spurred interest in gleaning insights into
health and wellness from the data collected by these ubiquitous devices, for
instance by detecting potential complications and promoting healthy behaviors.
Beyond personal use, data coming from wearables also have promising medical
applications. Physicians can monitor the health of patients remotely,
especially those with chronic conditions, and track their progress over time.
This is particularly useful for detecting changes that require prompt medical
attention. Moreover, the continuous physiological data from wearables along
with other devices can help doctors make more accurate diagnoses and develop
personalized treatment plans.

The abundance of data generated from wearable sensors has paved the way for
developing deep learning models to tap into these insights. However, deep
models rely on large volumes of high-quality, clean, and labeled data, which
can be difficult to obtain in the context of wearable signals. Data labels are
not always accurate due to factors like users’ subjective interpretations,
lack of domain expertise, and annotation cost. Inconsistent labels can
undermine the generalizability of deep learning models, especially for health
monitoring where misdiagnosis can have grave consequences. Therefore,
developing techniques to mitigate the effects of noisy labels is crucial to
fully realize the potential of deep learning for wearable time-series.

While there has been significant research on mitigating label noise in deep
learning (see Section 2) in the context of language and vision, to the best of
our knowledge, there has been no rigorous attempt at dealing with label
corruption in the context of deep networks for wearable sensor data. To this
end, we aim to investigate the impact of label noise and provide an effective
way to mitigate its impact on training deep neural networks for sensory data,
such as signals obtained from inertial measurement units (IMUs),
electroencephalography (EEG), and electrocardiography (ECG).

In this paper, we propose a novel technique to tackle the issue of noisy
labels, named Few-shot Human-in-the-Loop Refinement (FHLR). Our training
scenario consists of three main stages (see Figure 1 for an overview). In the
initial phase, our approach learns a seed model with weak labels, where labels
are generated by smoothing existing noisy ones in order to obtain a reliable
initial model that is less prone to overfitting to noisy annotations. In the
second phase, we leverage a small set of clean labels acquired from human
experts to fine-tune the initial model. As a last step, we apply model merging
(i.e., weighted averaging of learned model parameters) to create a more
accurate and robust model with better generalization. We evaluate our method
across four tasks and datasets, comparing against eight baselines, and show
that FHLR provides significantly better generalization in learning from noisy
labeled data than prior techniques.

Figure 1: Illustration of the proposed noisy label learning framework.
Overview of FHLR, a simple yet effective method for dealing with noisy labels
by pre-training a model with weak labels, fine-tuning with expert annotations,
and performing weight averaging to come up with the final model.

FHLR aims to enhance the performance of deep models in the context of wearable
time-series with noisy labels, while offering several advantages over
traditional methods. First, it does not make any assumptions about the
distribution of label noise, which makes it applicable to various real-world
noise profiles and different modalities. Second, incorporating human expertise
into the annotation process ensures that the labels are grounded in domain
knowledge, and yet, our ‘few shot’ approach does not require extensive
involvement from the experts and also enable the mitigation of annotation
noise present in real-world datasets. Third, building upon the success of
weight averaging of fine-tuned neural networks (Wortsman et al., 2022) and
learning from weak supervision (Lukasik et al., 2020), our approach offers a
powerful way for learning from noisy labeled data. To the best of our
knowledge, model averaging has not been explored earlier in learning under
label noise. Finally, our method does not rely on any supplementary neural
networks or modified loss functions, incurs no additional costs during
inference, and enables efficient training of a robust model using a minimal
number of clean examples that can be practically available in practice. In
this work, we make the following contributions:

  * •

High-impact domain. We study for the first time the effect of label noise on
learning models from wearable sensor data in the context of health and well-
being tasks, such as sleep-stage scoring.

  * •

Novel effective method. We propose a highly effective method (FHLR) for
addressing noisy labels through few-shot human-in-the-loop refinement that
outperforms several prior techniques.

  * •

Particularly robust to high noise levels. We empirically demonstrate that our
approach yields models with high generalizability and provides robustness
against low to high levels of noise in the label space.

  * •

Strong results in an array of competitive benchmarks. We show that our
embarrassingly simple averaging of seed and fine-tuned models exhibit better
performance than individual counterparts and on-par with computationally
expensive methods, such as model ensembles.

##  2 Related Work

Over the years, there has been significant interest in the study of learning
deep models from noisy labels within the scope of data-centric and robust deep
learning. In order to minimize the effects of label noise, recent research has
explored various strategies. One approach is to use regularization techniques
such as dropout (Arpit et al., 2017) which can help prevent overfitting and
improve generalization. Label cleaning and correction techniques have also
been proposed (Reed et al., 2014; Goldberger and Ben-Reuven, 2017; Li et al.,
2017; Veit et al., 2017; Song et al., 2019), where additional steps are
performed to identify and correct mislabeled instances in the training data.

Another strategy is instance re-weighting, where the contribution of each
training instance to the learning objective is adjusted based on its estimated
reliability or confidence. Mentornet (Jiang et al., 2018), Co-teaching (Ren et
al., 2018), and Meta-weight-net (Shu et al., 2019) are examples of methods
that assign different weights to instances based on their predicted
probabilities or distances to decision boundaries. Cross-validation has also
been used to tackle label noise (Northcutt et al., 2021), where the training
data is divided into multiple subsets and models are trained and evaluated on
different subsets to identify samples with incorrect labels. Other approaches
include meta learning (Zheng et al., 2021), self-learning (Han et al., 2019),
gradient clipping (Menon et al., 2020), and data augmentation (Zhang et al.,
2018; Cheng et al., 2020; Liang et al., 2020; Jiang et al., 2020), all of
which have been investigated to mitigate the effects of label noise.

In the context of the vision domain, label smoothing (Lukasik et al., 2020)
has been studied to tackle label noise. However, its feasibility for
modalities like sequential data remains uncertain, and this is the gap our
method aims to fill. Additionally, while the cross-validation approach
(Northcutt et al., 2021) has been successful in identifying samples with
incorrect labels, it comes with a significant training cost which may result
in discarding a large number of valuable training examples. Further, although
model merging has been explored in the context of ensemble learning, it has
not been widely used to tackle label noise.

To the best of our knowledge, no prior works have specifically studied
wearable time-series representation learning under label noise, additionally
assessing both symmetric (where mislabeling occurs randomly) and asymmetric
(where mislabeling occurs systematically or in a biased manner) noise.
Further, wearable sensing lacks reliable crowdsourcing unlike vision, where,
cheap image labels can be acquired via Mechanical Turk. Our work addresses
this shortcoming by proposing a highly effective yet simplistic approach. Our
method is complementary to existing approaches, as it does not modify the
primary objective function and can be used as a plug-in to achieve high
performance in learning from noisy labels.

##  3 Method

###  3.1 Preliminaries

Label Noise. Label noise refers to the misalignment between the ground truth
label $y^{*}$ and the observed label $y$ in a given dataset. In the context of
a $\mathcal{C}$-way classification problem, label noise can be modeled as a
class-conditional label flipping process $h\left(\cdot\right)$, where every
label in class $j\in\mathcal{C}$ may be independently mislabeled as class
$i\in\mathcal{C}$ with probability $p\left(y=i{\mid}y^{*}=j\right)$, denoted
by $p\left(y{\mid}y^{*}\right)$. Here, we assume that the instances of label
noise are data-independent, meaning that
$p\left(y{\mid}y^{*},x\right)=p\left(y{\mid}y^{*}\right)$, in line with
previous work (Northcutt et al., 2021). The label noise function
$h\left(y^{*},\mathcal{C}\right)$ allows for the definition of a
$\mathcal{C}\times\mathcal{C}$ noise distribution matrix, denoted by
$\mathcal{Q}_{y{\mid}y^{*}}$, where each column represents the probability
distribution for an input instance with ground truth label $y^{*}=i$ to be
assigned to label $j$. This matrix captures the inherent uncertainty in the
labeling process and can be used to study the effects of label noise on the
performance of learning algorithms. Based on these particulars, we can
describe label noise through the following statistical parameters: noise level
$n_{l}$ and noise sparsity $n_{s}$.

The label noise level ($n_{l}$) quantifies the extent of inaccurate labels
present in a given data corpus. Intuitively, a noise level of zero corresponds
to a “pristine” dataset, in which all observed labels correspond to their true
labels, while a noise level of one would represent a completely erroneous
dataset. Formally, it is defined as one minus the diagonal sum of the
conditional probability matrix $\mathcal{Q}_{y{\mid}y^{*}}$, denoted as
$n_{l}=1-\operatorname{diag}\left(\mathcal{Q}_{y{\mid}y^{*}}\right)$.
Similarly, the noise sparsity ($n_{s}$) quantifies the structure of label
noise present in a dataset. It is defined as the fraction of zeros in the off-
diagonals of the noise distribution matrix $\mathcal{Q}_{y{\mid}y^{*}}$
(Northcutt et al., 2021). Therefore, a high noise sparsity values indicate a
non-uniformity of label noise, which is common in most real-world datasets.
Specifically, zero noise sparsity corresponds to a random noise, confounding
instances across classes. The special case of ‘class-flipping’ occurs at
$n_{s}=1$, confusing instance pairs.

###  3.2 Problem Setup and Formulation

We consider a general $\mathcal{C}$-way classification as a supervised
learning task that aims to learn a function mapping an input instance
$\mathbf{x}$ to a corresponding ground truth label
$\mathbf{y}_{i}^{*}\in\\{1,\cdots,\mathcal{C}\\}$. The input space is denoted
by $\mathcal{X}=\mathbb{R}^{d}$ and the output space by
$\mathcal{Y}=\\{1,2,...,\mathcal{C}\\}$. The ground truth can also be
formulated as a one-hot encoded vector
$\mathbf{y}_{i}^{*}\in\\{0,1\\}^{\mathcal{C}}$, where $\mathcal{C}$ is the
number of classes. This indicates that the $\mathbf{y}_{i}^{*}$ is a binary
vector of length $\mathcal{C}$, where only one element is 1 and the rest are
0s, representing the true class of the sample $i$ among $\mathcal{C}$ possible
classes. A learner is given access to a set of training data
$\mathcal{D}={(\mathbf{x}_{i},\mathbf{y}_{i})}_{i=1}^{N}$ drawn from an
unknown joint data distribution $\mathcal{P}$ defined on
$\mathcal{X}\times\mathcal{Y}$. A neural network
$f(\mathbf{x};\theta):\mathcal{X}\to\mathbb{R}^{\mathcal{C}}$ minimizes the
empirical risk:

$\displaystyle
R_{\mathcal{L}}(f)=\mathbb{E}_{D}(\mathcal{L}_{\text{CE}}(f(\mathbf{x};\theta),\mathbf{y})),$

where $\theta$ are the parameters of the network, and $\mathcal{L}$ is a loss
function.

Specifically, $f_{y}(\mathbf{x})$ denotes the $y$-th element of
$f(\mathbf{x})$ corresponding to the ground-truth label $\mathbf{y}$. When
$n_{l}\neq 0$, the neural network $f(\mathbf{x};\theta)$ is trained on labels
$\mathbf{y}$, instead of the actual ground-truth labels $\mathbf{y}^{*}$. As a
result, our objective is to design a mitigation strategy that can either
correct noisy labels or provide a way to reduce their impact on the learning
process. Moreover, the ideal solution should maintain consistent performance
for different values of $0\leq n_{l}\leq 1$ to eliminate the need for any
prior assumptions regarding the level and distribution of noise.

###  3.3 Few-shot Human-in-the-Loop Refinement

We introduce Few-shot Human-in-the-Loop Refinement (FHLR), a highly effective
approach to training deep neural networks for sensory (time-series) data with
noisy labels. FHLR enables an efficient way to incorporate a few expert labels
for fine-tuning a seed model and apply weight averaging to merge models in
order to improve generalization. In this section, we describe an end-to-end
pipeline and provide a high-level overview of the approach in Figure 1.

Seed Training with Weak Labels. We begin with bootstrapping a deep model
$f_{\mathcal{B}}(\cdot)$ with noisy labeled data without discarding any
instances. Rather than using strongly labeled data (which may have noise)
directly at this stage, we generate ‘weak labels’ through label smoothing (LS)
(Szegedy et al., 2016), which produces softened one-hot encoded vectors
representing semantic information. These weak labels aid in the initial
training of neural networks, allowing them to learn representations even when
all labels are not high quality. Label smoothing creates weak labels by
replacing hard labels (a single index indicating a class) with softened labels
(a vector of weights that sum to 1, indicating the degree of class
membership).

Formally, for a dataset
$\mathbf{X}=\\{\mathbf{x}_{1},\mathbf{x}_{2},\ldots,\mathbf{x}_{n}\\}$ with
hard labels
$\mathbf{Y}=\\{\mathbf{y}_{1},\mathbf{y}_{2},\ldots,\mathbf{y}_{n}\\}$, label
smoothing creates weak labels
$\mathbf{\tilde{Y}}=\\{\mathbf{\tilde{y}}_{1},\mathbf{\tilde{y}}_{2},\dots,\mathbf{\tilde{y}}_{n}\\}$
by replacing hard labels (a single index $y_{i}\in[1,\ldots,\mathcal{C}]$
indicating a class) with softened labels
$\mathbf{\tilde{y}}i=[\tilde{y}^{1}_{i},\tilde{y}^{2}_{i},\dots,\tilde{y}^{\mathcal{C}}_{i}]$,
where $\sum_{c=1}^{\mathcal{C}}\tilde{y}^{c}_{i}=1$,
$0\leq\tilde{y}^{c}_{i}\leq 1$ indicating degree of membership in classes. For
instance, it’s possible for a person who is walking slowly to have sensor
readings that resemble those of someone who is standing still, which can
result in mislabeling. In such cases, an instance may be labeled as [0.4, 0.6]
instead of hard labeling of [0, 1], due to the ambiguity in the sensor data.
These weak labels preserve semantic relationships while acknowledging
ambiguity and uncertainty in the labels.

To seed train a model, FHLR uses label smoothing via constructing a mixing
matrix $\mathbf{M}$, which is a linear combination of the identity matrix
$\mathbf{I}$ and an all-ones matrix $\mathbf{J}$, controlled by a parameter
$\alpha$ (Lukasik et al., 2020). Specifically,
$\mathbf{M}=(1-\alpha)\cdot\mathbf{I}+\frac{\alpha}{N}\cdot\mathbf{J}$, where
$N$ is the number of classes. The resulting matrix $\mathbf{M}$ is then used
as the target distribution in the categorical cross-entropy loss function
during training, instead of using the one-hot encoded labels. As weight
averaging is one of the central components of FHLR, we also leverage
exponential moving average (EMA) as an additional regularizer (Izmailov et
al., 2018). EMA maintains a running average of the model weights calculated as
a decaying average of previous weights and current iteration weights. This
running average smooths out the rapid fluctuations in weights over the course
of training; making the model less sensitive to the specific instances and
providing robustness against overfitting.

Refinement with Few-shot Label Acquisition. To initiate the fine-tuning phase
of the seed model $f_{\mathcal{B}}(\cdot)$, we propose a human-in-the-loop
mechanism to obtain expert (or clean) labels for a small number of instances,
which is largely cost-effective since only a few examples have to be presented
to a human expert for labeling. Formally, given a dataset $D$ with instances
$(\mathbf{x}_{i},\mathbf{y}_{i})$, we select a subset
$\mathcal{S}\subset\mathcal{D}$ and obtain expert labels
$\mathbf{\widehat{y}}_{i}$ for each instance $\mathbf{x}_{i}\in\mathcal{S}$,
resulting in $\mathcal{D}_{\mathbf{e}}$. These labeled examples can then be
used to adapt the existing pretrained model with EMA as earlier stage. We note
that directly training on a smaller subset of examples result in a model of
subpar quality. Formally, $f_{\mathcal{T}_{\theta}}=\text{Fine-
tune}(f_{\mathcal{B}_{\theta}},\mathcal{D}_{\mathbf{e}},\eta)$, where $\eta$
represents the learning rate during fine-tuning (FT). The use of seed training
with smoothed labels and transfer learning is critical to the success of this
few-shot fine-tuning stage as it help reduce the amount of time and resources
required to learn high-quality model from scratch and enable an effective way
to leverage limited expert-labeled data.

Model Merging. The last phase involves the merge of learned models from
earlier stages, and as such, we propose a simple yet effective approach that
merges the seed $f_{\mathcal{B}_{\theta}}$ and fine-tuned
$f_{\mathcal{T}_{\theta}}$ models into an aggregate one with increased
performance. The key idea is to perform a weighted average of the parameters
of the constituent models to combine them into a unified model. This technique
assumes that the models are structurally identical and share the
initialization, which allows for the direct comparison and averaging of their
parameters.

Formally, let
$\mathcal{F}=\\{f_{\theta_{1}},f_{\theta_{2}},\ldots,f_{\theta_{n}}\\}$ be a
set of $n$ trained neural network models ($n=2$ in our case) with parameters
$\\{\theta_{1},\theta_{2},\ldots,\theta_{n}\\}$ and fixed weights
$\\{w_{1},w_{2},...,w_{n}\\}$ for each model. The parameters of the merged
model $\theta_{\text{merge}}$ are calculated as the weighted summation of the
parameters of the $n$ models:
$\theta_{\text{merge}}=w_{1}\times\theta_{1}+w_{2}\times\theta_{2}+\ldots+w_{n}\times\theta_{n}$.
We perform a simple weighted average based on its success in previous works
(Wortsman et al., 2022). The merged model thereby encapsulates the collective
strengths of all the constituent models $\mathcal{F}$, with their
contributions determined by the fixed predefined weights. The weighting
applied to each model’s parameters also allows us to emphasize a certain model
and subtly adjust the weaker models, yielding a well-balanced combined model
that strikes a balance. Furthermore, averaging the parameters has several
benefits over simply selecting one as it provides a simple and scalable
approach to harnessing an ensemble of models that reduces variability,
resulting in a merged model that is more robust and generalizes better.

Table 1: Performance evaluation of FHLR on different tasks against a range of
baselines. We report accuracy averaged over three trials along with standard
deviation. $n_{l}$ refers to the noise level, where $n_{l}=0$ is clean labeled
data (i.e., original labels provided in the corresponding dataset) and we use
fixed sparsity rate of $n_{s}=0.2$. CE, LS, PL, LC, CL, Bi-T, and FL refers to
cross-entropy, label smoothing, poly loss, logit clip, confident learning, bi-
tempered and focal loss, respectively.

Method | $n_{l}=0.0$ | $n_{l}=0.2$ | $n_{l}=0.4$ | $n_{l}=0.6$
---|---|---|---|---
CE |  79.7 $\pm$ 0.4 |  78.9 $\pm$ 0.7 |  61.3 $\pm$ 2.9 |  30.0 $\pm$ 12.2
LS |  79.3 $\pm$ 0.7 |  80.0 $\pm$ 0.9 |  62.6 $\pm$ 2.3 |  29.6 $\pm$ 13.2
Mixup |  78.7 $\pm$ 0.9 |  79.1 $\pm$ 0.4 |  62.9 $\pm$ 3.6 |  29.3 $\pm$ 12.6
PL |  79.3 $\pm$ 0.2 |  78.6 $\pm$ 1.1 |  62.1 $\pm$ 3.0 |  30.0 $\pm$ 12.2
Bi-T |  76.4 $\pm$ 0.4 |  77.5 $\pm$ 0.8 |  62.9 $\pm$ 5.2 |  27.5 $\pm$ 13.2
LC |  78.7 $\pm$ 1.3 |  79.0 $\pm$ 1.0 |  52.3 $\pm$ 12.6 |  30.2 $\pm$ 12.7
CL |  80.0 $\pm$ 0.5 |  78.9 $\pm$ 2.1 |  62.7 $\pm$ 3.3 |  29.1 $\pm$ 11.6
FL |  78.9 $\pm$ 0.5 |  78.4 $\pm$ 0.8 |  64.7 $\pm$ 2.4 |  29.1 $\pm$ 13.6
FHLR | 80.6 $\pm$ 0.3 | 80.0 $\pm$ 0.6 | 76.9 $\pm$ 1.1 | 74.1 $\pm$ 0.5

(a) Sleep Scoring

Method | $n_{l}=0.0$ | $n_{l}=0.2$ | $n_{l}=0.4$ | $n_{l}=0.6$
---|---|---|---|---
CE |  89.2 $\pm$ 1.5 |  85.6 $\pm$ 2.8 |  70.3 $\pm$ 10.8 |  44.4 $\pm$ 5.1
LS |  89.0 $\pm$ 0.8 |  85.3 $\pm$ 1.4 |  67.6 $\pm$ 11.0 |  36.9 $\pm$ 5.5
Mixup |  87.7 $\pm$ 1.5 |  89.2 $\pm$ 1.6 |  65.1 $\pm$ 10.8 |  39.6 $\pm$ 1.1
PL |  86.4 $\pm$ 1.6 |  84.7 $\pm$ 2.0 |  66.4 $\pm$ 9.6 |  39.3 $\pm$ 4.9
Bi-T |  85.9 $\pm$ 1.0 |  84.2 $\pm$ 2.1 |  68.3 $\pm$ 13.7 |  38.9 $\pm$ 8.1
LC |  85.9 $\pm$ 4.7 |  84.7 $\pm$ 4.7 |  67.0 $\pm$ 14.9 |  36.0 $\pm$ 7.6
CL |  87.7 $\pm$ 1.1 |  87.2 $\pm$ 0.9 |  73.0 $\pm$ 9.7 |  43.3 $\pm$ 7.6
FL |  84.8 $\pm$ 0.6 |  80.5 $\pm$ 3.8 |  64.8 $\pm$ 10.5 |  40.1 $\pm$ 7.2
FHLR | 91.2 $\pm$ 0.5 | 89.2 $\pm$ 0.5 | 85.6 $\pm$ 0.3 | 85.5 $\pm$ 0.4

(b) Activity Recognition

Method | $n_{l}=0.0$ | $n_{l}=0.2$ | $n_{l}=0.4$ | $n_{l}=0.6$
---|---|---|---|---
CE |  92.9 $\pm$ 1.5 |  91.0 $\pm$ 1.6 |  75.2 $\pm$ 2.3 |  25.5 $\pm$ 3.7
LS |  94.1 $\pm$ 0.0 |  87.8 $\pm$ 2.2 |  69.3 $\pm$ 7.6 |  29.2 $\pm$ 3.3
Mixup |  91.9 $\pm$ 1.5 |  86.0 $\pm$ 5.4 |  71.3 $\pm$ 5.3 |  25.9 $\pm$ 5.9
PL |  93.9 $\pm$ 0.2 |  82.0 $\pm$ 4.5 |  68.6 $\pm$ 7.9 |  24.8 $\pm$ 4.2
Bi-T |  90.5 $\pm$ 1.8 |  85.4 $\pm$ 4.8 |  71.1 $\pm$ 3.3 |  26.8 $\pm$ 5.8
LC |  90.9 $\pm$ 0.6 |  84.5 $\pm$ 5.7 |  76.5 $\pm$ 0.5 |  27.0 $\pm$ 2.8
CL |  94.0 $\pm$ 0.3 |  91.7 $\pm$ 1.7 |  80.0 $\pm$ 8.3 |  41.0 $\pm$ 11.6
FL |  91.9 $\pm$ 2.4 |  89.6 $\pm$ 0.7 |  70.3 $\pm$ 3.9 |  27.9 $\pm$ 2.6
FHLR | 94.7 $\pm$ 0.1 | 92.7 $\pm$ 0.7 | 89.3 $\pm$ 1.1 | 83.0 $\pm$ 4.5

(c) Cardiac Arrhythmia

Method | $n_{l}=0.0$ | $n_{l}=0.2$ | $n_{l}=0.4$ | $n_{l}=0.6$
---|---|---|---|---
CE |  84.4 $\pm$ 0.8 |  76.9 $\pm$ 2.6 |  65.2 $\pm$ 6.5 |  29.3 $\pm$ 15.3
LS |  84.3 $\pm$ 0.8 |  77.6 $\pm$ 1.5 |  66.1 $\pm$ 2.3 |  31.4 $\pm$ 10.6
Mixup |  83.0 $\pm$ 0.5 |  77.7 $\pm$ 2.3 |  68.7 $\pm$ 2.6 |  33.2 $\pm$ 17.4
PL |  83.7 $\pm$ 1.9 |  77.4 $\pm$ 1.3 |  63.5 $\pm$ 3.6 |  30.5 $\pm$ 12.0
Bi-T |  80.0 $\pm$ 1.0 |  75.4 $\pm$ 2.0 |  67.2 $\pm$ 1.6 |  33.0 $\pm$ 17.6
LC |  81.8 $\pm$ 1.1 |  75.3 $\pm$ 3.2 |  69.0 $\pm$ 0.5 |  31.0 $\pm$ 8.4
CL |  83.4 $\pm$ 0.3 |  78.8 $\pm$ 0.4 |  66.4 $\pm$ 4.1 |  30.5 $\pm$ 7.6
FL |  82.0 $\pm$ 0.9 |  73.4 $\pm$ 3.2 |  61.7 $\pm$ 5.3 |  30.7 $\pm$ 9.9
FHLR | 86.2 $\pm$ 0.1 | 81.5 $\pm$ 0.8 | 77.5 $\pm$ 1.0 | 72.6 $\pm$ 3.3

(d) Artifact Detection

##  4 Experimental Setup

We conduct an extensive evaluation across different noise profiles on several
publicly available datasets to determine the feasibility of our FHLR method in
comparison with several baselines ranging from regularization techniques to
cross-validation based methods.

###  4.1 Data and Tasks

We focus on a broad range of high-stakes tasks involving health signals
collected from wearables, including IMUs, EEG, and ECG, across four widely
used benchmark datasets. We provide the details of each of the considered
datasets below.

Sleep Scoring (SS). For sleep stage scoring with EEG, we use Physionet Sleep-
EDF dataset (Kemp et al., 2000) consisting of $61$ polysomnograms. The dataset
includes $2$ whole-night sleep recordings of EEGs from FPz-Cz and Pz-Oz
channels, EMG, EOG, and event markers from $20$ subjects. The signals are
provided at a sampling rate of $100$Hz, and sleep experts annotated each
$30$-second segment into eight classes. The classes include Wake (W), Rapid
Eye Movement (REM), N1, N2, N3, N4, Movement and Unknown (not scored). We
applied standard pre-processing to merge N3 and N4 stages into a single class
following the American Academy of Sleep Medicine standards, and removed the
unscored and movement segments. We utilize the Fpz-Cz channel from an initial
study that explored the effect of age on sleep in healthy individuals to
categorize sleep into $5$ classes, i.e., W, REM N1, N2, and N3 (Kemp et al.,
2000).

Activity Recognition (AR). We use the Heterogeneity Human Activity Recognition
(HHAR) dataset (Stisen et al., 2015) to recognize activities in daily living
from IMU signals (i.e., accelerometer and gyroscope) collected from a
smartphone. In total, nine participants performed $6$ activities (i.e.,
biking, sitting, standing, walking, stairs-up, and stairs-down) for five
minutes to obtain balanced class distributions. We employ the IMU signals
collected from smartphones in our experiments and segment them into fixed-size
windows of $400$ samples with $50\%$ overlap and only apply standard mean
normalization to the input.

Cardiac Arrhythmia (CA). For the task of arrhythmia detection, we consider the
Ningbo dataset (Zheng et al., 2022). Since the original data contain multi-
labels of cardiac arrhythmia, we use those samples which only have one
positive class as we focus on multi-class classification tasks. To that end,
we use instances of four classes that have more than three thousand instances,
where the final $4$ classes include atrial flutter, normal sinus rhythm, sinus
bradycardia, and sinus tachycardia. For data pre-processing, we window the ECG
signals into $5$-second segments with no overlap and use signals sampled at
$500$Hz with $12$ channels.

Artifact Detection (AD). We use the TUH Artifact EEG dataset which is part of
the TUH EEG Corpus (Obeid and Picone, 2016) to perform artifact recognition,
e.g., eye movements, which can be useful to decide if the signals are noise-
free for downstream applications. The dataset contains EEG signals recorded at
$250$Hz and annotated clinically into $5$ artifact classes. The TUH EEG Corpus
is the most extensive publicly available corpus comprising of thousands of
subjects and session recordings following the international $10-20$ system. We
use $23$ channels for the 01-tcp-ar EEG reference setup, as per the approach
in (Zanga, 2019). We use segments of length $512$ samples and pad with zeros
where necessary.

Table 2: Comparison of FHLR against prior techniques with asymmetric label noise for a fixed noise level $n_{l}=0.4$. Method | Sleep Scoring | Activity Recognition | Cardiac Arrhythmia | Artifact Detection
---|---|---|---|---
CE |  52.4 $\pm$ 1.7 |  62.0 $\pm$ 7.2 |  59.5 $\pm$ 8.4 |  57.0 $\pm$ 5.4
LS |  54.8 $\pm$ 0.5 |  57.6 $\pm$ 2.7 |  67.8 $\pm$ 2.2 |  54.6 $\pm$ 4.9
Mixup |  47.5 $\pm$ 11.0 |  51.3 $\pm$ 2.2 |  58.3 $\pm$ 3.3 |  57.3 $\pm$ 10.1
PL |  44.8 $\pm$ 10.3 |  53.2 $\pm$ 3.7 |  52.1 $\pm$ 9.6 |  54.7 $\pm$ 8.0
Bi-T |  40.5 $\pm$ 13.9 |  59.1 $\pm$ 2.7 |  59.1 $\pm$ 6.4 |  55.7 $\pm$ 7.1
LC |  46.1 $\pm$ 3.3 |  53.8 $\pm$ 2.6 |  53.7 $\pm$ 9.3 |  62.2 $\pm$ 4.3
CL |  52.0 $\pm$ 12.2 |  57.5 $\pm$ 3.6 |  70.8 $\pm$ 1.5 |  59.6 $\pm$ 7.1
FL |  52.9 $\pm$ 4.7 |  56.6 $\pm$ 0.9 |  62.9 $\pm$ 7.8 |  59.0 $\pm$ 9.3
FHLR | 77.6 $\pm$ 0.6 | 82.2 $\pm$ 2.5 | 90.9 $\pm$ 0.9 | 78.6 $\pm$ 0.6

###  4.2 Implementation Details

We employ a $1$D convolutional architecture that operates on the temporal
input signal. It consists of six repeated convolutional blocks with kernels of
size $8$, $8$, $8$, $6$, $6$, and $4$, filters ranging from $24$, $32$, $64$.
$72$, $96$ and $128$ in each convolutional layer, respectively. We use group
normalization after the convolutional layers with $4$ groups except for the
one after an input layer that has a group equal to the number of input
channels. We apply an ELU activation, max-pooling layers with pool size $8$,
and a stride of $2$ is used after even blocks. To aggregate the features, we
apply global average pooling of convolutional features and a final dense layer
with the number of units matching the classes. We apply L2 regularization with
a coefficient of $10^{-4}$ and a dropout layer after the last convolutional
block with a rate of $0.15$ to prevent overfitting.

We train the model with the Adam optimizer and learning rate of $0.001$ until
convergence on the training set. To generate smooth labels for seed model
training we use a smoothing factor of $\alpha=0.05$. For exponential moving
average of model weights during both FHLR training phases, we use a momentum
of $0.99$. In the refinement phase, we acquire labels for $100$ examples
selected in a stratified manner from an oracle, unless mentioned otherwise. In
the last model merging stage, we apply a weighted average of the seed and
fine-tuned models with the weight value of $w_{\mathcal{B}}=0.15$ for the seed
model in high noise profile and $w_{\mathcal{B}}=0.9$ low noise profiles. The
selection of these values is based on the observation that in case of high
noise it is feasible to stay close to fine-tuned model and vice versa and can
be selected using a validation set. In future work, we aim to investigate a
more principled approach to selecting $w$ that further improves
generalization.

###  4.3 Baselines and Evaluation

We compare our method with several baselines spanning loss correction, data
augmentation, pruning noisy examples via cross-validation and more.
Specifically, we include bi-tempered (Bi-T) loss (Amid et al., 2019), label
smoothing (LS) (Lukasik et al., 2020), mixup (Zhang et al., 2018), poly loss
(PL) (Leng et al., 2022), confident learning (CL) (Northcutt et al., 2021),
logit clip (LC) (Wei et al., 2022), focal loss (FL) (Lin et al., 2017), and
standard cross-entropy (CE) objective. For performance evaluation, we divide
the HHAR and SleepEDF datasets into train and test splits (a $70$:$30$ ratio)
with disjoint user groups and no overlap. For Ningbo and TUH Artifact EEG
datasets, we perform a standard random split. In all cases, we report accuracy
averaged over three independent trials.

##  5 Results

Comparative analysis with baseline methods. We begin the evaluation of our
method by comparing it with several baselines across four tasks in Table 1. We
vary the noise levels from $0$ to $0.6$ while keeping sparsity fixed at $0.2$.
We demonstrate that our method achieves strong performance across all tasks
and noise levels compared to prior techniques. On the sleep scoring task, FHLR
attains $80.6$% accuracy with no noise, outperforming all baselines. More
importantly, it maintains $74.1$% accuracy with a noise level as high as
$0.6$, substantially higher than other baselines, where LC achieves only
$30.2$%. Furthermore, we observe similar trends in activity recognition,
cardiac arrhythmia, and artifact detection tasks. We note that other methods,
including data augmentation and loss correction, suffer substantially as noise
levels increase. On the other hand, FHLR consistently outperforms baselines,
with absolute improvements up to $43$% compared to baselines at $0.6$ noise
level for sleep scoring.

Figure 2: Ablation of different label acquisition strategies.

Robustness to asymmetric label corruption. We next consider the evaluation of
our approach on asymmetric label noise, i.e., when noise sparsity equals one.
In this case, a special case of ‘class-flipping’ occurs, where instances of a
pair of classes are confused (Northcutt et al., 2021). The high sparsity noise
could be attributed to confusion between classes that are perceived as similar
by humans, e.g., mislabeling walking upstairs as walking rather compared to
structurally different activities like sitting or cycling.

Table 2 summarizes the results across four tasks and seven baselines. Our
method achieves the best performance in terms of classification accuracy,
demonstrating its effectiveness in dealing with asymmetric noise. Compared to
the cross-entropy objective, FHLR yields an improvement of $25$% on sleep
scoring, $20$% on activity recognition, $31$% on cardiac arrhythmia and $21$%
on artifact detection. On the other hand, other approaches show limited
robustness against noise with CL achieving $70.8\%$ on cardiac arrhythmia
while being several folds more computationally expensive as well as discarding
valuable data. Similarly, label smoothing on its own is not sufficient,
indicating that its effectiveness is limited to asymmetric label noise.

Effect of expert label acquisition techniques. The few-shot label acquisition
for refinement phase is a central component of our approach. To that end, we
study the impact of different strategies for selecting samples for which we
acquire labels from a human expert or an oracle. We perform evaluation with a
noise level of $n_{l}=0.4$ and sparsity of $n_{s}=0.2$ and compare stratified
(random) sampling with different uncertainty-based techniques, including
entropy, smallest margin, largest margin, and least confidence. Figure 2
presents results across four tasks when only the label acquisition function is
changed while keeping the rest of the components of FHLR fixed. We acquire
labels for $100$ instances as in previous experiments.

Figure 3: Performance improvement with model merging.

To make for a fair comparison with stratified sampling, we select instances
based on classes using labels predicted by the seed model to avoid over-
selection of instances from a particular class. We observe that entropy
performs well compared to other approaches on all tasks except for activity
recognition. In particular choosing examples based on least confident (i.e.,
lowest softmax probability) does not yield selection of quality instances. Our
approach of randomly selecting examples in a class-balanced manner provides
better performance across the board.

Table 3: Comparison of model merging via parameters averaging against ensembles and using Fisher-weighted averaging (Matena and Raffel, 2022). Task | Ensemble | Fisher | Conventional
---|---|---|---
Sleep Scoring | 76.3 $\pm$ 2.1 | 76.5 $\pm$ 2.2 | 76.9 $\pm$ 1.1
Activity Recognition | 83.3 $\pm$ 2.9 | 85.6 $\pm$ 0.6 | 85.1 $\pm$ 2.1
Cardiac Arrhythmia | 90.2 $\pm$ 1.1 | 88.7 $\pm$ 0.5 | 89.3 $\pm$ 1.1
Artifact Detection | 78.3 $\pm$ 1.0 | 76.7 $\pm$ 1.3 | 77.5 $\pm$ 1.0

Effectiveness of model merging. We now study the effect of model merging in
improving generalization under label noise. Figure 3 provides the results of
the evaluation and compares merging with a seed model, fine-tuning with a few
expert labels, and directly training a model from scratch using only a few
labeled examples. Our results highlight that parameter averaging of seed and
fine-tuned models improves performance; demonstrating that simple parameter
averaging is useful in leveraging fine-tuned models and priors from the seed
model to mitigate the effects of label noise.

Figure 4: Ablation of a varying number of shots, i.e., few clean examples.

Power of plain parameter averaging. Table 3 reports the performance of
different techniques to combine the models. On the considered tasks,
conventional parameter averaging performs as well as model ensembles and
Fisher-weighted averaging. For instance, on the sleep scoring task, the
ensemble approach yields $76.3$% accuracy, while Fisher-weighted averaging
achieves $76.5$%. In contrast, our approach, which simply averages model
parameters, attains higher accuracy of $76.9$%. Overall, these results suggest
that ‘conventional’ parameter averaging can be highly effective for merging
deep models than more complex techniques. The conventional approach likely
benefits from preserving more representative parameters through simple
averaging without increasing inference costs as ensembles.

Scaling up expert labels yields better generalization. We next vary the number
of clean labeled examples acquired during the refinement phase. For a noise
level of $n_{l}=0.4$ and sparsity $n_{s}=0.2$, we conduct an experiment to get
labels for randomly selected instances $\mathcal{S}$ as earlier while only
changing the number of examples (or shots). We also compare against the best-
performing baseline from Table 1 (i.e., confident learning for activity
recognition and cardiac arrhythmia) and correct the labels for the same number
of instances. Figure 4 presents the evaluation results indicating that, while
scaling the number of corrected labels consistently improves the performance
of our method, the baseline method does not show a substantial and tangible
performance boost when trained with an equal number of clean samples.

Component-wise analysis validates utility of FHLR. We conduct an ablation to
quantitatively demonstrates the utility of our three-stage method. Table 4
provides the result on artifact detection task for a same configuration as
used for the preceding experiment. Utilizing label smoothing alone results in
$63.8$% accuracy. The addition of exponential moving average provides further
gains to $68.0$%. Fine-tuning model parameters leads to a substantial $10$%
absolute improvement, achieving $74.5$% accuracy. By incorporating proposed
techniques model attains the highest accuracy of $77.5$%, highlighting the
resilience of FHLR in learning under label noise.

Components | Accuracy
---|---
LS | EMA | FT | Merge |
✓ |  |  |  | 63.8 $\pm$ 10.1
✓ | ✓ |  |  | 68.0 $\pm$ 6.7
✓ |  | ✓ |  | 74.5 $\pm$ 1.7
✓ | ✓ | ✓ |  | 76.9 $\pm$ 0.9
✓ |  | ✓ | ✓ | 75.5 $\pm$ 1.6
✓ | ✓ | ✓ | ✓ | 77.5 $\pm$ 1.0
Table 4: Ablating key components of FHLR on the artifact detection task.

Impact of annotators disagreement in refinement stage. We further conduct an
experiment to showcase the effectiveness of FHLR in a more realistic scenario
where there is no single source of ground truth. As is common in wearable
datasets (Sabeti, 2019), multiple annotators have disagreements that can have
an impact on the refinement phase. To study this, we introduced $10$ virtual
annotators (in the refinement phase) by varying the disagreement rate using
the Fleiss Kappa and compared it to our baselines (see Table 1 where
disagreement rate = $0$) for noise level of $0.4$ and sparsity of $0.2$ in
Table 5. Our results demonstrate the practical benefits of FHLR when learning
from datasets that are not straightforward to annotate because they require
domain expertise. The resilience of our method is evident in scenarios
characterized by potential annotator disagreement. Even when confronted with
such variability in the labeling of datasets for sleep scoring and activity
recognition tasks, our approach successfully circumvents catastrophic failure,
maintaining a high level of performance with a minimal decrease of only $2$%.
This indicates that our method ensure reliable model training even under less-
than-ideal conditions.

Task | Disagreement Rate | Accuracy | Fleiss Kappa
---|---|---|---
Sleep Scoring | 0.1 |  76.0$\pm$1.6 | 75.04
0.2 |  75.8$\pm$1.6 | 53.84
Activity Recognition | 0.1 |  82.9$\pm$1.9 | 77.57
0.2 |  80.1$\pm$2.4 | 57.69
Cardiac Arrhythmia | 0.1 |  88.1$\pm$1.4 | 74.07
0.2 |  86.7$\pm$1.5 | 52.49
Artifact Detection | 0.1 |  75.2$\pm$0.9 | 74.30
0.2 |  73.4$\pm$1.2 | 53.39
Table 5: Simulating human expert disagreement in the refinement phase.

##  6 Conclusion

This work proposed FHLR, a novel approach to mitigate the impact of label
noise by learning from weak labels, incorporating human expertise and model
merging. FHLR achieves significantly better generalization compared to several
prior techniques across four tasks. It provides an effective way to overcome
label noise without assumptions on noise distribution or extra components,
using only a modest number of verified labels. This enables building robust
models for health monitoring using wearables in the presence of annotation
noise. Overall, our approach has important implications for advancing deep
learning with noisy labels in various real-world applications.

## References

  * Amid et al. (2019) Ehsan Amid, Manfred KK Warmuth, Rohan Anil, and Tomer Koren.  Robust bi-tempered logistic loss based on bregman divergences.  _Advances in Neural Information Processing Systems_ , 32, 2019.
  * Arpit et al. (2017) Devansh Arpit, Stanisaw Jastrzebski, Nicolas Ballas, David Krueger, Emmanuel Bengio, Maxinder S Kanwal, Tegan Maharaj, Asja Fischer, Aaron Courville, Yoshua Bengio, et al.  A closer look at memorization in deep networks.  In _International conference on machine learning_ , pages 233–242. PMLR, 2017.
  * Cheng et al. (2020) Yong Cheng, Lu Jiang, Wolfgang Macherey, and Jacob Eisenstein.  Advaug: Robust adversarial augmentation for neural machine translation.  In _Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics_ , pages 5961–5970, 2020.
  * Goldberger and Ben-Reuven (2017) Jacob Goldberger and Ehud Ben-Reuven.  Training deep neural-networks using a noise adaptation layer.  In _International conference on learning representations_ , 2017.
  * Han et al. (2019) Jiangfan Han, Ping Luo, and Xiaogang Wang.  Deep self-learning from noisy labels.  In _Proceedings of the IEEE/CVF international conference on computer vision_ , pages 5138–5147, 2019.
  * Izmailov et al. (2018) Pavel Izmailov, Dmitrii Podoprikhin, Timur Garipov, Dmitry Vetrov, and Andrew Gordon Wilson.  Averaging weights leads to wider optima and better generalization.  _arXiv preprint arXiv:1803.05407_ , 2018.
  * Jiang et al. (2018) Lu Jiang, Zhengyuan Zhou, Thomas Leung, Li-Jia Li, and Li Fei-Fei.  Mentornet: Learning data-driven curriculum for very deep neural networks on corrupted labels.  In _International conference on machine learning_ , pages 2304–2313. PMLR, 2018.
  * Jiang et al. (2020) Lu Jiang, Di Huang, Mason Liu, and Weilong Yang.  Beyond synthetic noise: Deep learning on controlled noisy labels.  In _International conference on machine learning_ , pages 4804–4815. PMLR, 2020.
  * Kemp et al. (2000) Bob Kemp, Aeilko H Zwinderman, Bert Tuk, Hilbert AC Kamphuisen, and Josefien JL Oberye.  Analysis of a sleep-dependent neuronal feedback loop: the slow-wave microcontinuity of the eeg.  _IEEE Transactions on Biomedical Engineering_ , 47(9), 2000.
  * Leng et al. (2022) Zhaoqi Leng, Mingxing Tan, Chenxi Liu, Ekin Dogus Cubuk, Jay Shi, Shuyang Cheng, and Dragomir Anguelov.  Polyloss: A polynomial expansion perspective of classification loss functions.  In _International Conference on Learning Representations_ , 2022.
  * Li et al. (2017) Yuncheng Li, Jianchao Yang, Yale Song, Liangliang Cao, Jiebo Luo, and Li-Jia Li.  Learning from noisy labels with distillation.  In _Proceedings of the IEEE international conference on computer vision_ , pages 1910–1918, 2017.
  * Liang et al. (2020) Junwei Liang, Lu Jiang, and Alexander Hauptmann.  Simaug: Learning robust representations from simulation for trajectory prediction.  In _Computer Vision–ECCV 2020: 16th European Conference, Glasgow, UK, August 23–28, 2020, Proceedings, Part XIII 16_ , pages 275–292. Springer, 2020.
  * Lin et al. (2017) Tsung-Yi Lin, Priya Goyal, Ross Girshick, Kaiming He, and Piotr Dollár.  Focal loss for dense object detection.  In _Proceedings of the IEEE international conference on computer vision_ , pages 2980–2988, 2017.
  * Lukasik et al. (2020) Michal Lukasik, Srinadh Bhojanapalli, Aditya Menon, and Sanjiv Kumar.  Does label smoothing mitigate label noise?  In _International Conference on Machine Learning_ , pages 6448–6458. PMLR, 2020.
  * Matena and Raffel (2022) Michael S Matena and Colin A Raffel.  Merging models with fisher-weighted averaging.  _Advances in Neural Information Processing Systems_ , 35:17703–17716, 2022.
  * Menon et al. (2020) Aditya Krishna Menon, Ankit Singh Rawat, Sashank J Reddi, and Sanjiv Kumar.  Can gradient clipping mitigate label noise?  In _International Conference on Learning Representations_ , 2020.
  * Northcutt et al. (2021) Curtis Northcutt, Lu Jiang, and Isaac Chuang.  Confident learning: Estimating uncertainty in dataset labels.  _Journal of Artificial Intelligence Research_ , 70:1373–1411, 2021.
  * Obeid and Picone (2016) Iyad Obeid and Joseph Picone.  The temple university hospital eeg data corpus.  _Frontiers in Neuroscience_ , 10, 2016.
  * Reed et al. (2014) Scott Reed, Honglak Lee, Dragomir Anguelov, Christian Szegedy, Dumitru Erhan, and Andrew Rabinovich.  Training deep neural networks on noisy labels with bootstrapping.  _arXiv preprint arXiv:1412.6596_ , 2014.
  * Ren et al. (2018) Mengye Ren, Wenyuan Zeng, Bin Yang, and Raquel Urtasun.  Learning to reweight examples for robust deep learning.  In _International conference on machine learning_ , pages 4334–4343. PMLR, 2018.
  * Sabeti (2019) Elyas et al. Sabeti.  Signal quality measure for pulsatile physiological signals using morphological features.  _Informatics in medicine unlocked_ , 2019.
  * Shu et al. (2019) Jun Shu, Qi Xie, Lixuan Yi, Qian Zhao, Sanping Zhou, Zongben Xu, and Deyu Meng.  Meta-weight-net: Learning an explicit mapping for sample weighting.  _Advances in neural information processing systems_ , 32, 2019.
  * Song et al. (2019) Hwanjun Song, Minseok Kim, and Jae-Gil Lee.  Selfie: Refurbishing unclean samples for robust deep learning.  In _International Conference on Machine Learning_ , pages 5907–5915. PMLR, 2019.
  * Stisen et al. (2015) Allan Stisen, Henrik Blunck, Sourav Bhattacharya, Thor Siiger Prentow, Mikkel Baun Kjærgaard, Anind Dey, Tobias Sonne, and Mads Møller Jensen.  Smart devices are different: Assessing and mitigatingmobile sensing heterogeneities for activity recognition.  In _Proceedings of the 13th ACM Conference on Embedded Networked Sensor Systems_ , pages 127–140. ACM, 2015.
  * Szegedy et al. (2016) Christian Szegedy, Vincent Vanhoucke, Sergey Ioffe, Jon Shlens, and Zbigniew Wojna.  Rethinking the inception architecture for computer vision.  In _Proceedings of the IEEE conference on computer vision and pattern recognition_ , pages 2818–2826, 2016.
  * Veit et al. (2017) Andreas Veit, Neil Alldrin, Gal Chechik, Ivan Krasin, Abhinav Gupta, and Serge Belongie.  Learning from noisy large-scale datasets with minimal supervision.  In _Proceedings of the IEEE conference on computer vision and pattern recognition_ , pages 839–847, 2017.
  * Wei et al. (2022) Hongxin Wei, Huiping Zhuang, Renchunzi Xie, Lei Feng, Gang Niu, Bo An, and Yixuan Li.  Logit clipping for robust learning against label noise.  _arXiv preprint arXiv:2212.04055_ , 2022.
  * Wortsman et al. (2022) Mitchell Wortsman, Gabriel Ilharco, Samir Ya Gadre, Rebecca Roelofs, Raphael Gontijo-Lopes, Ari S Morcos, Hongseok Namkoong, Ali Farhadi, Yair Carmon, Simon Kornblith, et al.  Model soups: averaging weights of multiple fine-tuned models improves accuracy without increasing inference time.  In _International Conference on Machine Learning_ , pages 23965–23998. PMLR, 2022.
  * Zanga (2019) Alessio Zanga.  Pyeeglab: A simple tool for eeg manipulation, 2019.  URL https://dx.doi.org/10.5281/zenodo.3874461.
  * Zhang et al. (2018) Hongyi Zhang, Moustapha Cisse, Yann N Dauphin, and David Lopez-Paz.  mixup: Beyond empirical risk minimization.  In _International Conference on Learning Representations_ , 2018.
  * Zheng et al. (2021) Guoqing Zheng, Ahmed Hassan Awadallah, and Susan Dumais.  Meta label correction for noisy label learning.  In _Proceedings of the AAAI Conference on Artificial Intelligence_ , 2021.
  * Zheng et al. (2022) J Zheng, H Guo, and H Chu.  A large scale 12-lead electrocardiogram database for arrhythmia study (version 1.0. 0).  _PhysioNet 2022Available online: http://physionet. org/content/ecg-arrhythmia/1.0. 0/(accessed on 23 November 2022)_ , 2022.


# Spin norm and lambda norm

Chao-Ping Dong  School of Mathematical Sciences, Soochow University, Suzhou
215006, P. R. China<EMAIL_ADDRESS>and  Du Chengyu  School of
Mathematical Sciences, Soochow University, Suzhou 215006, P. R. China
<EMAIL_ADDRESS>
###### Abstract.

Given a $K$-type $\pi$, it is known that its spin norm (due to first-named
author) is lower bounded by its lambda norm (due to Vogan). That is,
$\|\pi\|_{\rm spin}\geq\|\pi\|_{\rm lambda}$. This note aims to describe for
which $\pi$ one can actually have equality. We apply the result to tempered
Dirac series. In the case of real groups, we obtain that the tempered Dirac
series are divided into $\\#W^{1}$ parts among all tempered modules with real
infinitesimal characters.

###### Key words and phrases:

lambda norm, spin norm, tempered representations

###### 2010 Mathematics Subject Classification:

Primary 22E46

##  1\. Introduction

Let $G$ be a _linear_ real reductive Lie group which is in the _Harish-Chandra
class_ [5]. That is,

  1. $\bullet$

$G$ has only a finite number of connected components;

  2. $\bullet$

The derived group $[G,G]$ has finite center;

  3. $\bullet$

The adjoint action $\operatorname{Ad}(g)$ of any $g\in G$ is an inner
automorphism of $\mathfrak{g}=(\mathfrak{g}_{0})_{\mathbb{C}}$, where
$\mathfrak{g}_{0}$ is the Lie algebra of $G$.

Let $\theta$ be a Cartan involution of $G$. We assume the subgroup
$K=G^{\theta}$ of fixed points of $\theta$ is a maximal compact subgroup of
$G$. Let $\mathfrak{g}_{0}=\mathfrak{k}_{0}\oplus\mathfrak{s}_{0}$ be the
corresponding Cartan decomposition of $\mathfrak{g}_{0}$. We drop the
subscript for the complexification.

Let $\hat{G}^{\rm temp,o}$ denote the set of irreducible tempered
representations with real infinitesimal character (up to equivalence). Let
$\hat{K}$ denote the set of $K$-types. The following bijection was noted by
Trapa [10], after Vogan’s paper [12].

######  Theorem 1.1.

Let $X$ be any irreducible tempered $(\mathfrak{g},K)$-module with real
infinitesimal character. Then $X$ has a unique lowest $K$-type which occurs
with multiplicity one. Moreover, the map

$\phi:\hat{G}^{\rm temp,o}\to\hat{K}$

defined by taking the lowest $K$-type, is a well-defined bijection.

Motivated by the lambda norm introduced by Vogan [11], the first-named author
introduced spin norm [4] for the classification of _Dirac series_ (i.e.,
irreducible unitary representations of $G$ with non-vanishing Dirac
cohomology). We refer the reader to [6] and references therein for the notion
of Dirac cohomology. It was proven in [4] that the spin norm of a $K$-type
$\pi$ is bounded below by its lambda norm. That is,

(1) $\|\pi\|_{\operatorname{spin}}\geqslant\|\pi\|_{\rm lambda}.$

This inequality turns out to have a nice interpretation in the setting of
Theorem 1.1. Indeed, let $\hat{G}^{\rm temp,d}$ collect the members of
$\hat{G}^{\rm temp,o}$ with non-zero Dirac cohomology. Put

$\hat{K}_{e}:=\\{\pi\in\hat{K}|~{}\|\pi\|_{\operatorname{spin}}=\|\pi\|_{\rm
lambda}\\}.$

######  Theorem 1.2.

_([2])_ The map $\phi$ restricts to $\hat{G}^{\rm temp,d}$ is a bijection onto
$\hat{K}_{e}$. More precisely, any member $\pi\in\hat{G}^{\rm temp,o}$ is a
Dirac series if and only if the inequality (1) becomes an equality on its
unique lowest $K$-type.

Given an arbitrary $K$-type $\pi$, it is not easy to compute neither
$\|\pi\|_{\rm lambda}$ nor $\|\pi\|_{\operatorname{spin}}$. Thus, it is subtle
to detect whether the inequality (1) is strict or not. This note aims to give
a criterion on this aspect. Our main result is Theorem 3.4. The main idea is
to insert an intermediate value between $\|\pi\|_{\rm lambda}$ and
$\|\pi\|_{\operatorname{spin}}$. As an application, our result suggests that
the tempered Dirac series should be separated into $\\#W^{1}$ parts. See (5)
for the definition of $W^{1}$.

The note is outlined as follows: In Section 2, we recall lambda norm and spin
norm. Then we deduce our main result in Section 3. The last section considers
tempered Dirac series.

##  2\. Preliminaries

In this section, we briefly recall the definitions of the spin norm and the
lambda norm.

###  2.1. The lambda norm

We keep the notations $K,G,\mathfrak{k},\mathfrak{s},\theta$, etc as in the
previous section. Let $T$ be a maximal torus of $K$ and $\mathfrak{t}_{0}$ be
the Lie algebra of $T$. Recall that the analytic Weyl group is defined by

$W(\mathfrak{k},\mathfrak{t})=N_{K}(T)/A_{K}(T).$

It acts on the root system $\Delta(\mathfrak{k},\mathfrak{t})$. Fix a choice
of positive roots $\Delta^{+}(\mathfrak{k},\mathfrak{t})$, and define

$R(G):=\\{r\in
W(\mathfrak{k},\mathfrak{t})|r\Delta^{+}(\mathfrak{k},\mathfrak{t})=\Delta^{+}(\mathfrak{k},\mathfrak{t})\\}.$

Given a $K$-type $\pi$, by Lemma 0.1 of [9], the collection of highest weights
of $\pi$ as $\mathfrak{k}$-module is a single orbit of $R(G)$ on $\hat{T}\in
i\mathfrak{t}^{\ast}_{0}$, where $\hat{T}$ is the abelian group of characters
of $T$.

Now given any $K$-type $\pi$, take a highest weight $\mu$ of it. Then $\mu\in
i\mathfrak{t}^{\ast}_{0}$ is dominant integral for
$\Delta^{+}(\mathfrak{k},\mathfrak{t})$. Denote by $\rho_{c}$ the half sum of
all roots in $\Delta^{+}(\mathfrak{k},\mathfrak{t})$. Choose a positive root
system $\Delta^{+}(\mathfrak{g},\mathfrak{t})$ making $\mu+2\rho_{c}$
dominant. Denote by $\rho$ the half sum of all roots in
$\Delta^{+}(\mathfrak{g},\mathfrak{t})$. Let $P$ be the projection map to the
dominant chamber $C(\mathfrak{g})$ corresponding to
$\Delta^{+}(\mathfrak{g},\mathfrak{t})$. Then $\|P(\mu+2\rho_{c}-\rho)\|$ is
independent of the choices of $\mu$ and
$\Delta^{+}(\mathfrak{g},\mathfrak{t})$, cf. Section 1 and Corrollary 2.4 of
[9]. Now we are ready to talk about the lambda norm.

######  Definition 2.1.

([11, 1]) For any $\pi\in\hat{K}$, the lambda norm of $\pi$ is defined to be

(2) $\|\pi\|_{\rm lambda}:=\|P(\mu+2\rho_{c}-\rho)\|,$

where $\mu$ is any highest weight of $\pi$. For any irreducible admissible
$(\mathfrak{g},K)$-module $X$, the lambda norm of $X$ is defined to be

(3) $\|X\|_{\rm lambda}:=\min_{\pi}\|\pi\|_{\rm lambda},$

where $\pi$ runs over all the $K$-types occurring in $X$. A $K$-type $\pi$ is
called a lowest $K$-type of $X$ if it occurs in $X$ and $\|\pi\|_{\rm
lambda}=\|X\|_{\rm lambda}$.

###  2.2. The spin norm

Although the original definition of the spin norm involves the spin module
$S_{G}$ of the Clifford algebra $C(\mathfrak{s})$, our discussion here does
not need a deep understanding of it. Our tool is mainly the root systems and
their Weyl groups.

######  Definition 2.2.

([4]) For any $\pi\in\hat{K}$, its spin norm is defined to be

$\|\pi\|_{\operatorname{spin}}:=\min\|\gamma+\rho_{c}\|,$

where $\gamma$ runs over all the highest weights of the $\tilde{K}$-types in
$\pi\otimes S_{G}$. For any irreducible admissible $(\mathfrak{g},K)$-module
$X$, its spin norm is defined to be

$\|X\|_{\operatorname{spin}}:=\min_{\pi}\|\pi\|_{\operatorname{spin}},$

where $\pi$ runs over all the $K$-types occurring in $X$. We call $\pi$ a spin
lowest $K$-type of $X$ if it occurs in $X$ and
$\|\pi\|_{\operatorname{spin}}=\|X\|_{\operatorname{spin}}$.

##  3\. When is the inequality (1) strict?

We fix a positive root system $\Delta^{+}(\mathfrak{k},\mathfrak{t})$, and
denote the half sum of roots in it by $\rho_{c}$. Let
$W(\mathfrak{g},\mathfrak{t})$ (resp., $W(\mathfrak{k},\mathfrak{t}))$) be the
Weyl group of $\Delta(\mathfrak{g},\mathfrak{t})$ (resp.,
$\Delta(\mathfrak{k},\mathfrak{t})$). Let $C(\mathfrak{k})$ be the closed
dominant Weyl chamber for $\Delta^{+}(\mathfrak{k},\mathfrak{t})$. For any
$\mu\in\mathfrak{t}^{*}$, we use $\\{\mu\\}$ to denote the unique weight in
$C(\mathfrak{k})$ to which $\mu$ is conjugate under the action of
$W(\mathfrak{k},\mathfrak{t})$. Let $\Delta^{+}(\mathfrak{g},\mathfrak{t})$ be
a positive root system of $\Delta(\mathfrak{g},\mathfrak{t})$ containing
$\Delta^{+}(\mathfrak{k},\mathfrak{t})$.

######  Lemma 3.1.

_([4, Lemma 3.5])_ For any $K$-type $\pi$ with a highest weight
$\mu\in\mathfrak{t}^{\ast}$, we have

(4) $\|\mu\|_{\operatorname{spin}}=\min_{w\in
W^{1}}\|\\{\mu-w\rho+\rho_{c}\\}+\rho_{c}\|,$

where

(5) $W^{1}:=\\{w\in W(\mathfrak{g},\mathfrak{t})|wC(\mathfrak{g})\subseteq
C(\mathfrak{k})\\}.$

######  Lemma 3.2.

_([7, §13.3, Lemma B])_ Let $\lambda\in C(\mathfrak{k})$. Then

$\|\lambda+\rho_{c}\|\geqslant\|w\lambda+\rho_{c}\|$

for any $w\in W(\mathfrak{k},\mathfrak{t})$. Moreover, the equality holds if
and only if $\lambda=w\lambda$.

######  Lemma 3.3.

Let $\Delta$ be a root system with Weyl group $W$. Fix a positive set
$\Delta^{+}$ of roots and denote by $\rho$ the half sum of all positive roots.
For any dominant weight $\lambda$, we have the following inequality

(6) $\|\lambda-\rho\|\leqslant\|\lambda-w\rho\|,~{}\forall w\in W.$

Moreover, if $\lambda$ is dominant with respect to $w\Delta^{+}$, we have

$\|\lambda-\rho\|=\|\lambda-w\rho\|$

Otherwise, the inequality (6) is strict.

###### Proof.

We first prove the inequality. Compute the following difference

($\ast$) $\|\lambda-\rho\|^{2}-\|\lambda-w\rho\|^{2}=-2(\lambda,\rho-w\rho).$

A widely known fact is that $\rho-w\rho$ is a sum of positive roots. The
weight $\lambda$ is dominant by assumption. Thus the pairing
$(\lambda,\rho-w\rho)$ is non-negative, and (6) follows.

Now suppose $\lambda$ is dominant with respect to $w\Delta^{+}$. Notice that
the half sum of positive roots with respect to $w\Delta^{+}$ is $w\rho$.
Applying (6) to $\lambda$, $w\Delta^{+}$ and $w\rho$ gives

$\|\lambda-w\rho\|\leqslant\|\lambda-w^{-1}(w\rho)\|=\|\lambda-\rho\|.$

Therefore, (6) becomes an equality in the current setting.

Now suppose $\lambda$ is not dominant with respect to the new positive set
$w\Delta^{+}$. Define

$D_{w}:=\\{\gamma\in\Delta^{-}|\gamma\in w\Delta^{+}\\},$

where $\Delta^{-}=-\Delta^{+}$. It is well-known that

$\rho-w\rho=\sum_{\gamma\in D_{w}}(-\gamma).$

By assumption, $\lambda$ is not dominant with respect to $w\Delta^{+}$. There
must exist $\beta\in w\Delta^{+}$ such that $(\lambda,\beta)<0$. But it cannot
live in $\Delta^{+}$, because $\lambda$ is dominant with respect to
$\Delta^{+}$. As a consequence, $\beta\in D_{w}$. Continuing with ($\ast$), we
have that

$-(\lambda,\rho-w\rho)=-\left(\lambda,\sum_{\gamma\in
D_{w}}(-\gamma)\right)=\left(\lambda,\sum_{\gamma\in
D_{w}}\gamma\right)\leqslant(\lambda,\beta)<0.$

Thus (6) is strict in this case. ∎

Let us state the main result of this section.

######  Theorem 3.4.

Let $\pi$ be an irreducible representation of $K$ with be a highest weight
$\mu$. Choose a positive root system $\Delta^{+}(\mathfrak{g},\mathfrak{t})$
making $\mu+2\rho_{c}$ dominant. Let $C(\mathfrak{g})$ be the closed dominant
Weyl chamber corresponding to $\Delta^{+}(\mathfrak{g},\mathfrak{t})$. Then
the inequality (1) is strict if and only if one of the following conditions
holds:

  1. _(a)_

$\mu+2\rho_{c}$ is irregular for $\Delta(\mathfrak{g},\mathfrak{t})$.

  2. _(b)_

$\mu-w\rho+\rho_{c}\notin C(\mathfrak{k})$ for all $w\in
W(\mathfrak{g},\mathfrak{t})$ such that $\mu+2\rho_{c}\in wC(\mathfrak{g})$.

###### Proof.

Let $P(\cdot)$ be the projection map to the cone $C(\mathfrak{g})$. It
suffices to show that

(7) $\|\pi\|_{\rm
lambda}=\|P(\mu+2\rho_{c}-\rho)\|\leq\|\mu+2\rho_{c}-\rho\|\leq\|\pi\|_{\rm
spin},$

that the first equality happens if and only if (a) holds, and that the second
equality happens if and only if (b) holds.

By the Pythagorean theorem, the first inequality in (7) holds, and it becomes
an equality if and only if $P(\mu+2\rho_{c}-\rho)=\mu+2\rho_{c}-\rho$, which
is equivalent to $\mu+2\rho_{c}-\rho\in C(\mathfrak{g})$. The latter is
equivalent to (a) since $\mu+2\rho_{c}\in C(\mathfrak{g})$ and $\mu+2\rho_{c}$
is integral.

Now let us consider the second inequality in (7). We collect all $w\in
W(\mathfrak{g},\mathfrak{t})$ such that $\mu+2\rho_{c}\in wC(\mathfrak{g})$ as
$W^{1}(\mu)$. Since $\mu+2\rho_{c}\in C(\mathfrak{k})$, it follows that
$W^{1}(\mu)\subseteq W^{1}$. Moreover, the identity element $e\in W^{1}(\mu)$
due to $\mu+2\rho_{c}\in C(\mathfrak{g})$.

Using Lemma 3.1 and 3.2, we have that

(8) $\|\pi\|_{\operatorname{spin}}=\min_{w\in
W^{1}}\|\\{\mu-w\rho+\rho_{c}\\}+\rho_{c}\|\geqslant\min_{w\in
W^{1}}\|\mu-w\rho+2\rho_{c}\|.$

Take $\lambda=\mu+2\rho_{c}$ and
$\Delta^{+}=\Delta^{+}(\mathfrak{g},\mathfrak{t})$ in Lemma 3.3. We have

(9) $\|\mu-w\rho+2\rho_{c}\|\geq\|\mu-\rho+2\rho_{c}\|.$

Furthermore, the inequality (9) is strict when $w\notin W^{1}(\mu)$; yet it is
an equality when $w\in W^{1}(\mu)$. Now the second inequality in (7) follows
from (8) and (9).

Assume (b) holds. For any $w\in W^{1}\setminus W^{1}(\mu)$, one has that

$\|\\{\mu-w\rho+\rho_{c}\\}+\rho_{c}\|\geqslant\|\mu-w\rho+2\rho_{c}\|>\|\mu-\rho+2\rho_{c}\|.$

On the other hand, for all $w\in W^{1}(\mu)$, one has that

$\|\\{\mu-w\rho+\rho_{c}\\}+\rho_{c}\|>\|\mu-w\rho+2\rho_{c}\|=\|\mu-\rho+2\rho_{c}\|.$

The first strict inequality is due to the assumption that
$\mu-w\rho+\rho_{c}\notin C(\mathfrak{k})$ and Lemma 3.2.

Assume (b) does not hold. Then there exists some $w_{0}\in W^{1}(\mu)$ such
that $\mu-w_{0}\rho+\rho_{c}\in C(\mathfrak{k})$. Therefore,

$\|\\{\mu-w_{0}\rho+\rho_{c}\\}+\rho_{c}\|=\|\mu-
w_{0}\rho+2\rho_{c}\|=\|\mu-\rho+2\rho_{c}\|.$

Since we have proven that

$\displaystyle\min_{w\in
W^{1}}\|\\{\mu-w\rho+\rho_{c}\\}+\rho_{c}\|\geq\|\mu-\rho+2\rho_{c}\|,$

we must have $\|\pi\|_{\operatorname{spin}}=\|\mu-\rho+2\rho_{c}\|.$

To sum up, the two inequalities in (7) are controlled by (a) and (b),
respectively. Thus $\|\pi\|_{\operatorname{spin}}>\|\pi\|_{\rm lambda}$
happens if and only if at least one of (a) and (b) holds. ∎

We record an interesting corollary from the above proof.

######  Corollary 3.5.

If $\mu+\rho_{c}-w\rho\in C(\mathfrak{k})$ for some $w\in W^{1}(\mu)$. Then

(10) $\|\mu\|_{\operatorname{spin}}=\|\mu+2\rho_{c}-\rho\|.$

##  4\. Application to tempered Dirac series

We call an irreducible tempered representations with non-zero Dirac cohomology
_a tempered Dirac series_. Combining Theorems 3.4 and 1.2, we have the
following.

######  Theorem 4.1.

Let $X$ be a tempered $(\mathfrak{g},K)$-module with real infinitesimal
character. Let $\pi$ be the unique lowest $K$-type of $X$ which has a highest
weight $\mu$. Then $H_{D}(X)=0$ if and only if

  * _(a)_

$\mu+2\rho_{c}$ is irregular for $\Delta(\mathfrak{g},\mathfrak{t})$; or

  * _(b)_

$\mu-w\rho+\rho_{c}$ is not dominant for
$\Delta^{+}(\mathfrak{k},\mathfrak{t})$ for any $w\in W^{1}(\mu)$.

######  Example 4.2.

In the special case that $W^{1}=\\{e\\}$, which is met for complex Lie groups,
$SL(2n+1,\mathbb{R})$, $SL(n,\mathbb{H})$ and the linear $E_{6(-26)}$, we
always have that $\mu+2\rho_{c}$ is regular for
$\Delta(\mathfrak{g},\mathfrak{t})$. Thus $H_{D}(X)=0$ if and only if
$\mu-\rho+\rho_{c}$ is dominant for $\Delta^{+}(\mathfrak{k},\mathfrak{t})$.

When $\\#W^{1}>1$, pick up two distinct elements $w_{1},w_{2}$ from $W^{1}$
such that $w_{1}C(\mathfrak{g})\cap w_{2}C(\mathfrak{g})$ is a codimension one
facet of $w_{1}C(\mathfrak{g})$. Then condition (a) holds for any $\mu$ such
that $\mu+2\rho_{c}\in w_{1}C(\mathfrak{g})\cap w_{2}C(\mathfrak{g})$. This
suggests that the tempered Dirac series of $G$ should be divided into
$\\#W^{1}$ parts by those irreducible tempered $X$ such that $H_{D}(X)$
vanishes.

From now on, we shall use a circle to stand for a $K$-type, and paint it if
and only if (1) is an equality. Let us see some concrete examples.

######  Example 4.3.

Consider ${\rm SL}(2,\mathbb{R})$, where
$\Delta(\mathfrak{g},\mathfrak{t})=\Delta(\mathfrak{s},\mathfrak{t})=\\{\pm
2\\}$. Then $\\#W^{1}=2$ and $C(\mathfrak{g})\cap sC(\mathfrak{g})=\\{0\\}$,
where $s$ is the non-trivial element in $W^{1}$. Condition (b) does not take
effect here since $\Delta(\mathfrak{k},\mathfrak{t})$ is empty. Thus $\mu=0$
is the unique $K$-type such that $\|\mu\|_{\operatorname{spin}}>\|\mu\|_{\rm
lambda}$, and the tempered Dirac series of $SL(2,\mathbb{R})$ are separated
into two parts. See Figure 1.

-404 Figure 1. Some $K$-types of $SL(2,\mathbb{R})$ (0,0)(4,4)(-4,-4)(4,-4) Figure 2. Some $K$-types of $Sp(4,\mathbb{R})$

######  Example 4.4.

Consider $G=Sp(4,\mathbb{R})$. Let $K=U(2)$ and $T=U(1)\times U(1)$. Thus
$\mathfrak{k}$ has a one-dimensional center. Fix

$\Delta^{+}(\mathfrak{k},\mathfrak{t})=\\{(1,-1)\\},\quad\Delta^{+}(\mathfrak{g},\mathfrak{t})=\\{(1,-1),(2,0),(0,2),(1,1)\\}.$

The corresponding simple roots are $\alpha_{1}=(1,-1)=2\rho_{c}$, and
$\alpha_{2}=(0,2)$. The highest weight of a $K$-type is represented by a pair
of integers $(x,y)$ such that $x\geq y$.

Condition (a) of says that the $K$-types on the three lines $y=1$, $x=-1$ and
$y=-x$ should _not_ be painted. These lines intersect at the point $(-1,1)$,
which is $-2\rho_{c}$. Condition (b) further says that $(1,0)$ and $(0,-1)$
should _not_ be painted. Now Figure 2 suggests that the tempered Dirac series
of $Sp(4,\mathbb{R})$ are separated into four parts.

######  Example 4.5.

Let $G$ be $G_{2(2)}$, the linear split $G_{2}$, which is centerless,
connected, but not simply connected. We adopt the simple roots of
$\Delta^{+}(\mathfrak{g},\mathfrak{t})$ and
$\Delta^{+}(\mathfrak{k},\mathfrak{t})$ as in Knapp [8]. Let $\alpha_{1}$ be
the short simple root and $\alpha_{2}$ be the long one. In this case,
$\Delta(\mathfrak{g},\mathfrak{t})$ is of type ${\rm G_{2}}$, while
$\Delta(\mathfrak{k},\mathfrak{t})$ is of type ${\rm A_{1}\times A_{1}}$. We
fix $\Delta^{+}(\mathfrak{k},\mathfrak{t})=\\{\gamma_{1},\gamma_{2}\\}$, where
$\gamma_{1}:=\alpha_{1}$ and $\gamma_{2}:=3\alpha_{1}+2\alpha_{2}$. Let
$\omega_{1},\omega_{2}$ be the fundamental weights for
$\Delta(\mathfrak{k},\mathfrak{t})$ such that
$(\omega_{i},\alpha_{j}^{\vee})=\delta_{ij}.$ The $K$-types are parameterized
via the highest weight theorem by
$[a,b]:=a\omega_{1}+b\omega_{2},~{}a,b\in\mathbb{Z}_{\geqslant 0}$ such that
$a+b$ is even.

We show some of the $K$-types in Figure 3, where the $a$-coordinates of the
bottom line are $0,2,4,6,8,\dots$, and so are the $b$-coordinates of the left-
most column.

Now condition (a) says that $K$-types on the two lines $a=b$ and $a=3b+4$
should _not_ be painted. These two lines intersect at $[-2,-2]=-2\rho_{c}$.
From Figure 3, one sees that the tempered Dirac series are divided into three
parts by the two lines. Condition (b) further says that $[2,0]$ should _not_
be painted.

To sum up, we have recovered Corollary 8.4 of [3].

[0,0][0,4][22,0] Figure 3. Some $K$-types of the linear split $G_{2}$

Funding

Dong is supported by the National Natural Science Foundation of China (grant
12171344).

## References

  * [1] J. Carmona, _Sur la classification des modules admissibles irréductibles_ , pp.11–34 in Noncommutative Harmonic Analysis and Lie Groups, J. Carmona and M. Vergne, eds., Lecture Notes in Mathematics 1020, Springer-Verlag, New York, 1983.
  * [2] J. Ding and C.-P. Dong, _Spin Norm, K-Types, and Tempered Representations_ , J. Lie Theory 26 (2016), 651–658.
  * [3] J. Ding, C.-P. Dong, and L. Yang, _Dirac series for some real exceptional Lie groups_ , J. Algebra 559 (2020) 379–407.
  * [4] C.-P. Dong, _On the Dirac cohomology of complex Lie group representations_ , Transform. Groups 18 (2013), 61-79. [Erratum: Transform. Groups 18 (2013), 595–597.]
  * [5] Harish-Chandra, _Harmonic analysis on real reductive Lie groups. I. The theory of the constant term_ J. Funct. Anal. 19 (1975), 104–204.
  * [6] J.-S. Huang and P. Pandžić, _Dirac cohomology, unitary representations and a proof of a conjecture of Vogan_ , J. Amer. Math. Soc. 15 (2002), 185–202.
  * [7] J. E. Humphreys, _Introduction to Lie Algebras and Representation Theory_ , Springer-Verlag, New York, 1972.
  * [8] A. Knapp, _Lie Groups, Beyond an Introduction, 2nd edition_ , Birkhäuser, 2002.
  * [9] S. Salamanca-Riba and D. Vogan, _On the classification of unitary representations of reductive Lie groups_ , Ann. of Math. 148 (1998), 1067–1133.
  * [10] P. Trapa, _A parametrization of $\hat{K}$ (after Vogan)_, Notes from an AIM workshop, July 2004.
  * [11] D. Vogan, _Representations of Real Reductive Groups_ , Birkhäuser, 1981.
  * [12] D. Vogan, _Unitarizability of certain series of representations_ , Ann. of Math. 120 (1984), 141–187.


# Generating Safe Autonomous Decision-Making in ROS

Yi Yang Tom Holvoet imec-DistriNet
Dept. of Computer Science
KU Leuven
B-3001 Leuven, Belgium<EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract

The Robot Operating System (ROS) is a widely used framework for building
robotic systems. It offers a wide variety of reusable packages and a pattern
for new developments. It is up to developers how to combine these elements and
integrate them with decision-making for autonomous behavior. The feature of
such decision-making that is in general valued the most is safety assurance.

In this research preview, we present a formal approach for generating safe
autonomous decision-making in ROS. We first describe how to improve our
existing static verification approach to verify multi-goal multi-agent
decision-making. After that, we describe how to transition from the improved
static verification approach to the proposed runtime verification approach. An
initial implementation of this research proposal yields promising results.

##  1 Introduction

Autonomous systems have the ability to make decisions to achieve predefined
goals without human or other guidance or control. As such, the heart of
autonomous systems is their autonomous decision-making. Throughout this
article, we use an autonomous mobile robot as an example. This autonomous
mobile robot is set to have specific goals, some prior knowledge of the world,
and safety specifications. Ideally, it should autonomously make decisions that
allow the system to achieve its goals while fully adhering to all provided
safety specifications. The most important requirements for autonomous
decision-making are effective behaviors and safety assurance.

The Robot Operating System (ROS) [22] is a collection of software libraries
and tools for developing robot applications. Due to its distinctive
features—modularity, extensive functional libraries, and open source, ROS has
become the most well-known framework for constructing robotic systems. In ROS,
a number of frequently used functions, including navigation, manipulation, and
locomotion, have been carefully developed as reusable packages. These
functions can be deployed by engineers, thereby reducing the burden of
development. Notably, the most well-developed functions are the implementation
of robotic actions, yet there is still significant space for advancement in
the decision-making of robots.

The safety of autonomous systems mainly refers to safe decision-making in
autonomous systems. For decision-making, we are studying agent programming
languages [23]. Compared with other agent programming languages, GOAL [14] is
particularly well suited for programming autonomous decision-making, because
it generates decisions during execution rather than relying on predefined plan
specifications. Formal verification is a convincing approach for providing
safety assurance of high-confidence systems [24]. Formal verification can be
categorized into static verification and runtime verification. Static
verification verifies the given properties of all possible runs of a program,
while runtime verification monitors one execution of a program and verifies
properties at runtime [2].

This is a research preview that outlines a well-defined research idea of
generating safe autonomous decision-making for autonomous systems developed
using ROS, combining ROS, decision-making, and formal verification. The
research idea is based on our static verification approach for verifying
autonomous decision-making. We have two contributions: first, we explain how
to improve the existing static verification approach to verify multi-goal
multi-agent decision-making; second, we describe how to transition from the
static verification approach to the runtime verification approach. The paper
is structured as follows. In Section 2, we introduce the related work to our
work. In Section 3, we briefly explain how to improve our static verification
approach to verify multi-goal multi-agent autonomous decision-making. In
Section 4, we introduce the rationale, the initial design of the architecture
of a decision-making node, and the analysis of the proposed runtime
verification approach for generating safe autonomous decision-making in ROS.
In Section 5, we draw conclusions and indicate future work.

##  2 Related Work

While model checking is popular in verifying agent programming languages [5]
[12], model checking is not a prevalent approach in verifying GOAL. GOAL has
many features in common with BDI APLs [9], but it focuses on logical
derivation, making it ideal for deductive verification. The inventors of GOAL
proposed the first verification framework for GOAL in [4]. This paper
demonstrates how to conduct verification for GOAL programs. [17] implemented
the verification framework proposed in [4] using Isabelle [21]. Isabelle’s
implementation provides high confidence for the verification framework, but
has limitations: first, it can only specify a subset of GOAL programs, with
only a single agent, a single goal, propositional features, and no
communication; second, it lacks an automated verification process, so users
have to be familiar with Isabelle.

As no well-developed ROS package for generating decision-making is widely
accepted by most users, decision-making remains a challenging issue in ROS. In
general, there are two approaches to generating decision-making in ROS:
providing a decision-making node in ROS, and connecting an agent programming
language to ROS.

The conventional approach to generating decision-making in ROS is to provide a
decision-making node. Both packages, i.e. [7] and [20], support the generation
of decisions in ROS. Both packages do not use formal verification to generate
decisions. In other words, neither of these two packages can ensure that ROS
will generate safe decisions. Moreover, the decision-making generation
procedures in both packages are problem-dependent, i.e., each unique problem
necessitates a unique implementation of the decision-making generation
process, which adds to the development difficulties for users.

For the purpose of programming complex decision-making, agent programming
languages have been developed. Many efforts have been made to provide safety
assurance for the generated decisions by agent programming languages [4] [5]
[12] [15]. By integrating an agent programming language with ROS, the
decision-making in ROS can benefit from the existing research findings on
agent programming languages.

[6] presents an interface for the Gwendolen agent programming language [11] to
communicate with ROS. Moreover, the AJPF model checker [12] is used to verify
the properties of the decisions generated by the Gwendolen language.
Therefore, the interface makes the generation of verified decisions feasible
in ROS. However, no performance comparison has been conducted between the
presented approach in [6] and the traditional approach. Rosbridge [8] is the
primary tool used to implement the interface, but Rosbridge is particularly
designed for facilitating web applications with ROS [8]. The connection of an
agent programming language to ROS is not quite in accordance with the design
intent of Rosbridge, which may result in certain performance concerns. [19]
describes a generic multi-layer architecture based on ROS-JADE integration for
autonomous transport vehicles. The cognitive layer of the proposed multi-layer
architecture is essentially a ROS-JADE node, serving as a communicating
function between ROS and JADE [3]. This paper focuses on the generic multi-
layer architecture instead of the details of the cognitive layer. The
validation of real settings and the efficiency issues remain for their future
work. Considering the architectural design of the ROS-JADE node, it lacks
safety assurance.

As a lightweight verification approach, runtime verification is usually
considered ideal to provide safety assurance for complicated systems, such as
robotic applications. Many runtime verification frameworks have been proposed,
such as ROSRV [16] and ROSMonitoring [13]. ROSRV and ROSMonitoring provide
safety assurance for autonomous systems by intercepting those messages that
violate safety requirements.

##  3 Static Verification

Our prior work [25] serves as the foundation for the proposed research idea.
GOAL sets itself apart from the majority of agent programming languages due to
the automated decision-making process. This distinctive feature was the
primary factor in our decision to adopt it as the instrument to program
autonomous decision-making. [25] is the initial proposal for verifying
autonomous decision-making by imposing single-goal and single-agent
restrictions on the GOAL program. [25] presents a justified algorithm
transforming a stratified GOAL program for a single agent and a single goal to
its equivalent transition system, equivalent in terms of operational
semantics. We now briefly describe how to substantially advanced the work
presented in [25] by removing these constraints on GOAL programs. The proposed
static verification approach is presumably to verify multi-goal multi-agent
decision-making in GOAL.

FO LogicPropertyConstraintSent MsgActionReceived MsgSubstate
UpdateSpecificationEncodingPrism ModelTS Generation Figure 1: Automated
translator for GOAL (Architecture)

Figure 1 shows the architecture of the automated translator. The automated
translator consists of two main modules: transition system (TS) Generation and
Encoding. The input of the automated translator is the specifications of a
multi-agent system that can be specified with GOAL. The output of the
automated translator is a Prism model. The automated translator transforms the
specifications into its operational-semantically equivalent Prism model that
can be directly processed by two efficient probabilistic symbolic model
checkers: Storm [10] and Prism [18].

The specification language is an extended version of the specification
language provided in [25]. The specification language is inherited from the
the formalization of the syntax and semantics of the internal logic of GOAL.
The first-order (FO) logic used for the formalization can properly represent
the essential characteristics of GOAL programs, including durative actions,
multiple goals, multiple agents, and agent communication. The FO logic
employed for the formalization serves as a specification language. The
specification language can properly specify a multi-agent system in a modular
way. We point out that the specification language is suitable for expressing
the decision-making generating processes of autonomous systems in addition to
GOAL programs. In other words, the specification language can be used to
specify the decision-making generating process rather than GOAL. The
specifications can be categorized as system-level specifications and agent-
level specifications. System-level specifications include knowledge base,
communication rules, event processing rules, action generation rules, domains
for multi-variables, and constants. Agent-level specifications describe the
belief bases and the goal base of an agent.

The crucial step of verifying GOAL programs is the transformation from the
GOAL programs to an operational-semantically equivalent transition system. We
briefly explain the key concepts of the transformation. In GOAL, the mental
state of an agent is a pair consisting of its beliefs and goals [4]. For a
GOAL program for a multi-agent system with n agents, each agent has its own
mental state. The state of the GOAL program is an n-tuple, whose element is a
substate. Precisely, the mental state of an agent is a substate of the GOAL
program for a multi-agent system. Each mental state is associated with
substate properties. This property is the minimal model of the FO theory
consisting of the beliefs and the knowledge base. Based on the logical
derivation and the minimal model generation, feasible decisions are generated.
A generated decision of a GOAL program is mapped to an action of the
transition system. Executed decisions can modify the mental state of an agent.
We can conclude that a GOAL program only generates safe decision-making if the
generated operational-semantically equivalent transition system satisfies all
given safety properties. This is predicated on the assumption that the
specification of the GOAL program properly renders the internal logic of the
GOAL program. Notably, we use the automated decision-making mechanism to
implement the transformation, and the key components of the automated
decision-making mechanism are automated logical derivation and minimal model
generation. Instead of being problem-dependent, the decision-making generation
is logic-dependent, which makes it easier for users to conduct verification.

##  4 Runtime Verification Approach

###  4.1 Rationale

The improved static verification approach can provide autonomous systems with
the result of PCTL model checking analysis. Assuming that the specifications
accurately represent the internal logic of the autonomous decision-making, the
static verification approach offers advanced verification results, including
convincing safety assurance for the decision-making generation process.
However, the static verification approach suffers from certain inherent
limitations, such as processing real-time information and the state-space
explosion. Based on the existing static verification approach, we propose a
runtime verification approach to complement the existing static verification
approach. The main component of the proposed runtime verification approach is
a decision-making node in ROS. We draw attention to the fact that the runtime
verification of autonomous decision-making can benefit from the specification
language of the automated translator and the automated decision-making
generation.

Comparison | Static Verification | Runtime Verification
---|---|---
DM Generation | Same | Same
Specification language | Same | Same
Specification Provider | User | User and Sensor
State Space | All States | One State
Analysis | PCTL model checking | Safety Checking
Table 1: Comparison

In summary, Table 1 presents a comparison between the improved static
verification approach and the proposed runtime verification approach. Both
approaches share the same implementation of the decision-making generation,
and they use the same specification language as the input. Users should
provide all specifications in the static verification approach, whereas users
and sensors provide all specifications in the runtime verification approach.
While the runtime verification approach only generates one state at a time,
the static verification approach always generates the entire state space.
While the static verification approach can perform PCTL model checking, the
proposed runtime verification approach only checks the safety at runtime. As
the existing static verification approach cannot handle real-time information,
this will raise safety concerns at runtime. As a complementary approach, the
proposed runtime verification approach focuses on safety checking.

###  4.2 Architecture for a Decision-Making Node

Figure 2 presents the architecture for the decision-making node in ROS. For a
multi-agent system, the decision-making node is expected to generate real-time
safe decisions.

Data ProcessingSpecificationSensor$Agent_{1}$$Agent_{n}$FO
LogicPropertyCurrent StateConstraintSent MsgActionReceived MsgUpdated
StateUpdated PropertySafety CheckingDM NodeSafe Safe Unsafe  Figure 2:
Decision-Making Node (Architecture)

Using a multi-agent system consisting of n agents, we demonstrate the
similarities and differences between the improved static verification approach
and the proposed runtime verification approach.

In terms of the specification language, these system-level specifications are
predefined by users in both the static verification approach and the runtime
verification approach. However, the agent-level specifications are differently
provided in these two approaches. Users and sensors provide the agent-level
specifications in the static verification approach and the runtime
verification approach, respectively.

The static verification approach and the runtime verification approach share
the same implementation of the decision-making generation, but they also
contain many modifications to state-space generation and verification. In
terms of state-space generation, the entire state space is generated at once
via the static verification approach. Specifically, the static method
generates every agent decision that could be made to move the system from the
initial state to the desired state. The runtime verification approach, on the
other hand, only generates one decision at a time, moving from the current
state to the following state. In terms of verification, the static
verification approach employs probabilistic model checking, using the existing
efficient model checkers to verify the properties of the whole state space.
The runtime verification approach, on the other hand, merely uses invariant
checking while benefiting from intrinsically generated properties during the
decision-making generation. As in the static verification approach, each
substate is automatically associated with its property. The property checking
of the decision-making node can be as simple as checking that all safety
specifications are contained in the substate property. The time complexity of
this invariant-checking operation is anticipated to be $O(1)$.

Real-time data processing is the key difference between the static
verification approach and the runtime verification approach. Real-time data
cannot be processed by the static verification method, but they can be
processed by the runtime verification approach. Sensors send the decision-
making node the real-time beliefs and goals of the agents within the multi-
agent system. The decision-making generation module anticipates the ground
predicates that the sensor data has been transformed into by the data
processing module. The decision-making node generates real-time decisions
based on real-time beliefs and goals. Real-time information will presumably be
beneficial for decision-making generation for more accuracy.

###  4.3 Analysis

As the first attempt to transition the static verification approach to the
runtime verification approach, the proposed runtime verification approach is
expected to be a complementary approach to the improved static verification
approach. The main core of the runtime verification approach can hugely
benefit from the implementation of the static verification approach. The
proposed approach can provide safety assurance at runtime, and it does not
suffer from the state-space explosion.

In our setting, each multi-agent system only facilitates one decision-making
node, and the decision-making node can only make sequential decisions.
Presumably, parallelism could be a bottleneck of the proposed runtime
verification approach.

Furthermore, we point out one important issue in the runtime verification
approach. We need to generate a transformation between the high-level
decision-making and low-level abilities of autonomous agents to enable
communication between the decision-making node. The granularity of the
decision-making should be properly designed. If the granularity is too high,
the decision-making node has to handle too much data, which will incur
unnecessary computational costs and reduce the efficiency of generating
decisions. If the granularity is too low, the decision-making node has
insufficient control over the autonomous agents.

##  5 Conclusion and Future Work

This paper provides a research preview on how to generate safe autonomous
decision-making in ROS. In summary, the proposed runtime verification will be
achieved by a two-stage extension of our existing static verification
approach. First, we describe how to extend our existing static verification
approach to verify multi-goal multi-agent autonomous decision-making. Second,
we explain how to transition the improved static verification approach to the
proposed runtime verification approach. The main component of the runtime
verification approach is a decision-making node. We provided an overview of
the architecture of the decision-making node. The decision-making node is
expected to generate safe decisions at runtime. We also mentioned that
parallelism could be the possible bottleneck of the proposed runtime
verification.

We have implemented the initial version of the improved static verification
approach, and we validated the initial implementation through two case
studies. Our case studies are based on the GOAL source code, provided in the
GOAL example project Tower and Coffee of the Eclipse plugin for GOAL.
Moreover, we point out that the development of the decision-making node can
hugely benefit from the existing implementation of the static verification
approach, because they share the same implementation of the decision-making
generation. Notably, the static verification approach generates all feasible
states from the initial state to the desired state at a time, whereas the
runtime verification approach only generates the following state. The static
verification approach requires the probabilistic model checking of the whole
state space, while the runtime verification approach only requires invariant
checking. Therefore, the runtime verification approach is expected to have
better performance concerning efficiency than the static verification
approach. Initial tests confirm this assumption, yet a thorough analysis will
have to validate our hypothesis.

We will fully implement the proposed runtime verification approach in the near
future. After that, we will use a multi-agent system consisting of three
autonomous mobile robots to validate the improved static verification approach
and the runtime verification approach. We also plan to prove the correctness
of our implementation of the decision-making node in the future.

## Acknowledgements

This research is partially funded by the Research Fund KU Leuven.

## References

  * [1]
  * [2] Wolfgang Ahrendt, Gordon J Pace & Gerardo Schneider (2012): _A unified approach for static and runtime verification: framework and applications_.  In: International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Springer, pp. 312–326, 10.1007/978-3-642-34026-0_24.
  * [3] Fabio Bellifemine, Federico Bergenti, Giovanni Caire & Agostino Poggi (2005): _JADE—a java agent development framework_.  In: Multi-agent programming, Springer, pp. 125–147, 10.1007/0-387-26350-0_5.
  * [4] Frank S de Boer, Koen V Hindriks, Wiebe van der Hoek & J-J Ch Meyer (2007): _A verification framework for agent programming with declarative goals_.  Journal of Applied Logic 5(2), pp. 277–302, 10.1016/j.jal.2005.12.014.
  * [5] Rafael H Bordini, Michael Fisher, Carmen Pardavila & Michael Wooldridge (2003): _Model checking agentspeak_.  In: Proceedings of the second international joint conference on Autonomous agents and multiagent systems, pp. 409–416, 10.1145/860575.860641.
  * [6] Rafael C Cardoso, Angelo Ferrando, Louise A Dennis & Michael Fisher (2020): _An interface for programming verifiable autonomous agents in ROS_.  In: Multi-Agent Systems and Agreement Technologies, Springer, pp. 191–205, 10.1007/978-3-642-38700-5_3.
  * [7] Cogniteam (2019): _Decision Making Package_.  Available at http://wiki.ros.org/decision_making.
  * [8] Christopher Crick, Graylin Jay, Sarah Osentoski, Benjamin Pitzer & Odest Chadwicke Jenkins (2017): _Rosbridge: Ros for non-ros users_.  In: Robotics Research, Springer, pp. 493–504, 10.1007/978-3-319-29363-9_28.
  * [9] Lavindra De Silva, Felipe Rech Meneguzzi & Brian Logan (2020): _BDI agent architectures: A survey_.  In: Proceedings of the 29th International Joint Conference on Artificial Intelligence (IJCAI), 2020, Japão., 10.24963/ijcai.2020/684.
  * [10] Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen & Matthias Volk (2017): _A storm is coming: A modern probabilistic model checker_.  In: International Conference on Computer Aided Verification, Springer, pp. 592–600, 10.1007/978-3-662-49674-9_8.
  * [11] Louise A Dennis & Berndt Farwer (2008): _Gwendolen: A BDI language for verifiable agents_.  In: Proceedings of the AISB 2008 Symposium on Logic and the Simulation of Interaction and Reasoning, Society for the Study of Artificial Intelligence and Simulation of Behaviour, Citeseer, pp. 16–23.  Available at https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.141.1549&rep=rep1&type=pdf.
  * [12] Louise A Dennis, Michael Fisher, Matthew P Webster & Rafael H Bordini (2012): _Model checking agent programming languages_.  Automated software engineering 19(1), pp. 5–63, 10.1007/s10515-011-0088-x.
  * [13] Angelo Ferrando, Rafael C Cardoso, Michael Fisher, Davide Ancona, Luca Franceschini & Viviana Mascardi (2020): _ROSMonitoring: a runtime verification framework for ROS_.  In: Annual Conference Towards Autonomous Robotic Systems, Springer, pp. 387–399, 10.1023/A:1022920129859.
  * [14] Koen V Hindriks (2009): _Programming rational agents in GOAL_.  In: Multi-agent programming, Springer, pp. 119–157, 10.1016/S0004-3702(00)00079-5.
  * [15] Gerard J. Holzmann (1997): _The model checker SPIN_.  IEEE Transactions on software engineering 23(5), pp. 279–295, 10.1016/B978-0-444-89874-6.50028-3.
  * [16] Jeff Huang, Cansu Erdogan, Yi Zhang, Brandon Moore, Qingzhou Luo, Aravind Sundaresan & Grigore Rosu (2014): _ROSRV: Runtime verification for robots_.  In: International Conference on Runtime Verification, Springer, pp. 247–254, 10.1007/978-3-319-11164-3_20.
  * [17] Alexander Birch Jensen, Koen V Hindriks & Jørgen Villadsen (2021): _On Using Theorem Proving for Cognitive Agent-Oriented Programming_.  In: 13th International Conference on Agents and Artificial Intelligence, Science and Technology Publishing, pp. 446–453, 10.5220/0010349504460453.
  * [18] Marta Kwiatkowska, Gethin Norman & David Parker (2002): _PRISM: Probabilistic symbolic model checker_.  In: International Conference on Modelling Techniques and Tools for Computer Performance Evaluation, Springer, pp. 200–204, 10.1007/3-540-46029-2_13.
  * [19] Jon Martin, Oskar Casquero, Brais Fortes & Marga Marcos (2018): _A generic multi-layer architecture based on ROS-JADE integration for autonomous transport vehicles_.  Sensors 19(1), p. 69, 10.1023/A:1020975419546.
  * [20] Joao Messias (2015): _Markov Decision Making Package_.  Available at http://wiki.ros.org/markov_decision_making.
  * [21] Tobias Nipkow, Lawrence C Paulson & Markus Wenzel (2002): _Isabelle/HOL: a proof assistant for higher-order logic_.  2283, Springer Science & Business Media, 10.1007/3-540-45949-9_3.
  * [22] Morgan Quigley, Ken Conley, Brian Gerkey, Josh Faust, Tully Foote, Jeremy Leibs, Rob Wheeler, Andrew Y Ng et al. (2009): _ROS: an open-source Robot Operating System_.  In: ICRA workshop on open source software, 3, Kobe, Japan, p. 5.  Available at http://robotics.stanford.edu/~ang/papers/icraoss09-ROS.pdf.
  * [23] Yoav Shoham (1993): _Agent-oriented programming_.  Artificial intelligence 60(1), pp. 51–92, 10.1016/0004-3702(93)90034-9.
  * [24] Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui & John Fitzgerald (2009): _Formal methods: Practice and experience_.  ACM computing surveys (CSUR) 41(4), pp. 1–36, 10.5555/3065491.3065655.
  * [25] Yi Yang & Tom Holvoet (2022): _Making Model Checking Feasible for GOAL_.  In: 10th International Workshop on Engineering Multi-Agent Systems.  Available at https://emas.in.tu-clausthal.de/2022/papers/paper4.pdf.