11institutetext: TU Wien, Vienna, Austria
11email<EMAIL_ADDRESS>
# Communication Modalities

Roman Kuznets This research was funded by the Austrian Science Fund (FWF)
project ByzDEL (P33600). 0000-0001-5894-8724

###### Abstract

Epistemic analysis of distributed systems is one of the biggest successes
among applications of logic in computer science. The reason for that is that
agents’ actions are necessarily guided by their knowledge. Thus, epistemic
modal logic, with its knowledge and belief modalities (and group versions
thereof), has played a vital role in establishing both impossibility results
and necessary conditions for solvable distributed tasks. In distributed
systems, knowledge is largely attained via communication. It has been standard
in both distributed systems and dynamic epistemic logic to treat incoming
messages as trustworthy, thus, creating difficulties in the epistemic analysis
of byzantine distributed systems where faulty agents may lie. In this paper,
we argue that handling such communication scenarios calls for additional
modalities representing the informational content of messages that should not
be taken at face value. We present two such modalities: _hope_ for the case of
fully byzantine agents and _creed_ for non-uniform communication protocols in
general.

###### Keywords:

Distributed systems Modal logic Epistemic logic Byzantine agents

##  1 Introduction

In their paper _On the Unusual Effectiveness of Logic in Computer Science_
[14], Halpern et al. list “the deployment of epistemic logic to reason about
knowledge in multi-agent systems” as one of the “areas of computer science on
which logic has had a definite and lasting impact” and support their thesis
with multiple examples. This should come as no surprise since knowledge is
inextricably linked with action. Moses [22] recently formalized this in the
form of the _Knowledge of Preconditions Principle_ (KoP):

###### Knowledge of Preconditions Principle

If $\varphi$ is a necessary condition for agent $i$ performing action
$\alpha$, then $K_{i}\varphi$ (i.e., agent $i$’s knowledge of $\varphi$) is
also a necessary condition for agent $i$ performing action $\alpha$.

The logic commonly used to reason about knowledge is _epistemic modal logic_
[16], with its semantics of _Kripke models_ consisting of possible worlds.
According to this semantics, knowledge is limited by how well agents are able
to pinpoint the real world among the many worlds they consider possible: the
fewer possibilities considered, the more the agent knows.

This semantics is adapted to the specific needs of distributed systems in the
_runs and systems framework_ [8], with global states of the distributed system
playing the role of possible worlds and with each agent’s local states
determining what this agent considers possible. As a result, all global states
where the agent has the same local state are indistinguishable for the agent,
resulting in rather strong properties of knowledge, including factivity
(whatever is known must be true), as well as positive and negative
introspection (the agent knows what it knows and what it does not know). In
modal terms, this corresponds to (the multimodal version of) logic S5.

While the form of messages in distributed systems is not restricted, it is
assumed that agents interpret each message they receive based on the common a
priori knowledge of the _joint protocol_ , i.e., of the protocols of each
agent. This assumption of common a priori knowledge of the protocols is akin
to the common knowledge of the model pointed out by Artemov as an assumption
in epistemic modal logic in general [1]. In particular, it completely
abstracts away any difficulties of interpreting messages correctly.

The other side of this coin, however, is that it is not clear how to interpret
messages that are not sent according to a pre-determined protocol. A prominent
example of this can be found in _byzantine distributed systems_ , i.e.,
distributed systems with _fully byzantine_ agents [20], i.e., agents that can
arbitrarily deviate from their protocols. In particular, a fully byzantine
agent can send any message at any time, independent of both its local state
and its (correct) protocol. Thus, it should come as no surprise that, until
recently, the standard epistemic analysis of distributed systems did not
extend to byzantine distributed systems.111There were papers about knowledge
in “byzantine” or “fault-tolerant” distributed systems, such as [24, 7, 15],
but the types of failures there is restricted to crashes and/or omissions,
meaning that all messages are still sent according to the pre-determined
protocol.

Providing the epistemic analysis of distributed systems with fully byzantine
agents was the goal of the project “ByzDEL: Reasoning about Knowledge in
Byzantine Distributed Systems” funded by the Austrian Science Fund (FWF) that
Roman Kuznets led in TU Wien with Ulrich Schmid as the co-PI. In this paper,
we report (some of) the findings of our team.

The difficulty of interpreting a message in byzantine systems is that the
recipient must consider the possibility of the sender being faulty. With
faulty agents able to lie, there seems to be no increase in the recipient’s
knowledge. And yet distributed protocols work for byzantine systems. One of
the basic observations is that, under the common assumption of having at most
$f$ byzantine agents, receiving the same message from $f+1$ distinct agents is
sufficient to guarantee the message veracity. But counting is not part of
epistemic modal logic, making it hard to explain this increase in knowledge in
the modal language of knowledge.

One of the byzantine distributed problems we analyzed was the Firing Rebels
with Relay [9], which is related to both the Byzantine Firing Squad by Burns
and Lynch [2] and the consistent broadcasting primitive Srikanth and Toueg
[29], the latter used for fault-tolerant clock synchronization and byzantine
synchronous consensus. In the course of this analysis [11], we discovered a
new modality we called _hope_ $H_{i}$. In this paper, we show that
$H_{i}\varphi$ represents exactly the informational content of receiving
message $\varphi$ from agent $i$ and argue that the language with both
knowledge and hope modalities for each agent is the right language for the
epistemic analysis of byzantine distributed systems.

In byzantine systems, a message is either taken at face value or ignored,
depending on whether the sender is correct or byzantine. However, many
communicative situations call for a more nuanced way of interpreting
information than all or nothing. For instance, the quantity maxim of Grice
[13] may allow to extract additional information from the message by
considering what could have been said but was not. To address such more
complex types of communication we propose a generalization of hope modality
that we call _creed_.

