[500]Theory of computation Distributed algorithms [300]Networks John Q. Open
and Joan R. Access 2 42nd Conference on Very Important Topics (CVIT 2016) CVIT
2016 CVIT 2016 December 24–27, 2016 Little Whinging, United Kingdom 42 23 TU
Wien,
Austriahugorincongaleana@gmail.comhttp://orcid.org/0000-0002-8152-1275Supported
by the Doctoral College on Resilient Embedded Systems at TU Wien, and the DMAC
project P32431.

# An Asynchronous Graph Characterization of Byzantine Firing Rebels

Hugo Rincon Galeana

###### Abstract

Byzantine agreement tasks have been studied extensively through many diverse
frameworks ranging from epistemic modal logic to combinatorial, topological
and even game theoretical approaches. Among byzantine agreement tasks, firing
rebels with relay is of particular interest, since it is a basic primitive
necessary for solving more complex tasks such as Consistent Broadcast. The
epistemic logic approach has yielded both necessary conditions and sufficient
knowledge conditions for solving firing rebels with relay. However, these
conditions are stated in terms of knowledge and in principle do not explore
the conditions on the communication structure which is often assumed to be
complete. That is, any process is assumed to be capable of communicating with
any other process at any time.

In this paper, we characterize byzantine firing rebels solvability with and
without relay in terms of the communication structure of the system. We define
a relation between asynchronous message schedules and directed graph
sequences, which we call network abstractions. This allows us to capture the
message relay capabilities of the system into a combinatorial object. Although
there are some similarities between network abstractions and causal cones,
there is a fundamental difference. Namely, causal cones allow only to look at
events in the past, while network abstractions allow us to reason about future
possibilities. Thus enabling us to reason about liveness properties, which can
not be expressed by looking only at past events.

Furthermore, we formalize our characterization by using a temporal epistemic
logic for byzantine systems. Such formulation constitutes the necessary and
sufficient a-priori knowledge regarding network connectivity for solving
firing rebels with relay.

###### keywords:

byzantine resilience, epistemic logic, dynamic networks, message adversaries,
asynchronous systems, graph sequences, causal cones

##  1 Introduction

Agreement tasks in general have had a rich development. There exists numerous
characterizations for consensus, from the very general epistemic
characterization due to Halpern and Moses [13] to more specific and particular
results [31, 33, 2, 32, 25].

More specific results on agreement tasks restrict their focus to either the
failure assumptions, the communication restrictions of the system or both [9,
26, 27, 11]. Among the failure assumptions, we can consider crash failures,
omission failures, byzantine failures and even benign settings where no
explicit failure is part of the system model. Communication assumptions on the
other hand are stated in terms of synchrony [23, 15] and the communication
primitive. Namely, we may consider systems that communicate by either message
passing or a shared memory object in a synchronous, semi-synchronous or fully
asynchronous manner.

We consider an asynchronous system with a global time to which processes do
not necessarily have access. For each run, we consider a message schedule that
associates message sending times to message receiving times. In this approach
we consider message schedules as potential causal cones [16]. Although casual
cones necessarily relate to the past, message schedules relate to future
possibilities. In this sense, one might consider causal cones as a backward
information trace, and schedules as forward information dissemination
possibilities.

In this paper, we will focus on systems with byzantine faults and asynchronous
communication [3]. We consider unrestricted byzantine processes, which can
deviate arbitrarily from the protocol. Such systems are better known from the
classic Byzantine Generals problem [20]. We consider, however, a more relaxed
agreement task known as the firing rebels, which is closely related to the
firing squad problem [10, 8].

In the firing rebels problem we assume that there is a global event, namely
the START event, which may be witnessed by some of the processes. We also
assume that processes can execute a FIRE action on which we impose the
following restrictions:

  1. 1.

Correctness: If sufficiently many processes observed a START event, then all
correct agents must execute FIRE eventually.

  2. 2.

Unforgeability: If a correct process executes FIRE, then START was observed by
a correct process.

  3. 3.

Relay: If a correct process executes FIRE, then eventually all correct
processes execute FIRE.

Firing rebels with and without relay has been studied from an epistemic logic
framework [10]. This approach has yielded a knowledge based characterization
for firing rebels without relay, and necessary conditions for firing rebels
with relay. Further results have yielded sufficient conditions for gaining
belief [28]. However, it should be noted that neither of these results impose
any network or communication restrictions on the system.

Firing rebels with relay is one of the weakest agreement problems in byzantine
resilient systems. It is a weaker primitive than consistent broadcast, which
in turn is a basic primitive for byzantine agreement. For example, the
topological characterization of shared-memory byzantine resilient tasks given
by Mendes, Tasson and Herlihy [21] rely on a consistent broadcast primitive.

#### Contributions:

In this paper we provide the following contributions

  * •

A framework that enables us to represent the communication potential of an
asynchronous system as a sequence of communication graphs. Namely network
abstractions and path closed schedules.

  * •

A characterization of firing rebels with relay in terms of its communication
network topology. Thus setting minimal network topology conditions for
byzantine agreement tasks.

  * •

A simple asynchronous protocol for firing rebels with relay with bounded
message size.

  * •

A temporal epistemic logic formulation of necessary and sufficient a-priori
knowledge for solving firing rebels with relay.

#### Paper organization:

First in the introduction we give a general outline of the context, we provide
a brief description of the paper organization, and we establish connections to
related work. In Section 2 we provide the description of the system, as well
as the general assumptions of our paper. We also define the basic concepts for
establishing our results. In Section 3 we provide algorithms for firing rebels
with, and without relay. Furthermore, we provide a characterization in terms
of network connectivity using the framework provided in the previous section.
In Section 4 we provide a temporal epistemic logic formulation of the
characterization presented in Section 3. Finally in Section 5 we close with a
general overview of the results and some ideas for future work.

#### Related Work

In this paper we generalize the notion of syncausal cones and process-time
graphs [19, 4]. The generalization follows from also considering potential
future message traces instead of only past message traces. This enables us to
formulate liveness properties of the system, which is not possible by only
looking at the past.

Network abstractions bear some resemblance to message adversaries [1] in the
sense that both approaches represent the network topology as directed graph
sequences. A fundamental difference lies in what the directed graphs
represent. In the message adversary framework, a directed graph represents all
the point to point communication at a given round in a synchronous setting. In
our context, we rather match the paths in a graph to message relay
opportunities in an asynchronous setting.

A closely related problem, namely the byzantine firing squad problem has been
characterized by Charron-Bost and Moran [6]. In their approach however, they
assume a synchronous static graph setting, and require that all processes
execute FIRE at the same time. In contrast we assume a setting with
asynchronous starts, events and communication. We also drop the requirement
that processes execute FIRE in a synchronous manner.

Furthermore this work builds upon existing results on the Firing Rebels
problem [10, 17, 16, 28]. Concretely we use the temporal epistemic framework
to formulate our network conditions in Section 4.

##  2 System Model

We consider a finite set of processes $\Pi=\\{p_{1},\ldots,p_{n}\\}$ with
unique ids that communicate through message passing. A subset of processes
$B\subseteq\Pi$ is allowed to deviate arbitrarily from the protocol. The
membership of a process in $B$ is generally assumed to be static and a priori
unknown for any other process. We call $B$ the set of byzantine processes
[20], and assume that $|B|\leq f$ for some a priori known $f\geq 1$. Since
firing rebels is the weakest agreement task that we will consider, which has
been shown to need a majority of correct processes [10], we will assume
throughout this work that $n\geq 2f+1$.

Although byzantine processes may behave arbitrarily and thus, e.g., omit
sending messages or send messages with incorrect information, they cannot
forge their ids. We assume that byzantine agents can successfully simulate
correct process behavior, i.e. any global state $s$ reached by only correct
processes is indistinguishable for correct processes in another global state
setting $s^{\prime}$ where the byzantine processes simulate a subset of the
correct processes. Notice that this assumption is in line with the concept of
fully-byzantine systems [18].

As usual, processes execute a protocol, given as a state machine. Whenever the
adversary schedules a process to take a step, it applies its transition
function to its current local state and some subset of the received but not
yet processed messages to compute a new local state and a set of messages to
be sent. The adversary determines when a sent messages is delivered to the
receiver. We allow our processes to also experience externally triggered
_events_ $E\in\mathbf{E}$, which happen at most once at every process, and are
processed in the subsequent state transition.

We do not generally require any synchrony properties other than the existence
of a linear global time and Zeno-freedom: Every event in the system (a step of
a process, a message delivery or an external event) happens at some objective
global time, taken from a linearly ordered time set $\mathbb{T}$ that is
usually either $\mathbb{N}$ or $\mathbb{R}$, and at most finitely many events
may occur in a finite time interval. Note that processes do not necessarily
have access to global time or even an internal notion of time, other than
their local state transition histories, albeit such means could be added later
on.

In general, we consider systems with asynchronous starts, as it is usually
assumed for asynchronous systems, and sometimes also for partially synchronous
and even synchronous systems [30, 7]. That is, processes may start their
execution at different times and are not a priori aware of the already active
processes. Messages that are sent to a process that is not active at the time
of the message reception are lost without a trace. For convenience, we will
assume that a process starts its execution when the external event WAKE has
occured.

System-wide, this leads to executions (also called runs) that can be
represented by the generated sequence of configurations, which are the vectors
of the local states of all the processes and their unprocessed messages sets
taken at the global time when some process takes a step.

