# Fire!††thanks: Funded by the Austrian Science Fund (FWF) project ByzDEL
P33600.

Krisztina Fruzsa Roman Kuznets Ulrich Schmid PhD student in the FWF doctoral
program LogiCS (W1255).TU Wien<EMAIL_ADDRESS>
###### Abstract

In this paper, we provide an epistemic analysis of a simple variant of the
fundamental consistent broadcasting primitive for byzantine fault-tolerant
asynchronous distributed systems. Our Firing Rebels with Relay (FRR) primitive
enables agents with a local preference for acting/not acting to trigger an
action (FIRE) at all correct agents, in an all-or-nothing fashion. By using
the epistemic reasoning framework for byzantine multi-agent systems introduced
in our TARK’19 paper, we develop the necessary and sufficient state of
knowledge that needs to be acquired by the agents in order to FIRE. It
involves eventual common hope (a modality related to belief), which we show to
be attained already by achieving eventual mutual hope in the case of FRR. We
also identify subtle variations of the necessary and sufficient state of
knowledge for FRR for different assumptions on the local preferences.

##  1 Motivation and Background

In their PODC’18 paper “Silence” [14], Goren and Moses introduced and
epistemically analyzed _silent choirs_ as a fundamental primitive for message-
optimal protocols in synchronous fault-tolerant distributed systems where
computing nodes (agents111Since distributed systems are just one instance of
multi-agent systems, we will use the term “agent” instead of “process.”) can
crash. In synchronous systems, where one can time-out messages, it is well-
known [21] that an agent can convey information also by _not_ sending some
message. In a system where the sender may also crash, however, the receiver
cannot infer this information from not receiving the message. Still, if only
up to $f$ of the $n>f$ agents in a system may crash, a silent choir of $f+1$
agents that convey identical information suffices: at least one agent in the
choir must be correct, so its silence can be relied on.

Whereas silent choirs also work in systems where the faulty agents may behave
arbitrarily (byzantine [22]), the problem of not conveying information
faithfully now also plagues messages that _are_ sent, as they could originate
from a faulty sender or forwarding agent. In this paper, we will introduce and
epistemically analyze a fundamental primitive _Firing Rebels with Relay_
(FRR), which nicely captures exactly these issues. It is a simplified version
of the _consistent broadcasting_ primitive introduced by Srikanth and Toueg in
[28], which has been used as a pivotal building block in distributed
algorithms for byzantine fault-tolerant clock synchronization [7, 12, 27, 28,
31] and synchronous consensus [29], for example.

Informally, FRR requires that _every_ correct agent perform an action called
$\operatorname{FIRE}$, in an all-or-none fashion (though not necessarily
simultaneously), and only if at least one correct agent locally observed a
trigger event called $\operatorname{START}$. Note that we have replaced the
need to broadcast explicit information by just triggering an action, which
makes FRR essentially a non-synchronous variant of the Firing Squad problem
[5], hence its name. In crash-prone systems, FRR is trivial to solve, even for
large $f$: Indeed, every agent who observes $\operatorname{START}$ or receives
a notification message (for the first time) just invokes $\operatorname{FIRE}$
and sends a notification message to everyone. This guarantees that if a single
correct agent observes $\operatorname{START}$, every correct agent will invoke
$\operatorname{FIRE}$ (agents that crash during the run may or may not issue
$\operatorname{FIRE}$ here). Observe that this solution involves a trivial
silent choir, namely, when no agent observes $\operatorname{START}$.

In the presence of byzantine agents, however, this solution does not work, as
faulty agents may send a notification without having observed anything. A
correct solution for FRR must, hence, prevent the faulty agents from
triggering $\operatorname{FIRE}$ at any correct agent. In this paper, we will
establish the necessary and sufficient state of knowledge for correctly
solving FRR in our epistemic reasoning framework for byzantine multi-agent
systems [18, 19, 20]. At least since the ground-breaking work by Halpern and
Moses [15], the knowledge-based approach [9] has been known as a powerful tool
for analyzing distributed systems. In a nutshell, it uses epistemic logic [17]
to reason about knowledge and belief in distributed systems. As agents take
actions (e.g., $\operatorname{FIRE}$) based on the accumulated local
knowledge, reasoning about the latter is useful both for protocol design and
impossibility proofs.

In the _runs-and-systems_ framework for reasoning about multi-agent systems
[9, 15], the set of all possible runs $r$ (executions) of a system $I$
determines the Kripke model, formed by pairs $(r,t)$ of a run $r\in I$ and
time $t\in\mathbb{N}$ representing global states $r(t)$. Note that time is
modeled as discrete for simplicity, without necessarily being available to the
agents. Two pairs $(r,t)$ and $(r^{\prime},t^{\prime})$ are indistinguishable
for agent $i$ iff $i$ has the same local state in both global states
represented by those points, formally, if
$r_{i}(t)=r_{i}^{\prime}(t^{\prime})$. A modal _knowledge operator_ $K_{i}$ is
used to capture that agent $i$ knows some fact $\varphi$ in run $r\in I$ at
time $t\in\mathbb{N}$. Formally, $(I,r,t)\models K_{i}\varphi$ iff for every
$r^{\prime}\in I$ and for every $t^{\prime}$ with
$r_{i}(t)=r_{i}^{\prime}(t^{\prime})$ it holds that
$(I,r^{\prime},t^{\prime})~{}\models~{}\varphi$. Note that $\varphi$ can be a
formula containing arbitrary atomic propositions like
$\overline{\mathit{occurred}}(e)$ (event $e$ occurred) or $correct_{i}$ ($i$
did not fail yet), as well as other knowledge operators and temporal
modalities like $\lozenge$ (eventually) and $\Box$ (always), combined by
standard logical operators $\neg,\wedge,\vee$, and $\to$. For example,
$(I,r,t)~{}\models~{}\lozenge{K_{i}\overline{\mathit{occurred}}(e)}$ states
that there is some time $t^{\prime}\geq t$ when $i$ knows that event $e$
occurred. Important additional modalities for a group $G$ of agents are
_mutual knowledge_ $E_{G}\varphi\colonequals\bigwedge_{i\in G}K_{i}\varphi$
and _common knowledge_ $C_{G}\varphi$ that can be informally expressed as an
infinite conjunction $C_{G}\varphi\equiv E_{G}\varphi\wedge
E_{G}(E_{G}\varphi)\wedge\dots$; in other words, this means that every agent
in $G$ knows $\varphi$, and every agent in $G$ knows that every agent in $G$
knows $\varphi$, and so on.

Actions performed by the agents when executing a protocol take place when they
have accumulated some specific epistemic knowledge. According to the pivotal
_Knowledge of Preconditions Principle_ [23], it is universally true that if
$\varphi$ is a necessary condition for agent $i$ to take a certain action then
$i$ may act only if $K_{i}\varphi$ is true. For example, in order for agent
$i$ to decide on 0 in a binary consensus algorithm, $i$ must know that some
agent $j$ has started with initial value $x_{j}=0$, i.e., $K_{i}(\exists
j:x_{j}=0)$ must hold true. Showing that agents act without having attained
the respective necessary knowledge is, hence, a very effective way for proving
incorrectness of protocols. Conversely, optimal distributed algorithms can be
designed by letting agents act as soon as all respective necessary knowledge
has been established. Prominent examples are the protocols based on silent
choirs analyzed in [14] and the _unbeatable_ consensus protocols introduced in
[6], which are not just worst-case optimal but also not strictly dominated
w.r.t. termination time by any other protocol in _any_ execution.

Related work: The knowledge-based approach has been used for studying several
distributed computing problems in systems with uncertainty but no failures. In
[4], Ben-Zvi and Moses considered the simple _ordered response_ problem in
distributed systems, where the agents had to respond to an external
$\operatorname{START}$ event by executing a special one-shot action
$\operatorname{FIRE}$ in a given order $i_{1},i_{2},\dots$. The authors showed
that, in every correct solution, agent $i_{k}$ has to establish nested
knowledge $K_{i_{k}}K_{i_{k-1}}\dots
K_{i_{1}}\overline{\mathit{occurred}}(\operatorname{START}){}$ before it can
issue $\operatorname{FIRE}$ and that this nested knowledge is also sufficient.
In the conference version [2] of [4], the authors also considered the
_simultaneous response_ problem where all agents had to issue
$\operatorname{FIRE}$ at the same time. It requires the group $G$ of firing
agents to establish common knowledge
$C_{G}\overline{\mathit{occurred}}(\operatorname{START}){}$ [15]. This work
was later extended to responses that are not simultaneous but tightly
coordinated in time [3, 13].

