reorganisation multi-files

Recherche/BFT-ARBover/2_Primitives/index.tex

@@ -0,0 +1,22 @@
+\subsection{Reliable Broadcast (RB)}
+
+\RB provides the following properties in the model.
+\begin{itemize}[leftmargin=*]
+  \item \textbf{Integrity}: Every message received was previously sent. $\forall p_i:\ \RBreceived_i(m) \Rightarrow \exists p_j:\ \RBcast_j(m)$.
+  \item \textbf{No-duplicates}: No message is received more than once at any process.
+  \item \textbf{Validity}: If a correct process broadcasts $m$, every correct process eventually receives $m$.
+\end{itemize}
+
+\subsection{Group Election Object}
+
+We consider a Groupe Election object ($\GE[r]$) per round $r \in \mathcal{R}$ with the following properties.
+
+There are three operations: $\CANDIDATE(r), \CLOSE(r)$ and $\READGE(r)$ such that:
+\begin{itemize}
+  \item \textbf{Termination.} A $\CANDIDATE(r), \CLOSE(r)$ or $\READGE(r)$ operation invoked by a correct process always returns.
+  \item \textbf{Election.} If there exists at least one $\CLOSE(r)$ operation and let $\CLOSE(r)^\star$ denote the first $\CLOSE(r)$ in the linearization order. If some correct process $p$ invokes $\CANDIDATE(r)$ and the invocation of $\CANDIDATE(r)$ appears before $\CLOSE(r)^\star$ in the linearization order, then $\Winners_r \neq \emptyset$.
+  \item \textbf{Prefix Inclusion.} If $\CLOSE(r)^\star$ exists, then there exists a set $\Winners_r \subseteq \Pi$ such that, for any process $p_j$: $p_j \in \Winners_r$ iff $p_j$ invokes $\CANDIDATE(r)$ and its $\CANDIDATE(r)$ operation is linearized before $\CLOSE(r)^\star$.
+  \item \textbf{Stability.} If $\CLOSE(r)^\star$ exists, then every $\READGE(r)$ operation linearized after
+  $\CLOSE(r)^\star$ returns exactly $\Winners_r$.
+  \item \textbf{READ Validity.} The invocation of $op = \READGE(r)$ by a process $p$ returns the list of valid invocations of $\CANDIDATE(r)$ that appears before $op$ in the linearization order along with the names of the processes that invoked each operation.
+\end{itemize}