The paper is structured as follows. In Sect. 2, we recall the standard
representation of knowledge in distributed systems via the runs and systems
framework and the resulting logic S5 for the knowledge modality. In Sect. 3,
we show how our analysis of byzantine distributed systems forces to relativize
knowledge to the agent’s correctness, resulting in the so-called modality of
belief as defeasible knowledge. In Sect. 4, we discuss our novel hope modality
for representing information obtained by communication in byzantine
distributed systems. In Sect. 5, we introduce the creed modality that
generalizes hope and can be used to describe communication in _heterogeneous
distributed systems_ , with more complex agent types than just correct and
byzantine. Finally, in Sect. 6, we provide conclusions.

##  2 Knowledge Modality

As already mentioned, Kripke models are the standard tool for semantic
reasoning about modality in general and _knowledge modality_ in particular.
Throughout the paper, we assume that there is a finite set $A=\\{1,\dots,n\\}$
of _agents_ denoted $i,j,a,b,\dots$ and a countably infinite set
$\mathsf{Prop}$ of (_propositional_) _atoms_ denoted $p,q,p_{1},\dots$

######  Definition 1 (Multi-agent Kripke models)

A _Kripke model_ for the set $A$ of agents is a tuple $M=\langle
S,\mathcal{R},V\rangle$ that consists of a non-empty set $S$ of _(possible)_
_worlds_ , a function $\mathcal{R}\colon A\to 2^{S\times S}$ mapping each
agent $i\in A$ to a binary _accessibility relation_ $\mathcal{R}_{i}\subseteq
S\times S$ on $S$, and a _valuation function_ $V\colon\mathsf{Prop}\to 2^{S}$
mapping each atom $p\in\mathsf{Prop}$ to a set $V(p)\subseteq S$ of worlds
where $p$ is true.

The truth of a formula $\varphi$ from the grammar $\varphi\coloncolonequals
p\mid\neg\varphi\mid(\varphi\land\varphi)\mid K_{i}\varphi$ with
$p\in\mathsf{Prop}$ and $i\in A$ is recursively defined as follows: for a
world $s\in S$, we have $M,s\vDash p$ iff $s\in V(p)$, classical boolean
connectives, and $M,s\vDash K_{i}\varphi$ iff $M,t\vDash\varphi$ whenever
$s\mathcal{R}_{i}t$.

For a given interpreted system $I$ consisting of a set $R$ of runs, the
corresponding Kripke model is constructed as follows:

######  Definition 2 (Runs and systems)

If $R$ is the set of runs of a given distributed system, then its _global
states_ can be represented by pairs $(r,t)$ of a run $r\in R$ and time
instance $t\in\mathbb{N}$, meaning that the set of possible worlds
$S\colonequals R\times\mathbb{N}$. It is assumed that, for each global state
$(r,t)$ each agent $i\in A$ is in its _local state_ $r_{i}(t)$. The
accessibility relations $\sim_{i}$ are defined based on local states:
$(r,t)\sim_{i}(r^{\prime},t^{\prime})$ iff
$r_{i}(t)=r^{\prime}_{i}(t^{\prime})$. The resulting Kripke model $\langle
R\times\mathbb{N},\sim,V\rangle$ describes the knowledge of agents.

It is easy to see that these $\sim_{i}$ are equivalence relations, hence, the
logic for reasoning about knowledge in distributed systems ends up being
(multimodal) S5. In particular, it validates factivity ${\sf
t}:K_{i}\varphi\to\varphi$, positive introspection ${\sf 4}:K_{i}\varphi\to
K_{i}K_{i}\varphi$, and negative introspection ${\sf 5}:\neg K_{i}\varphi\to
K_{i}\neg K_{i}\varphi$ for each agent $i\in A$. (See [12] for details.)

Applying the Kripke definition of knowledge to an interpreted system $I$
yields

$I,r,t\vDash
K_{i}\varphi\qquad\Longleftrightarrow\qquad\Bigl{(}r_{i}(t)=r^{\prime}_{i}(t^{\prime})\quad\Longrightarrow\quad
I,r^{\prime},t^{\prime}\vDash\varphi\Bigr{)}.$ (1)

Thus, agent $i$’s local state $r_{i}(t)$ determines what $i$ knows at global
state $(r,t)$ (modulo the a priori assumptions about the whole system). This
explains why programming can be done based on agents’ local states, despite it
creating the erroneous impression of agent’s knowledge not being taken into
account, in seeming violation of the Knowledge of Preconditions Principle
(KoP). It is this model of knowledge (1) that was so successful in analyzing
fault-free distributed systems [8].

As already mentioned in the introduction, this model does not easily translate
to byzantine distributed systems, with the exception of certain types of so-
called _benign_ faults, e.g., crashes and omissions [24, 7, 15]. This
exception can also be explained via KoP. Recall that actions are determined by
knowledge, which is determined by the local state. Both crashes and (send)
omissions represent the type of byzantine behavior involving a faulty agent
_not_ doing something assigned by the protocol, rather than _doing_ something
in violation of the protocol. With no actions performed differently, no need
arises to modify how knowledge is modeled in runs and systems, nor the agent’s
local state.222One could point out that inaction could be viewed as a kind of
action, but temporary inaction is how asynchrony is modeled in distributed
systems, and the same methodology applies here more or less as is. By
contrast, if a faulty agent can perform a different action, it is not clear
how to reflect this in its knowledge and local state. This becomes especially
obvious when considering _fully byzantine_ agents that can perform any action.
How does their knowledge determine their arbitrary actions? Does it mean that
their knowledge should be inconsistent, which would be incompatible with the
logic of knowledge S5?