The knowledge-based approach has also been successfully applied to fault-
tolerant synchronous distributed systems. Agents suffering from crash or
omission failures have been studied in [25, 26], primarily in the context of
agreement problems [8, 16], which require some form of common knowledge.
Important ingredients here are the indexical set of correct agents and a
related belief operator $B_{i}\varphi\colonequals
K_{i}(correct_{i}\rightarrow\varphi)$ [24], which states that agent $i$ knows
$\varphi$ to be true in all runs where $i$ is correct. This notion of
“defeasible knowledge” also underlies a variant of common knowledge that has
been used successfully for characterizing simultaneous distributed agreement
[25, 26]. Closer related to our FRR problem is eventual distributed agreement
studied in [16], where the stronger notion of continual common knowledge
proved its value. The latter needs to hold throughout a run, i.e., from the
beginning, which makes sense here since it is only applied to conditions on
the initial state. Continual common knowledge does not seem readily applicable
to FRR, however, as $\operatorname{START}$ can occur at any time in a run.
More recent results are the already mentioned unbeatable consensus algorithms
in synchronous systems with crash failures [6] and the silent-choir based
message-optimal protocols [14].

Detailed contributions: We rigorously define the FRR problem and its weaker
variant FR, without the all-or-nothing requirement (agreement), in epistemic
terms and identify the necessary and sufficient state of knowledge that must
be established by a correct agent in order to issue $\operatorname{FIRE}$ in
every correct solution for FRR. Since FRR involves distributed agreement, the
required state of knowledge involves some form of (eventual) common knowledge
of $\overline{\mathit{occurred}}(\operatorname{START}){}$. Interestingly, it
turned out that establishing the respective eventual mutual knowledge (namely,
“eventual mutual hope” where the hope modality is defined as
$H_{i}\varphi\colonequals correct_{i}\to B_{i}\varphi$) already implies the
required common knowledge (namely, “eventual common hope”). We also identify
subtle variations of the necessary and sufficient state of knowledge for FRR
for different assumptions on the occurrence of $\operatorname{START}$.

Whereas identifying the necessary and sufficient state of knowledge for the
agents to $\operatorname{FIRE}$ does not immediately lead to efficient
practical protocols, it is an important first step towards this goal. Indeed,
as for the ordered response problem in [4], for example, we expect this
knowledge to lead to necessary and sufficient _communication structures_ ,
which must be present in every run of any correct protocol solving FRR.
Knowing the latter would not only enable us to decide right away whether the
communication guarantees provided by some distributed system allow to solve
FRR, but also facilitate the design of efficient protocols.

Paper organization: In Section 2, we introduce some minimal basic notation
from our modeling framework [20]. In Section 3, we provide the detailed
definition and an epistemic analysis of the FRR problem. Some conclusions and
directions of future work in Section 4 complete our paper.

##  2 Preliminaries

In this section, we outline the basic concepts and facts that are employed in
our epistemic analysis of Firing Rebels with Relay (FRR). Our analysis was
actually performed within the rigorous framework (that is based on the
standard runs-and-systems framework) first developed in [20], which
incorporates agents’ ability to arbitrarily deviate from normative behavior.
This framework enables one to formally express the epistemic limitations (of
the agents) that the presence of possibly fully byzantine agents in the system
imposes.

In particular, we proved in [19] that asynchronous agents in a system with
fully byzantine agents can never _know_ that a particular event took place or
even that an agent performed a particular action (since the local state of a
malfunctioning agent may have been corrupted, the above statement applies even
to the agent’s knowledge of its own actions). This rather disappointing result
stems from the inability of even correct agents to exclude the possibility of
the so-called _brain-in-a-vat scenario_. In other words, an agent can never be
sure that the events and actions recorded in its local history truly happened
as recorded rather than being figments of its own malfunction. To make matters
worse, agents can also never _know_ that they are correct either. Thus, unable
to rely on knowledge or their own correctness, our agents are forced to rely
instead on _belief_ $B_{i}\varphi\colonequals
K_{i}(correct_{i}\rightarrow\varphi)$ (cf. [24]). In this paper, we show that
even belief is not always appropriate and needs to be replaced with a modality
we called _hope_ defined as $H_{i}\varphi\colonequals correct_{i}\to
B_{i}\varphi$ (for a detailed explanation see Remark 11).

Since the epistemic analysis presented in this paper is protocol-independent
and does not rely on the artefacts of our modeling, we omit all details
irrelevant to the task at hand and present our findings in an epistemic
language with temporal modalities that is interpreted in Kripke models
generated by runs in our framework. The purpose of this section is to provide
all the necessary ingredients (referring the reader to [18, 19, 20] for full
details of the said framework).

We fix a finite set $\mathcal{A}=\\{1,\dots,n\\}$ of _asynchronous agents_
with _perfect recall_. Each agent $i\in\mathcal{A}$ can perform _actions_
(according to its protocol), e.g., send _messages_. One of the actions any
agent can perform is $\operatorname{FIRE}$. Agents also witness _events_
(triggered by the _environment_) such as message delivery. One of the events
that can be observed by any agent is $\operatorname{START}$. We use a discrete
time model governed by a global clock with domain $\mathbb{T}=\mathbb{N}$. All
events taking place after clock time $t\in\mathbb{T}$ and no later than $t+1$
are grouped into a _round_ denoted $t+{}$½ and are treated as happening
simultaneously. Apart from actions, everything in the system is governed by
the _environment_. Unlike the environment, agents only have limited local
information, in particular, being asynchronous, do not have access to the
global clock. This is achieved by allowing them not to perform actions in some
rounds and allowing them, in the absence of either actions or events, to stay
in the same local state for several rounds in a row. The agents have perfect
recall in the sense that, once recorded in their local history, actions and
events are never forgotten.

No assumptions apart from liveness are made about the communication. Messages
can be lost, arbitrarily delayed, and/or delivered in the wrong order. In
addition, the environment may cause at most $f$ agents to become _byzantine_
faulty. A byzantine faulty agent can perform any action irrespective of its
protocol and “observe” events that did not happen. It can also have false
memories about actions it has performed. At the same time, like the global
clock, such malfunctions are not directly visible to an agent.

Throughout the paper, horizontal bars signify phenomena that are correct. Note
that the absence of this bar should not be equated to faultiness but rather
means the absence of a claim of correctness.

Agent $i$’s local view of the system immediately after round $t+{}$½, referred
to as (_process-time_ or _agent-time_) _node_ $(i,t+1)$, is recorded in $i$’s
_local state_ $r_{i}(t+1)$, also called $i$’s  _local history_. A _run_ $r$ is
a sequence of _global states_
$r(t)=\bigl{(}r_{\epsilon}(t),r_{1}(t),\dots,r_{n}(t)\bigr{)}$ of the whole
system consisting of the _state $r_{\epsilon}(t)$ of the environment_ and
local states $r_{i}(t)$ of every agent. Unlike local states, the global state
of the system necessarily updates every round to include all actions and
events that happened (even the empty set thereof is faithfully recorded and
modifies the global state). The set of all global states is denoted
$\mathscr{G}$.

What happens in each round is determined by nondeterministic protocols
${P_{i}}$ of the agents, the nondeterministic protocol $P_{\epsilon}$ of the
environment, and chance, the latter implemented as the _adversary_ part of the
environment (the exact technical details are not important for this paper).

In our epistemic analysis, we consider pairs $(r,t)$ of a run $r$ and time
$t$. A _valuation function_ $\pi$ determines whether an atomic proposition
from $\mathit{Prop}$ is true in run $r$ at time $t$. The determination is
arbitrary except for a small set of _designated atomic propositions_ whose
truth value at $(r,t)$ is fully determined by the state of the system. More
specifically, for $i\in\mathcal{A}$ and $t\in\mathbb{T}$,

$correct_{i}$ is true at $(r,t)$ iff no faulty event happened to $i$ by time
$t$;

$\overline{\mathit{occurred}}_{i}(o)$ is true at $(r,t)$ iff $i$’s local
history $r_{i}(t)$ contains an _accurate_ record of action/event $o$ occurring
(for example, in this paper we use action $o=\operatorname{FIRE}$ and event
$o=\operatorname{START}$);

$\overline{\mathit{occurred}}(o)\colonequals\bigvee\nolimits_{i\in\mathcal{A}}\overline{\mathit{occurred}}_{i}(o)$.

