# Lighting and Rotation Invariant Real-time Detector Based on YOLOv5: Vehicle
Wheel Detector

Michael Shenoda  College of Computing & Informatics
Drexel University
Philadelphia, PA, United States
<EMAIL_ADDRESS>
###### Abstract

Creating an object detector, in computer vision, has some common challenges
when initially developed based on Convolutional Neural Network (CNN)
architecture. These challenges are more apparent when creating model that
needs to adapt to images captured by various camera orientations, lighting
conditions, and environmental changes. The availability of the initial
training samples to cover all these conditions can be an enormous challenge
with a time and cost burden. While the problem can exist when creating any
type of object detection, some types are less common and have no pre-labeled
image datasets that exists publicly. Sometime public datasets are not reliable
nor comprehensive for a rare object type. Vehicle wheel is one of those
example that been chosen to demonstrate the approach of creating a lighting
and rotation invariant real-time detector based on YOLOv5 architecture. The
objective is to provide a simple approach that could be used as a reference
for developing other types of real-time object detectors.

##  I Introduction

Surprisingly humans are really good at understanding visual content of an
image and instantly provide information about the objects within.
Unfortunately, this task is a hard problem in computer vision. Since 2012
Convolutional Neural Network (CNN) has became so popular for object detection
and classification tasks, but yet the challenges to create reliable models can
get overwhelming. Looking at the YOLO architecture, it has taken a leap
forward as being the architecture of choice for real-time detectors. The
original version of YOLO was designed for real-time object detection as
primary focus. Then the latest version YOLOv5 has retained the same focus with
the simplification of the development process of creating custom models with
the power of image augmentation techniques. It provides the ability to
visualize metrics, and get insights of changes made on each model update using
integration with Weights and Biases machine learning tool. While the end
result of a well designed model works well in terms of performance and
accuracy, the amount of initial development can be daunting. The objective in
this paper is to outline a general guideline to achieve a model that can be
adaptive to lighting and rotation changes with minimal initial images samples.
These guidelines are being presented with a practical example by implementing
a model that is capable of detecting vehicle wheels in images captured with
various camera orientations, and lighting conditions. After getting an
overview of the YOLOv5 architecture and methodology, the basic approach is
summarized as series of steps that can be easily followed:

1\. Understand the immediate use case of the detector.
2\. Select the model size of YOLOv5 for the detector.
3\. Understand the relationship of the object to the surroundings and how to
propose specific views captured to optimize the visual appearance of the
object.
4\. Collect initial image samples to cover the various camera orientations and
lighting conditions.
5\. Train the initial model with the initial image samples, with weights
transferred from an existing YOLOv5 model, then evaluate.
6\. Collect 3D synthetic images to cover the variety of visual appearances of
the object and also covers various rotations.
7\. Use ground truth labels extracted from the 3D models, if available. Or use
initial model to pre-label the 3D synthetic images, then manually review them
to remove any false positives and fine tune any bounding box as necessary.
8\. Train the model with the 3D synthetic images with weights transferred from
initial training session then evaluate
9\. Collect sample images from publicly available image datasets that
represents the desired views of the object with various lighting conditions.
10\. Use previous model to pre-label the public image samples, then manually
review them to remove any false positives and fine tune any bounding box as
necessary.
11\. Train the model with the public image samples with weights transferred
from previous training session then evaluate
12\. Finally the model should be sufficient to automatically label images
collected specifically for the use case.

Figure 1: The Proposed General Guideline for Model Development

The work presented here is a humble approach towards a simple way to develop a
custom model that can be easily prototyped and speed up the effort of creating
an initial model that is reliable enough for providing machine labeled images
with minimal manual review. The main goal is to allow the machine learning
engineer to carefully craft the initial model than can be used later on to
automatically label images for a non-technical person to manually review and
perform any refinement to the bounding boxes.

##  II Overview of YOLOv5

YOLO is one of the best architecture and family of object detection models
providing sate of the art performance with its focus on real-time detection
and classification. YOLO for stands for You Only Look Once. The initial
YOLO[1] was created by Joseph Redmon and later published YOLOv2[2] and
YOLOv3[3] papers. Joseph’s work was further advanced by Alexey Bochkovskiy who
has published YOLOv4 in 2020. [4] YOLOv5, created by Ultralytics, is a family
of object detection architectures and models pretrained on the COCO dataset
that represents their open-source research into computer vision AI methods,
and incorporating lessons learned and best practices. It is a continuation on
the great work that has been initially developed in the earlier versions[5].
It’s important to note that YOLOv5 is built using PyTorch while previous
YOLOv4 was built using Darknet. Using the PyTorch approach has simplified the
development since it uses python by default.

The YOLOv5 model structure consists of two main blocks and the overall
architecture is shown below:

Figure 2: YOLOv5 architecture overview

The model consists of two parts, Backbone and Head. Backbone is responsible
for extracting low level features using convolutional layers in combination
with Spatial Pixel Pair Features (SPPF) layer.
Head is responsible for extracting the high level feature maps and performing
the detections, applying anchor boxes on the feature maps to generate the
final output vector of classes probabilities and bounding boxes.

The YOLOv5 models originally came in four different sizes which are small,
medium, large, and xlarge. The size of the model depends on the complexity of
the detection and classification task. Recent version 6.0 has introduced the
nano size which was primarily developed to be very lightweight to fit ultra
small devices.

Figure 3: YOLOv5 model size comparison

The nice aspect about YOLOv5 that models are defined declaratively using yaml
configuration files. Yaml configuration describes the model definition without
the need to programmatically define it in Python. This aspect makes it superb
for rapid model development. The other powerful aspect of YOLOv5 is the image
augmentation capability that it provides, especially when starting with very
small number of samples.

It’s important to note when training custom dataset, a new model file needs to
be created for the detector. One of the important parameters is the number of
classes. In this case, we need to set to 1 for a simple detector of single
object type like vehicle wheel.

##  III Proposed General Guideline of Model Development

###  III-A Understanding the use case

The proposed wheel detector has direct use case of providing vehicle axle
count that can be used in application such as traffic analysis, and tolling
systems. The end goal is to provide a reliable method of detecting the vehicle
wheels regardless of camera orientation and lighting conditions.

Figure 4: Wheel Detector Use Case

###  III-B Model Size Selection

Based on the published performance of the different YOLOv5 model sizes, the
medium size has been chosen for the wheel detector to provide a good
combination of accuracy and performance. The medium size model definition file
has been copied from the original yolov5m.yaml then modified the number of
classes to be 1, since dealing with a single type.