Regarding protocols, we will primarily assume a flooding full-information
protocol, where all processes will broadcast their full history whenever they
make a step. Although highly impractical and inefficient, such a protocol is
favorable for exploring solvability/impossibility issues. However, we will
also present a minimalistic protocol, in terms of message size and processing,
that solves firing rebels with relay.

###  2.1 Network and event schedules

Contrasting traditional modeling, we make (some) actions and even potential
actions of the adversary explicit by means of _message schedules_.
Intuitively, a message schedule $\sigma$ tells at what time $\sigma(p,q,t)$ a
process $q$ _would_ receive a message from process $p$ if such a message was
sent to it at time $t$. A simple example of a message schedule is
$\sigma(p,q,t)=t+\delta_{pq}$, as used in [4], where $\delta_{pq}$ is an a
priori known bound on the end-to-end delay of the messages from $p$ to $q$.
General message schedules extend this to message delay bounds that can vary
with time, e.g., caused by network bandwidth fluctuations or outages. Note
carefully, however, that message schedules are not intended to model
variations caused by the protocol execution itself, like message sizes,
receiver queueing effects or network congestion.

######  Definition 2.1 (Message Schedules).

We say that
$\sigma:\Pi\times\Pi\times\mathbb{T}\rightarrow\mathbb{T}\cup\\{\infty\\}$ is
a _message schedule_ , if for any $p,q\in\Pi$ and $t\in\mathbb{T}$,
$\sigma(p,q,t)>t$. We denote $(p,q,t)=\infty$ if a message sent from $p$ to
$q$ at time $t$ will never be delivered.

Regarding events, which are traditionally considered instantaneous [4], we
allow events to have a starting and an ending time. Similar to message
schedules, we also consider event schedules in our framework. An additional
advantage of this modeling is that events can now be treated as self-messages,
albeit with a schedule independent to true message communication.

######  Definition 2.2 (Event schedule).

Let $S\subseteq\Pi$ be a set of processes. We say that
$\sigma_{E}:S\rightarrow\mathbb{T}\times\mathbb{T}$ is an _event schedule_ for
the triggering of the event $E\in\mathbf{E}$ at some process, if
$\sigma_{E}(p)=(t_{i},t_{f})$ whenever event $E$ starts to happen at process
$p$ at time $t_{i}$ and finishes at time $t_{f}<\infty$. Otherwise, if
$t_{f}=\infty$, then the event will never be processed at $p$ and in such a
case we would simply consider that $p\notin S$.

The communication possible in a given system is described by a set of possible
message schedules, which is arbitrary. There is a subtle relation between the
set of possible runs of a given system and its set of possible message
schedules, however: For every run, there must be at least one corresponding
message schedule (there may be many, which may differ at times where no
messages are sent in the run). On the one hand, it depends both on the sender
process scheduling and the protocol whether a message is actually sent at some
time $t$ in a run or not. On the other hand, the message schedule must
faithfully reflect the delay of every message actually sent in the run.

Hence, the protocol and the sender process scheduling typically restrict the
range of $t$ on which a message schedule needs to be applied. In order to
simplify our reasoning, we will thus consider only _discrete fragments_ of
message schedules, which are defined as follows:

######  Definition 2.3 (Discrete fragments).

We say that $F_{\sigma}:F\rightarrow\mathbb{T}\cup\\{\infty\\}$ is a _discrete
fragment_ of a message schedule $\sigma$ if
$F\subseteq\Pi\times\Pi\times\mathbb{T}$ is countable.

Note that the restriction of general message schedules to discrete fragments
does not sacrifice expressiveness, since any protocol can send at most a
countable number of messages anyway.

Given a message schedule $\sigma$ corresponding to a given run $r$ of a
protocol, the discrete fragment of $\sigma$ induced by $r$ is the set of all
tuples $(p,q,t)\subseteq\Pi\times\Pi\times\mathbb{T}$ where $p$ sent/did not
send a message to $q$ at time $t$. Note that including times where $p$ did not
send a message allows for utilizing communication-by-time [19, 12]. We hence
define:

######  Definition 2.4 (Run fragments).

Let $r$ be a run of protocol $\mathcal{P}$ in a distributed system with some
corresponding message schedule $\sigma$ and event schedules $\sigma_{E}$,
$E\in\mathbf{E}$. We define the run fragment $F_{r}$ induced by $r$ as the
discrete fragment induced by $F=\mathcal{M}\cup\mathcal{E}$, where

  * •

$\mathcal{M}=\\{(p,q,t)\;|\;\textrm{p decided to communicate or stay silent to
q at a time t }\\}$ is the part of the fragment that corresponds to messages

  * •

$\mathcal{E}=\bigcup\limits_{E\in\mathbf{E}}\\{(p,p,t_{i}),(p,p,t_{f})\;|\;\sigma_{E}(p)=(t_{i},t_{f})\\}$
is the part of the fragment that corresponds to events.

Note that our Zeno-freedomness assumption guarantees that processes can only
send finitely many messages in finite time, which translates to
$|F_{\sigma[t_{1},t_{2}]}|<\infty$, where
$F_{\sigma[t_{1},t_{2}]}=\\{(p,q,t)\;|\;t\in[t_{1},t_{2}]\\}$ for every finite
time interval $[t_{1},t_{2}]$.

We conclude this subsection by noting that discrete fragments bear some
similarity to Lamport’s happens-before relation [19] and process-time graphs
[4]. In fact, they could just be considered as an alternative representation.
However, a fundamental difference is that the traditional approaches involve
only successfully delivered messages. Fragments, like the syncausality
relation introduced in [4], also incorporate deliberately or erroneously not
taken message sending opportunities.

###  2.2 Network abstractions

In this section, we will use the representation of runs based on discrete
fragments of message schedules for defining a higher-level communication
abstraction. Our _network abstractions_ primarily abstract away time, albeit
in a way that does not obfuscate the essential causality relations. We will
introduce our approach for message schedules first, and explain later how to
incorporate event schedules.

A core property of a discrete fragment of a message schedule $F_{\sigma}$ is
path-closedness with respect to some directed graph $G$ on $\Pi$. Informally,
it guarantees that $F_{\sigma}$ contains some causal message chain for every
directed path in $G$. Conversely, $G$ will be called a static network
abstraction of $F_{\sigma}$ in this case.

######  Definition 2.5 (Path-closed fragment).

Let $F_{\sigma}:F\rightarrow\mathbb{T}\cup\\{\infty\\}$ be a discrete fragment
of a message schedule $\sigma$ and $G$ a directed graph with $V(G)=\Pi$.

We say that $F_{\sigma}$ is _path-closed with respect to $G$_, if, for any
simple directed path $\mathcal{P}=(x_{1},\ldots,x_{k})$ in $G$ (i.e., without
repeating vertices), there exists a time sequence $(t_{1},\ldots,t_{k-1})$
such that, for any $0\leq i\leq k-1$, the following holds:

  1. 1.

$(x_{i},x_{i+1},t_{i})\in F_{\sigma}$

  2. 2.

$\sigma(x_{i},x_{i+1},t_{i})<t_{i+1}$

######  Definition 2.6 (Static network abstraction).

Let $F_{\sigma}$ be a discrete fragment of a message schedule $\sigma$. We say
that a directed graph $G$ on $\Pi$ is a _static network abstraction_ of
$F_{\sigma}$ if $F_{\sigma}$ is path-closed with respect to $G$.

The intuition behind a static network abstraction $G$ of a discrete fragment
$F_{\sigma}$ is hence that there is an _opportunity_ for relaying messages as
described by $G$. No information about _when_ this opportunity emerges is
provided, however. Moreover, there is no guarantee that this opportunity
emerges more than once.

It should also be noted that, in general, static network abstractions of a
discrete fragment $F_{\sigma}$ are not unique. Furthermore, if both $G_{1}$
and $G_{2}$ are static network abstractions of $F_{\sigma}$, $G_{1}\cup G_{2}$
is not necessarily a static network abstraction. For example, $(p\to q)\in
G_{1}$ and $(q\to r)\in G_{2}$ do not need to be consecutive in $F_{\sigma}$,
i.e., do not form a causal chain $(p\to q\to r)$.

Static network abstractions can nevertheless be extended to finite graph
sequences $\mathbf{G}=(G_{1},\ldots,G_{k})$. The intuition underlying
Definition 2.7 is that since a single graph represents a set of single causal
chains, a sequence of graphs represents a set of causal chains formed by path
concatenation. If $\mathbf{P}_{1}$ and $\mathbf{P}_{2}$ denote the sets of
simple paths of $G_{1}$ and $G_{2}$, respectively, we define their path
concatenation as
$\mathbf{P}_{1}\oplus\mathbf{P}_{2}=\\{(x_{1},x_{2},\dots,x_{m})|(x_{1},\dots,x_{k})\in\mathbf{P}_{1},(x_{k},\dots,x_{m})\in\mathbf{P}_{2},1<k<m,\mbox{$x_{i}\neq
x_{j}$ for $1\leq i,j\neq i\leq m$}\\}$.

######  Definition 2.7 (Finite network abstraction).

Let $G_{1},\ldots,G_{k}$ be static network abstractions of the same discrete
fragment $F_{\sigma}$ of a message schedule $\sigma$, and
$\mathbf{P}_{1},\ldots,\mathbf{P}_{k}$ their corresponding sets of simple
paths. We say that $G_{1}\cdot G_{2}\cdot\ldots\cdot G_{k}$ is a _finite
network abstraction_ of $F_{\sigma}$ if, for any simple path
$P=(x_{1},\ldots,x_{m})\in\mathbf{P}_{1}\oplus\ldots\oplus\mathbf{P}_{k}$,
there is a time sequence $(t_{1},\ldots,t_{m-1})$ such that for any $1\leq
i\leq m-1$:

  1. 1.