An _interpreted system_ is a pair $I=(R,\pi)$ where $R$ is the set of
considered runs. The language is $\varphi\coloncolonequals
p\mid\lnot\varphi\mid(\varphi\land\varphi)\mid
K_{i}\varphi\mid\lozenge\varphi\mid Y\varphi$ where $p\in\mathit{Prop}$ and
$i\in\mathcal{A}$; derived Boolean connectives are defined in the usual way;
$\Box\varphi\colonequals\lnot\Diamond\lnot\varphi$. Truth for these _formulas_
is defined in the standard way, in particular, for a run $r\in R$, time
$t\in\mathbb{T}$, atomic proposition $p\in\mathit{Prop}$, agent
$i\in\mathcal{A}$, and formula $\varphi$, we have $(I,r,t)\models p$ iff
$(r,t)\in\pi(p)$, and $(I,r,t)\models K_{i}\varphi$ iff
$(I,r^{\prime},t^{\prime})\models\varphi$ for any $r^{\prime}\in R$ and
$t^{\prime}\in\mathbb{T}$ such that $r_{i}(t)=r^{\prime}_{i}(t^{\prime})$, and
$(I,r,t)\models\lozenge\varphi$ iff $(I,r,t^{\prime})\models\varphi$ for some
$t^{\prime}\geq t$, and $(I,r,t)\models Y\varphi$ iff $t>0$ and
$(I,r,t-1)\models\varphi$ . A formula $\varphi$ is valid in $I$, written
$I\models\varphi$, iff $(I,r,t)\models\varphi$ for all $r\in R$ and
$t\in\mathbb{T}$.

##  3 The Firing Rebels Problem

In [28], Srikanth and Toueg introduced the consistent broadcasting primitive,
which proved its value in several different contexts, ranging from low-level
byzantine fault-tolerant tick generation in various system models [7, 12, 27,
31] to classic clock synchronization [28] to Byzantine Agreement [29]. As
argued already in Section 1, it gave rise to our _Firing Rebels with Relay_
problem FRR [10], which can be seen as a natural generalization of a _silent
choir_ in byzantine fault-tolerant systems [14]. As an important building
block for designing byzantine fault-tolerant systems, it is therefore a
natural target for a detailed epistemic analysis in our framework [20].

Our Firing Rebels problems assume that every agent $i\in\mathcal{A}$ may
observe an event $\operatorname{START}$ and may generate an action
$\operatorname{FIRE}$ according to the following specification:

######  Definition 1 (Firing Rebels with and without Relay).

A system is consistent with _Firing Rebels (FR)_ for $f\geq 0$ when all runs
satisfy:

  * (C)

_Correctness_ : If at least $2f+1$ agents learn that $\operatorname{START}$
occured at a correct agent, all correct agents perform $\operatorname{FIRE}$
eventually.

  * (U)

_Unforgeability_ : If a correct agent performs $\operatorname{FIRE}$, then
$\operatorname{START}$ occurred at a correct agent.

Moreover, the system is consistent with _Firing Rebels with Relay (FRR)_ if
every run also satisfies:

  * (R)

_Relay_ : If a correct agent performs $\operatorname{FIRE}$, all correct
agents perform $\operatorname{FIRE}$ eventually.

######  Remark 2 (Variants of Correctness).

A different specification for Correctness can sometimes be found in
literature: “ _If at least $f+1$ reliable agents locally observed
$\operatorname{START}$, then some reliable agent fires eventually_” (see,
e.g., [5]). Here, a reliable agent is one that _will always_ follow its
protocol, which corresponds to a forever correct agent in our terminology. In
the case of FRR, by invoking (R), this specification implies “ _If at least
$f+1$ reliable agents locally observed $\operatorname{START}$, then all
reliable agents fire eventually_.” Relying on such a specification in
asynchronous settings is problematic, however, because reliability depends on
the future behavior of the system. Even complete knowledge of the global
state, at a given time in a run, does not allow to identify the reliable
agents whose observations of $\operatorname{START}$ could be relied upon.
Thus, we require $2f+1$ arbitrary (correct or faulty) agents instead. Of
course, given the limit of $f$ faulty agents per run, at least $f+1$ (not
necessarily the same) of these agents will remain reliable in every run.
Moreover, we relax the condition of the $2f+1$ agents locally observing
$\operatorname{START}$ to each of them learning that $\operatorname{START}$
happened to some correct agent. This is preferable, because direct observation
is only one possible way of ascertaining that $\operatorname{START}$ occurred.
For instance, if an agent has already determined222Strictly speaking, the
agent in this situation _does not know_ that the $f$ agents are faulty, but
rather that they are faulty if it itself is not. By the same token, whenever
we say “learned,” “determined,” or “ascertained” above, what we mean is
reasoning under the assumption of its own correctness, i.e., the belief
modality $B_{i}$ rather than the knowledge modality $K_{i}$. who the $f$
faulty agents are, e.g., due to their erratic behavior in the past, then a
confirmation of $\operatorname{START}$ from just one other agent would be
sufficient.

We use the following abbreviations:

$\displaystyle\noindent B_{i}\varphi$ $\displaystyle\colonequals
K_{i}(correct_{i}\to\varphi)$ $\displaystyle H_{i}\varphi$
$\displaystyle\colonequals correct_{i}\to B_{i}\varphi=correct_{i}\to
K_{i}(correct_{i}\to\varphi)$ $\displaystyle E^{B}\varphi$
$\displaystyle\colonequals\bigwedge\nolimits_{j\in\mathcal{A}}B_{j}\varphi$
$\displaystyle E^{H}\varphi$
$\displaystyle\colonequals\bigwedge\nolimits_{j\in\mathcal{A}}H_{j}\varphi$
$\displaystyle E^{\lozenge{B}}\varphi$
$\displaystyle\colonequals\bigwedge\nolimits_{j\in\mathcal{A}}\lozenge{B}_{j}\varphi$
$\displaystyle E^{\lozenge{H}}\varphi$
$\displaystyle\colonequals\bigwedge\nolimits_{j\in\mathcal{A}}\lozenge{H}_{j}\varphi$

It has been shown in [11] that hope is a normal modality, in particular,
$\models H_{i}(\varphi\land\psi)\to H_{i}\varphi\land H_{i}\psi$. We define
eventual common hope $C^{\lozenge{H}}\varphi$ as the greatest fixed point of
the equation $\chi\leftrightarrow E^{\lozenge{H}}(\varphi\land\chi)$ in the
standard way (using the Knaster–Tarski theorem [30]) and use the following
properties (the general versions of which can be found in Lemma 11.5.7 in
[9]): for any interpreted system $I$,

$\displaystyle I\quad\models\qquad C^{\lozenge{H}}\varphi\leftrightarrow
E^{\lozenge{H}}(\varphi\land C^{\lozenge{H}}\varphi);$ (1)
$\displaystyle\textnormal{if}\qquad I\quad\models\quad\psi\to
E^{\lozenge{H}}(\varphi\land\psi),\qquad\textnormal{then}\qquad
I\quad\models\quad\psi\to C^{\lozenge{H}}\varphi.$ (2)

###  3.1 Modeling

######  Definition 3.

For an agent $i\in\mathcal{A}$, we define:

$\displaystyle\overline{start}_{i}$ $\displaystyle\quad\colonequals\quad
Y{\overline{\mathit{occurred}}_{i}(\operatorname{START})}\wedge correct_{i}$
$\displaystyle\overline{fire}_{i}$
$\displaystyle\quad\colonequals\quad\overline{\mathit{occurred}}_{i}(FIRE)\wedge
correct_{i}$ $\displaystyle\overline{start}$
$\displaystyle\quad\colonequals\quad\bigvee\nolimits_{j\in\mathcal{A}}\overline{start}_{j}$
$\displaystyle\overline{fire}$
$\displaystyle\quad\colonequals\quad\bigvee\nolimits_{j\in\mathcal{A}}\overline{fire}_{j}$

Note that for one of these formulas to be true, it is necessary for (one of)
the involved agent(s) to be correct not only at the time the event/action in
question occurred but also at the time of the evaluation. Using the yesterday
modality $Y$ in $\overline{start}_{i}$ accounts for the fact that agents
cannot act on a precondition in the same round it is established.

Using Def. 3, we can translate the specification of FRR (stated in Def. 1) as
follows:

######  Definition 4 (Modeling Firing Rebels).

An interpreted system $I$ is consistent with Firing Rebels with Relay for
$f\geq 0$ if the following conditions Correctness (C), Unforgeability (U), and
Relay (R) hold:

(C) $\displaystyle
I\qquad\models\qquad\bigvee\limits_{\parbox{36.98866pt}{\scriptsize\centering$G\subseteq\mathcal{A}$\\\
$|G|\\!=\\!2f\\!+\\!1$\@add@centering}}\bigwedge\limits_{j\in
G}K_{j}(correct_{j}\rightarrow\overline{start})\rightarrow{\bigwedge\limits_{i\in\mathcal{A}}\lozenge{(}correct_{i}\to\overline{fire}_{i}})$
(U) $\displaystyle
I\qquad\models\qquad\overline{fire}\rightarrow\overline{start}$ (R)
$\displaystyle
I\qquad\models\qquad\overline{fire}\rightarrow{\bigwedge_{i\in\mathcal{A}}\lozenge{(}correct_{i}\to\overline{fire}_{i})}$