Another important consideration during model selection is the available GPU
and the training input image size. The GPU used in this case is Nvidia GeForce
RTX 3050 Ti with available dedicated GPU memory of 4 GB. I choose 512x512
image size based on initial testing on what can be fit in the available GPU
memory. By default YOLOv5 uses a square size for the input and I decided to
keep it that way. The reason behind that is the uncertainty of the image size
for the final use case of the detector. In this case, square input size
minimizes the amount of pixel padding that needs to be added to a vertical or
horizontal rectangular image thus maximizing the image content. Of course, if
the final image size is known, it will be optimized to build a detector with
input size that matches the aspect ratio of final deployment image size.

Figure 5: Reason for Using Square Detector Input Size Figure 6: Reason for Not
Using Rectangular Detector Input Size

###  III-C Understanding Visual Appearance of Object

The appearance of the wheel can vary based on the camera orientation and
different wheel types based on different vehicle types. Also, the positioning
of the wheel while the vehicle is turning left or right. Collection of images
to be able to cover from simple camera angles to complex scenarios. In
addition, images samples should be collected to cover various image capturing
quality. For example, samples need to cover low resolution, blurriness, and
environmental changes such as fog, harsh sun light, harsh shadows, etc.

Considering the simple camera angles of straight on 90 degree, angled 45
degree, and steep angled 20 degrees as shown in the following figure:

Figure 7: Simple Camera Angles

Considering the complex scenarios where the wheel could be occluded, partially
visible, blurred, or ultra steep angle. Here are some of the examples:

Figure 8: Complex Scenarios to Consider

###  III-D Training Initial Model and Evaluation

Initial image samples have been manually captured to cover various camera
orientation as well as slight shadows and sun light conditions. Total initial
samples are 72 images, below are some of the images to visualize.

Figure 9: Initial Image Samples Part1 (total of 49 samples) Figure 10: Initial
Image Samples Part2 (total of 23 samples)

The initial image samples have been manually labeled using LabelImg [7], a
python tool for labeling images using bounding boxes that supports YOLO
bounding box format. YOLO label format for an object is defined as the
following:
(object-class) (x) (y) (width) (height)
object-class is a numerical index of the object class, which in out case it’s
0, for single object.
x and y represent the object center and are expressed as relative pixel
position.
width and height represent the width and height of the object, and expressed
as relative size.
It uses relative pixel position and relative size to accommodate different
scaling of the image without worrying about absolute numbers [1].

Figure 11: Image Labeling using LabelImg

The initial model has been trained with the following parameters:
input size = 512
batch size = 4
model weights = yolov5m.pt
validation spit ratio = 0.22

Let’s evaluate the initial model starting with the metrics:

Figure 12: Initial Model Training Object Loss Figure 13: Initial Model
Training Box Loss Figure 14: Initial Model Validation Object Loss Figure 15:
Initial Model Validation Box Loss Figure 16: Initial Model Mean Average
Precision Figure 17: Initial Model F1 and Precision vs Recall Curves

The metrics looks reasonable for the initial training. The training and
validation loss seems consistent, but the mean average precision is only
hovering around 0.8. Let’s check the detection performance on random samples
from validation set.

Figure 18: Initial Model Detection on Validation Set

The model does good job of detecting the wheels on the validation set. Before
getting overexcited, we need to consider that the validation set is not far
off from how the training set looks visually. We will need to test how the
model would perform on the 3D synthetic images, which weren’t part of the
training yet. That should give a better insight of how the model would behave
on images that it hasn’t seen before during the training.

Figure 19: Initial Model Detection on 3D Synthetic Images

We can clearly see that the model has false positive on other parts of the
vehicles. It detects truck mirror as a wheel and also mud flap of the semi
truck. Also, some of the bounding boxes are not precisely localizing the
wheel.

###  III-E Training with Synthetic Images and Evaluation

3D synthetic image samples have been collected to cover various camera
orientation with the goal of providing different varieties of vehicle wheel
shapes. Total synthetic samples collected 165 images. Below are some of the
images to visualize. The 3D synthetic images here are just yet another 2D
images that were gathered from Hum3D [8]. Ideally, we would use ground the
truth labels wheel labels extracted from the 3D model and unnecessary for
labeling those images by machine or human. Unfortunately, due to lack of time
for learning a 3D simulation software that provides such capabilities, such as
Carla Simulator, I decided to not to pursue that route. In this case, the
wheel have been automatically labeled by machine using the initial model then
manually reviewed and corrected using LabelImg [7] annotation tool.

Figure 20: 3D Synthetic Images

The model has been trained with 3D synthetic images added to the initial
sample images with the following parameters:
input size = 512
batch size = 6
model weights = last.pt, from previous training session
validation spit ratio = 0.22
Let’s evaluate the model starting with the metrics:

Figure 21: (3D Synthetic Images) Training Object Loss Figure 22: (3D Synthetic
Images) Training Box Loss Figure 23: (3D Synthetic Images) Validation Object
Loss Figure 24: (3D Synthetic Images) Validation Box Loss Figure 25: (3D
Synthetic Images) Mean Average Precision Figure 26: (3D Synthetic Images) F1
vs Confidence and Precision vs Recall

The metrics looks better. The training and validation loss seems consistent,
and the mean average precision is getting up to the 0.9 ranges
Let’s check the detection performance on random samples from validation set.

Figure 27: (3D Synthetic Images) Detection Validation Set

The model has improved and the validation looks good. Now, let’s test on some
of the next image samples that are collected from CompCars [9] public dataset.

Figure 28: (3D Synthetic Images) Detection on CompCars Images

Overall, the detection is looking good in terms of bounding box accuracy, but
there are some miss detection and false positives. It seems like the false
positives are shapes that looks like wheel and reflective dark gray ground
that has same color shade as the vehicle tire!

###  III-F Training with added Public Images and Evaluation

The public datasets that have been selected are CompCars and OpenImages. I
decided to start with CompCars, since it has a comprehensive dataset that
contains 163 car makes with 1,716 car models [9] as well as combination of
different roads with nature and buildings. The ability to get comprehensive
set of vehicles is ideal to get variety of vehicle wheel shapes. Also,
CompCars provide a close up view of the cars which makes it ideal for the
model to learn more details about the different wheels introduced.
Total of 827 images have been manually selected from CompCars to machine label
them using the previous trained model then manually verified by LabelImg.
Below are some of the image examples from CompCars:

Figure 29: CompCars Image Samples