$(x_{i},x_{i+1},t_{i})\in F_{\sigma}$

  2. 2.

$\sigma(x_{i},x_{i+1},t_{i})<t_{i+1}$

  3. 3.

$\sigma(x_{m-1},x_{m},t_{m-1})<\infty$

We can extend Definition 2.7 to infinite sequences in a natural way by
considering all finite prefixes.

######  Definition 2.8 (Dynamic network abstraction).

Let $\mathcal{G}=G_{1},\ldots,G_{i},\ldots$ be an infinite graph sequence. We
say that $\mathcal{G}$ is a _dynamic network abstraction_ of a discrete
fragment $F_{\sigma}$ of a message schedule $\sigma$, if any finite prefix $P$
of $\mathcal{G}$ is a finite network abstraction of $F_{\sigma}$.

######  Remark 2.9.

We note that if finitely many graphs $\\{G_{1},\ldots,G_{k}\\}$ all repeat
infinitely often in a network abstraction of a schedule fragment $F_{\sigma}$,
then $G^{\omega}$ is a dynamic network abstraction of $F_{\sigma}$, where
$G=G_{1}\cup\ldots\cup G_{k}$ is the union graph consisting of all edges of
$G_{1},\ldots,G_{k}$.

We will now generalize our network abstractions to also incorporate events,
which will be called _communication abstractions_ in the sequel. Recall that
we advocated already earlier to think of events as self-messages.
Consequently, we can encode event occurrences as graphs consisting of only
loops, with the convention that a loop counts as a simple path. This allows us
to seamlessly interweave events and message chains.

######  Definition 2.10 (Event graph).

Let $E$ be an event that is triggered and processed by the processes
$S_{E}\subseteq\Pi$ in the event part $\mathcal{E}$ of a run fragment $F_{r}$.
The _event graph_ $G_{E}=\langle V(G_{E}),E(G_{E})\rangle$ for $E$ occurring
in $\mathcal{E}$ is defined by $V(G_{E})=\Pi$, and $E(G_{E})=\\{(p,p)\;|\;p\in
S_{E}\\}$.

######  Definition 2.11 (Finite communication abstraction).

For a run fragment $F_{r}$ of a run $r$ with message schedule $\sigma$ and
event schedules $\sigma_{E}$, $E\in\mathbf{E}$, let $G_{1},\ldots,G_{k}$ be a
sequence consisting of either network abstractions or event graphs of $F_{r}$,
and $\mathbf{P}_{1},\ldots,\mathbf{P}_{k}$ their corresponding sets of simple
paths (with loops considered as simple paths). We say that
$G_{1}\cdot\ldots\cdot G_{k}$ is a _finite communication abstraction_ of
$F_{r}$ if, for any simple path
$P=(x_{1},\ldots,x_{m})\in\mathbf{P}_{1}\oplus\ldots\oplus\mathbf{P}_{k}$,
there is a finite time sequence $(t_{1},\ldots,t_{m})$ such that for $1\leq
i\leq m-1$:

  1. 1.

If $x_{i}\neq x_{i+1}$, then $(x_{i},x_{i+1},t_{i})\in\mathcal{M}$

  2. 2.

If $x_{i}\neq x_{i+1}$, then $\sigma(x_{i},x_{i+1},t_{i})<t_{i+1}$

  3. 3.

If $x_{m-1}\neq x_{m}$, then $\sigma(x_{m-1},x_{m},t_{m-1})<\infty$

  4. 4.

If $x_{i}=x_{i+1}$, representing event $E$, then
$\sigma_{E}(x_{i})=(t_{i},t^{\prime})$ and $t^{\prime}<t_{i+1}$

######  Definition 2.12 (Dynamic communication abstraction).

Let $\mathcal{G}$ be an infinite graph sequence consisting of either network
abstractions or event graphs for a run fragment $F_{r}$. We say that
$\mathcal{G}$ is a _dynamic communication abstraction_ of $F_{r}$ if any
finite prefix $P$ of $\mathcal{G}$ is a finite communication abstraction of
$F_{r}$.

Recall that we assumed that the processes start executing when they have
experienced the external event WAKE, which is assumed to eventually occur at
every process. We can thus safely assume that every communication abstraction
starts with the WAKE event graph. It will therefore be omitted throughout the
rest of our paper.

##  3 Firing Rebels

Firing rebels is a byzantine resilient task that is the cornerstone for other
byzantine resilient communication primitives, such as consistent broadcast. We
assume that there exists a START event that can be witnessed by processes at
any given time. In turn, processes can communicate through messages, and
execute a FIRE action. In firing rebels we require that if enough correct
processes witness a START event, then eventually all correct processes should
fire. However, in order to prevent trivial solutions, we must also require
that a correct agent executes a FIRE action only when a START event occurred
at a correct agent. In the following, we consider the same settings for firing
rebels as Fruzsa et al [10].

######  Definition 3.1 (Firing rebels).

Consider the following conditions on a system with at most $f\geq 0$ byzantine
processes.

  1. C

Correctness: If at least $2f+1$ processes learn that START occurred at a
correct agent, then all correct processes perform $FIRE$ eventually.111Notice
that this notion of correctness refers to processes that will never exhibit
byzantine behavior.

  2. U

Unforgeability: If a correct process executes FIRE, then START occurred at a
correct process.

  3. R

Relay: If a correct process executes FIRE, then eventually all correct
processes execute FIRE.

We say that a protocol solves Firing Rebels if any run satisfies correctness
and unforgeability. Furthermore, we say that a protocol solves Firing Rebels
with Relay if it also satisfies the relay property.

In order to improve the proof for the Firing Rebels characterization, we will
state some useful graph theoretic definitions and lemmas.

######  Definition 3.2 (Strong vertex connectivity).

Let $G=\langle V,E\rangle$ be a directed graph with respective set of vertices
$V$ and edges $E$. We say that $G$ is $k$ strongly vertex-connected if $|V|>k$
and for any vertex subset $S\subset V$ such that $|S|<k$, the subgraph induced
by $V\setminus S$ is strongly connected.

######  Theorem 3.3 (Menger’s theorem).

Let $G$ be a directed graph. $G$ is $k$ strongly vertex connected iff for any
pair of vertices $v,w$, $v\neq w$; there exist at least $k$ internally
disjoint paths from $v$ to $w$.

Although Menger’s theorem is traditionally stated for undirected graphs, it
can also be generalized to directed graphs and beyond [5].

######  Lemma 3.4 (Source Lemma).

Let $G$ be a $k$ strongly vertex connected directed graph. For any set of
vertices $S$ and any vertex $v$ such that $v\notin S$ and $|S|=k$. Then there
exist $k$ disjoint paths from $S$ to $v$.

######  Proof 3.5.

Consider a set $S$ such that $|S|=k$ and a vertex $v\notin S$. Let $w$ be a
vertex foreign to $G$, i.e. $w\notin V(G)$. Consider graph $G^{\prime}=\langle
V(G^{\prime}),E(G^{\prime})\rangle$, where $V(G^{\prime})=V(G)\cup\\{w\\}$ and
$E(G^{\prime})=E(G)\cup\\{(w,u),(u,w)\;|\;u\in S\\}$.

Notice that $G^{\prime}$ is also $k$ strongly vertex connected. Let $U\subset
V(G^{\prime})$ be a vertex set such that $|U|<k$. If $w\in U$, then
$G^{\prime}\setminus U=G\setminus(U\setminus\\{w\\})$. Since
$|U\setminus\\{w\\}|<|U|<k$, then $G^{\prime}\setminus U$ is strongly
connected. If $w\notin U$ it is sufficient to show that $w$ is reachable and
can reach the rest of $G^{\prime}\setminus U$. This follows from $G\setminus
U$ being strongly connected. Since $|U|<k$, and $|S|=k$, then $S\setminus
U\neq\varnothing$. It follows that there exists a vertex $u\in S\setminus U$.
Notice that edges $(w,u)$ and $(u,w)\in G^{\prime}\setminus U$. Since $u\in
G\setminus U$, then $u$ is strongly connected to all vertices in $G\setminus
U$. Therefore $w$ is also strongly connected to all vertices in $G\setminus
U$. It follows that $G^{\prime}\setminus U$ is strongly connected, completing
the proof that $G^{\prime}$ is $k$ connected.

From Theorem 3.3 it follows that there are at least $k$ internally disjoint
paths $P_{1},\ldots,P_{k}$ from $w$ to any other vertex $v\notin S$. Since $w$
is only adjacent to $S$, then necessarily any $P_{i}\setminus\\{w\\}$, $1\leq
i\leq k$, is a path from $S$ to $v$. Since each $P_{i}$ is internally
disjoint, then so are $P_{i}\setminus\\{w\\}$.

Lemma 3.4 relates strong vertex connectivity to redundant reachability from
any source of a given size $k$. This condition may be too strong for some
applications such as firing rebels without relay. Therefore we propose the
following definition.

######  Definition 3.6 (Strong root).

Let $G$ be a directed graph and $S\subseteq V(G)$. We say that $S$ is a
$k$-strong root of $G$ if for any vertex $v\notin S$ there exist at least $k$
disjoint paths from $S$ to $v$.

######  Theorem 3.7.

Let $G$ be a directed graph. $G$ is $k$-vertex strongly connected iff any set
$S$ such that $|S|=k$ is a $k$-strong root.

######  Proof 3.8.