######  Remark 5 (Variants of eventuality).

The phrase _all correct agents fulfill $\varphi_{i}$ eventually_ in Def. 1 can
be formalized in two different ways:

  * •

${\bigwedge_{i\in\mathcal{A}}\lozenge{(correct_{i}\to\varphi_{i}})}$ states
that each agent will either become faulty at some point in the future or will
fulfill its respective $\varphi_{i}$ at some point in the future.

  * •

$\lozenge{\bigwedge_{i\in\mathcal{A}}(correct_{i}\to\varphi_{i}})$ states that
there is one moment in the future by which every agent still correct fulfills
its respective $\varphi_{i}$.

The second statement is a strengthening of the first by demanding agents to
have one common moment by which all correct agents fulfill their respective
$\varphi_{i}$’s. On the other hand, the first variant is a more intuitive
reading that is more widely applicable. Fortunately, for our model of FRR with
$\varphi_{i}=\overline{fire}_{i}$, the two formulations are equivalent
because, due to agents having perfect recall,
$correct_{i}\to\overline{fire}_{i}$ is a stable fact.

###  3.2 Necessary and Sufficient Level of Knowledge

The goal of this subsection is to

  1. (a)

strengthen the given necessary conditions on a single agent’s firing — namely,
that $\overline{start}$ must hold by Unforgeability (U) and
$\bigwedge_{i\in\mathcal{A}}\lozenge{(}correct_{i}\to\overline{fire}_{i})$
must hold by Relay (R) — to statements that describe the state of knowledge
necessary for the agent to achieve before firing;

  2. (b)

show that firing upon reaching this state of knowledge is sufficient for
satisfying the conditions Unforgeability (U) and Relay (R) on all correct
agents eventually firing;

  3. (c)

show how Correctness (C) helps simplify these necessary and sufficient
conditions in the presence of sufficiently many agents.

Thus, protocols prescribing an agent to fire as soon as this state of
knowledge is achieved are correct and optimal in the sense that firing earlier
would violate the necessary conditions whereas firing prescribed by this state
of knowledge is guaranteed to fulfill all requirements of FRR.

Note that the case when insufficiently many agents learn that START occurred
at a correct agent trivially satisfies condition (C). In this case, FRR
reduces to (U)+(R), a problem with a trivial solution of all correct agents
not firing. It is the combination of all all three conditions that makes FRR a
problem worth the analysis.

The first lemma formalizes the fact that, since agents have perfect recall of
their past perceptions, reasoning under the assumption of their own
correctness leads them to _believe_ that these perceptions were accurate. For
instance, an agent who recalls observing $\operatorname{START}$ believes that,
unless it is faulty, a correct agent (namely, itself) observed
$\operatorname{START}$. (A formal proof can be found in the Appendix on p.
Appendix.)

######  Lemma 6.

For any interpreted system $I$ and any agent $i\in\mathcal{A}$:

$\displaystyle I$ $\displaystyle\quad\models\quad\overline{fire}_{i}\to
B_{i}\overline{fire}_{i}$ (3) $\displaystyle I$
$\displaystyle\quad\models\quad\overline{fire}_{i}\to B_{i}\overline{fire}$
(4) $\displaystyle I$ $\displaystyle\quad\models\quad\overline{start}_{i}\to
B_{i}\overline{start}_{i}$ (5) $\displaystyle I$
$\displaystyle\quad\models\quad\overline{start}_{i}\to B_{i}\overline{start}$
(6)

Unforgeability (U) states that $\overline{start}$ is a necessary condition for
a correct agent firing. It follows from the Knowledge of Preconditions
Principle that any correct agent must ascertain $\overline{start}$ (modulo its
own correctness) before firing. We formalize this argument and provide an
independent proof:

######  Lemma 7 (State of knowledge necessary for firing in presence of
Unforgeability (U)).

Let $I$ be an interpreted system consistent with Unforgeability (U). For any
agent $i\in\mathcal{A}$,

$I\quad\models\quad\overline{fire}_{i}\to B_{i}\overline{start}.$ (7)

###### Proof.

Immediately follows from (4), (U), and monotonicity/normality of $B_{i}$. ∎

######  Corollary 8.

For any interpreted system consistent with FR, (7) is satisfied for all
agents.

Similarly, lifting the Relay condition (R) to the level of agent’s knowledge
yields the requirement that, in order to fire, an agent must believe that all
correct agents eventually will have fired.

######  Lemma 9 (State of knowledge necessary for firing in presence of Relay
(R)).

Let $I$ be an interpreted system consistent with Relay (R). For any agent
$i\in\mathcal{A}$,

$I\quad\models\quad\overline{fire}_{i}\to
B_{i}{\bigwedge\nolimits_{j\in\mathcal{A}}\lozenge{(}correct_{j}\rightarrow\overline{fire}_{j})}.$
(8)

###### Proof.

Immediately follows from (4), (R), and monotonicity of $B_{i}$. ∎

Combining the conditions necessary for (U) and (R), we establish the following
level of knowledge necessary for firing in FRR (a proof can be found in the
Appendix on p. Appendix):

######  Theorem 10 (State of knowledge necessary for firing in presence of
both (U) and (R)).

Let $I$ be an interpreted system consistent with (U) and (R). For any agent
$i\in\mathcal{A}$,

$I\qquad\models\qquad\overline{fire}_{i}\to
B_{i}\left(\overline{start}\wedge{E^{\lozenge{H}}\overline{start}}\right).$

######  Remark 11 (Emergence of hope).

Note that $I\models\overline{fire}_{i}\to
B_{i}{E^{\lozenge{B}}\overline{start}}$ does not generally hold. We cannot
strengthen the necessary condition by replacing eventual mutual hope with
eventual mutual belief, i.e., by omitting $correct_{j}$ therein. In other
words, the use of hope for deeper iterations of knowledge modalities is
crucial for the correct formulation. Indeed, in the case of our notion of
belief, agent $i$ can rarely have unconditional beliefs about another agent
$j$’s  _beliefs_. The problematic situation is when agent $j$’s perception is
compromised. In that case, agent $i$ has no way of ascertaining what $j$’s
erroneous input data might be and, hence, cannot determine what a correct
agent would have inferred from these incorrect inputs. According to our notion
of belief, whether agent $i$ itself is correct or not, it reasons assuming
that its own perceptions are the objective reality. The $correct_{j}$
assumption is, therefore, necessary to anchor $j$ to the same (allegedly)
objective reality contemplated by $i$, even though $j$’s access to the facts
of this objective reality is generally different from $i$’s. Note also that
$j$’s reasoning is generally happening in the future relative to $i$’s current
reasoning, meaning that we also implicitly assume reality to be stable.

######  Remark 12 (Relation to indexical sets).

Another approach to describing beliefs of fault-prone agents is via so-called
indexical sets [9, 26], which are variable (non-rigid) sets that can be used
to represent the set of all correct agents at every point in the system. While
our results could be reformulated in terms of indexical sets, there were
several reasons for us to choose another language. Besides the ability to
reason about all agents, whether correct or faulty, in a uniform way, we tried
to stay as close as possible to the standard language of epistemic modal
logic. Perhaps more importantly, however, was the moral lesson of the already
mentioned Knowledge of Preconditions Principle [23], which reveals how
important it is for an agent to know all ingredients affecting its behavior,
correctness of itself and other agents being one of them. Thus, we believe
that the transparent and explicit use of correctness in our language is
advantageous. An immediate example is the distinction between belief and hope
discussed in Remark 11, which would have remained somewhat obscured in the
indexical set notation.

######  Remark 13 (Eventual mutual hope is not sufficient).

While using
$B_{i}\left(\overline{start}\wedge{E^{\lozenge{H}}\overline{start}}\right)$ as
a trigger for agent $i$ firing will ensure Unforgeability (U), it is too weak
to guarantee Relay (R). Indeed, consider a system with 3 agents ($n=3$), at
most one of which can become faulty ($f=1$). In such a system, receiving the
same information from two independent sources is sufficient to believe in its
validity, while information from only one source without observing it first
hand is not. Suppose that the protocol forces a correct agent to notify all
other agents whenever it observed $\operatorname{START}$. Consider a run where
agent $b$ is byzantine from the beginning, whereas agents $c_{1}$ and $c_{2}$
remain correct. Let $c_{1}$ and $c_{2}$ each observe $\operatorname{START}$
and, hence, notify all agents about it. Meanwhile $b$ falsely notifies $c_{2}$
that it too observed $\operatorname{START}$ but will never duplicate this
message to $c_{1}$. Thus,

  * •

