\documentclass{paper}

\setlength {\parindent} {0 pt}
\setlength {\parskip} {1.5 ex plus 0.5 ex minus 0.2 ex}

\usepackage{fullpage}
\usepackage{eurosym}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{graphicx}
%\usepackage{wasysym}
\usepackage[usenames]{color}

\usepackage{enumerate}
\usepackage{cite}
\usepackage{float}
\usepackage{xspace}


\usepackage[noend,linesnumbered,boxed]{algorithm2e}
\SetAlCapSkip{0.2cm}


%\usepackage {hyperref}

\newcommand {\mathset} [1] {\ensuremath {\mathbb {#1}}}
\newcommand {\R} {\mathset {R}}
\newcommand {\Q} {\mathset {Q}}
\newcommand {\Z} {\mathset {Z}}
\newcommand {\EX} {\mathbf {E}}
\newcommand {\script} [1] {\ensuremath {\mathcal {#1}}}
\newcommand {\etal} {\textit {et al.}}
\newcommand {\eps} {\varepsilon}
\newcommand {\eqdef} {:=}
\newcommand {\boruvka}{Bor\r{u}vka}
\newcommand {\wspd}{\texttt{wspd}}
\newcommand {\rC}{\texttt{rC}}
\newcommand {\mC}{\texttt{mC}}
\newcommand {\me}{\texttt{me}}
\newcommand {\send}{\texttt{send}}
\newcommand {\receive}{\texttt{receive}}
\newcommand {\majority}{\texttt{majority}}
\DeclareMathOperator {\emst}{emst}
\DeclareMathOperator {\conv}{CH}
\DeclareMathOperator {\argmin}{argmin}
\DeclareMathOperator {\DT}{DT}
\DeclareMathOperator {\UC}{UC}
\DeclareMathOperator {\LC}{LC}

\newtheorem {theorem} {Satz}
\newtheorem {inv}[theorem] {Invariante}
\newtheorem {fact}[theorem] {Fakt}
\newtheorem {problem}[theorem] {Problem}
\newtheorem {obs}[theorem] {Beobachtung}
\newtheorem {lemma}[theorem] {Lemma}
\newtheorem {observation}[theorem] {Observation}
\newtheorem {corollary}[theorem] {Corollary}
\newtheorem {claim}[theorem] {Claim}
\newtheorem {definition}[theorem] {Definition}


\title{Byzantine Generals}
\author{Wolfgang Mulzer}

\begin{document}
\maketitle

Let $G$ be a set of $n$ generals.
Each general $g \in G$ has a \emph{choice} 
$c_g \in \{A, R\}$, and the generals must 
reach a \emph{common consensus} $c^*$ that is close
to the majority vote.
Unfortunately, there are $t$ \emph{traitors} among the
generals.
We describe how the loyal generals
can reach a common agreement despite the presence of 
traitors. For this, each loyal general executes the 
following algorithm. The local variable $\me$ stores 
the id of the current general. The associative arrays
$\rC$ and $\mC$ contain the current general's views on
the other generals' choices.
The function $\majority$ receives a multi-set of choices
and returns the most popular choice among them (breaking
ties in favor of $R$).
\begin{algorithm}[htb]
$\rC[\perp] \gets c_\me$\\
\For{$i := 0,\dots,t$}{ 
    \For{all pairwise distinct generals 
      $g_1 \rightarrow \dots \rightarrow g_{i+1}$ in 
      $G \setminus \{\textup\me\}$}{
        $\send\big(\me, g_{i+1}, \rC[g_1 \rightarrow \dots \rightarrow 
	g_i]\big)$
	\label{ll:send}
    }
    \For{all pairwise distinct generals 
      $g_1 \rightarrow \dots \rightarrow g_{i+1}$ in 
      $G \setminus \{\textup\me\}$}{
        $\receive\big(g_{i+1}, 
	\rC[g_1 \rightarrow \dots \rightarrow g_{i+1}]\big)$
    }
}
\For{$i := t+1,\dots,0$}{ 
    \For{all pairwise distinct generals 
      $g_1 \rightarrow \dots \rightarrow g_{i}$ in 
      $G \setminus \{\textup\me\}$}{
        $\mC[g_1 \rightarrow \dots \rightarrow g_i] = 
	\majority\big(\rC[g_1 \rightarrow \dots \rightarrow g_i] \cup 
                   \mC[g_ \rightarrow \dots \rightarrow 
		   g_i \rightarrow ?]\big)$
		   \label{ll:majority}
    } 
}
$c^* \gets \mC[\perp]$
\caption{The Byzantine Generals Algorithm.}
\label{alg:bg}
\end{algorithm}

\begin{lemma}
\label{lem:bg}
Let $n \geq 3t + 1$. The Byzantine Generals algorithm
has the following two properties:
\begin{enumerate}[(a)]
\item
For all $i = 1, \dots, t + 1$ and for all pairwise 
distinct generals $g_1 \rightarrow \dots \rightarrow g_i$:
if $g_i$ is loyal, then for all loyal generals 
$g \not\in \{g_1, \dots,g_i\}$, we have:
\[
    g.\textup\mC[g_1 \rightarrow \dots \rightarrow g_i] = 
    g.\textup\rC[g_1 \rightarrow \dots \rightarrow g_i] = 
    g_i.\textup\rC[g_1 \rightarrow \dots \rightarrow g_{i-1}].
\]
\item
For all $i = 1, \dots ,t$ and for all pairwise 
distinct generals $g_1 \rightarrow  \dots  \rightarrow g_i$:
if $g_1, \dots, g_i$ are all traitors, then
for all loyal generals $g, g' \not\in  \{g_1, \dots ,g_i\}$, 
we have:
\[
 g.\textup\mC[g_1 \rightarrow \dots \rightarrow g_i] 
 = g'.\textup\mC[g_1 \rightarrow \dots \rightarrow g_i].
\]
\end{enumerate}
\end{lemma}

\begin{proof}
We begin with property (a).
The proof is by  reverse induction on $i$.
First, let $i = t+1$.
In this case, by Line~\ref{ll:majority} from 
Algorithm~\ref{alg:bg}, we have
for any loyal general $g \not\in \{g_1, \dots, g_{t+1}\}$, 
\[
  g.\mC[g_1 \rightarrow \dots \rightarrow g_{t+1}] = 
  g.\rC[g_1 \rightarrow \dots \rightarrow g_{t+1}] =
  g_{t+1}.\rC[g_1 \rightarrow \dots \rightarrow g_{t}],
\]
since $g_{t+1}$ is loyal.
Next, we perform the inductive step from
$i + 1$ to $i$. Since $g_i$ is loyal, general $g_i$ sends the 
same value $g_i.\rC[g_1 \rightarrow \dots \rightarrow g_{i-1}]$ to all 
generals $g' \not\in \{g_1, \dots, g_i\}$ in Line~\ref{ll:send}  of 
Algorithm~\ref{alg:bg}. 
Thus, using the inductive hypothesis, for all loyal generals 
$g' \notin \{g, g_1, \dots, g_i\}$, we have 
\[
 g.\mC[g_1 \rightarrow \dots \rightarrow g_i \rightarrow g'] = 
 g.\rC[g_1 \rightarrow \dots \rightarrow g_i \rightarrow g'] = 
 g_i.\rC[g_1 \rightarrow  \dots \rightarrow g_{i-1}] = 
 g.\rC[g_1 \rightarrow \dots \rightarrow g_i].
\]
Since $n \geq 3t + 1$ and since $i \leq t$, the set 
$G \setminus \{g, g_1, \dots, g_i\}$ contains at least 
$t$ loyal  generals and at most $t$ traitors.
Thus, according to line~\ref{ll:majority} in Algorithm~\ref{alg:bg},
\[
  g.\mC[g_1 \rightarrow \dots \rightarrow g_i] = 
  \majority\big(g.\rC[g_1 \rightarrow \dots \rightarrow g_i] \cup 
  g.\mC[g_1 \rightarrow \dots \rightarrow g_i \rightarrow ?]\big)
   =  g.\rC[g_1 \rightarrow \dots \rightarrow g_i].
\]
This concludes the proof of (a), and we continue with the proof
of property (b). Again, we use reverse induction on $i$.
For the base case, let $i = t$.
Since $g_1 \rightarrow \dots \rightarrow g_t$ are all traitors, 
and since there are only $t$ traitors overall, 
all generals in $G \setminus \{g_1, \dots ,g_t\}$ 
are loyal. Thus, the multisets
\[
g.\rC[g_1 \rightarrow \dots \rightarrow g_t] \cup 
g.\mC[g_1 \rightarrow \dots \rightarrow  g_t \rightarrow ?]
\]
and 
\[
g'.\rC[g_1 \rightarrow \dots \rightarrow g_t] \cup 
g'.\mC[g_1 \rightarrow \dots \rightarrow  g_t \rightarrow ?]
\]
are identical,
so $g.\mC[g_1 \rightarrow \dots \rightarrow g_t] = 
g'.\mC[g_1 \rightarrow \dots \rightarrow g_t]$, as claimed.
Next, we perform the inductive step from
$i+1$ to $i$.
By (a), we have
\[
	g.\mC[g_1 \rightarrow \dots \rightarrow g_i \rightarrow g'] 
	= g.\rC[g_1 \rightarrow \dots \rightarrow g_i \rightarrow g']
	= g'.\rC[g_1 \rightarrow \dots \rightarrow g_i]
\]
and
\[
	g'.\mC[g_1 \rightarrow \dots \rightarrow g_i \rightarrow g] 
	= g'.\rC[g_1 \rightarrow \dots \rightarrow g_i \rightarrow g]
	= g.\rC[g_1 \rightarrow \dots \rightarrow g_i]
\]
Let $h \in G \setminus \{g_1, \dots, g_i, g, g'\}$.
If $h$ is loyal, then again by (a), we have
\begin{multline*}
	g.\mC[g_1 \rightarrow \dots \rightarrow g_i \rightarrow h] =
	g.\rC[g_1 \rightarrow \dots \rightarrow g_i \rightarrow h] =
	h.\rC[g_1 \rightarrow \dots \rightarrow g_i] 
	 \\
	= g'.\rC[g_1 \rightarrow \dots \rightarrow g_i \rightarrow h] =
	g'.\mC[g_1 \rightarrow \dots \rightarrow g_i \rightarrow h].
\end{multline*}
If $h$ is a traitor, then $g_1, \dots, g_i, h$ are all traitors,
and by the inductive hypothesis, we have
\[
  g.\mC[g_1 \rightarrow \dots \rightarrow g_i \rightarrow h] = 
  g'.\mC[g_1 \rightarrow \dots \rightarrow g_i \rightarrow h] = 
\]
By line~\ref{ll:majority} from Algorithm~\ref{alg:bg}, it follows that 
$g.\mC[g_1 \rightarrow \dots \rightarrow g_i] = 
g'.\mC[g_1 \rightarrow \dots \rightarrow g_i]$, as claimed.
\end{proof}

\begin{theorem}
Suppose that $n \geq 3t+1$.
For any two loyal generals $g, g' \in G$, Algorithm~\ref{alg:bg}
ensures that $g.\mC[g'] = c_{g'}$, $g'.\mC[g] = c_g$, and
$g.\mC[h] = g'.\mC[h]$, for any $h \in G \setminus \{g, g'\}$.
\end{theorem}
\begin{proof}
This is a direct consequence of Lemma~\ref{lem:bg}, by setting
$i = 1$.
\end{proof}
\end{document}