Assume that $G$ is $k$-vertex strongly connected, and $S$ such that $|S|$. It
follows from Lemma 3.4 that $S$ is a $k$-strong root.

Now assume that $G$ is not $k$-vertex strongly connected. Then there exists a
vertex set $S\subseteq V(G)$ of size $k-1$ that separates a vertex $x$ from a
vertex $y$, i.e. $x$ can not reach $y$ in $G\setminus S$. Notice that
$S\cup\\{x\\}$ is not a k-strong root of $G$, otherwise there would exist $k$
disjoint paths from $S\cup\\{x\\}$ to $y$. Since $|S|=k-1$, then there is at
least one path from $x$ to $y$ that bypasses $S$, contradicting that $S$
separates $x$ from $y$.

1 $H\leftarrow\varnothing$;

2 if  _$witness(\mathbf{START})$_ then

3 $H\leftarrow\\{\mathbf{START}\\}$;

4 fire;

5 while  _true_ do

6 $\mathbf{broadcast}(H)$;

7

8while  _$\mathbf{true}$_ do

9 $temp\leftarrow\mathbf{receive}()$;

10 if  _$\mathbf{pid}\notin temp.chain$_ then

11 $H\leftarrow H\cup\\{temp.chain+temp.sendid\\}$;

12

13 if  _$disjoint(H)\vee witness(\mathbf{START})$_ then

14 $H\leftarrow\\{\mathbf{START}\\}$;

15 fire;

16 while  _$\mathbf{true}$_ do

17 $\mathbf{broadcast}(H)$;

18

19 $\mathbf{broadcast}(H)$;

20

Algorithm 1 A protocol for firing rebels without relay

Consider Algorithm 1 for solving firing rebels without relay. A process
executing Algorithm 1 stores an initially empty collection of message relay
chains attesting to a START event into a variable H. An example of a message
relay chain is $p_{1}(p_{4}(START))$. In this example, a process received a
message chain from $p_{1}$ claiming that $p_{1}$ in turn received a message
from $p_{4}$ claiming that a START event occurred.

$H$ is eagerly broadcasted as soon as it is non-empty. Upon receiving a
message chain attesting to a START event, the process checks if itself is
already part of such a message chain. If it is not part of the message chain,
then it appends the sender id to all the message chains and updates $H$. Once
a process either witnesses a START event or receives at least $f+1$ disjoint
chains attesting to START, it will fire and only broadcast singleton
$\\{START\\}$ ever after.

More precisely, in Algorithm 1: $witness$ is a subroutine that informs a
process whether or not it witnessed a particular global event; broadcast is a
subroutine that attempts to send a particular message to all possible outgoing
communication channels; fire triggers the FIRE action on the executing
process; $temp$ is a local variable intended for storing a single message
chain; pid is the local attribute of the executing process corresponding to
its id, with attributes $chain$ and $sendid$ that correspond to the message
chain and the sender’s id respectively; $disjoint$ is a subroutine that takes
a collection of message chains and verifies if there are at least $f+1$
disjoint message chains attesting to START.

######  Lemma 3.9.

Algorithm 1 satisfies Correctness for any run $r$ with a communication
abstraction $ST\cdot G$, where $ST$ is the START event graph, $S$ is the
participating set of $ST$, and $S$ is a $2f+1$ strong root of $G$.

######  Proof 3.10.

If the START event is witnessed by less than $2f+1$ processes, then
Correctness holds by vacuity. Therefore, we may assume that a set $S$ of
$2f+1$ processes witnessed a START event. Notice that all correct processes
from $S$ will enter either enter line 2 or line 11, and therefore fire by
executing either line 4 or line 13 respectively.

Consider a correct process $v$ such that $v\notin S$. By assumption, there are
$2f+1$ disjoint paths from $S$ to $v$ in $G$. Since the paths are disjoint and
there are at most $f$ faulty processes, then there are at least $f+1$ paths in
$G$ containing only correct processes. We consider $f+1$ such paths, namely
$P_{1},\ldots,P_{f+1}$.

Consider a process $w\in P_{i}$. If $w$ enters line 2 or line 11 before their
scheduled relay opportunity $t_{w}$ in $P_{i}$, then they will use their edges
at time $t_{w}$ to broadcast START according to lines 6 and 15. Otherwise,
from the hypothesis that $ST\cdot G$ is a communication abstraction, they will
relay a START from a previous process in $P_{i}$. Therefore $v$ will receive a
relayed $START$ message chain suffix from each path $P_{i}$. Since the paths
$P_{i}$ are disjoint and formed only by correct processes, then $v$ will
receive at least $f+1$ disjoint message chains attesting to START. Therefore,
$v$ will enter line 11 and inevitably fire by executing line 13.

######  Lemma 3.11.

Algorithm 1 satisfies Unforgeability for any run $r$.

######  Proof 3.12.

Let $p$ be any correct process executing Algorithm 1 that fires. Since line 4
and line 14 are the only lines where fire is executed, then either $p$
witnessed a START event or it received at least $f+1$ disjoint chains of a
START event. Since there are at most $f$ byzantine faulty agents, then a START
event was witnessed by a correct process.

######  Lemma 3.13 (Firing rebels impossibility).

Let $r$ be a run of a protocol $P$ in an asynchronous fully byzantine
$f$-resilient system with a START event witnessed by a set $S$ of $2f+1$
processes. If there is no directed graph $G$ such that $S$ is a $2f+1$-strong
root and $ST\cdot G$ is a communication abstraction of $F_{r}$, then $P$ does
not solve Firing Rebels.

######  Proof 3.14.

It follows from the hypothesis that $S$ cannot relay $2f+1$ disjoint START
message chains to at least one process $v\notin S$. Assume for the sake of a
contradiction otherwise. Let $G^{\prime}$ be the graph that represents all
possible message chain relays originating at $S$. From the contradiction
hypothesis, it follows that $S$ can reach any other vertex with $2f+1$
disjoint START message chains. It follows that $S$ is a strong root of
$G^{\prime}$, and $ST\cdot G^{\prime}$ is a communication abstraction
contradicting the hypothesis.

Let $\mathcal{P}$ be a set of disjoint paths from $S$ to $v$ of maximal size
that happen after the START event. Notice that $|\mathcal{P}|<2f+1$. Let $B$
be a set of $f$ sources from $\mathcal{P}$. Notice that $S\setminus B$ has
less than $f+1$ disjoint paths to $v$. Otherwise $S$ would have at least
$2f+1$ disjoint paths to $v$ contradicting the maximality of $\mathcal{P}$.
Therefore, there is a set $U$ of at most $f$ vertices that breaks each path
from $S\setminus B$ to $v$.

Since the system is fully-byzantine, there is a run $r_{1}$ with the same
communication possibilities as $r$ but where $B$ is byzantine. Furthermore
assume that the byzantine behavior is to simulate that they did not witness a
START event. Notice that for $v$, $r_{1}$ is indistinguishable from a run
$r_{2}$ where no START event happened, and all vertices in $U$ are byzantine
processes simulating the relay paths from $S\setminus B$. Since $r_{2}$ is
indistinguishable from $r_{1}$ to process $v$ and in $r_{2}$ no START event
happened, then $v$ should not fire at run $r_{1}$ in order to satisfy
Unforgeability. However, at run $r_{1}$ there are $2f+1$ witnesses of a START
event. Therefore $v$ should fire at run $r_{1}$ in order to satisfy
Correctness.

######  Theorem 3.15 (Firing Rebels solvability).

Firing Rebels is solvable in a uniform byzantine system iff for any run $r$
such that $r$ has a START event with at least $2f+1$ witnesses, the run
fragment $F_{r}$ admits a communication abstraction $ST\cdot G$ where $ST$ is
the START event graph, and the $G$ is $2f+1$ strongly rooted with respect to
the witnesses of START.

######  Proof 3.16.

Solvability is given by Algorithm 1 while the impossibility is given by Lemma
3.13.

###  3.1 Firing Rebels with Relay

We have provided a network characterization of byzantine systems that are able
to satisfy both Correctness and Unforgeability. Although necessary for solving
more complex agreement tasks, these two conditions are too weak on their own
to be of any practical interest. In the following we will provide a
characterization for satisfying the relay property in addition to Correctness
and Unforgeability.

Recall that Relay imposes an all or nothing restriction to the fire action,
while Correctness forces correct processes to fire in the presence of a
sufficiently large quorum of START witnesses. It follows that any quorum large
enough to force a fire action should eventually reach all correct processes.
Therefore, we can consider that the Relay condition in addition to the
Correctness property imposes a liveness property on the system. It is natural
to suspect that a finite-lived communication network is not sufficient for
Relay, at least in the asynchronous case.

In order to complete our characterization of Firing Rebels with Relay, we need
to introduce another concept similar to the strong root. However, we are now
interested instead in vertices that can be reached through sufficiently many
disjoint paths. Since our interest has shifted to processes that can receive
sufficiently many disjoint message chains instead of processes that can send
sufficiently many disjoint message chains, we will call this new concept a co-
root.

######  Definition 3.17.

Let $G$ be a directed graph, we say that a vertex set $C$ is a $k$ co-root of
$G$ with respect to a vertex set $B$ if for any vertex $v\in C$, there is a
vertex set $S(v)$ that can reach $v$ through $k$ disjoint paths that do not
intersect $B$.