The model has been trained with CompCars images added to the previous sample
images with the following parameters:
input size = 512
batch size = 6
model weights = last.pt, from previous training session
validation spit ratio = 0.22

Let’s evaluate the model starting with the metrics:

Figure 30: CompCars Model Train Object Loss Figure 31: CompCars Model Train
Box Loss Figure 32: CompCars Model Validation Object Loss Figure 33: CompCars
Model Validation Box Loss Figure 34: CompCars Detection on Random Validation
Set

The model has performed well on the validation set.
Then tested the model with CompCars on some of the samples from OpenImages to
check the detection performance.

Figure 35: CompCars Model Testing on OpenImages Samples

It seems that the detection results are inconsistent. I decided to choose
OpenImages as the next image set for training, since it contains some real
examples that are visually close to the final use case of the detector. The
total number of samples from OpenImages are 179 images that have been machine
labeled using the previous trained model. Manual review has been done on the
automatically labeled images. It seems that the model gets better every time
with less manual edits needed to be made.

Figure 36: OpenImages Samples

The model has been trained with the samples from OpenImages added to the
previous sample images with the following parameters:
input size = 512
batch size = 6
model weights = last.pt, from previous training session
validation spit ratio = 0.22

Let’s evaluate the model starting with the metrics:
This time will be comparing the metrics from OpenImages and CompCars in same
plots so we can get better insight since they are getting very close to each
other.

Figure 37: OpenImages and CompCars mAP Figure 38: OpenImages and CompCars
Train Object Loss Figure 39: OpenImages and CompCars Train Box Loss Figure 40:
OpenImages and CompCars Validation Object Loss Figure 41: OpenImages and
CompCars Validation Box Loss

Looking at those plots and trying to understand what just happened, it was an
aha moment. The metrics all of the sudden started to look bad. Mean average
precision has dropped. The interesting insight here is the bounding box loss.
We can clearly see OpenImages has gotten worse than CompCars. At the same
time, the actual object loss has remained very similar to each other. That’s
where I realized that my samples from OpenImages contains very small vehicle
sizes and their wheels are obviously too small after scaling down the image to
512 pixels during the training. Those small bounding boxes can encounter
rounding issues at that small scale of 512 input size. This especially
magnified with rectangular image sizes that are far from the aspect ratio of a
square. That’s when I came to realization that I need to crop the OpenImages
to vehicle size region of interest in order to maximize the wheel size in the
image. I utilized the existing YOLOv5 model to do the detection and save the
cropped images based on the bounding boxes of the detection with
classification of bus, car, truck, and others. Every other type of object has
been used as negative samples with empty label files.

Before I proceeded with my theory, I decided to test the detector on
completely different image found to mimic the final ideal use case for the
detector.

Figure 42: Model with OpenImages Model Test on Rectangular Full Image

A good example here if we look at the white van, highlighted with red arrow on
the full view rectangular image, we can see how the localization has loose
bounding box around the wheels.

Figure 43: Model with OpenImages Test on Cropped Image

After comparing the same vehicle on the cropped view, we can clearly see that
the localization of the wheels have tight bounding boxes. This clearly
explains why the object loss plot looked better than the box loss plot.

The next approach is to remove the full resolution sample images then train
the model with cropped objects views extracted from the full images. Total
cropped images are 1157 that got machine labeled and manually reviewed.

Finally, the model has been trained with the samples from OpenImages cropped
added to the previous sample images, with the full view removed. The following
parameters used for the training:
input size = 512
batch size = 6
model weights = last.pt, from previous training session
validation spit ratio = 0.22

Let’s evaluate the model and check the metrics:
Again, we will be comparing the metrics from OpenImages, CompCars, and
OpenImage-crop in same plots so we can get better insight since they are
getting really close to each other.

Figure 44: OpenImages-Crop Model mAP Figure 45: OpenImages-Crop Model Train
Object Loss Figure 46: OpenImages-Crop Model Train Box Loss Figure 47:
OpenImages-Crop Model Train Object Loss Figure 48: OpenImages-Crop Model Train
Box Loss

We can clearly see that the model has improved with the cropped images from
OpemImages dataset. This confirms the theory once more with evidence based on
the metrics.

###  III-G Final Model Evaluation

Let’s put everything into prospective and look the all metrics from all
iterations.

Figure 49: Wheel Model All mAP Figure 50: Wheel Model Train Object Loss Figure
51: Wheel Model Train Box Loss Figure 52: Wheel Model Validation Object Loss
Figure 53: Wheel Model Validation Box Loss

Based on the metrics evaluation, the model seem to be in a good stage. It’s
time to test with image samples that resemble the final use case of the model.
Based on the detection testing results, the model has performed very well and
the images are showing in the Final Model Testing Results section.

##  IV Limitations and Future Improvements

The main limitation of this model is the input square size. For the final
inference, you should try to stay close to a square image as possible. The
advice here is to build a model that is optimized for the final deployment
image size and transfer the weights from this model to your final optimized
model. Future work would include the ground truth wheel labels extracted from
3D simulation such as CARLA [11] or other type of 3D simulator based on the
type of objects of interest. Future improvement or addition to this work is
the ability to provide semantic segmentation for the detector.

##  V Conclusion

In conclusion, the vehicle wheel detector model has reached a reliable phase
that is a good starting point for further improvement for a final deployment
use case. We can clearly see the benefit of an iterative analytical approach
of building a deep neural network model. Crafting the model in an iterative
approach can give the insights needed to correct mistakes early on in the
model development. It’s important to try to understand how the model behavior
changes with addition of samples and how metrics and visual validation can be
a key to create a reliable model. The guideline proposed to create the vehicle
wheel detector is intended to be used as a future reference for creating any
kind of detector.

##  VI Final Model Testing Results

Figure 54: Final Model Test 1 Figure 55: Final Model Test 2 Figure 56: Final
Model Test 3 Figure 57: Final Model Test 4 Figure 58: Final Model Test 5
Figure 59: Final Model Test 6 Figure 60: Final Model Test 7 Figure 61: Final
Model Test 8 Figure 62: Final Model Test 9 Figure 63: Final Model Test 10
Figure 64: Final Model Test 11 Figure 65: Final Model Test 12