One of our first achievements [18, 17] was a new framework extending the runs
and systems framework with machinery for handling fully byzantine agents
without losing the modeling of knowledge according to (1). Without getting
into all the technical details of our solution [19, 26], the main idea behind
it was to decouple the arbitrary actions of faulty agents from their
knowledge. In our framework, all faulty actions are perpetrated by the
(adversarial accept of the) environment. Thus, a faulty agent retains its
knowledge according to (1) but loses the control of its actions.

Another barrier we had to overcome stemmed from the tension between the
factivity of S5 knowledge and the necessity to represent faulty sensors and,
more generally, to give faulty agents the ability to be mistaken. This was
solved by shifting the knowledge corruption to the level of local states. In
order to enable agents to be wrong, our framework imbues the environment with
the ability to falsify events, actions, and/or messages and to record these
“fake” events into the agent’s local state. The result is that the agent’s
knowledge is subjectively factive, in compliance with S5, but may not match
the objective reality, e.g., the agent may subjectively “know” that it has
received a particular message even though in reality no such message was ever
sent. Of course, to ensure overall logical consistency, that requires to drop
the a priori assumption that every received message must have been sent, which
is routinely made in distributed systems with at most crash and omission
failures.

To summarize, by extending runs and systems framework to the case of fully
byzantine agents, which may have false memories, lie, and violate their
protocol, our framework [18, 17, 19] finally provided a model for analyzing
knowledge of agents in fully byzantine distributed systems, while retaining
the traditional S5 logical properties of knowledge.

Paradoxically, one of the first results of this analysis made it clear that
knowledge is too strong to be used for triggering actions in byzantine
environments. For instance, a natural trigger for an agent’s action would be
some triggering event. However, we showed [18] that the subjective nature of
the factivity of agents’ knowledge has the following consequence: in a fully
byzantine distributed system, no agent (correct or faulty) can know that a
particular event took place objectively. We proved this by formalizing the
infamous _brain in a vat_ thought experiment [25] in our framework and showing
that in any global state $(r,t)$ each agent $i$ has an indistinguishable
global state $(r^{\prime},t^{\prime})$ where $i$ is a “brain in a vat,” i.e.,
all actions and events recorded in $i$’s local state
$r_{i}(t)=r^{\prime}_{i}(t^{\prime})$ are fake in run $r^{\prime}$: none of
them took place. The inability to distinguish $(r,t)$ from
$(r^{\prime},t^{\prime})$ precludes agent $i$ from knowing in run $r$ that any
action or event took place, even if all agents are correct in run $r$.
Moreover, this result applies to a wide range of distributed systems, both
asynchronous [18] and synchronous [27].

This result might seem quite devastating in light of KoP. How can an agent
react to a triggering event if the agent cannot know that such an event
happened?

##  3 Belief Modality

The solution is known at least since [21], where Moses proposed to define a
_belief modality_ as knowledge relativized to the agent’s
correctness.333Albeit in a slightly different language involving _indexical
sets_. In our language, this modality is represented by

$B_{i}\varphi\colonequals K_{i}(\mathit{correct}_{i}\to\varphi),$ (2)

where $\mathit{correct}_{i}\in\mathsf{Prop}$ are finitely many designated
propositional atoms, one per agent, with truth value determined by whether
agent $i$ is correct or not. Later in [23], Moses and Shoham dubbed this
modality _belief as defeasible knowledge_ and axiomatized it as ${\sf K45}$
with two additional axioms:

$\mathit{correct}_{i}\to(B_{i}\varphi\to\varphi)\qquad\text{and}\qquad
B_{i}\mathit{correct}_{i},$ (3)

where K45 means that $B_{i}$ has positive and negative introspection but not
necessarily factivity. However, the first additional axiom means that $B_{i}$
is factive for correct agents. Consequently, if a correct agent $i$ performs
an action based on $B_{i}\varphi$, then $\varphi$ is guaranteed to hold. While
this may not hold true for a faulty agent $i$, those actions do not have to
follow the protocol anyway. As a result, in a fully byzantine distributed
system, the way to program a reaction to a triggering event $\varphi$ is to
use $\mathit{correct}_{i}\to\varphi$ as a trigger instead. While knowledge
$K_{i}\varphi$ is not achievable [18, 27], belief
$B_{i}\varphi=K_{i}(\mathit{correct}_{i}\to\varphi)$ may be, and it results in
the same actions for correct agents.

The necessity to replace knowledge $K_{i}\varphi$ with belief $B_{i}\varphi$
in byzantine distributed systems is the first conclusion we formally derived
in our framework.

However, while belief enables one to describe agent’s actions, it is not
sufficient to explain how agents learn by communication. The problem lies in
the ability of byzantine agents to lie: if agent $i$ receives a message
$\varphi$ from agent $j$ and considers a possibility that this message is a
lie, what can $i$ learn? Were $j$ guaranteed to be truthful, then
$K_{j}\varphi$ would be a precondition for sending $\varphi$ in fault-free
systems per KoP, from which $\varphi$ would follow by factivity. As just
discussed, the precondition in byzantine scenarios would be the weaker
$B_{j}\varphi$, which is also factive for a correct $j$. Yet, when the
truthfulness assumption is removed, in particular, in the case of $j$ being
fully byzantine, then even $B_{j}\varphi$ becomes too strong. In fact, since a
faulty $j$ can send any message independent of its knowledge, the
informational content of $\varphi$ would be non-existent, i.e., trivial.

But communication is the main tool for solving distributed tasks. If agents
cannot learn from messages, then how does communication help solve the task?

##  4 Hope Modality

We propose the answer to this question in the form of the _hope modality_ [10]

$H_{i}\varphi\quad\colonequals\quad\mathit{correct}_{i}\to
B_{i}\varphi\quad=\quad\mathit{correct}_{i}\to
K_{i}(\mathit{correct}_{i}\to\varphi).$