correct $c_{2}$ observed $\operatorname{START}$ and eventually received 2
confirmations of $\operatorname{START}$ from $c_{1}$ and $b$;

  * •

correct $c_{1}$ observed $\operatorname{START}$ and eventually received 1
confirmation of $\operatorname{START}$ from $c_{2}$;

  * •

faulty $b$ did not observe $\operatorname{START}$ but was eventually notified
of $\operatorname{START}$ by both $c_{1}$ and $c_{2}$.

In this situation, all agents eventually believe that $\operatorname{START}$
was correctly observed ($c_{1}$ and $c_{2}$ saw it themselves, whereas $b$ has
2 independent confirmations). Moreover, $c_{2}$ has a reason to believe in the
eventual mutual hope of $\operatorname{START}$. Indeed, hope would be
trivially satisfied for a faulty agent, whereas any correct agent would
eventually receive at least 2 confirmations out of 3 that $c_{2}$ itself
possesses. Thus, according to the proposed knowledge threshold, $c_{2}$ should
fire. On the other hand, $c_{1}$ will never fire because it cannot be sure
that $b$ will eventually hope that $\operatorname{START}$ occurred. In
$c_{1}$’s mind, if $b$ were correct and $c_{2}$ were faulty and did not send a
confirmation to $b$, then $b$ would only ever receive 1 confirmation, which is
not sufficient to make it trust $\operatorname{START}$ truly occurred. Hence,
$c_{1}$ would never fire, and Relay (R) would be violated.

The issue here is that $B_{i}{E^{\lozenge{H}}{\overline{start}}}$ for one
correct agent $i$ does not generally imply that eventually
$B_{j}{E^{\lozenge{H}}{\overline{start}}}$ for all other correct agents $j$.

Thus, although $B_{i}{E^{\lozenge{H}}{\overline{start}}}$ is necessary before
$i$ can fire and is in principle actionable, acting on it may be premature.
The necessary state of knowledge must be further strengthened. Since FRR
involves an agreement property (one correct agent fires only if all other
correct agents also fire eventually), it is not very surprising that, in fact,
some form of common knowledge, specifically _eventual common hope_ , plays a
role. We have shown (see a proof in the Appendix on p. Appendix) that
Unforgeability and Relay together imply that, in order to fire an agent must
ascertain (modulo its own correctness) both that $\operatorname{START}$ was
observed by some correct agent and the eventual common hope of the same fact:

######  Theorem 14 (State of knowledge necessary for firing in presence of
both (U) and (R)).

Let $I$ be an interpreted system consistent with (U) and (R). For any agent
$i\in\mathcal{A}$,

$I\quad\models\quad\overline{fire}_{i}\to
B_{i}{\left(\overline{start}\wedge{C^{\Diamond H}{\overline{start}}}\right)}.$
(9)

######  Corollary 15.

For any interpreted system consistent with FRR, (9) is satisfied for all
agents.

We now show (see a proof in the Appendix on p. Appendix) that, unlike belief
in eventual mutual hope (see Remark 13), belief in eventual _common_ hope is
sufficient to fulfill Unforgeability and Relay, i.e., that firing as soon as
the necessary state of knowledge from Theorem 14 is achieved does guarantee
that both (U) and (R) are fulfilled:

######  Theorem 16 (Sufficient conditions for (U) and (R)).

For any interpreted system $I$:

  1. 1.

(U) is fulfilled if
$I\quad\models\quad\bigwedge\nolimits_{i\in\mathcal{A}}(\lnot
B_{i}{\overline{start}}\to\lnot\overline{fire}_{i})$.

  2. 2.

Both (U) and (R) are fulfilled if

$I\models\bigwedge\limits_{i\in\mathcal{A}}\Bigl{(}\Bigl{(}\lnot
B_{i}{\left(\overline{start}\wedge{C^{\Diamond
H}{\overline{start}}}\right)}\to\lnot\overline{fire}_{i}\Bigr{)}\land\Bigl{(}B_{i}{\left(\overline{start}\wedge{C^{\Diamond
H}{\overline{start}}}\right)}\to\lozenge{(correct_{i}\to\overline{fire}_{i}})\Bigr{)}\Bigr{)}.$
(10)

######  Remark 17 (Belief in $\overline{start}$ is not redundant).

Since common knowledge is the strongest type of knowledge and knowledge is
supposed to be factive, it might be tempting to think that the conjunct
$\overline{start}$ is redundant in the formulations of Theorems 10, 14, and
16.2. The difference in our setting is that the relevant epistemic state is
_eventual_ , meaning that it need not be factual at present. Still, one might
question how it could be possible to achieve even an eventual
knowledge/belief/hope without the event actually happening. Indeed, if there
is no reason for agents to expect $\operatorname{START}$ to necessarily occur,
their predictions about $\operatorname{START}$ occurring can only rely on it
already having occurred. This observation is formalized in Lemma 23 and the
immediately following corollary.

######  Definition 18 (Potentially persistent formulas).

A formula $\varphi$ is called _potentially persistent_ in an interpreted
system $I=(R,\pi)$ if, for any run $r\in R$ and any time $t\in\mathbb{T}$ such
that $(I,r,t)\models\varphi$, there exists a run $r^{\prime}\in R$ such that
$r^{\prime}(t)=r(t)$ — i.e., $r^{\prime}$ is an alternative continuation of
the global state $r(t)$ — and such that
$(I,r^{\prime},t)\models\square{\varphi}$. In other words, a true potentially
persistent formula can stay true forever.

The following 3 lemmas follow from definitions (proofs of the last two are in
the Appendix on p. Appendix).

######  Lemma 19.

$I\models\lnot correct_{i}\to\square{\lnot correct_{i}}$ for any
$i\in\mathcal{A}$ and interpreted system $I$.

######  Lemma 20.

$I\models K_{i}\lozenge{\lnot}\varphi\to K_{i}\lnot\varphi$ for any
$i\in\mathcal{A}$ and $\varphi$ potentially persistent in an interpreted
system $I$.

######  Lemma 21.

$I\models B_{i}\lozenge{(correct_{i}\to\varphi)}\leftrightarrow
K_{i}\lozenge{(correct_{i}\to\varphi)}$ for any $i\in\mathcal{A}$, formula
$\varphi$, and interpreted system $I$, i.e., believing something eventually
happens modulo one’s own correctness is as strong as knowing it eventually
happens modulo one’s own correctness.

######  Corollary 22.

$I\models B_{i}\lozenge{H_{i}\varphi}\leftrightarrow
K_{i}\lozenge{H_{i}\varphi}$ for any $i\in\mathcal{A}$, formula $\varphi$, and
interpreted system $I$.

######  Lemma 23 (Early local belief).

If $correct_{i}\land\lnot\overline{start}$ is potentially persistent in an
interpreted system $I$,

$I\qquad\models\qquad B_{i}\lozenge{H_{i}\overline{start}}\to
B_{i}\overline{start}.$

###### Proof.

A proof can be found in the Appendix on p. Appendix. ∎

Noting that $I\models C^{\Diamond H}{\overline{start}}\to
E^{\lozenge{H}}{\overline{start}}$ because of the normality of the hope
modality [11], we can derive:

######  Corollary 24.

If $correct_{i}\land\lnot\overline{start}$ is potentially persistent in an
interpreted system $I$, then

$\displaystyle I\qquad\models\qquad B_{i}E^{\lozenge{H}}{\overline{start}}\to
B_{i}\overline{start},$ (11) $\displaystyle I\qquad\models\qquad
B_{i}C^{\Diamond H}{\overline{start}}\to B_{i}\overline{start}.$ (12)

######  Remark 25 (Conditions on dropping $B_{i}\overline{start}$).

If, contrary to the conditions of the early local belief lemma,
$\overline{start}$ is inevitable, agents _may_ be able to predict the eventual
arrival of $\operatorname{START}$ before the fact. For instance, if
$\operatorname{START}$ eventually happens to every agent, i.e., if
$I\models\lozenge{\overline{\mathit{occurred}}_{i}(\operatorname{START})}$,
then $I\models\lozenge{B_{i}\overline{start}}$ for every agent
$i\in\mathcal{A}$. It follows that $I\models CC^{\Diamond
H}{\overline{start}}$, i.e., it is common knowledge, from the very beginning,
that there is eventual common hope of $\overline{start}$. Thus, this state of
knowledge is achieved independently of $\operatorname{START}$ happening, and
triggering $\operatorname{FIRE}$ risks violating Unforgeability (U).