## References

  * [1] J. Redmon, S. Divvala, R. Girshick and A. Farhadi, ”You Only Look Once: Unified, Real-Time Object Detection,” 2016 IEEE Conference on Computer Vision and Pattern Recognition (CVPR), 2016, pp. 779-788, doi: 10.1109/CVPR.2016.91.
  * [2] Redmon, Joseph and Ali Farhadi. “YOLO9000: Better, Faster, Stronger.” 2017 IEEE Conference on Computer Vision and Pattern Recognition (CVPR) (2017): 6517-6525.
  * [3] Redmon, Joseph and Ali Farhadi. “YOLOv3: An Incremental Improvement.” ArXiv abs/1804.02767 (2018): n. pag.
  * [4] Bochkovskiy, Alexey et al. “YOLOv4: Optimal Speed and Accuracy of Object Detection.” ArXiv abs/2004.10934 (2020): n. pag.
  * [5] YOLOv5 in PyTorch https://github.com/ultralytics/yolov5
  * [6] Xu, Renjie et al. “A Forest Fire Detection System Based on Ensemble Learning.” Forests 12.2 (2021): 217. Crossref. Web.
  * [7] LabelImg is a graphical image annotation tool and label object bounding boxes in images https://github.com/tzutalin/labelImg
  * [8] Hum3D.com, a ParaART, LLC company
  * [9] The Comprehensive Cars (CompCars) dataset
  * [10] Open Images Dataset V6
  * [11] CARLA https://carla.org/


* Mino [2003] Y. Mino, Perturbative approach to an orbital evolution around a supermassive black hole, Phys. Rev. D 67, 084027 (2003), arXiv:gr-qc/0302075 .
  * Sago  _et al._ [2005] N. Sago, T. Tanaka, W. Hikida, and H. Nakano, Adiabatic radiation reaction to the orbits in Kerr spacetime, Prog. Theor. Phys. 114, 509 (2005), arXiv:gr-qc/0506092 .
  * Isoyama  _et al._ [2019] S. Isoyama, R. Fujita, H. Nakano, N. Sago, and T. Tanaka, “Flux-balance formulae” for extreme mass-ratio inspirals, PTEP 2019, 013E01 (2019), arXiv:1809.11118 [gr-qc] .
  * Gal’tsov [1982] D. Gal’tsov, Radiation reaction in the Kerr gravitational field, J. Phys. A: Math. Gen. 15, 3737 (1982).
  * Bourg  _et al._ [tionb] P. Bourg, A. Pound, and S. D. Upton, Simple, efficient method of calculating the Detweiler–Whiting singular field to very high order (in preparationb).
  * Friedlander  _et al._ [1998] F. G. Friedlander, G. Friedlander, M. S. Joshi, M. Joshi, and M. C. Joshi,  _Introduction to the Theory of Distributions_ (Cambridge University Press, 1998).
  * Penrose [1965] R. Penrose, Zero rest-mass fields including gravitation: asymptotic behaviour, Proceedings of the Royal Society of London. Series A. Mathematical and physical sciences 284, 159 (1965).
  * Mädler and Winicour [2016] T. Mädler and J. Winicour, Bondi-Sachs Formalism, Scholarpedia 11, 33528 (2016), arXiv:1609.01731 [gr-qc] .
  * Grant and Moxon [2022] A. M. Grant and J. Moxon, Flux-balance laws in scalar self-force theory, arXiv preprint arXiv:2209.13829 (2022).
  * Bini and Damour [2016] D. Bini and T. Damour, Conservative second-order gravitational self-force on circular orbits and the effective one-body formalism, Phys. Rev. D 93, 104040 (2016), arXiv:1603.09175 [gr-qc] .
  * Bini  _et al._ [2019] D. Bini, T. Damour, and A. Geralico, Novel approach to binary dynamics: application to the fifth post-Newtonian level, Phys. Rev. Lett. 123, 231104 (2019), arXiv:1909.02375 [gr-qc] .
  * Albertini  _et al._ [2022] A. Albertini, A. Nagar, A. Pound, N. Warburton, B. Wardell, L. Durkan, and J. Miller, Comparing second-order gravitational self-force, numerical relativity, and effective one body waveforms from inspiralling, quasicircular, and nonspinning black hole binaries, Phys. Rev. D 106, 084061 (2022), arXiv:2208.01049 [gr-qc] .
  * Chrzanowski [1976] P. L. Chrzanowski, Applications of metric perturbations of a rotating black hole: Distortion of the event horizon, Physical Review D 13, 806 (1976).
  * Price  _et al._ [2007] L. R. Price, K. Shankar, and B. F. Whiting, On the existence of radiation gauges in Petrov type II spacetimes, Classical and Quantum Gravity 24, 2367 (2007).


# A Logic for Repair and State Recovery in Byzantine Fault-tolerant Multi-
agent Systems

Hans van Ditmarsch111University of Toulouse, CNRS, IRIT Krisztina Fruzsa222TU
Wien, Austria. PhD student in the FWF doctoral program LogiCS (W1255) and also
supported by the FWF project DMAC (P32431). Roman Kuznets333TU Wien, Austria.
Funded by the FWF ByzDEL project (P33600) Ulrich Schmid444TU Wien, Embedded
Computing Systems Group, Austria.

###### Abstract

We provide a novel epistemic logical language and semantics for modeling and
analysis of byzantine fault-tolerant multi-agent systems, with the intent of
not only facilitating reasoning about the agents’ fault status but also
supporting model updates for repair and state recovery. Besides the standard
knowledge modalities, our logic provides additional agent-specific hope
modalities capable of expressing that an agent is not faulty, and also dynamic
modalities enabling change to the agents’ correctness status. These dynamic
modalities are interpreted as model updates that come in three flavours: fully
public, more private, and/or involving factual change. Tailored examples
demonstrate the utility and flexibility of our logic for modeling a wide range
of fault-detection, isolation, and recovery (FDIR) approaches in mission-
critical distributed systems. By providing complete axiomatizations for all
variants of our logic, we also create a foundation for building future
verification tools for this important class of fault-tolerant applications.

##  1 Introduction and Overview

#### State of the art.