This modality emerged naturally in our analysis of the distributed task we
called Firing Rebels with Relay (FRR) [11], which is an asynchronous variant
of the Byzantine Firing Squad problem [2] and is closely related to the
consistent broadcasting primitive [29]. Only later did we understand the
proper meaning of hope.

$H_{j}\varphi$ is precisely the informational content of a message $\varphi$
received from agent $j$ in a byzantine distributed system. Indeed, as we just
discussed, two options should be considered while interpreting $\varphi$:
agent $j$ is either correct or faulty. If $j$ is correct, then $B_{j}\varphi$
is the precondition for sending $\varphi$; if $j$ is faulty, then the
precondition is trivial, i.e., $\top$. Collecting both possibilities, one
concludes

$(\mathit{correct}_{j}\to
B_{j}\varphi)\land(\neg\mathit{correct}_{j}\to\top)\qquad\leftrightarrow\qquad
H_{j}\varphi.$ (4)

The first axiomatization of hope, in the style of Moses–Shoham [23] was
obtained by Fruzsa in 2019 [10]: hope is axiomatized as ${\sf K45}$ plus the
same two axioms (3) with hope $H_{i}\varphi$ replacing belief $B_{i}\varphi$,
plus one more additional axiom

$\neg\mathit{correct}_{i}\to H_{i}\varphi.$

Both Moses–Shoham’s axiomatization of belief and Fruzsa’s initial
axiomatization of hope lack the substitution property: e.g., substituting an
arbitrary formula $\varphi$ for $\mathit{correct}_{i}$ in the axiom
$H_{i}\mathit{correct}_{i}$ yields $H_{i}\varphi$. Validating all
$H_{i}\varphi$ would have trivialized the hope modality, and would have
rendered all communication useless. Thus, the logic of hope in [10] is not a
normal modal logic.

Fortunately, an alternative axiomatization of hope [4] can remove this
obstacle. It turns out that expressing the correctness atoms through hope as

$\mathit{correct}_{i}\colonequals\neg H_{i}\bot,$ (5)

produces an equivalent representation of hope that is axiomatized as KB4,
i.e., a normal modal logic with axiom 4 for positive introspection as earlier
and with ${\sf b}:\varphi\to H_{i}\neg H_{i}\neg\varphi$ replacing 5.

So far we discussed four syntactic constructs to be used for describing
reasoning about _knowledge and communication_ in byzantine distributed
systems:

knowledge modalities

for preconditions of actions;

correctness atoms

for determining whether an agent is correct or faulty;

belief modalities

for weaker preconditions of actions in byzantine settings;

hope modalities

for the informational content of messages.

In view of (5) and (2) it is clear that knowledge and hope modalities for each
agent suffice. As shown in [4], correctness atoms cannot be expressed through
knowledge. It, therefore, follows from (5) that neither can hope.

Thus, we posit that, at a minimum, a language suitable for reasoning about
knowledge and communication in byzantine distributed systems should contain
knowledge and hope modalities for each agent.

######  Definition 3 (Axiomatization of knowledge and hope [4])

The logic KH of knowledge and hope has the following axioms and inference
rules:

$\begin{array}[]{l@{:\quad}l@{\qquad}l@{:\quad}l}\lx@intercol\hfil\text{all
propositional tautologies}\hfil\lx@intercol\\\ {\sf
d}_{\rightarrow}^{H}&H_{i}\neg H_{i}\bot&{\sf
k}^{K}&K_{i}(\varphi\to\psi)\to(K_{i}\varphi\to K_{i}\psi)\\\
\lx@intercol\hfil\hfil\lx@intercol&{\sf 4}^{K}&K_{i}\varphi\to
K_{i}K_{i}\varphi\\\ \lx@intercol\hfil\hfil\lx@intercol&{\sf 5}^{K}&\neg
K_{i}\varphi\to K_{i}\neg K_{i}\varphi\\\
\lx@intercol\hfil\hfil\lx@intercol&{\sf t}^{K}&K_{i}\varphi\to\varphi\\\ {\sf
MP}&\displaystyle\frac{\varphi\quad\varphi\to\psi}{\psi}&{\sf
Nec}^{K}&\displaystyle\frac{\varphi}{K_{i}\varphi}\\\ \lx@intercol\hfil{\sf
kh}:\quad H_{i}\varphi\leftrightarrow\bigl{(}\neg H_{i}\bot\to K_{i}(\neg
H_{i}\bot\to\varphi)\bigr{)}\hfil\lx@intercol\end{array}$

Kripke models for this logic are a simple generalization of models from Def. 1
that has two accessibility relations per agent:

######  Definition 4 (Kripke models for knowledge and hope [4])

A _Kripke model for knowledge and hope_ for the set $A$ of agents is a tuple
$M=\langle S,\mathcal{K},\mathcal{H},V\rangle$ that consists of a set
$S\neq\varnothing$, a valuation function $V\colon\mathsf{Prop}\to 2^{S}$, and
functions $\mathcal{K},\mathcal{H}\colon A\to 2^{S\times S}$ mapping each
agent $i\in A$ to binary accessibility relations $\mathcal{K}_{i}$ and
$\mathcal{H}_{i}$ on $S$ respectively such that each $\mathcal{K}_{i}$ is an
equivalence relation (reflexive, transitive, and symmetric), each
$\mathcal{H}_{i}$ is a partial equivalence relation (transitive and
symmetric), and, in addition, $\mathcal{H}_{i}\subseteq\mathcal{K}_{i}$ for
each $i\in A$ and $s\mathcal{K}_{i}t$ implies $s\mathcal{H}_{i}t$ whenever
$s\mathcal{H}_{i}s^{\prime}$ and $t\mathcal{H}_{i}t^{\prime}$ for some worlds
$s^{\prime}$ and $t^{\prime}$ for each $i\in A$.