On the other hand, even if $\operatorname{START}$ is assured, it may not
always be possible to predict it in advance. While sufficient for dropping the
conjunct $\overline{start}$ from the conditions triggering
$\operatorname{FIRE}$ in Theorem 16.2, the potential persistency of
$correct_{i}\land\lnot\overline{start}$ is not necessary. Indeed, (12) can
hold even when $\operatorname{START}$ is always guaranteed to happen. For
instance, in an interpreted system where $\operatorname{START}$ happens
exactly once per run, no agent ever becomes faulty, and, in addition, agents
never communicate, $I\models\lnot B_{i}E^{\lozenge{H}}{\overline{start}}$
because only the agent who observed $\operatorname{START}$ can learn that it
already occurred. All the others can only be sure that $\operatorname{START}$
will occur eventually. By (1), also $I\models\lnot
B_{i}C^{\lozenge{H}}{\overline{start}}$. Thus, both implications (11) and (12)
are vacuously true, allowing to drop $\overline{start}$ without affecting the
behavior of agents, though admittedly in such interpreted systems agents
should never fire anyways.

The following “Lifting Lemma” shows that Correctness (C) lifts eventual mutual
hope to eventual common hope. This way, the arbitrarily deep nested hope
implied by the latter effectively collapses, a phenomenon that has also been
reported for other problems [2]. A proof of the lemma can be found in the
Appendix on p. Appendix.

######  Lemma 26 (Lifting Lemma).

Let $I$ be an interpreted system consistent with (C) and let
$|\mathcal{A}|\geq 3f+1$, where $f\geq 0$ is the maximum number of byzantine
faulty agents in a run. Furthermore, assume that

$I\qquad\models\qquad\overline{fire}_{i}\to
B_{i}\left(\overline{start}\wedge{E^{\lozenge{H}}\overline{start}}\right)$
(13)

holds. Then,

$I\qquad\models\qquad E^{\lozenge{H}}{\overline{start}}\to{C^{\Diamond
H}{\overline{start}}}.$ (14)

######  Corollary 27.

Let $I$ be an interpreted system with at least $3f+1$ agents. If $I$ is
consistent with FRR, then (14) holds.

###### Proof.

In interpreted systems consistent with (U) and (R), property (13) follows from
Theorem 10. ∎

##  4 Conclusions and Future Work

We introduced a problem called Firing Rebels with Relay (FRR) and its weaker
variant called Firing Rebels (FR), which capture the essentials of a well-
known building block for byzantine fault-tolerant distributed algorithms. The
main purpose of our paper was to determine the state of knowledge correct
agents must achieve in order to act ($\operatorname{FIRE}$) according to the
specification of the problem at hand. Through a detailed epistemic analysis,
we established that the necessary and sufficient levels of knowledge required
for acting rely on the novel notion of eventual common hope. We also found the
conditions under which a single level of eventual mutual hope can guarantee
infinitely many levels of eventual common hope and explored the surprisingly
non-trivial relationship of the eventual common hope of $\operatorname{START}$
with the actual appearance of $\operatorname{START}$.

Regarding future work, our next step is to complete the characterization of
(eventual) common hope. More precisely, what remains to be done is developing
an independent axiomatization of the (eventual) common hope modality based on
our existing axiomatization of the hope modality (which does not depend on the
knowledge modality). In addition, we are working on identifying necessary and
sufficient communication structures and optimal protocols for FRR.

## References

  * [1]
  * [2] Ido Ben-Zvi & Yoram Moses (2010): _Beyond Lamport’s _Happened-Before_ : On the Role of Time Bounds in Synchronous Systems_.  In Nancy A. Lynch & Alexander A. Shvartsman, editors: DISC 2010: Distributed Computing, LNCS 6343, Springer, pp. 421–436, 10.1007/978-3-642-15763-9_42.
  * [3] Ido Ben-Zvi & Yoram Moses (2013): _Agent-Time Epistemics and Coordination_.  In Kamal Lodaya, editor: ICLA 2013: Logic and Its Applications, LNCS 7750, Springer, pp. 97–108, 10.1007/978-3-642-36039-8_9.
  * [4] Ido Ben-Zvi & Yoram Moses (2014): _Beyond Lamport’s _Happened-before_ : On Time Bounds and the Ordering of Events in Distributed Systems_.  Journal of the ACM 61(2:13), 10.1145/2542181.
  * [5] James E. Burns & Nancy A. Lynch (1987): _The Byzantine Firing Squad Problem_.  In Franco P. Preparata, editor: Parallel and Distributed Computing, Advances in Computing Research: A research annual 4, JAI Press, pp. 147–161.  Available at https://apps.dtic.mil/docs/citations/ADA154770.
  * [6] Armando Castañeda, Yannai A. Gonczarowski & Yoram Moses (2014): _Unbeatable Consensus_.  In Fabian Kuhn, editor: DISC 2014: Distributed Computing, LNCS 8784, Springer, pp. 91–106, 10.1007/978-3-662-45174-8_7.
  * [7] Danny Dolev, Matthias Függer, Markus Posch, Ulrich Schmid, Andreas Steininger & Christoph Lenzen (2014): _Rigorously modeling self-stabilizing fault-tolerant circuits: An ultra-robust clocking scheme for systems-on-chip_.  Journal of Computer and System Sciences 80(2), pp. 860–900, 10.1016/j.jcss.2014.01.001.
  * [8] Cynthia Dwork & Yoram Moses (1990): _Knowledge and Common Knowledge in a Byzantine Environment: Crash Failures_.  Information and Computation 88(2), pp. 156–186, 10.1016/0890-5401(90)90014-9.
  * [9] Ronald Fagin, Joseph Y. Halpern, Yoram Moses & Moshe Y. Vardi (1995): _Reasoning About Knowledge_.  MIT Press.
  * [10] Patrik Fimml (2018): _Temporal-Epistemic Logic in Byzantine Message-Passing Contexts_.  Master’s thesis, Technische Universität Wien, Institut für Computer Engineering.  Available at http://publik.tuwien.ac.at/files/publik_273448.pdf.
  * [11] Krisztina Fruzsa (2019): _Hope for Epistemic Reasoning with Faulty Agents!_ In: ESSLLI 2019 Student Session, FOLLI.  Available at http://esslli2019.folli.info/wp-content/uploads/2019/08/tentative_proceedings.pdf.
  * [12] Matthias Függer & Ulrich Schmid (2012): _Reconciling fault-tolerant distributed computing and systems-on-chip_.  Distributed Computing 24(6), pp. 323–355, 10.1007/s00446-011-0151-7.
  * [13] Yannai A. Gonczarowski & Yoram Moses (2013): _Timely Common Knowledge: Characterising Asymmetric Distributed Coordination via Vectorial Fixed Points_.  In Burkhard C. Schipper, editor: TARK 2013: Theoretical Aspects of Rationality and Knowledge, pp. 79–93.  Available at http://www.tark.org/proceedings/tark_jan7_13/p79-gonczarowski.pdf.
  * [14] Guy Goren & Yoram Moses (2018): _Silence_.  In: PODC 2018: Principles of Distributed Computing, ACM, pp. 285–294, 10.1145/3212734.3212768.
  * [15] Joseph Y. Halpern & Yoram Moses (1990): _Knowledge and Common Knowledge in a Distributed Environment_.  Journal of the ACM 37(3), pp. 549–587, 10.1145/79147.79161.
  * [16] Joseph Y. Halpern, Yoram Moses & Orli Waarts (2001): _A characterization of eventual Byzantine agreement_.  SIAM Journal on Computing 31(3), pp. 838–865, 10.1137/S0097539798340217.
  * [17] Jaakko Hintikka (1962): _Knowledge and Belief: An Introduction to the Logic of the Two Notions_.  Cornell University Press.
  * [18] Roman Kuznets, Laurent Prosperi, Ulrich Schmid & Krisztina Fruzsa (2019): _Causality and Epistemic Reasoning in Byzantine Multi-Agent Systems_.  In Lawrence S. Moss, editor: TARK 2019: Theoretical Aspects of Rationality and Knowledge, EPTCS 297, Open Publishing Association, pp. 293–312, 10.4204/EPTCS.297.19.
  * [19] Roman Kuznets, Laurent Prosperi, Ulrich Schmid & Krisztina Fruzsa (2019): _Epistemic Reasoning with Byzantine-Faulty Agents_.  In Andreas Herzig & Andrei Popescu, editors: FroCoS 2019: Frontiers of Combining Systems, LNCS 11715, Springer, pp. 259–276, 10.1007/978-3-030-29007-8_15.
  * [20] Roman Kuznets, Laurent Prosperi, Ulrich Schmid, Krisztina Fruzsa & Lucas Gréaux (2019): _Knowledge in Byzantine Message-Passing Systems I: Framework and the Causal Cone_.  Technical Report TUW-260549, TU Wien.  Available at https://publik.tuwien.ac.at/files/publik_260549.pdf.
  * [21] Leslie Lamport (1978): _Time, Clocks, and the Ordering of Events in a Distributed System_.  Communications of the ACM 21(7), pp. 558–565, 10.1145/359545.359563.
  * [22] Leslie Lamport, Robert Shostak & Marshall Pease (1982): _The Byzantine Generals Problem_.  ACM Transactions on Programming Languages and Systems 4(3), pp. 382–401, 10.1145/357172.357176.
  * [23] Yoram Moses (2015): _Relating Knowledge and Coordinated Action: The Knowledge of Preconditions Principle_.  In R. Ramanujam, editor: TARK 2015: Theoretical Aspects of Rationality and Knowledge, EPTCS 215, Open Publishing Association, pp. 231–245, 10.4204/EPTCS.215.17.
  * [24] Yoram Moses & Yoav Shoham (1993): _Belief as defeasible knowledge_.  Artificial Intelligence 64(2), pp. 299–321, 10.1016/0004-3702(93)90107-M.
  * [25] Yoram Moses & Mark R. Tuttle (1986): _Programming Simultaneous Actions Using Common Knowledge: Preliminary Version_.  In: 27th Annual Symposium on Foundations of Computer Science, IEEE, pp. 208–221, 10.1109/SFCS.1986.46.
  * [26] Yoram Moses & Mark R. Tuttle (1988): _Programming Simultaneous Actions Using Common Knowledge_.  Algorithmica 3, pp. 121–169, 10.1007/BF01762112.
  * [27] Peter Robinson & Ulrich Schmid (2011): _The Asynchronous Bounded-Cycle model_.  Theoretical Computer Science 412(40), pp. 5580–5601, 10.1016/j.tcs.2010.08.001.
  * [28] T. K. Srikanth & Sam Toueg (1987): _Optimal Clock Synchronization_.  Journal of the ACM 34(3), pp. 626–645, 10.1145/28869.28876.
  * [29] T. K. Srikanth & Sam Toueg (1987): _Simulating authenticated broadcasts to derive simple fault-tolerant algorithms_.  Distributed Computing 2(2), pp. 80–94, 10.1007/BF01667080.
  * [30] Alfred Tarski (1955): _A lattice-theoretical fixpoint theorem and its applications_.  Pacific Journal of Mathematics 5(2), pp. 285–309, 10.2140/pjm.1955.5.285.
  * [31] Josef Widder & Ulrich Schmid (2009): _The Theta-Model: achieving synchrony without clocks_.  Distributed Computing 22(1), pp. 29–47, 10.1007/s00446-009-0080-x.