Notice that $C$ is a co-root of $G$ iff the minimum in-degree of $C$ in
$G\setminus B$, denoted by $\delta_{G\setminus B}^{-}(C)$, is at least $k$.
This follows from the fact that if a vertex has an in-degree less than $k$,
then it can not be reached by $k$ disjoint paths. Furthermore, since we are
assuming graphs with at most an edge per vertex pair, then the incoming edges
to a vertex of in-degree $k$ form on their own $k$ disjoint paths.

In the following, we present Algorithm 2 which solves Firing Rebels with Relay
whenever there is a persistent and sufficiently strong communication network.

1 $H\leftarrow\varnothing$;

2 $V\leftarrow\varnothing$;

3 $wit\leftarrow\mathbf{false}$;

4 $ready\leftarrow\mathbf{false}$;

5 while  _$\mathbf{true}$_ do

6 $temp\leftarrow\mathbf{receive}()$;

7 if  _$\mathbf{pid}\notin temp.chain$_ then

8 if  _isSTART(temp)_ then

9 $H\leftarrow H\cup\\{temp.chain+temp.sendid\\}$;

10

11 if  _isREADY(temp)_ then

12 $V\leftarrow V\cup\\{temp.chain+temp.sendid\\}$

13 if  _$\neg wit\wedge(disjoint1(H)\vee witness(\mathbf{START}))$_ then

14 $wit\leftarrow\mathbf{true}$;

15 $H\leftarrow H\cup\\{START\\}$

16 if  _$\neg ready\wedge(disjoint1(V)\vee disjoint2(H))$_ then

17 $ready\leftarrow\mathbf{true}$;

18 $H\leftarrow\\{START\\}$;

19 $V\leftarrow\\{READY\\}$;

20 fire;

21 while  _ true_ do

22 $\textbf{broadcast}(H)$;

23 $\textbf{broadcast}(V)$;

24

25 if  _$\neg wit$_ then

26 $\mathbf{broadcast}(H)$;

27 else

28 $\mathbf{broadcast}(\\{\mathbf{START}\\})$;

29 if  _ $V\neq\varnothing$_ then

30 $\textbf{broadcast}(V)$;

31

Algorithm 2 A protocol for Firing Rebels with Relay

Although Algorithm 2 is substantially different from Algorithm 1, it is also
very closely related to it in the sense that Algorithm 2 works essentially as
a two phase Firing Rebels algorithm. We keep track of two different types of
message chains, namely, START and READY message chains. The START message
chains attest to a START event happening, while the READY message chains
attest to $2f+1$ claims of START events. Although it may seem artificial to
create a READY message type for something that can in principle be expressed
through START messages, it actually relaxes the connectivity conditions of the
network.

$H$ represents all the received message chains of type START, initially set to
empty. Symmetrically $V$ represents the received message chains of type READY,
initially set to empty. We also keep boolean flags, $wit$ and $ready$ that
track whether the executing process believes that a START event occurred and
if it is ready to fire, respectively. Whenever a process receives a message,
it stores both the message and sender id into a variable $temp$. Function
$disjoint1$ checks if at least $f+1$ disjoint message chains have been
received, while $disjoint2$ checks if at least $2f+1$ disjoint message chains
have been received. Functions isSTART and isREADY check whether a message
chain corresponds to a START message chain or to a READY message chain
respectively.

######  Lemma 3.18.

Algorithm 2 satisfies Unforgeability for any run $r$.

######  Proof 3.19.

Unforgeability follows from conditioning fire to the presence of at least
$2f+1$ disjoint chains. This can either be learned by receiving directly the
$2f+1$ disjoint chains, or by receiving $f+1$ independent claims that $2f+1$
disjoint chains occurred. Notice that these conditions correspond to the If
guard of line 15, which must be successfully passed in order to execute fire.

######  Lemma 3.20.

Algorithm 2 satisfies Correctness for any run $r$ with a run fragment $F_{r}$
that admits a communication abstraction $ST\cdot G_{1}\cdot G_{2}\cdot G_{3}$
such that $S$ is the participating set of $ST$, $S$ is a strong $2f+1$ root of
$G_{1}$; for any set $B$ of size $f$, $G_{2}$ has a $2f+1$ co-root with
respect to $B$ of size $f+1$; and $G_{3}$ is $2f+1$ strong vertex connected.

######  Proof 3.21.

Let us assume that $ST$ has a participating set $S$ of at least $2f+1$
processes, otherwise Correctness follows from vacuity. Since $S$ is a $2f+1$
strong root of $G_{1}$, then any process $p\notin S$ has at least $2f+1$
disjoint paths from $S$ to $p$ after the START event. Since $ST\cdot G_{1}$ is
a communication abstraction of $F_{r}$, there are $2f+1$ disjoint message
chain relay opportunities from $S$ to $p$. Recall that there are at most $f$
byzantine processes. Therefore, if $p$ is correct then it will eventually
receive at least $f+1$ disjoint message chains and enter line 12. Let $P_{p}$
be the last of the $f+1$ disjoint message chains from $G_{1}$ to reach $p$.

Since there are at most $f$ faulty processes, there is a set $B$ of $f$
processes that contains all faulty processes. Let $Q$ be a $2f+1$ co-root of
$G_{2}$ with respect to $B$ of size $f+1$. Let $q\in Q$. Notice that $q$ is
correct and has at least $2f+1$ correct in-neighbors in $G_{2}$, namely
$w_{1},\ldots,w_{2f+1}$. Notice that each edge $(w_{1},q),\ldots,(w_{2f+1},q)$
is a path in $G_{2}$. Since $ST\cdot G_{1}\cdot G_{2}$ is a communication
abstraction of $F_{r}$, and each $P_{(1,w_{i})}\in G_{1}$ then there is a
message relay opportunity that is represented by $P_{w_{i}}+(w_{i},q)$. Since
each $w_{i}$ at the end of $P_{w_{i}}$ broadcasts $\\{\mathbf{START}\\}$, then
$q$ receives at least $2f+1$ $\\{\mathbf{START}\\}$ messages from its in-
neighbors. Therefore $q$ will successfully enter the conditional at line 15.

Notice that we can think of $ST\cdot G_{1}\cdot G_{2}$ as a $READY$ event
where $Q$ is the participating set of $READY$. Recall that $G_{3}$ is $2f+1$
connected, and therefore any set of size $2f+1$ is a $2f+1$ strong root of
$G_{3}$. In particular $Q\cup B$ is a $2f+1$ strong root of $G_{3}$. It
follows that there are $2f+1$ disjoint paths from $Q\cup B$ to any other
vertex $v$. Therefore, there are at least $f+1$ disjoint paths from $Q$ to any
vertex $v$ that do not intersect $B$. It follows that there are $f+1$ disjoint
message relay paths to any correct process $p\notin Q$ that relay a READY
message. Therefore, eventually any correct process, either belongs to $Q$ or
eventually will receive $f+1$ disjoint message chains attesting to $READY$.
Thus all correct processes will eventually enter line 15 and fire.

######  Lemma 3.22.

Algorithm 2 satisfies Relay for any run $r$ with a run fragment $F_{r}$ that
admits a dynamic network abstraction $\mathcal{G}=G_{1}\cdot\ldots\cdot
G_{k}\cdot\ldots$ such that each $G_{i}$ is $2f+1$ connected and for any
vertex set $B$ of $f$ processes, $G_{i}$ admits a $2f+1$ co-root with respect
to $B$ of size $f+1$.

######  Proof 3.23.

Let us assume that a correct process $p$ fires at an arbitrary time $t_{1}$.
Since $p$ fired, it follows that the execution of $p$ entered line 15
successfully. If $p$ entered line 15 because it received $f+1$ disjoint chains
of a READY message, then at least one chain originated at a correct process
$p^{\prime}$. Inductively, there is a correct process $q$ that entered line 15
because it received $2f+1$ disjoint START chains. It follows that there are at
least $f+1$ START events originating at correct processes.

Notice that this setting is indistinguishable from a START event where also
all byzantine processes witnessed the START event. Since we assume that
$\mathcal{G}$ is infinite, $r$ does not exhibit Zeno behavior and any suffix
of $\mathcal{G}$ satisfies the conditions of Lemma 3.20, then it follows from
Lemma 3.20 that any correct process will eventually fire.

Recall that in Firing Rebels without relay, the case where less than $2f+1$
processes witness a START event is trivial, since a correct process is not
forced to fire. However this changes when we add the Relay condition. This is
because byzantine processes may simulate correct processes that witness a
START event in order to trigger a correct process to fire.

First we will show that finite communication abstractions are not enough for
solving Firing Rebels with Relay.

######  Lemma 3.24.

Let $G_{1}\ldots G_{k}$ be a finite graph sequence, and $P$ a protocol for an
asynchronous uniform byzantine system with at most $f$ byzantine processes
that solves Firing Rebels, i.e satisfies Correctness and Unforgeability. There
exists a run $r$ such that $ST\cdot G_{1}\cdot G_{2}\cdot\ldots\cdot G_{k}$ is
a finite communication abstraction of $F_{r}$ but $P$ does not satisfy Relay.

######  Proof 3.25.

Assume for a contradiction that there exists a finite graph sequence
$G_{1},\ldots G_{k}$ such that whenever a run fragment $F_{r}$ admits $ST\cdot
G_{1}\cdot\ldots\cdot G_{k}$ as a finite communication abstraction, $P$ solves
Firing Rebels with Relay.

Consider a run $r$ with a START event with a witness set $S$ and such that
$F_{r}$ admits $G_{1}\cdot\ldots\cdot G_{k}$ as a finite communication
abstraction, $S=\\{p\\}$ and all processes are correct. Since
$G_{1},\ldots,G_{k}$ is a finite graph sequence, then there is a finite time
$t_{1}$ such that $F_{r}$ admits $ST\cdot G_{1}\cdot\ldots\cdot G_{k}$ within
time $t_{1}$.