The truth of a formula $\varphi$ from the grammar $\varphi\coloncolonequals
p\mid\neg\varphi\mid(\varphi\land\varphi)\mid K_{i}\varphi\mid H_{i}\varphi$
with $p\in\mathsf{Prop}$ and $i\in A$ is the same as in Def. 1 except
$M,s\vDash K_{i}\varphi$ iff $M,t\vDash\varphi$ whenever $s\mathcal{K}_{i}t$,
with the new clause $M,s\vDash H_{i}\varphi$ iff $M,t\vDash\varphi$ whenever
$s\mathcal{H}_{i}t$.

We illustrate how to model communication in byzantine distributed systems:

###### Example 1

It is standard in distributed systems to restrict the number of byzantine
agents to at most $f$ for some $0\leq f\leq n$. Indeed, such a restriction is
typically necessary for the distributed task at hand to be solvable, with
$n\geq 2f+1$ or $n\geq 3f+1$ being a common necessary condition. In light of
(5), this can be formalized as

$\mathit{Byz}_{\\!f}\colonequals\bigvee\limits_{G\subseteq
A\atop|G|=n-f}\,\,\bigwedge\limits_{i\in G}\neg H_{i}\bot.$

Using the standard group notion of mutual hope
$E^{H}_{G}\varphi\colonequals\bigwedge_{i\in G}H_{i}\varphi$ for a group
$G\subseteq A$ of agents, we can derive factivity of mutual hope for
sufficiently large groups: whenever $|G|\geq f+1$,

${\sf KH}+\mathit{Byz}_{\\!f}\quad\vdash\quad E^{H}_{G}\varphi\to\varphi.$ (6)

As simple as the derivation of (6) might seem, it faithfully formalizes the
process of learning in byzantine distributed systems: if the same message is
received from $f+1$ distinct agents, then one of them must be correct,
ensuring the veracity of the message.

Other examples formalizing specifications of byzantine systems by knowledge
and hope, as well as other properties derived using the logic from Def. 4 can
be found in [4].

More syntactic constructs may be added to the logic of knowledge and hope as
needed. For instance, our analysis of the FRR problem [11] is done in a
language with the addition of temporal modality $\Diamond\varphi$ for
“$\varphi$ holds at some point in the future” and a mixed temporal–epistemic
fixpoint group modality $C^{\Diamond H}\varphi$ of _eventual common hope_.
Another example can be found in [5], where dynamic operators in the style of
Dynamic Epistemic Logic [6] are used to (self-)correct agents.

One last thing to discuss about hope is the origins of the name. Initially,
hope was chosen as an attitude similar to but weaker than belief. Indeed, in
our logic, ${\sf KH}\vdash B_{i}\varphi\to H_{i}\varphi$. However, it is
reasonable to ask whether one would actually say “hope” in colloquial speech
in the same situations where our hope modality is employed. Here is one such
example. It often happens that, meeting someone familiar after a long break, I
may not be sure about the name of their child. Say, the name “Florian” comes
to mind, but it might also be “Miro.” I clearly do not _know_ it is Florian.
But, in fact, my memory may be so fuzzy that I cannot even say that I
_believe_ it to be Florian: it may be more that, in my mind, it is, say,
Florian with 85% probability. Sometimes, in such situations, I still venture,
in the name of politeness, to ask about Florian, _hoping_ that I got the name
right. And that is the meaning of hope that our hope modality embodies.

##  5 Creed Modality

The breakdown of hope from (4) underscores the all-or-nothing dichotomy of
correct/faulty agents: correct agents are completely trusted, while faulty
agents are completely distrusted. The same approach, however, can also be
applied in less discriminating circumstances. In this section, we show how
hope can be generalized from byzantine distributed systems, where agents are
either correct or faulty, to _heterogeneous distributed systems_ where agents
may belong to several different types with each type communicating in its own
way that need not be fully known to other agent types. We start by
illustrating the utility of this approach by solving one of Smullyan’s puzzles
[28, Puzzle 28].

######  Example 2 (Knights and knaves [3])

All inhabitants of an island are either _knights_ who always tell the truth or
_knaves_ who always lie. Agents $a$ and $b$ are two of these inhabitants.
Agent $a$ makes the following statement: “At least one of us two is a knave.”
What are $a$ and $b$?

Here we have two types of agents: knights and knaves. Thinking of utterances
as actions that have preconditions, we can reformulate the definition of these
two types as follows: the precondition for agent $j$ saying $\varphi$ is

  * •

$\varphi$, and, according to KoP, $K_{j}\varphi$ for a knight;

  * •

$\neg\varphi$, and, according to KoP, $K_{j}\neg\varphi$ for a knave.

Consequently, the analog of (4) for agent $j$’s utterance of $\varphi$ would
in this case be

$(\mathit{knight}_{j}\to K_{j}\varphi)\land(\mathit{knave}_{j}\to
K_{j}\neg\varphi),$

where $\mathit{knight}_{j}$ and $\mathit{knave}_{j}$ are atoms that, like
$\mathit{correct}_{j}$ for hope, signify the type of agent $j$. The above
statement of agent $a$ can be formalized in this language as
$\varphi\colonequals\mathit{knave}_{a}\lor\mathit{knave}_{b}$. Accordingly,
the informational content of this $\varphi$ amounts to

$\bigl{(}\mathit{knight}_{a}\to
K_{a}(\mathit{knave}_{a}\lor\mathit{knave}_{b})\bigr{)}\land\bigl{(}\mathit{knave}_{a}\to
K_{a}\neg(\mathit{knave}_{a}\lor\mathit{knave}_{b})\bigr{)}.$ (7)