## Appendix

###### Proof of Lemma 6.

The argument is the same for $\operatorname{FIRE}$ and $\operatorname{START}$.
We only provide it for the former. Let $I=(R,\pi)$. Consider a run $r\in{R}$
and a node $(i,t)\in{\mathcal{A}\times\mathbb{T}}$. Assume
$(I,{r},{t})\models\overline{fire}_{i}$. Since $i$ has perfect recall and this
was a correct $\operatorname{FIRE}$ action, it was recorded and still remains
in $i$’s local history $r(t)$. Consider any $r^{\prime}\in R$ and
$t^{\prime}\in\mathbb{N}$ such that
$r_{i}\left(t\right)=r^{\prime}_{i}\left(t^{\prime}\right)$. Then
$r^{\prime}_{i}\left(t^{\prime}\right)$ also contains a record of
$\operatorname{FIRE}$. If $(I,{r^{\prime}},{t^{\prime}})\models correct_{i}$,
this record must correspond to a correct action and, consequently,
$(I,{r^{\prime}},{t^{\prime}})\models\overline{fire}_{i}$. Since
$(I,{r^{\prime}},{t^{\prime}})\models correct_{i}\to\overline{fire}_{i}$
whenever $r_{i}\left(t\right)=r^{\prime}_{i}\left(t^{\prime}\right)$, we have
$(I,{r},{t})\models K_{i}(correct_{i}\rightarrow\overline{fire}_{i})$, i.e.,
$(I,{r},{t})\models B_{i}\overline{fire}_{i}$. The other statement about FIRE
follows from $\models\overline{fire}_{i}\to\overline{fire}$ and the
monotonicity/normality of $B_{i}$.∎

###### Proof of Theorem 10.

Since the system is consistent with (U), (7) holds according to Lemma 7. Thus,
given that $B_{i}$ is a normal modality, it only remains to show that

$I\qquad\models\qquad\overline{fire}_{i}\to
B_{i}{E^{\lozenge{H}}\overline{start}}.$ (15)

Since the system is consistent with (R), (8) holds according to Lemma 9. Using
the replacement property for positive subformulas and the already discussed
validity $I\models\overline{fire}_{j}\to B_{j}\overline{start}$ from (7), we
obtain $I\models\overline{fire}_{i}\to
B_{i}{\bigwedge\nolimits_{j\in\mathcal{A}}\lozenge{\bigl{(}correct_{j}\rightarrow
B_{j}\overline{start}\bigr{)}}}$, in other words, (15). ∎

###### Proof of Theorem 14.

Since (7) holds by Lemma 7, it is sufficient to demonstrate
$I\models\overline{fire}_{i}\to B_{i}{C^{\Diamond H}{\overline{start}}}$.
Combining (R) with (4) by applying the replacement property for positive
subformulas, we obtain
$I\models\overline{fire}\to{E^{\lozenge{H}}{\overline{fire}}}$. Thus, using
(2) with $\varphi=\psi=\overline{fire}$, we conclude
$I\models\overline{fire}\to C^{\Diamond H}{\overline{fire}}$. Since the
greatest fixed point of a monotone operator is itself monotone, it follows
from (U) that $I\models\overline{fire}\to C^{\Diamond H}{\overline{start}}$.
It remains to use (4) and monotonicity of $B_{i}$ to obtain
$I\models\overline{fire}_{i}\to B_{i}C^{\Diamond H}{\overline{start}}$. ∎

###### Proof of Theorem 16.

For either assumption, $I\models\overline{fire}_{i}\to
B_{i}{\overline{start}}$. Since

$I\quad\models\quad\overline{fire}_{i}\to correct_{i}\qquad\text{and}\qquad
I\quad\models\quad
correct_{i}\rightarrow(B_{i}{\varphi}\rightarrow\varphi)\quad\text{for any
formula~{}$\varphi$},$ (16)

we have $I\models\overline{fire}_{i}\to\overline{start}$ for each
$i\in\mathcal{A}$. Since $\overline{fire}$ is
$\bigvee_{i\in\mathcal{A}}\overline{fire}_{i}$, (U) holds by propositional
reasoning.

It remains to show that Relay (R) holds under the assumption of (10). Once
again, it is sufficient to demonstrate that, for each $i\in\mathcal{A}$,

$I\qquad\models\qquad\overline{fire}_{i}\to\bigwedge\nolimits_{j\in\mathcal{A}}\lozenge{(}correct_{j}\to\overline{fire}_{j}).$
(17)

It follows from the first conjunct of (10) that
$I\models\overline{fire}_{i}\to B_{i}{{C^{\Diamond H}{\overline{start}}}}$.
Using (16) again, we conclude that $I\models\overline{fire}_{i}\to{C^{\Diamond
H}{\overline{start}}}$. Since $I\models C^{\Diamond
H}{\varphi}\to\bigwedge_{j\in\mathcal{A}}\lozenge{H_{j}(\varphi\land
C^{\Diamond H}{\varphi})}$ for any formula $\varphi$ according to (1),

$I\qquad\models\qquad\overline{fire}_{i}\to\bigwedge\nolimits_{j\in\mathcal{A}}\lozenge{\Bigl{(}correct_{j}\to
B_{j}{\bigl{(}\overline{start}\wedge{C^{\Diamond
H}{\overline{start}}}}\bigr{)}\Bigr{)}}.$ (18)

Using the second conjunct of (10) and monotonicity of $B_{j}$ and $\lozenge{}$
in (18), we obtain

$I\qquad\models\qquad\overline{fire}_{i}\to\bigwedge\nolimits_{j\in\mathcal{A}}\lozenge{\Bigl{(}correct_{j}\to\lozenge{\bigl{(}correct_{j}\to\overline{fire}_{j}}\bigr{)}\Bigr{)}}.$