The epistemic analysis of distributed systems via the runs-and-systems
framework [bookof4, HM90, Mos15TARK] was also extended [PKS19:TR,
KPSF19:FroCos, KPSF19:TARK] to _fault-tolerant_ distributed systems with
_byzantine_ agents [lamport1982byzantine]. Byzantine agents555The term
‘byzantine’ is not always used consistently in the literature. In some
instances, agents were called byzantine despite exhibiting only restricted
(sometimes even benign [DworkM90]) types of faults. In those terms, agents
considered in this paper would be called ‘fully byzantine.’ constitute the
worst-case scenario in terms of fault-tolerance: not only can they arbitrarily
deviate from their respective protocols, but their perception of own actions
and observed events can be corrupted, possibly unbeknownst to them, resulting
in false memories. Whether byzantine agents are actually present in a system
or not, the very possibility of their presence has drastic and debilitating
effects on the epistemic state of all agents, including the correct (i.e.,
non-faulty) ones, due to their inability to rule out so-called _brain-in-a-
vat_ scenarios [PutnamBrainBook]: a brain-in-a-vat agent is a faulty agent
with completely corrupted perceptions that provide no reliable information
about the system [KPSF19:FroCos]. In such a system, _no_ agent can ever know
certain elementary facts, such as their own or some other agent’s correctness,
no matter whether the system is asynchronous [KPSF19:FroCos] or synchronous
[schlogl2020persistence]. Agents can, however, sometimes know their own
faultiness or obtain belief of some other agents’ faultiness [SS23:TARK].

Since knowledge is hence often impossible to achieve in systems with byzantine
agents, [KPSF19:FroCos] also introduced a weaker epistemic notion called
_hope_. It was initially defined as

$H_{i}\varphi\colonequals\mathit{correct_{i}}\rightarrow
K_{i}(\mathit{correct_{i}}\rightarrow\varphi),$

where the designated atom $\mathit{correct_{i}}$ represents agent $i$’s
correctness. In this setting, one can define belief as
$B_{i}\varphi\colonequals K_{i}(\mathit{correct_{i}}\rightarrow\varphi)$
[SS23:TARK]. Hope was successfully used in [FKS21] to analyze the _Firing
Rebels with Relay_ (FRR) problem, a simplified version of the _consistent
broadcasting_ primitive [ST87], which has been used as a pivotal building
block in distributed algorithms, e.g., for byzantine fault-tolerant clock
synchronization [DFPS14:JCSS, FS12:DC, RS11:TCS, ST87, WS09:DC], synchronous
consensus [ST87:abc], and as a general reduction of distributed task
solvability in systems with byzantine failures to solvability in systems with
crash failures [MTH14:STOC].

Although the hope modality was already axiomatized in [Fru19:ESSLLI], the
special nature of $\mathit{correct_{i}}$ precluded the resulting logic from
being a normal modal logic. In [hvdetal.aiml:2022], an alternative complete
axiomatization for hope was introduced, in which the designated atoms denoting
correctness of individual agents were replaced by

$\mathit{correct_{i}}\colonequals\neg H_{i}\bot$.

This facilitated the definition of a joint logic combining $\mathsf{KB4}_{n}$
hope modalities with the $\mathsf{S5}_{n}$ knowledge modalities, which is
normal and where one can formalize some of the main properties of byzantine
fault-tolerant distributed systems, including bounds on the number of
byzantine agents, as frame-characterizable axioms.

Whereas the resulting logic is well-suited for modeling and analyzing classic
byzantine fault-tolerant distributed computing problems like FRR, where once
faulty an agent remains faulty, this is not the case for distributed systems
where faulty agents may become correct again. Indeed, solutions for problems
like FRR employ _fault-masking techniques_ based on replication [Sch90], which
prevent the adverse effects of the faulty agents from contaminating the
behavior of the correct agents but do not attempt to change the behavior of
the faulty agents. Unfortunately, fault masking is only feasible if at most
some fraction $f$ of the overall $n$ agents in the system may become faulty
(e.g., $n\geq 3f+1$ in the case of FRR). Should it ever happen that more than
$f$ agents become faulty in a run, no properties can typically be guaranteed
anymore, which would be devastating in mission-critical applications.

_Fault-detection, isolation, and recovery_ (FDIR) is a different fault-
tolerance technique, which attempts to discover and repair agents that became
faulty in order to subsequently re-integrate them into the system. The primary
target here are permanent faults, which do not go away “by itself” after some
time but rather require explicit corrective actions. Pioneering fault-tolerant
systems implementations like MAFT [KWFT88] and GUARDS [PABB99] combined fault-
masking techniques like byzantine agreement [lamport1982byzantine] and FDIR
approaches to harvest the best of both worlds.

Different paradigms have been proposed for implementing the different steps in
FDIR. Fault-detection could be done by a central FDIR unit that is implemented
in some very reliable technology and oversees the whole distributed system.
The single point of failure provided by such a central FDIR unit is avoided in
the alternative distributed FDIR, which employs distributed diagnosis [WLS97],
e.g., is based on evidence [AR89], and is typically combined with byzantine
consensus [lamport1982byzantine] to ensure agreement among the replicated FDIR
units. Agents diagnosed as faulty are subsequently forced to reset and execute
built-in self tests, possibly followed by repair actions like hardware
reconfiguration. At a very abstract level, the FDI steps of FDIR cause a
faulty agent to become correct again, in the sense that from that point it
would start faithfully executing its protocol based on its current local state
and the information it receives in the future.

Whereas the above FDI steps cause a faulty agent to become correct again,
this, however, is not enough to enable the agent to participate correctly in
the (on-going) execution of the remaining system. The latter also requires a
successful _state recovery_ step R, which makes the local state of the agent
consistent w.r.t. the current global system state. Many different recovery
techniques have been proposed for this purpose, ranging from pro-active
recovery [Rus96] where the local state of _every_ agent is periodically
replaced by a majority-voted version, to techniques based on checkpointing &
rollback or message-logging & replay, see [EAWJ02] for a survey. The common
aspect of all these techniques is that the local state of the recovering agent
is changed based on the information originating from other agents.

#### Our contribution.

In this paper, we provide the first logic that not only allows to reason about
the fault status of agents, but also provides mechanisms for updating the
model so as to change the fault status of agents, as well as their local
states. Instead of handling such dynamics in the byzantine extension of the
runs-and-systems framework [PKS19:TR, KPSF19:FroCos, KPSF19:TARK], i.e., in a
temporal epistemic setting, we do it in a dynamic epistemic setting: we
restrict our attention to the instants where the ultimate goal of (i) the FDI
steps (successfully repairing a faulty processor) and (ii) the R step
(recovering the repaired processor’s local state) is reached, and investigate
the dynamics of the agents’ correctness/faultiness and its interaction with
knowledge at these instants. This approach allows us to separate the issue of
verifying the correctness of the specification of an FDIR mechanism from the
problem of guaranteeing the correctness of its protocol implementation, and
focus on the former.