Using normal modal reasoning, factivity of knowledge, and the puzzle’s a
priori assumption $\mathit{knight}_{j}\leftrightarrow\neg\mathit{knave}_{j}$,
we can easily derive $\mathit{knight}_{a}\land\mathit{knave}_{b}$ from (7).
This provides the answer to the puzzle: $a$ is a knight while $b$ is a knave.

In this vein, we defined _creed modality_ [3] as a generalization of hope:

$\mathbb{C}_{a}^{L\setminus S}\varphi\colonequals S_{a}\to
K_{a}f_{LS}(\varphi)$

where $L$ is the type of the listening agent, $S$ is a possible type the
speaking agent $a$ might have, and $f_{LS}(\varphi)$ is the strongest
precondition for speaking $\varphi$ by an $S$-type agent that $L$-type agents
are aware of. Using creed, an $L$-type agent can extract the following
informational content from a message $\varphi$ of agent $a$:

$\mathbb{C}_{a}^{L\setminus
S_{1}}\varphi\land\dots\land\mathbb{C}_{a}^{L\setminus S_{k}}\varphi$

where $S_{1},\dots,S_{k}$ are all the agent types the listener thinks $a$ may
belong to.

##  6 Conclusions

In this paper, we have proposed the minimal language needed to reason about
knowledge and its increase via communication in byzantine distributed systems.
This language should include, for each agent, knowledge modality to describe
preconditions for this agent’s actions and hope modality to describe what
other agents learn from this agent’s messages. Hope modality first appeared in
the epistemic analysis of a particular distributed task, a simplified version
of consistent broadcasting, further proving its indispensability for reasoning
about knowledge and communication in distributed systems with fully byzantine
agents.

Looking beyond hope, we have shown the first glimpse of how to logically model
communication among agents of different types and different communication
strategies, the situation that is to become more and more widespread as
distributed systems grow both in size and in complexity. The research into
this novel creed modality is only in its initial stages.

###  6.0.1 Acknowledgements

This paper summarizes a particular strain of the results obtained within the
framework of the Austrian Science Fund (FWF) project ByzDEL (P33600). Many
people contributed to our research project and shared their ideas and
expertise over the years, whether officially or unofficially participating in
or simply collaborating with the project. Some are cited. Others collaborated
on other topics or contributed in less visible but nevertheless tangible and
crucial ways. I will provide an alphabetical list of people involved in the
project in all these various capacities, to whom I am immensely thankful for
joining me on this exciting ride: Giorgio Cignarale, Hans van Ditmarsch,
Stephan Felber, Patrik Fimml, Krisztina Fruzsa, Lucas Gréaux, Yoram Moses,
Laurent Prosperi, Sergio Rajsbaum, Rojo Randrianomentsoa, Hugo Rincón Galeana,
Thomas Schlögl, Ulrich Schmid, Thomas Studer, and Tuomas Tahko.