Consider a run $r^{\prime}$ that has exactly the same relay opportunities as
$r$ until time $t_{1}$. Let $B=\\{b_{1},\ldots,b_{f}\\}$ be the byzantine
processes in $r^{\prime}$, $p\notin B$. We assume that each $b_{i}$ stays
silent until time $t_{1}$, while the rest of processes execute $P$. After time
$t_{1}$ the byzantine processes simulate to be witnesses of a START event,
while communicating only to $f$ correct processes
$D=\\{c_{1},\ldots,c_{f}\\}$, $p\notin D$. We assume that in run $r^{\prime}$
after time $t_{1}$ there are message opportunities from each process in $B$ to
each process in $D$ in $r^{\prime}$. Furthermore, we assume that there exist
message opportunities for any pair of processes within $D\cup\\{p\\}$ after
the processes in $B$ were able to communicate to the processes in $D$.
Finally, after all the message opportunities within $D\cup\\{p\\}$ have been
used, we assume that no more communication is possible in $r^{\prime}$.

Notice that in run $r$, since $p$ is the only witness to a START event, then
$r$ is indistinguishable for any other process to a run $r_{1}$ where
$\\{p\\}$ is the only byzantine process and simulates being a witness to a
START event. Since $P$ satisfies Unforgeability and Relay, no correct process
fires in $r_{1}$. Since $r_{1}$ and $r$ are indistinguishable for any correct
process that is not $p$, then also in $r$ no correct process fires.

Now consider a run $r_{2}$ that has $D\cup B\cup\\{p\\}$ as the participating
set from START. The same communication opportunities as $r^{\prime}$, however
we assume that all processes are correct, and that $B$ witnesses START at the
same time that $B$ start simulating in run $r^{\prime}$. Furthermore, assume
that after the message opportunities from $r^{\prime}$, there are all possible
messages opportunities from $D\cup B\cup\\{p\\}$ to the rest of the processes.

Notice that for processes in $D\cup\\{p\\}$, runs $r^{\prime}$ and $r_{2}$ are
indistinguishable. Since $P$ satisfies correctness, $P$ should fire at run
$r_{2}$. Therefore, from run indistinguishability, in $r^{\prime}$ all
processes in $D\cup\\{p\\}$ should also fire. On the other hand, for processes
in $\Pi\setminus(D\cup B\cup\\{p\\})$, $r^{\prime}$ is indistinguishable from
$r$, since they can’t receive any message after $t_{1}$. Since no correct
process fires in run $r$, then by run indistinguishability, all processes in
$\Pi\setminus(D\cup B\cup\\{p\\})$ do not fire. Therefore, the Relay condition
does not hold at run $r^{\prime}$.

Since an infinite graph sequence is necessary, then it is no longer necessary
to consider the timing of a START event. This is because no matter when the
START event occurs, there will always exist an infinite graph suffix after the
START event due to the impossibility of Zeno behavior.

######  Lemma 3.26.

Let $r$ be a run of a protocol $P$ that solves Firing Rebels such that $r$
does not admit a dynamic communication abstraction of $2f+1$ vertex strongly
connected graphs. Then $P$ does not satisfy Relay at a run $r^{\prime}$.

######  Proof 3.27.

First, notice that if $r$ does not admit an infinite graph sequence as a
dynamic communication abstraction, then from Lemma 3.24, $P$ does not satisfy
Relay at a run $r^{\prime}$.

Note that if $r$ admits a dynamic network abstraction where any set $Z$ is a
$2f+1$ strong root infinitely often, then $r$ also admits a dynamic network
abstraction where all the graphs are $2f+1$ connected. Simply notice that for
each vertex set $U$ of size $2f+1$, there is a graph $G_{U}$ in the dynamic
network abstraction that repeats infinitely often, and has $U$ as a $2f+1$
strong root. It follows from Remark 2.9 and Theorem 3.7 that all of the
$G_{U}$ graphs can be compacted into a $2f+1$ strongly vertex connected graph
that repeats infinitely often.

Therefore, there exists a set $Z$ of $2f+1$ processes that can reach all other
processes through $2f+1$ disjoint paths only finitely often in $F_{r}$.
Therefore, there is a time $t_{0}$ after which $Z$ is not a $2f+1$ strong
root. It follows from Lemma 3.13 that if there is a START event after $t_{0}$
it, then $P$ cannot solve firing rebels at a run $r^{\prime}$ that has the
same message opportunities as $r$, but a START event only after $t_{0}$.

######  Lemma 3.28.

Let $r$ be a run of a protocol $P$ in an asynchronous uniformly byzantine
$f$-resilient system with a START event witnessed by a set $S$ of $2f+1$
processes. If for any process set $B$ such that $|B|=f$, the message fragment
$F_{r}$ does not admit a dynamic network abstraction
$\mathcal{G}=G_{1},\ldots,G_{i},\ldots$ such that each $G_{i}$ is
$2f+1$-strongly vertex connected and has a $2f+1$ co-root with respect to $B$,
$S_{i},\;|S_{i}|=f+1$ with respect to $B$, then $P$ cannot solve Firing Rebels
with Relay.

######  Proof 3.29.

Notice that a precondition for Firing is that START occurred at a correct
process, and that all other correct processes will eventually learn that START
occurred at a correct process. However, all processes will learn that a START
event occurred regardless of byzantine behavior iff there are at least $f+1$
correct witnesses to a START event. By applying the Knowledge of Preconditions
Principle [22], it follows that a correct process should know that at least
$f+1$ correct processes witnessed a START event. Since byzantine processes are
able to simulate correct processes that witnessed a START event, then a
process needs to learn that $2f+1$ processes claim a START event happening.
Notice that a process might learn this by either witnessing it directly, i.e.
receiving at least $2f+1$ disjoint chains attesting to START; or indirectly,
i.e. receiving $f+1$ disjoint chains attesting to a happening of $2f+1$ START
events. Inductively, there must always be a set of processes that learn
directly $2f+1$ happenings of START. Since byzantine processes may omit
communicating, then there should always be at least $f+1$ correct witnesses
that receive $2f+1$ messages. Since byzantine processes may choose to omit to
send information, then the $f+1$ direct witnesses should always be reachable
from at least $2f+1$ correct processes.

Consider run $r$, and a vertex set $B$ of size $f$. Notice that if $F_{r}$
does not admit a graph sequence $\mathcal{G}=G_{1},\ldots,G_{i},\ldots$ where
each $G_{i}$ has a $2f+1$ co-root with respect to $B$, then any dynamic
network abstraction of $F_{r}$ has only finitely often a $2f+1$ co-root of
size $f+1$ with respect to $B$. Otherwise, we can apply Remark 2.9 to obtain a
graph sequence where each graph is $2f+1$ strong vertex connected and has
$2f+1$ co-root w.r.t $B$ of size $f+1$. It follows that there is a time
$t_{0}$ after which any network abstraction of $r$ does not have a $2f+1$ co-
root w.r.t $B$ of size $f+1$.

Consider a run $r^{\prime}$ with the same message opportunities as $r$, such
that $B$ is the byzantine set, and with a START event with participating set
of $2f+1$ processes that occurs after $t_{0}$. Consider that the byzantine
behavior is just staying silent. Let us assume for a contradiction that the
Correctness property holds, then . It follows from the first part of the proof
that all correct processes learned at some point that at least $2f+1$ START
events occurred. If all processes learned this directly, then they received
$2f+1$ messages attesting to START. Since all processes in $B$ were silent,
this implies that the correct process set form a $2f+1$ co-root w.r.t. $B$ of
size at least $2f+1$, contradicting that there are no $2f+1$ co-roots w.r.t
$B$ of size $f+1$ after $t_{0}$. Notice also that if a process learned
indirectly that there are at least $2f+1$ START events, then it received $f+1$
disjoint message chains attesting to the existence of $2f+1$ START events.
Since all processes in $B$ are silent, then all $f+1$ disjoint chains must
have originated at correct processes. Inductively, we can find a set of $f+1$
correct processes that witnessed directly the $2f+1$ START events. It follows
that the direct witnesses are a $2f+1$ co-root w.r.t $B$ of size $f+1$, also
contradicting that there are no $2f+1$ co-roots w.r.t $B$ of size $f+1$ after
$t_{0}$. It follows that the Correctness condition does not hold.

######  Theorem 3.30 (Firing Rebels with Relay Solvability).

Firing Rebels with Relay is solvable in a uniform byzantine system iff for any
run $r$, $F_{r}$ admits a dynamic network abstraction $\mathcal{G}=G^{\omega}$
where $G$ is a $2f+1$ strongly vertex connected graph such that for any vertex
set $B$ of size $f$, $G$ has a $2f+1$ co-root w.r.t $B$ of size $f+1$.

######  Proof 3.31.

This is a consequence of Lemma 3.18, Lemma 3.20, Lemma 3.22, Lemma 3.24, Lemma
3.26, Lemma 3.28, and from noticing that there are only finitely many possible
graphs. However we consider infinite graph sequences, therefore there is a
single graph that repeats infinitely often. Furthermore, since $2f+1$
connectivity and co-rootedness are closed with respect to union, since they
are existential conditions, then we can apply Remark 2.9 to obtain a single
graph that has all desired properties and repeats infinitely often.

##  4 Epistemic Logic for Byzantine Agents

