]> AND Private Git Repository - hdrcouchot.git/blob - annexePreuveMarquagefldblement.tex
Logo AND Algorithmique Numérique Distribuée

Private GIT Repository
preuve promela:debut de traduction
[hdrcouchot.git] / annexePreuveMarquagefldblement.tex
1 On considère   le  mode
2 $f_l: \Bool^l \rightarrow \Bool^l$ t.q. le $i^{\textrm{ème}}$ composant 
3 est défini par 
4 \begin{equation}
5 {f_l}(x)_i =
6 \left\{
7 \begin{array}{l}
8 \overline{x_i} \textrm{ if $i$ is odd} \\
9 x_i \oplus x_{i-1} \textrm{ if $i$ is even}
10 \end{array}
11 \right.
12 \end{equation}\label{eq:fqq}
13
14 Prouvons que la matrice de Markov associée est doublement stochastique.
15
16 the Markov chain is stochastic by construction. 
17
18 Let us prove that its Markov chain is doubly stochastic by induction on the 
19 length $l$.
20 For $l=1$ and $l=2$ the proof is obvious. Let us consider that the 
21 result is established until $l=2k$ for some $k \in \Nats$.
22
23 Let us then firstly prove the doubly stochasticity for $l=2k+1$.
24 Following notations introduced in~\cite{bcgr11:ip}, 
25 Let  $\textsc{giu}(f_{2k+1})^0$ and $\textsc{giu}(f_{2k+1})^1$ denote
26 the subgraphs of $\textsc{giu}(f_{2k+1})$ induced by the subset $\Bool^{2k} \times\{0\}$
27 and $\Bool^{2k} \times\{1\}$ of $\Bool^{2k+1}$ respectively.
28 $\textsc{giu}(f_{2k+1})^0$ and   $\textsc{giu}(f_{2k+1})^1$ are isomorphic to $\textsc{giu}(f_{2k})$.
29 Furthermore, these two graphs are linked together only with arcs of the form
30 $(x_1,\dots,x_{2k},0) \to (x_1,\dots,x_{2k},1)$ and 
31 $(x_1,\dots,x_{2k},1) \to (x_1,\dots,x_{2k},0)$.
32 In $\textsc{giu}(f_{2k+1})$ the number of arcs whose extremity is $(x_1,\dots,x_{2k},0)$
33 is  the same than the number of arcs whose extremity is $(x_1,\dots,x_{2k})$ 
34 augmented with 1, and similarly for $(x_1,\dots,x_{2k},1)$.
35 By induction hypothesis, the Markov chain associated to $\textsc{giu}(f_{2k})$ is doubly stochastic. All the vertices $(x_1,\dots,x_{2k})$ have thus the same number of 
36 ingoing arcs and the proof is established for $l$ is $2k+1$.
37
38 Let us then  prove the doubly stochasticity for $l=2k+2$.
39 The map $f_l$ is defined by 
40 $f_l(x)= (\overline{x_1},x_2 \oplus x_{1},\dots,\overline{x_{2k+1}},x_{2k+2} \oplus x_{2k+1})$.
41 With previously defined  notations, let us focus on 
42 $\textsc{giu}(f_{2k+2})^0$ and   $\textsc{giu}(f_{2k+2})^1$ which are isomorphic to $\textsc{giu}(f_{2k+1})$. 
43 Among configurations of $\Bool^{2k+2}$, only four suffixes of length 2 can be
44 obviously observed, namely, $00$, $10$, $11$ and $01$.
45 Since 
46 $f_{2k+2}(\dots,0,0)_{2k+2}=0$, $f_{2k+2}(\dots,1,0)_{2k+2}=1$, 
47 $f_{2k+2}(\dots,1,1)_{2k+2}=0$ and $f_{2k+2}(\dots,0,1)_{2k+2}=1$, the number of 
48 arcs whose extremity is 
49 \begin{itemize}
50 \item $(x_1,\dots,x_{2k},0,0)$
51  is the same than the one whose extremity is $(x_1,\dots,x_{2k},0)$ in $\textsc{giu}(f_{2k+1})$ augmented with 1 (loop over configurations $(x_1,\dots,x_{2k},0,0)$).
52 \item $(x_1,\dots,x_{2k},1,0)$
53  is the same than the one whose extremity is $(x_1,\dots,x_{2k},0)$ in $\textsc{giu}(f_{2k+1})$ augmented with 1 (arc from configurations 
54 $(x_1,\dots,x_{2k},1,1)$ to configurations 
55 $(x_1,\dots,x_{2k},1,0)$) 
56 \item $(x_1,\dots,x_{2k},0,1)$
57  is the same than the one whose extremity is $(x_1,\dots,x_{2k},0)$ in $\textsc{giu}(f_{2k+1})$ augmented with 1 (loop over configurations $(x_1,\dots,x_{2k},0,1)$).
58 \item $(x_1,\dots,x_{2k},1,1)$
59  is the same than the one whose extremity is $(x_1,\dots,x_{2k},1)$ in $\textsc{giu}(f_{2k+1})$ augmented with 1 (arc from configurations 
60 $(x_1,\dots,x_{2k},1,0)$ to configurations 
61 $(x_1,\dots,x_{2k},1,1)$).
62 \end{itemize}
63 Thus all the vertices $(x_1,\dots,x_{2k})$ have  the same number of 
64 ingoing arcs and the proof is established for $l=2k+2$.