## References

  * [1] S. Artemov.  Observable models.  In S. Artemov and A. Nerode, editors, Logical Foundations of Computer Science: International Symposium, LFCS 2020, Deerfield Beach, FL, USA, January 4–7, 2020, Proceedings, volume 11972 of Lecture Notes in Computer Science, pages 12–26. Springer, 2020.  doi:10.1007/978-3-030-36755-8_2.
  * [2] J. E. Burns and N. A. Lynch.  The Byzantine firing squad problem.  In F. P. Preparata, editor, Parallel and Distributed Computing, volume 4 of Advances in Computing Research: A Research Annual, pages 147–161. JAI Press, 1987.
  * [3] G. Cignarale, R. Kuznets, H. Rincon Galeana, and U. Schmid.  Logic of communication interpretation: How to not get lost in translation.  In U. Sattler and M. Suda, editors, Frontiers of Combining Systems: 14th International Symposium, FroCoS 2023, Prague, Czech Republic, September 20–22, 2023, Proceedings, volume 14279 of Lecture Notes in Artificial Intelligence, pages 119–136. Springer, 2023.  doi:10.1007/978-3-031-43369-6_7.
  * [4] H. van Ditmarsch, K. Fruzsa, and R. Kuznets.  A new hope.  In D. Fernández-Duque, A. Palmigiano, and S. Pinchinat, editors, Advances in Modal Logic, volume 14, pages 349–369. College Publications, 2022.  Available from: http://www.aiml.net/volumes/volume14/22-vanDitmarsch-Fruzsa-Kuznets.pdf.
  * [5] H. van Ditmarsch, K. Fruzsa, R. Kuznets, and U. Schmid.  A logic for repair and state recovery in byzantine fault-tolerant multi-agent systems.  In Proceedings of IJCAR 2024: International Joint Conference on Automated Reasoning, Lecture Notes in Computer Science. Springer, 2024.  Accepted.  doi:10.48550/arXiv.2401.06451.
  * [6] H. van Ditmarsch, W. van der Hoek, and B. Kooi.  Dynamic Epistemic Logic, volume 337 of Synthese Library.  Springer, 2007.  doi:10.1007/978-1-4020-5839-4.
  * [7] C. Dwork and Y. Moses.  Knowledge and common knowledge in a Byzantine environment: Crash failures.  Information and Computation, 88(2):156–186, October 1990.  doi:10.1016/0890-5401(90)90014-9.
  * [8] R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi.  Reasoning About Knowledge.  MIT Press, 1995.  doi:10.7551/mitpress/5803.001.0001.
  * [9] P. Fimml.  Temporal-epistemic logic in Byzantine message-passing contexts.  Master’s thesis, TU Wien, Vienna, Austria, 2017.  doi:10.34726/hss.2017.38943.
  * [10] K. Fruzsa.  Hope for epistemic reasoning with faulty agents!  In A. Pavlova, M. Y. Pedersen, and R. Bernardi, editors, Selected Reflections in Language, Logic, and Information: ESSLLI 2019, ESSLLI 2020 and ESSLLI 2021, Student Sessions, Selected Papers, volume 14354 of Lecture Notes in Computer Science, pages 93–108. Springer, 2023.  doi:10.1007/978-3-031-50628-4_6.
  * [11] K. Fruzsa, R. Kuznets, and U. Schmid.  Fire!  In J. Halpern and A. Perea, editors, Proceedings of the Eighteenth Conference on Theoretical Aspects of Rationality and Knowledge, Beijing, China, June 25–27, 2021, volume 335 of Electronic Proceedings in Theoretical Computer Science, pages 139–153. Open Publishing Association, 2021.  doi:10.4204/EPTCS.335.13.
  * [12] J. Garson.  Modal logic.  In E. N. Zalta and U. Nodelman, editors, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Spring 2023 edition, 2023.  Available from: https://plato.stanford.edu/archives/spr2023/entries/logic-modal/.
  * [13] H. P. Grice.  Logic and conversation.  In P. Cole and J. L. Morgan, editors, Speech Acts, volume 3 of Syntax and Semantics, pages 41–58. Brill, 1975.  doi:10.1163/9789004368811_003.
  * [14] J. Y. Halpern, R. Harper, N. Immerman, P. G. Kolaitis, M. Y. Vardi, and V. Vianu.  On the unusual effectiveness of logic in computer science.  Bulletin of Symbolic Logic, 7(2):213–236, June 2001.  doi:10.2307/2687775.
  * [15] J. Y. Halpern, Y. Moses, and O. Waarts.  A characterization of eventual Byzantine agreement.  SIAM Journal on Computing, 31(3):838–865, 2001.  doi:10.1137/S0097539798340217.
  * [16] J. Hintikka.  Knowledge and Belief: An Introduction to the Logic of the Two Notions.  Cornell University Press, 1962.
  * [17] R. Kuznets, L. Prosperi, U. Schmid, and K. Fruzsa.  Causality and epistemic reasoning in byzantine multi-agent systems.  In L. S. Moss, editor, Proceedings of the Seventeenth Conference on Theoretical Aspects of Rationality and Knowledge, Toulouse, France, 17–19 July 2019, volume 297 of Electronic Proceedings in Theoretical Computer Science, pages 293–312. Open Publishing Association, 2019.  doi:10.4204/EPTCS.297.19.
  * [18] R. Kuznets, L. Prosperi, U. Schmid, and K. Fruzsa.  Epistemic reasoning with byzantine-faulty agents.  In A. Herzig and A. Popescu, editors, Frontiers of Combining Systems: 12th International Symposium, FroCoS 2019, London, UK, September 4–6, 2019, Proceedings, volume 11715 of Lecture Notes in Artificial Intelligence, pages 259–276. Springer, 2019.  doi:10.1007/978-3-030-29007-8_15.
  * [19] R. Kuznets, L. Prosperi, U. Schmid, K. Fruzsa, and L. Gréaux.  Knowledge in Byzantine message-passing systems I: Framework and the causal cone.  Technical Report TUW-260549, TU Wien, 2019.  Available from: https://publik.tuwien.ac.at/files/publik_260549.pdf.
  * [20] L. Lamport, R. Shostak, and M. Pease.  The Byzantine Generals Problem.  ACM Transactions on Programming Languages and Systems, 4(3):382–401, July 1982.  doi:10.1145/357172.357176.
  * [21] Y. Moses.  Resource-bounded knowledge.  In M. Y. Vardi, editor, Proceedings of the Second Conference on Theoretical Aspects of Reasoning About Knowledge, pages 261–275. Morgan Kaufmann, 1988.  Available from: https://dl.acm.org/doi/abs/10.5555/1029718.1029741.
  * [22] Y. Moses.  Relating knowledge and coordinated action: The Knowledge of Preconditions principle.  In R. Ramanujam, editor, Proceedings Fifteenth Conference on Theoretical Aspects of Rationality and Knowledge, Carnegie Mellon University, Pittsburgh, USA, June 4–6, 2015, volume 215 of Electronic Proceedings in Theoretical Computer Science, pages 231–245. Open Publishing Association, 2016.  doi:10.4204/EPTCS.215.17.
  * [23] Y. Moses and Y. Shoham.  Belief as defeasible knowledge.  Artificial Intelligence, 64(2):299–321, December 1993.  doi:10.1016/0004-3702(93)90107-M.
  * [24] Y. Moses and M. R. Tuttle.  Programming simultaneous actions using common knowledge.  Algorithmica, 3(1–4):121–169, November 1988.  doi:10.1007/BF01762112.
  * [25] A. Pessin and S. Goldberg.  The Twin Earth Chronicles: Twenty Years of Reflection on Hilary Putnam’s “The Meaning of ‘Meaning’ ”.  M. E. Sharpe, 1995.  doi:10.4324/9781315284811.
  * [26] T. Schlögl.  An extension framework for epistemic reasoning in byzantine distributed systems.  Master’s thesis, TU Wien, Vienna, Austria, 2020.  doi:10.34726/hss.2020.69444.
  * [27] T. Schlögl, U. Schmid, and R. Kuznets.  The persistence of false memory: Brain in a vat despite perfect clocks.  In T. Uchiya, Q. Bai, and I. Marsá Maestre, editors, PRIMA 2020: Principles and Practice of Multi-Agent Systems: 23rd International Conference, Nagoya, Japan, November 18–20, 2020, Proceedings, volume 12568 of Lecture Notes in Artificial Intelligence, pages 403–411. Springer, 2021.  doi:10.1007/978-3-030-69322-0_30.
  * [28] R. M. Smullyan.  What Is the Name of This Book? — The Riddle of Dracula and Other Logical Puzzles.  Prentice–Hall, 1978.
  * [29] T. K. Srikanth and S. Toueg.  Optimal clock synchronization.  Journal of the ACM, 34(3):626–645, July 1987.  doi:10.1145/28869.28876.