Although the results are presented in a combinatorial setting, there is a
close relation to epistemic modal logic. In particular to the hope modality
[10, 29] that captures the knowledge gain upon receiving a message from a
possibly faulty agent.

In the following we will give a brief overview of epistemic logic for
byzantine distributed systems, however we will avoid elaborating on many of
the details that can be found in standard Epistemic Logic literature [14].
Furthermore, we build upon existing notation and results from published
results [28, 10, 17, 29].

In the epistemic logic setting, we assume that there is a set of possible
worlds $\mathcal{W}$, which represent global states of the distributed system.
We also assume that properties of the global states of a system may be
represented by propositions. Therefore, formulas that represent properties of
the system are to be evaluated at each of the possible worlds.

We consider a set of agents $\mathcal{A}$, which we assume to be represent the
set of processes $\Pi$ in the distributed system. We also assume that there is
an indistinguishability relation in $\mathcal{W}$, $\mathcal{R}$ indexed by
the set of agents $\mathcal{A}$, which indicates which worlds are
indistinguishable for an agent $a\in\mathcal{A}$. Since we are interested in
modeling process/agent knowledge, we assume that the relation $R$ at any given
agent $a$ is an equivalence relation. In particular, we say that an agent $a$,
in a model $M$ at a world $w$ knows $\varphi$, denoted by $M,w\vDash
K_{a}\varphi$ if $M,w^{\prime}\vDash\varphi$ for any $w^{\prime}$ such that
$(w,w^{\prime})\in R_{a}$. That is, $\varphi$ holds at any world that $a$
considers possible.

If we consider a system where processes can only gain additional knowledge
through communication, and we assume that there might be processes which
deviate arbitrarily from the protocol, then direct knowledge about a global
state is potentially not achievable [17]. Therefore in byzantine systems,
knowledge must be relativized to process correctness. This yields the
definition for belief as defeasible knowledge
$B_{i}\varphi:=K_{a}(correct_{a}\rightarrow\varphi)$ [24].

Belief however, corresponds to local states of processes, but not to
information gains from messages. We can say that the belief gain of an agent
$a$ that receives a message stating $\varphi$ from an agent $b$ can be stated
as $correct_{b}\rightarrow B_{b}(\varphi)$. This corresponds to the hope
modality as defined by Fruzsa et al: $H_{a}\varphi:=correct_{a}\rightarrow
B_{a}\varphi$ [10, 29, 17].

Notice that hope chains correspond to relayed message chains. For instance, a
message chain where process $a$ communicated $\varphi$ to $b$, and $b$ in turn
relayed such a message to $c$ corresponds to $B_{c}(H_{b}(H_{a}(\varphi)))$.
Furthermore Schlögl and Schmid [28] showed that $f+1$ disjoint hope chains of
$\varphi$ are sufficient for acquiring belief of $\varphi$. Furthermore, hope
formulas can be used to express that a process is a witness to an event such
as a START event. If a proposition $p$ represents $START$ occurred, then
$H_{a}p$ can be interpreted as $a$ is a witness of a START event.

Now, in order to incorporate time into our settings, we will use in addition
to possible worlds, and indistinguishability; a time parameter for evaluating
formulas. Since we are incorporating time into the logics, then we will also
make use of temporal modalities such as $\Diamond\varphi$ for eventually
$\varphi$, and $\Box\varphi$ for always $\varphi$ in addition to the already
mentioned epistemic modalities, namely, belief (denoted by $B_{a}\varphi)$,
hope (denoted by $H_{a}\varphi$) and knowledge (denoted by $K_{a}\varphi$).

In this section we will translate our network conditions to necessary and
sufficient a-priori knowledge for solving Firing Rebels with Relay using a
restricted full-information flooding protocol. That is, information about the
network that is available from the start and commonly known to all processes
across all possible executions; in contrast to information gained from
communication.

###  4.1 Vertex Connectivity

Recall that the first condition is that there is a $2f+1$ strongly vertex
connected network abstraction that repeats infinitely often. However, we can
use Lemma 3.4 to translate this condition as a liveness condition in terms of
hope chains.

For convenience we will assume that all hope chains do not repeat the same
agent more than once. Schlögl and Schmid showed that for the purposes of
belief gain, one need only consider such hope chains [28]. Notice then that
the the set of all possible hope chains that do not repeat agents, denoted by
$\mathcal{H}$, is finite.

Let $T=\\{a_{1},\ldots,a_{2f+1}\\}$ be agents with corresponding formulas
$\Phi=\\{\varphi_{1},\ldots,\varphi_{2f+1}\\}$, and $b\in\mathcal{A}\setminus
T$ an arbitrary agent not in $T$. Let $F(T,\Phi,b)$ be the set of all possible
sets of $2f+1$ disjoint hope chains originating at $T$ and reaching $b$,
$\rho$ is a map that associates each of the hope chains to the index of the
source agent. Consider the following formula:

$H_{a_{1}}\varphi_{1}\wedge\ldots\wedge
H_{a_{2f+1}}\varphi_{2f+1}\rightarrow\Diamond(\bigvee\limits_{\Sigma\in
F(T,\Phi,b)}[\bigwedge\limits_{\sigma\in\Sigma}H_{\sigma}(\varphi_{\rho(\sigma)})])$
(1)

This equation represents that at any given time, if $2f+1$ different agents
$a_{i}$ hope for a formula $\varphi_{i}$, then eventually there will be $2f+1$
hope chains relative to each formula $\varphi_{i}$ from the $2f+1$ agents to
an external agent $b$. Since hope chains correspond to message relay chains,
we are assuming a flooding protocol, and hope formulas are persistent, then
this formula matches that $T$ can eventually reach $b$ through $2f+1$ disjoint
paths.

Notice that this formula only depends on $T$, $b$, and $\Phi$, therefore we
can define a map $\Psi$ that matches each choice of $T$, $b$, and $\Phi$ to a
formula $\Psi(T,\Phi,b)$. This yields the following formula

$\Box(\forall T\subset\mathcal{A}.\forall\Phi\subset\mathcal{F}.\forall
b\notin T.(|T|=2f+1\wedge|\Phi|=2f+1)\rightarrow\Psi(T,\Phi,b))$ (2)

It follows from the previous observations regarding (1), and Lemma 3.4 that
(2) corresponds to $2f+1$ strong vertex connectivity.

Notice that for the purpose of firing rebels, we may restrict the formulas in
$\Phi$ to only consider conjunctions of hope chains that do not repeat agents,
and only relative to the proposition $START$, which represents that a $START$
event happened. We denote $\hat{\mathcal{H}}$ as set of formulas formed by the
conjunction of hope chains from $\mathcal{H}$ relative to proposition $START$.

$\Box(\forall T\subset\mathcal{A}.\forall\Phi\subset\hat{\mathcal{H}}.\forall
b\notin T.(|T|=2f+1\wedge|\Phi|=2f+1)\rightarrow\Psi(T,\Phi,b))$ (3)

It follows from the finiteness of $\mathcal{A}$ and $\hat{\mathcal{H}}$ that
formula (3) can be rewritten without quantifiers and cardinality checks.

###  4.2 Co-Roots

Let $B$ be a set of $f$ agents. Recall that a co-root should be a set of $f+1$
agents not in $B$ such that each agent has at least $2f+1$ in neighbors. Let
$C(B)$ be the set of all possible subsets of $\mathcal{A}$ of size $f+1$ that
do not intersect $B$. Let $S(B,a)$ be the set of all possible subsets of
$\mathcal{A}$ of size $2f+1$ that do not intersect $B\cup\\{a\\}$. Let $\Phi$
be a set of $2f+1$ formulas, and $\sigma$ an arbitrary indexing map that
assigns to any set of agents $\Delta$ of size $2f+1$ a bijection between such
$\Delta$ and $\Phi$. The following formula expresses that there is a co-root
w.r.t $B$ of size at least $f+1$.

$\bigvee\limits_{\Sigma\in
C(B)}\bigwedge\limits_{a\in\Sigma}\bigvee\limits_{\Delta\in
S(B,a)}\bigwedge\limits_{b\in\Delta}H_{b}(\sigma(\Delta)(b))\rightarrow\Diamond
H_{a}H_{b}(\sigma(\Delta)(b))$ (4)

Notice that the formulas from $\Phi$ need not even be hope chains, but we can
assume that the only formula that we need to relay directly is the proposition
that $START$ occurred.

Therefore, we can reduce formula (4) into the following:

$\bigvee\limits_{\Sigma\in
C(B)}\bigwedge\limits_{a\in\Sigma}\bigvee\limits_{\Delta\in
S(B,a)}\bigwedge\limits_{b\in\Delta}H_{b}(START)\rightarrow\Diamond
H_{a}H_{b}(START)$ (5)

Notice that formula (5) depends only on $B$, therefore there is a mapping
$G(B)$ that yields the respective formula (5) for each possible choice of $B$.
This yields the following formula:

$\Box(\forall B\subset\mathcal{A}.(|B|=f\rightarrow G(B))$ (6)

It follows from the finiteness of $\mathcal{A}$ that formula (6) can be
rewritten without quantifiers or cardinality checks.

######  Corollary 4.1.

Formulas (3) and (6) constitute the necessary and sufficient a-priori
knowledge for solving Firing Rebels with Relay in a distributed system with
$n$ agents (processes) and at most $f$ fully byzantine agents, where further
knowledge gain is acquired only by message passing.

##  5 Conclusions

In this paper we provided necessary and sufficient network conditions for
solving firing rebels with relay in an asynchronous context. In order to do
so, we defined the concept of network abstractions in order to capture
asynchronous communication properties into graph sequences. It follows that
network liveness properties translate naturally into connectivity properties
of the graphs constituting the network abstraction.

We formulated two algorithms that solve firing rebels with and without relay
respectively in any network that satisfies the conditions of our
characterization. Furthermore, we showed that we can always build a run where
firing rebels is not solvable if the conditions are not met, even in the
presence of a full-information flooding protocol. The algorithms that we
present, are not full-information, and they store and broadcast a bounded
amount of information. However, since we assume that the system is
asynchronous, we can not restrict attempted broadcasts, and thus we can not
get rid of the flooding nature of the algorithms.

Finally we translated our characterization into temporal epistemic formulas
related to the Hope and Belief modalities for byzantine systems. This formulas
then constitute the liveness guarantees that the system is capable of relaying
information in a sufficiently reliable manner. The a-priori knowledge of these
liveness properties is what enables processes to safely execute FIRE.

#### Future Work

Although we proved that the conditions characterize the network connectivity
conditions for firing rebels in an asynchronous byzantine system, the temporal
epistemic conditions rely on the one-to-one translation between message relay
chains and hope chains. It would be interesting to derive the necessity and
sufficiency of the formulas in Section 4 in a more explicit manner, and
connect them to the existing conditions for acquiring belief [28], as well the
necessary knowledge conditions for firing rebels with relay [10].

Another interesting direction could be to define a potency modality i.e. a
modality that represents the capacity of agents to enforce certain formulas.
This would enable us to offload the full-information assumption on the
protocol analysis and shift it to a potency formula that holds independently
of the protocol. At the same time, such a modality could be used for protocol
synthesis from epistemic logic.

## References

  * [1] Yehuda Afek and Eli Gafni.  Asynchrony from synchrony.  In Distributed Computing and Networking, volume 7730 of Lecture Notes in Computer Science, pages 225–239. Springer Berlin Heidelberg, 2013.
  * [2] Dan Alistarh, Faith Ellen, and Joel Rybicki.  Wait-free approximate agreement on graphs.  In Tomasz Jurdziński and Stefan Schmid, editors, Structural Information and Communication Complexity, pages 87–105, Cham, 2021\. Springer International Publishing.
  * [3] Chagit Attiya, Danny Dolev, and Joseph Gil.  Asynchronous byzantine consensus.  In PODC, pages 119–133. ACM, 1984.
  * [4] Ido Ben-Zvi and Yoram Moses.  Beyond Lamport’s happened-before: On time bounds and the ordering of events in distributed systems.  J. ACM, 61(2):13:1–13:26, April 2014.
  * [5] T. Böhme, F. Göring, and J. Harant.  Menger’s theorem.  J. Graph Theory, 37(1):35–36, may 2001.
  * [6] Bernadette Charron-Bost and Shlomo Moran.  The firing squad problem revisited.  Theoretical Computer Science, 793:100–112, 2019.
  * [7] Bernadette Charron-Bost and Shlomo Moran.  Minmax algorithms for stabilizing consensus.  Distributed Comput., 34(3):195–206, 2021.
  * [8] B A Coan, D Dolev, C Dwork, and L Stockmeyer.  The distributed firing squad problem.  In Proceedings of the Seventeenth Annual ACM Symposium on Theory of Computing, STOC ’85, page 335–345, New York, NY, USA, 1985. Association for Computing Machinery.
  * [9] Michael J. Fischer, Nancy A. Lynch, and M. S. Paterson.  Impossibility of distributed consensus with one faulty process.  Journal of the ACM, 32(2):374–382, April 1985.
  * [10] Krisztina Fruzsa, Roman Kuznets, and Ulrich Schmid.  Fire!  In Joseph Y. Halpern and Andrés Perea, editors, Proceedings Eighteenth Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2021, Beijing, China, June 25-27, 2021, volume 335 of EPTCS, pages 139–153, 2021.
  * [11] Emmanuel Godard and Eloi Perdereau.  k-Set Agreement in Communication Networks with Omission Faults.  In Panagiota Fatourou, Ernesto Jiménez, and Fernando Pedone, editors, 20th International Conference on Principles of Distributed Systems (OPODIS 2016), volume 70 of Leibniz International Proceedings in Informatics (LIPIcs), pages 8:1–8:17, Dagstuhl, Germany, 2017. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.
  * [12] Guy Goren and Yoram Moses.  Silence.  J. ACM, 67(1), jan 2020.
  * [13] Joseph Y. Halpern and Yoram Moses.  Knowledge and common knowledge in a distributed environment.  J. ACM, 37(3):549–587, 1990.
  * [14] Barteld Kooi Hans van Ditmarsch, Wiebe Hoek.  Dynamic Epistemic Logic, pages 11–42.  Springer Netherlands, Dordrecht, 2008.
  * [15] Maurice Herlihy and Nir Shavit.  The topological structure of asynchronous computability.  J. ACM, 46(6):858–923, nov 1999.
  * [16] Roman Kuznets, Laurent Prosperi, Ulrich Schmid, and Krisztina Fruzsa.  Causality and epistemic reasoning in byzantine multi-agent systems.  In Lawrence S. Moss, editor, Proceedings 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.
  * [17] Roman Kuznets, Laurent Prosperi, Ulrich Schmid, and Krisztina Fruzsa.  Epistemic reasoning with byzantine-faulty agents.  In Andreas Herzig and Andrei Popescu, editors, Frontiers of Combining Systems, pages 259–276, Cham, 2019. Springer International Publishing.
  * [18] Roman Kuznets, Laurent Prosperi, Ulrich Schmid, Krisztina Fruzsa, and Lucas Gréaux.  Knowledge in byzantine message-passing systems i framework and the causal cone.  Eprint, TU Wien, 2019.
  * [19] Leslie Lamport.  Time, clocks, and the ordering of events in a distributed system.  Commun. ACM, 21(7):558–565, 1978.
  * [20] Leslie Lamport, Robert Shostak, and Marshall Pease.  The byzantine generals problem.  ACM Trans. Program. Lang. Syst., 4(3):382–401, jul 1982.
  * [21] Hammurabi Mendes, Christine Tasson, and Maurice Herlihy.  Distributed computability in byzantine asynchronous systems.  In Proceedings of the Forty-Sixth Annual ACM Symposium on Theory of Computing, STOC ’14, page 704–713, New York, NY, USA, 2014. Association for Computing Machinery.
  * [22] Yoram Moses.  Relating knowledge and coordinated action: The knowledge of preconditions principle.  Electronic Proceedings in Theoretical Computer Science, 215:231–245, jun 2016.
  * [23] Yoram Moses and Sergio Rajsbaum.  A layered analysis of consensus.  SIAM J. Comput., 31(4):989–1021, apr 2002.
  * [24] Yoram Moses and Yoav Shoham.  Belief as defeasible knowledge.  Artificial Intelligence, 64(2):299–321, 1993.
  * [25] Thomas Nowak, Ulrich Schmid, and Kyrill Winkler.  Topological characterization of consensus under general message adversaries.  In Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing, PODC ’19, page 218–227, New York, NY, USA, 2019. Association for Computing Machinery.
  * [26] Michael Saks and Fotios Zaharoglou.  Wait-free k-set agreement is impossible: The topology of public knowledge.  In Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing, STOC ’93, page 101–110, New York, NY, USA, 1993. Association for Computing Machinery.
  * [27] Nicola Santoro and Peter Widmayer.  Time is not a healer.  In B. Monien and R. Cori, editors, STACS 89, pages 304–313, Berlin, Heidelberg, 1989. Springer Berlin Heidelberg.
  * [28] Thomas Schlögl and Ulrich Schmid.  A sufficient condition for gaining belief in byzantine fault-tolerant distributed systems.  In Rineke Verbrugge, editor, Proceedings Nineteenth conference on Theoretical Aspects of Rationality and Knowledge, Oxford, United Kingdom, 28-30th June 2023, volume 379 of Electronic Proceedings in Theoretical Computer Science, pages 487–506. Open Publishing Association, 2023.
  * [29] Hans van Ditmarsch, Krisztina Fruzsa, and Roman Kuznets.  A new hope.  Advances in Modal Logic, 14:349–369, 2022.
  * [30] Josef Widder and Ulrich Schmid.  Booting clock synchronization in partially synchronous systems with hybrid process and link failures.  Distributed Computing, 20(2):115–140, August 2007.
  * [31] Kyrill Winkler, Ami Paz, Hugo Rincon Galeana, Stefan Schmid, and Ulrich Schmid.  The Time Complexity of Consensus Under Oblivious Message Adversaries.  In Yael Tauman Kalai, editor, 14th Innovations in Theoretical Computer Science Conference (ITCS 2023), volume 251 of Leibniz International Proceedings in Informatics (LIPIcs), pages 100:1–100:28, Dagstuhl, Germany, 2023. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.
  * [32] Kyrill Winkler, Ulrich Schmid, and Yoram Moses.  A Characterization of Consensus Solvability for Closed Message Adversaries.  In Pascal Felber, Roy Friedman, Seth Gilbert, and Avery Miller, editors, 23rd International Conference on Principles of Distributed Systems (OPODIS 2019), volume 153 of Leibniz International Proceedings in Informatics (LIPIcs), pages 17:1–17:16, Dagstuhl, Germany, 2020. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.
  * [33] Étienne Coulouma, Emmanuel Godard, and Joseph Peters.  A characterization of oblivious message adversaries for which consensus is solvable.  Theoretical Computer Science, 584:80–90, 2015.  Special Issue on Structural Information and Communication Complexity.