To get (17), it remains to note that
$I\models\lozenge{\Bigl{(}\varphi\to\lozenge{(\varphi\to\psi)}\Bigr{)}}\to\lozenge{(\varphi\to\psi)}$
for all formulas $\varphi$ and $\psi$. ∎

###### Proof of Lemma 20.

Let $I=(R,\pi)$. Assume that $(I,r,t)\not\models K_{i}\lnot\varphi$ for some
$r\in R$ and $t\in\mathbb{T}$. Then there exists another run $r^{\prime}\in R$
and time $t^{\prime}\in\mathbb{T}$ such that
$r_{i}(t)=r^{\prime}_{i}(t^{\prime})$ and
$(I,r^{\prime},t^{\prime})\models\varphi$. By the potential persistence of
$\varphi$, there exists an alternative continuation $r^{\prime\prime}\in R$ of
the prefix $r^{\prime}(t^{\prime})$ such that
$r^{\prime\prime}(t^{\prime})=r^{\prime}(t^{\prime})$ and
$(I,r^{\prime\prime},t^{\prime})\models\square{\varphi}$. Thus,
$(I,r^{\prime\prime},t^{\prime})\not\models\lozenge{\lnot\varphi}$. It remains
to note that
$r^{\prime\prime}_{i}(t^{\prime})=r_{i}^{\prime}(t^{\prime})=r_{i}(t)$. Hence,
$(I,r,t)\not\models K_{i}\lozenge{\lnot\varphi}$. ∎

###### Proof of Lemma 21.

The right-to-left direction is trivial. Hence, we prove the implication from
left to right. Firstly, $\lnot correct_{i}\to(correct_{i}\to\varphi)$ is a
propositional tautology. Hence,

$I\qquad\models\qquad\square{\lnot
correct_{i}}\to\square{(correct_{i}\to\varphi)}.$

Using Lemma 19, the fact that $I\models\square{\psi}\to\lozenge{\psi}$ by
seriality of temporal modalities, and knowledge necessitation, we obtain

$I\qquad\models\qquad K_{i}\bigl{(}\lnot
correct_{i}\to\lozenge{(correct_{i}\to\varphi)}\bigr{)}.$

By epistemically internalized propositional reasoning,

$I\quad\models\quad
K_{i}\bigl{(}correct_{i}\to\lozenge{(correct_{i}\to\varphi)}\bigr{)}\land
K_{i}\bigl{(}\lnot correct_{i}\to\lozenge{(correct_{i}\to\varphi)}\bigr{)}\to
K_{i}\lozenge{(correct_{i}\to\varphi)}.$

Since we have just shown the second conjunct above to be valid, we obtain the
desired

$I\qquad\models\qquad
K_{i}\bigl{(}correct_{i}\to\lozenge{(correct_{i}\to\varphi)}\bigr{)}\to
K_{i}\lozenge{(correct_{i}\to\varphi)}.\qed$

###### Proof of Lemma 23.

By Corollary 22, $I\models B_{i}\lozenge{H_{i}\overline{start}}\to
K_{i}\lozenge{H_{i}\overline{start}}$. Applying factivity of knowledge and
propositional reasoning to the expanded version of
$K_{i}\lozenge{H_{i}\overline{start}}$ yields

$I\qquad\models\qquad K_{i}\lozenge{\bigl{(}correct_{i}\to
K_{i}(correct_{i}\to\overline{start})\bigr{)}}\to
K_{i}\lozenge{(correct_{i}\to\overline{start})}.$

Since $correct_{i}\land\lnot\overline{start}$ is potentially persistent, and
its negation is equivalent to $correct_{i}\to\overline{start}$, we have by
Lemma 20 that

$I\qquad\models\qquad K_{i}\lozenge{(correct_{i}\to\overline{start})}\to
K_{i}{(correct_{i}\to\overline{start})}$

Combining all implications together, we conclude that $I\models
B_{i}\lozenge{H_{i}\overline{start}}\to B_{i}\overline{start}$. ∎

###### Proof of Lemma 26.

Let $I=(R,\pi)$. Assume $(I,{r},{t})\models E^{\lozenge{H}}{\overline{start}}$
for some $r\in R$ and time $t\in\mathbb{T}$. This means that, for every agent
$j\in\mathcal{A}$, there is some $t_{j}^{\prime}\geq t$ such that
$(I,{r},{t_{j}^{\prime}})\models H_{j}{\overline{start}}$. Since
$|\mathcal{A}|\geq 3f+1$, it follows that there exists a group $G$ of $2f+1$
correct agents such that $(I,{r},{t_{j}^{\prime}})\models
H_{j}{\overline{start}}$ for all $j\in G$. Since these agents are
correct,333While we only use the fact that agent $j\in G$ is correct at
$t^{\prime}_{j}$, these agents will necessarily remain correct throughout run
$r$. we have $(I,{r},{t_{j}^{\prime}})\models B_{j}{\overline{start}}$, i.e.,
$(I,{r},{t_{j}^{\prime}})\models
K_{j}({correct_{j}\rightarrow\overline{start}})$ for all $j\in G$. Let
$t^{\prime}\colonequals\max\\{t^{\prime}_{j}\mid j\in G\\}$. We claim that

$(I,{r},{t^{\prime}})\qquad\models\qquad\bigwedge\nolimits_{j\in
G}K_{j}({correct_{j}\rightarrow\overline{start}}).$ (19)

Indeed, for any agent $j\in G$ consider any alternative run $\overline{r}\in
R$ and time $\overline{t^{\prime}}\in\mathbb{T}$ such that
$\overline{r}_{j}(\overline{t^{\prime}})=r_{j}(t^{\prime})$. Given that
$t^{\prime}\geq t^{\prime}_{j}$ and our agents have perfect recall, there must
exist some time $\overline{t^{\prime}_{j}}\leq\overline{t^{\prime}}$ such that
$\overline{r}_{j}(\overline{t^{\prime}_{j}})=r_{j}(t^{\prime}_{j})$. Thus,
$(I,{\overline{r}},{\overline{t^{\prime}_{j}}})\models
correct_{j}\rightarrow\overline{start}$. Since the latter formula is stable,
it remains true in $\overline{r}$ by the time $\overline{t^{\prime}}$. We
showed that $(I,{\overline{r}},{\overline{t^{\prime}}})\models
correct_{j}\rightarrow\overline{start}$ whenever
$\overline{r}_{j}(\overline{t^{\prime}})=r_{j}(t^{\prime})$, meaning
$(I,{r},{t^{\prime}})\models K_{j}({correct_{j}\rightarrow\overline{start}})$.
This argument applies to every $j\in G$, hence, (19) is demonstrated for the
group $G$ of $2f+1$ correct agents.

Correctness (C) applied to $G$ at time $t^{\prime}$ ensures
$(I,{r},{t^{\prime}})\models\bigwedge_{i\in\mathcal{A}}\lozenge{(}correct_{i}\to\overline{fire}_{i})$,
and, since $t\leq t^{\prime}$, we also have

$(I,{r},{t})\qquad\models\qquad\bigwedge\nolimits_{i\in\mathcal{A}}\lozenge{(}correct_{i}\to\overline{fire}_{i}).$

Given that $r$ and $t$ were chosen arbitrarily, we have proved

$I\qquad\models\qquad
E^{\lozenge{H}}{\overline{start}}\to\bigwedge\nolimits_{i\in\mathcal{A}}\lozenge{(}correct_{i}\to\overline{fire}_{i}).$

Using (13), we can conclude

$I\qquad\models\qquad
E^{\lozenge{H}}{\overline{start}}\to\bigwedge\nolimits_{i\in\mathcal{A}}\lozenge{\bigl{(}correct_{i}\to
B_{i}{(\overline{start}\land{E^{\lozenge{H}}{\overline{start}})}}\bigr{)}},$

i.e.,

$I\qquad\models\qquad
E^{\lozenge{H}}{\overline{start}}\to\bigwedge\nolimits_{i\in\mathcal{A}}\lozenge{H}_{i}{(\overline{start}\land{E^{\lozenge{H}}{\overline{start}})}}.$

In other words, we have demonstrated

$I\qquad\models\qquad E^{\lozenge{H}}{\overline{start}}\to
E^{\lozenge{H}}{(\overline{start}\land E^{\lozenge{H}}{\overline{start}})}.$

Using (2) with $\psi=E^{\lozenge{H}}{\overline{start}}$ and
$\varphi=\overline{start}$, we conclude

$I\qquad\models\qquad E^{\lozenge{H}}{\overline{start}}\to{C^{\Diamond
H}{\overline{start}}}.\qed$