Among the additional advantages of our approach are simplicity and clarity of
exposition: instead of large (typically infinite) temporal epistemic models
encountered in runs-and-systems modeling, our approach relies on (often
finite) snapshots of the relevant epistemic information encoded in flat,
static Kripke models as the input and the output of our updates. It is also
worth mentioning, that if the dynamics is a function of the static information
only, as it is in our case, we do not gain expressivity (because the formulas
with dynamic modalities can be rewritten to equivalent formulas in the
underlying logical language with no such modalities). Note that this is the
case in many dynamic epistemic logics, such as public announcement logic
[plaza:1989, gerbrandyetal:1997] and action model logic [baltagetal:1998,
hvdetal.del:2007]. Other kinds of dynamics than change of correctness can be
envisaged, such as change of knowledge. In this work we focus on change of
correctness.

In order to introduce the core features of our logic and its update
mechanisms, we use a simple example. (It will be further developed in
LABEL:example:public and LABEL:example:bdiagnosesa.) Consider two agents $a$
and $b$, each knowing their own local states, where global state $ij$, with
$i,j\in\\{0,1\\}$, means that $a$’s local state is $i$ and $b$’s local state
is $j$. To describe agent $a$’s local state $i$ we use a propositional state
variable $p_{a}$, where $p_{a}$ is true if $i=1$ in global state $ij$ and
$p_{a}$ is false if $i=0$, and similarly for $b$’s local state $j$ and
variable $p_{b}$. We assume that $a$ is correct in $00$ and that $b$ is
correct in $01$, $10$, and $11$.

The knowledge and hope of the agents is represented in a Kripke model $M$ for
our system consisting of four states (worlds), shown in the left part of the
figure below. Knowledge $K_{i}$ is interpreted by a knowledge relation
$\mathcal{K}_{i}$ and hope $H_{i}$ is interpreted by a hope relation
$\mathcal{H}_{i}$. Worlds that are $\mathcal{K}_{i}$-indistinguishable are
connected by an $i$-labeled link, where we assume reflexivity, symmetry (and,
later, also transitivity). Worlds $ij$ that are in the non-empty part of the
$\mathcal{H}_{i}$ relation, where agent $i$ is correct, have the $i$ outlined
as $\mathbb{0}$ or $\mathbb{1}$. For example, in the world depicted as
$0\mathbb{1}$ below agent $a$ is incorrect and agent $b$ is correct.

$\mathbb{0}0$$1\mathbb{0}$$0\mathbb{1}$$1\mathbb{1}$$b$$b$$a$$a$$\stackrel{{\scriptstyle\text{$a$
becomes more
correct}}}{{\Longrightarrow}}$$\mathbb{0}0$$1\mathbb{0}$$\mathbb{01}$$\mathbb{11}$$b$$b$$a$$a$

Now assume that we want agent $a$ to become correct in states $01$ and $11$
where $p_{b}$ is true. For example, this could be dictated by an FDIR
mechanism that caused $b$ to diagnose $a$ as faulty. Changing the fault status
of $a$ accordingly (while not changing the correctness of $b$) results in the
updated model on the right in the above figure. Note that $a$ was correct in
state $00$ in the left model, but did not know this, whereas agent $a$ knows
that she is correct in state $00$ after the update. Such a model update will
be specified in our approach by a suitable _hope update formula_ for every
agent, which, in the above example, is $\neg H_{a}\bot\lor p_{b}$ for agent
$a$ and $\neg H_{b}\bot$ for agent $b$.

The way we model such an update of the agents’ fault status in a dynamic
epistemic logic is novel. Note that we change relation $\mathcal{H}_{a}$ while
keeping relation $\mathcal{K}_{a}$ intact (relations $\mathcal{H}_{b}$ and
$\mathcal{K}_{b}$ remain the same). For agent $b$, however, we could
simultaneously have changed the relation $\mathcal{H}_{b}$ while keeping
relation $\mathcal{K}_{b}$ intact. This is characteristic of our approach: we
change the hope relation but not the knowledge relation. Now the way we change
the hope relation is uncommon for a dynamic epistemic logic: we _expanded_ the
relation. This is possible in a structured way because a knowledge relation
contains the hope relation. Such relational expansion is, purely technically,
associated with _belief contraction_ [agm:1985]. Although _belief expansion_
[plaza:1989, baltagetal:1998, hvdetal.del:2007] and _belief revision_
[hvd.prolegomena:2005, baltagetal:2006, jfak.jancl:2007] are common fare in
dynamic epistemic logic, we do not know of mechanisms for belief contraction,
where we should note that there is a prior tradition of belief contraction in
dynamic (not epistemic) logic [jfak.logcol:1989, segerberg:1999] (see also
[hvdetal.del:2007, Chapter 3]). An update corresponding to belief contraction
is, we think, novel in dynamic epistemic logic.

Clearly, different FDIR approaches will require different hope update formulas
for describing their effects. In order to enlarge the class of FDIR approaches
covered, we actually provide two variants of our hope update mechanism:
_public_ updates in which in any given world the agents are certain about the
exact hope updates occurring at other agents, and _private_ updates (strictly
speaking, semi-private updates [hvd.jolli:2002]) in which the agents may be
uncertain about the hope updates occurring at other agents, while they still
know what the different possible hope updates are. We do not propose fully
private updates in which an agent is not even aware (does not consider
possible) that a hope update has affected some other agent, although
technically this is quite possible.

Whereas the agents’ local states do not necessarily have to be changed when
becoming correct, our logic provides an additional update mechanism for
accomplishing this as well. More specifically, we assume that local states are
maintained in atomic propositions and use an appropriate _factual change_
mechanism for such an update. For example, simultaneously with becoming
correct, agents may also change their local state by making false the atomic
proposition that records that step 134 of the protocol was (erroneously)
executed. Analogous to hope update formulas, suitable _factual change
formulas_ are used to encode how facts will change. Again, different recovery
mechanisms will require different factual change formulas.

A peculiarity of our updates in modal logic is that hope update formulas and
factual change formulas may not be true after the update, although they must
be true before the update. This is the phenomenon of so-called _unsuccessful
updates_ [hvdetal.synthese:2006].

#### Paper organization.

In Section 2, we briefly recall the syntax and semantics of the logical
language for knowledge and hope introduced in [hvdetal.aiml:2022]. In Section
3, we expand this language with dynamic modalities for changing the hope
relation in a public way and give a complete axiomatization for the semantics.
More specifically, we show that the expressivity of the logical language does
not change when adding those dynamic modalities: we provide a reduction
showing that formulas with dynamic modalities are equivalent to formulas
without (with merely knowledge and hope modalities). We also provide examples
that demonstrate the flexibility and utility of our logic to model various
FDIR schemes, including making agents more correct, modeling self-correcting
agents who learned that they are faulty, ensuring that that there are at most
$f$ byzantine agents, etc. In LABEL:sec.semi-private, we generalize our
setting to private updates. We also provide a complete axiomatization of the
resulting semantics, which is again a rewrite system, and some application
examples. In LABEL:sec.factual, we add factual change to our setting. Some
conclusions in LABEL:sec:conclusions complete our paper.