# Valid Widgets Contain Legal Subwidgets

Nathan Donagi  Lower Merion High School

(June 2022)

##  1 Introduction

The purpose of this paper is to prove a linear algebra result. This has to do
with the geometry of “widgets”. For us a widget is a collection of n pairs of
points in a vector space. (The pairs represent the different possible spin
states of a particle.) We investigate linear relations among such collections.
A corollary of our theorem was conjectured in [DO22] where it arose in an
attempt to understand some issues in super string theory. In that paper an
investigation of perturbative superstring theory with Ramond punctures
required the special case when the ambient dimension is n. Here we prove the
general case.

##  2 Notation

  * •

A widget is a set of n pairs of points in a vector space.

  * •

A section is a subset containing at most one point from each pair of points.

  * •

A legal widget is one in which every single section spans a space of dimension
at most n-1.

  * •

A subwidget is a subset of $k<n$ pairs out of the n pairs of points in a
widget. (Note that this must be a proper subset.)

  * •

A full widget is one in which the points span a space of dimension greater
than or equal to n.

  * •

A valid widget is one that is both legal and full.

  * •

A point’s opposite is the other point within a pair.

  * •

Label the pairs $p_{1}$, $p_{2}$, $p_{3}$ etc.

  * •

Label the points $p_{1}^{+}$, $p_{1}^{-}$, $p_{2}^{+}$, $p_{2}^{-}$ etc.

##  3 Results

Our main result is:

######  Theorem 1.

Every valid widget contains a legal subwidget.

######  Corollary 1.1.

A widget is valid $\iff$ it is full and contains a legal subwidget.

It is fairly simple to see that if a widget contains a legal subwidget, the
widget must be legal because choosing one point from each of the k pairs that
span the subwidget will span at most a k-1 dimensional space. Therefore adding
n-k extra points always span at most n-1 dimensions.

######  Corollary 1.2.

If a widget is valid then it contains a subwidget which is legal but not full.

A valid widget must contain a legal subwidget, that subwidget is then either
full or not. If it is full it is then also a valid widget and therefore must
also contain a legal subwidget. Therefore by induction it is clear that one of
the subwidgets of the original widget must therefore be legal but not full.

Corollary 1.2 is a rephrasing of a conjecture in [DO22].

##  4 Proof

###### Proof.

We denote the positive section: $g={p_{1}^{+},...,p_{n}^{+}}$.

For every i from 1 to n we let $g_{i}$ denote the section obtained by removing
$p_{i}^{+}$ from g, and we let $s_{i}$ denotes the subwidget obtained by
removing $p_{i}$ from the widget.

Assume there is a valid widget that does not contain a legal subwidget. Then
no subwidget can be legal and therefore at least one section of the first n-1
pairs spans a n-1 space (otherwise the first n-1 pairs would be a legal
subwidget). WLOG let that be $g_{n}$.

######  Lemma 2.

Replacing $p_{i}^{+}$ by $p_{i}^{+}+c*p_{i}^{-}$ for some constant c will keep
a valid widget valid.

###### Proof.

For all sections s taken from $s_{i}$, if s spans a n-1 dimensional space then
for the widget to be legal both $p_{i}^{+}$ and $p_{i}^{-}$ must be in the
span of s. Therefore adding some multiple of $p_{i}^{-}$ to $p_{i}^{+}$ will
result in a new point that is also in the span of every section taken from
$s_{i}$. Else since the span of s has at most dimension n-2, adding the point
$p_{i}^{+}+c*p_{i}^{-}$ will increase the dimension to at most n-1. Therefore
the legality of the widget does not change. Also the fullness of the widget
does not change as the total span of the widget has not changed.∎

Call k the number of positive sections $g_{i}$ of a valid widget that span
less than an n-1 space. We claim that for any valid widget that does not
contain a legal subwidget, for some $k>0$, it is possible to create a new
valid widget with a lower k. Let $g_{i}$ be one section that spans less than
an n-1 space, with the span q of dimension n-2. The dimension of q can not be
less than n-2 because at least one section $g_{j}$ spans a n-1 space.

If the opposites of every single point in $g_{i}$ are also in q, that means
that every single point of each pair is in an n-2 space, and therefore there
are n-1 pairs spanning a n-2 space, and therefore there is a legal subwidget.

So the opposite of some point in $g_{i}$ isn’t in q. Therefore there is an
infinite number of multiples c of that point’s opposite that can be added to
it that then result in $g_{i}$ spanning a n-1 space. At most a finite number
of these c could result in the span of a different section to go down in
dimension, so there must therefore be a c that doesn’t. Therefore it is
possible to create a new widget with the same validity with a lower k.

Through induction it is therefore possible to transform any widget that
doesn’t contain a legal subwidget into one in which either k=0 or it contains
a legal subwidget.

If k=0 for the transformed widget, then every single section $g_{i}$ (for i
from 1 to n) spans a n-1 space. Obviously then the sections g1 and g2 both
span a n-1 space. The points $p_{1}^{+}$,$p_{1}^{-}$ must therefore be in the
span of $g_{1}$. Therefore every point in $g_{2}$ is in the span of $g_{1}$
and since the span of both $g_{2}$ and $g_{1}$ have the same dimension they
must be the same. This exact same logic can be used to yield that the span of
any section $g_{i}$ (for i from 1 to n) is the same n-1 space. Therefore every
point in the transformed widget must be in that, so the transformed widget is
therefore not full, and not valid. By Lemma 2 the original widget was not
valid either, contradicting the assumption.

∎

## References

  * [DO22] Donagi R. and Ott N., “The Bad Locus In The Moduli Of Super Riemann Surfaces With Ramond Punctures”, to appear, arXiv:2208.02478.