ajout biblio

Recherche/BFT-ARBover/4_ARB_with_RB_DL/index.tex

@@ -318,8 +318,7 @@ history of operations) are uniquely determined.
 
 \paragraph{State machine replication over \ARB.}
 Assume a system that exports a FIFO-\ARB primitive with the guarantees that if a correct process invokes $\ABbroadcast(m)$, then every correct process eventually $\ABdeliver(m)$ and the invocation eventually returns.
-Following the classical \emph{state machine replication} approach
-such as described in Schneider~\cite{Schneider90}, we can implement a fault-tolerant service by ensuring the following properties:
+Following the classical \emph{state machine replication} approach described by Schneider~\cite{Schneider90}, we can implement a fault-tolerant service by ensuring the following properties:
 \begin{quote}
   \textbf{Agreement.} Every nonfaulty state machine replica receives every request. \\
   \textbf{Order.} Every nonfaulty state machine replica processes the requests it receives in
@@ -332,7 +331,7 @@ Which are cover by our FIFO-\ARB specification.
 
 
 \begin{theorem}[From \ARB to synchronous \DL]\label{thm:arb-to-dl}
-  In an asynchronous message-passing system with crash failures, assume a FIFO Atomic Reliable Broadcast primitive with Integrity, No-duplicates,Validity, and the liveness of $\ABbroadcast$. Then there exists an implementation of a DenyList object that satisfies Termination, Validity, and Anti-flickering properties.
+  In an asynchronous message-passing system with crash failures, assume a FIFO Atomic Reliable Broadcast primitive (in the standard Total Order / Atomic Broadcast sense of~\cite{Defago2004}) with Integrity, No-duplicates, Validity, and the liveness of $\ABbroadcast$. Then there exists an implementation of a DenyList object that satisfies Termination, Validity, and Anti-flickering properties.
 \end{theorem}
 
 \begin{proof}