_Utility of our logic._ We conclude this section with summarizing the utility
of our accomplishments. Besides contributing novel model update mechanisms to
the state-of-the-art in dynamic epistemic logic, the main utility of our logic
is that it enables epistemic reasoning and verification of FDIR mechanism
_specifications_. Whereas every FDIR mechanism is, of course, implemented via
(complex) protocols, its ultimate goal can be abstractly described as a
transformation from the epistemic model where the protocol execution had
started to the epistemic model where it has completed. Note carefully that
even a fully verified protocol implementation of some FDIR mechanism would be
meaningless if its specification allowed for unintended effects.

It is precisely this that our logic enables us to focus on: our hope
update/factual change formulas formally and exhaustively specify what the
respective model update accomplishes, i.e., encode both the preconditions for
changing some agent’s fault status/atomic propositions and the actual change.
Given an initial model and these update formulas, our logic thus enables one
to check (even automatically) whether the updated model has all the properties
intended by the designer, whether certain state invariants are preserved by
the update, etc. Needless to say, there are many reasons why a chosen
specification might be wrong in this respect: the initial model might not
provide all the required information, undesired fault status changes could be
triggered in some worlds, or supporting information required for an agent to
recover its local state might not be available. The ability to (automatically)
verify the absence of such undesired effects of the specification of an FDIR
mechanism is hence important in the design of mission-critical distributed
systems.

##  2 A Logic of Hope and Knowledge

The logic of hope and knowledge was proposed in [hvdetal.aiml:2022]. We give a
succinct presentation of its language, structures, semantics, and
axiomatization. Throughout our presentation, let
$\mathcal{A}\colonequals\\{1,\dots,n\\}$ be a finite set of agents and let
$\mathsf{Prop}$ be a nonempty countable set of atomic propositions.

#### Syntax.

We start with $\mathsf{Prop}$ and continue by forming formulas by closing
under the boolean connectives $\neg$ and $\land$ and also under the unary
modal operators (one for each agent) $K_{1},\dots,K_{n}$ and
$H_{1},\dots,H_{n}$ to obtain language $\mathcal{L}_{\mathit{KH}}$:

$\varphi\coloncolonequals p\mid\neg\varphi\mid(\varphi\wedge\varphi)\mid
K_{i}\varphi\mid H_{i}\varphi,$

where $p\in\mathsf{Prop}$ and $i\in\mathcal{A}$. We take $\top$ to be the
abbreviation for some fixed propositional tautology and $\bot$ for $\neg\top$.
We also use standard abbreviations for the remaining boolean connectives,
$\widehat{K}_{i}\varphi$ for the dual modality $\neg K_{i}\neg\varphi$, for
‘agent $a$ considers $\varphi$ possible’, $\widehat{H}_{i}\varphi$ for $\neg
H_{i}\neg\varphi$, and $E_{G}\varphi$ for mutual knowledge $\bigwedge_{i\in
G}K_{i}\varphi$ in a group $G\subseteq\mathcal{A}$. Finally, we define belief
$B_{i}\varphi$ as $K_{i}(\neg H_{i}\bot\rightarrow\varphi)$; we recall $\neg
H_{i}\bot$ means that $i$ is correct, see the introduction.

#### Structures.

A _Kripke model_ is a tuple $M=(W,\pi,\mathcal{K},\mathcal{H})$ where $W$ is a
nonempty set of _worlds_ (or  _states_),
$\pi\colon\mathsf{Prop}\to\mathcal{P}(W)$ is a _valuation function_ mapping
each variable to the set of worlds where it is true, and
$\mathcal{K}:\mathcal{A}\rightarrow\mathcal{P}(W\times W)$ and
$\mathcal{H}:\mathcal{A}\rightarrow\mathcal{P}(W\times W)$ are functions that
assign to each agent $i$ a _knowledge (accessibility) relation_
$\mathcal{K}_{i}\subseteq W\times W$ respectively a _hope (accessibility)
relation_ $\mathcal{H}_{i}\subseteq W\times W$, where we have written
$\mathcal{K}_{i}$ resp. $\mathcal{H}_{i}$ for $\mathcal{K}(i)$ and
$\mathcal{H}(i)$. We further write $\mathcal{H}_{i}(w)$ for
$\\{v\mid(w,v)\in\mathcal{H}_{i}\\}$ and $w\mathcal{H}_{i}v$ for
$(w,v)\in\mathcal{H}_{i}$, and similarly for $\mathcal{K}_{i}$.

We require knowledge relations $\mathcal{K}_{i}$ to be equivalence relations
and hope relations $\mathcal{H}_{i}$ to be shift-serial (that is, if
$w\mathcal{H}_{i}v$, then there exists a $z\in W$ such that
$v\mathcal{H}_{i}z$). In addition, the following two properties should also be
satisfied:

$\displaystyle\mathcal{H}\mathrm{in}\mathcal{K}$
$\displaystyle:\qquad\mathcal{H}_{i}\subseteq\mathcal{K}_{i},$
$\displaystyle\mathrm{one}\mathcal{H}$ $\displaystyle:\qquad(\forall w,v\in
W)(\mathcal{H}_{i}(w)\neq\varnothing\land\mathcal{H}_{i}(v)\neq\varnothing\land
w\mathcal{K}_{i}v\Longrightarrow w\mathcal{H}_{i}v).$

It can be shown that all $\mathcal{H}_{i}$ relations are so-called _partial
equivalence relations_ : they are transitive and symmetric binary relations
[mimo].

The class of Kripke models $(W,\pi,\mathcal{K},\mathcal{H})$ (given
$\mathcal{A}$ and $\mathsf{Prop}$) is named $\mathcal{K}\mathcal{H}$.

#### Semantics.

Let a model $M=(W,\pi,\mathcal{K},\mathcal{H})\in\mathcal{K}\mathcal{H}$ and a
world $w\in W$ be given. We inductively define truth for formulas
$\varphi\in\mathcal{L}_{\mathit{KH}}$ at world $w$ of Kripke model $M$ as
follows:

$\begin{array}[]{lll}M,w\models p&\text{iff}&w\in\pi(p)\\\
M,w\models\neg\varphi&\text{iff}&M,w\not\models\varphi\\\
M,w\models\varphi\wedge\psi&\text{iff}&M,w\models\varphi\text{ and
}M,w\models\psi\\\ M,w\models K_{i}\varphi&\text{iff}&M,v\models\varphi\text{
for all $v$ such that }w\mathcal{K}_{i}v\\\ M,w\models
H_{i}\varphi&\text{iff}&M,v\models\varphi\text{ for all $v$ such that
}w\mathcal{H}_{i}v\end{array}$

where $p\in\mathsf{Prop}$. A formula $\varphi$ is _valid in model $M$_,
denoted $M\models\varphi$, iff $M,w\models\varphi$ for all $w\in W$, and it is
_valid_ , notation $\models\varphi$ (or
$\mathcal{K}\mathcal{H}\models\varphi$) if it is valid in all models
$M\in\mathcal{K}\mathcal{H}$. We denote the domain $W$ of model $M$ as
$\mathcal{D}(M)$.

#### Axiomatization.

The axiom system $\mathscr{K\\!\\!H}$ for knowledge and hope is given in Table
1.

$\begin{array}[]{ll}P&\text{all propositional tautologies}\\\
H^{\dagger}&H_{i}\neg H_{i}\bot\\\ K^{K}&K_{i}(\varphi\rightarrow\psi)\land
K_{i}\varphi\rightarrow K_{i}\psi\\\ 4^{K}&K_{i}\varphi\rightarrow
K_{i}K_{i}\varphi\\\ 5^{K}&\neg K_{i}\varphi\rightarrow K_{i}\neg
K_{i}\varphi\\\ T^{K}&K_{i}\varphi\rightarrow\varphi\\\
\mathit{KH}&H_{i}\varphi\leftrightarrow(\neg H_{i}\bot\rightarrow K_{i}(\neg
H_{i}\bot\rightarrow\varphi))\\\ \mathit{MP}&\text{from }\varphi\text{ and
}\varphi\rightarrow\psi\text{ infer }\psi\\\ \mathit{Nec}^{K}&\text{from
}\varphi\text{ infer }K_{i}\varphi\end{array}$ Table 1: Axiom system
$\mathscr{K\\!\\!H}$.

######  Theorem 1 ([hvdetal.aiml:2022]).

$\mathscr{K\\!\\!H}$ is sound and complete with respect to
$\mathcal{K}\mathcal{H}$.

##  3 Public Hope Update

In this section, we will add dynamic modalities to our logic, which implement
our public hope update mechanism.

###  3.1 Syntax and Semantics

######  Definition 2 (Logical language).

Language $\mathcal{L}_{\mathit{KH}}^{\textit{pub}}$ is obtained by adding the
construct $[\underbrace{\varphi,\dots,\varphi}_{n}]\varphi$ to the BNF of
$\mathcal{L}_{\mathit{KH}}$. $\dashv$

We read a formula of the shape $[\varphi_{1},\dots,\varphi_{n}]\psi$ as
follows: after revising or updating hope for agent $i$ with respect to
$\varphi_{i}$, for all agents $i\in\mathcal{A}$ simultaneously, $\psi$ (is
true). We call the formula $\varphi_{i}$ the hope update formula for agent
$i$. We abbreviate $(\varphi_{1},\dots,\varphi_{n})$ as $\vec{\varphi}$.

######  Definition 3 (Semantics of public hope update).

Let a tuple $\vec{\varphi}\in(\mathcal{L}_{\mathit{KH}}^{\textit{pub}})^{n}$,
a model $M=(W,\pi,\mathcal{K},\mathcal{H})\in\mathcal{K}\mathcal{H}$, and a
world $w\in W$ be given. Then

$M,w\models[\vec{\varphi}]\psi\quad\text{iff}\quad
M^{\vec{\varphi}},w\models\psi,$

where
${M^{\vec{\varphi}}}\colonequals{(W,\pi,\mathcal{K},\mathcal{H}^{\vec{\varphi}})}$
such that for each agent $i\in\mathcal{A}$:

$w\mathcal{H}^{\chi}_{i}v\qquad\text{iff}\qquad w\mathcal{K}_{i}v,\quad
M,w\models\chi,\quad\text{and}\quad M,v\models\chi$

and where we write $\mathcal{H}^{\chi}_{i}$ for
$(\mathcal{H}^{\vec{\varphi}})_{i}$ if the $i$-th formula in $\vec{\varphi}$
is $\chi$. $\dashv$

If $M,w\not\models\chi$, then $\mathcal{H}^{\chi}_{i}(w)=\varnothing$: agent
$i$ is faulty in state $w$ after the update, and $H_{i}\bot$ is true. Whereas
if $M,w\models\chi$, then $\mathcal{H}^{\chi}_{i}(w)\neq\varnothing$ and $\neg
H_{i}\bot$ is true in $w$: agent $i$ is correct. If the hope update formula
for agent $i$ also is $\neg H_{i}\bot$, then $\neg H_{i}\bot$ is true in the
same states before and after the update. Therefore $\mathcal{H}^{\neg
H_{i}\bot}_{i}=\mathcal{H}_{i}$: the hope relation for $i$ does not change. On
the other hand, if the hope update formula for agent $i$ is $H_{i}\bot$, then
$\mathcal{H}^{H_{i}\bot}_{i}(w)=\varnothing$ iff
$\mathcal{H}_{i}(w)\neq\varnothing$: the correctness of agent $i$ flips in
every state. If we wish to model that agent $a$ becomes _more correct_ , then
the hope update formula for agent $a$ should have shape $\neg
H_{a}\bot\vee\varphi$: the left disjunct $\neg H_{a}\bot$ guarantees that in
all states where $a$ already was correct, she remains correct.

As we often merely update the hope relation for a single agent, we find it
convenient to have a special notation for that. We write

$[\varphi]_{i}\psi\quad\text{ for }\quad[\neg H_{1}\bot,\dots,\neg
H_{i-1}\bot,\,\,\varphi,\,\,\neg H_{i+1}\bot,\dots,\neg H_{n}\bot]\psi$

where the hope update formula for agent $i$ is $\varphi$ while all other
agents $j\neq i$ have the trivial hope update formula such that their hope
relations remain unaffected. Similarly, we write $[\varphi]_{G}\psi$ if the
hope update formulas for all agents $i\in G$ is $\varphi$ and other agents
have the trivial hope update formula.