fsfd

diff --git a/annexePromelaProof.tex b/annexePromelaProof.tex
index dbc5774c131f8fda93f4de707cedf2edcace8dfa..1f70e9fa587944560b29c723c7a19f42e3274a2e 100644 (file)
--- a/annexePromelaProof.tex
+++ b/annexePromelaProof.tex
@@ -228,11 +228,7 @@ to      $F(Xd^{l+1}_{k\,0},      \ldots,Xd^{l+1}_{k\,n-1})$.      Thanks      to
 \end{Proof}
 
 
 \end{Proof}
 
 

-\begin{theorem}[Soundness wrt universal convergence property]\label{Theo:sound}
-  Let $\phi$ be  a DDN model and $\psi$ be its  translation.  If $\psi$ verifies
-  the  LTL  property  (\ref{eq:ltl:conv})  under weak  fairness  property,  then
-  iterations of $\phi$ are universally convergent.
-\end{theorem}
+\promelasound*

 \begin{Proof}
 %   For  the  case  where  the  strategy  is  finite,  one  notice  that  property
 %   verification  is achieved  under  weak fairness  property.  Instructions  that
 \begin{Proof}
 %   For  the  case  where  the  strategy  is  finite,  one  notice  that  property
 %   verification  is achieved  under  weak fairness  property.  Instructions  that


@@ -259,12 +255,8 @@ to      $F(Xd^{l+1}_{k\,0},      \ldots,Xd^{l+1}_{k\,n-1})$.      Thanks      to
 % \end{Corol}
 
 
 % \end{Corol}
 
 

+\promelacomplete*

 
 

-\begin{theorem}[Completeness wrt universal convergence property]\label{Theo:completeness}
-  Let $\phi$ be a  DDN model and $\psi$ be its translation.   If $\psi$ does not
-  verify the LTL property  (\ref{eq:ltl:conv}) under weak fairness property then
-  the iterations of $\phi$ are divergent.
-\end{theorem}

 \begin{Proof}
   For models $\psi$  that do not verify the  LTL property (\ref{eq:ltl:conv}) it
   is easy  to construct corresponding iterations  of the DDN,  whose strategy is
 \begin{Proof}
   For models $\psi$  that do not verify the  LTL property (\ref{eq:ltl:conv}) it
   is easy  to construct corresponding iterations  of the DDN,  whose strategy is

diff --git a/images/faig.dot b/images/faig.dot
new file mode 100644 (file)
index 0000000..82fa8d8
--- /dev/null
+++ b/images/faig.dot
@@ -0,0 +1,30 @@
+digraph  {
+000 [shape="none"label="000", pos="10.5,10!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+001 [shape="none"label="001", pos="11.7320508076,11!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+010 [shape="none", label="010", pos="12.5,10!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+011 [shape="none", label="011", pos="13.7320508076,11!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+100 [shape="none", label="100", pos="10.5,8!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+101 [shape="none", label="101", pos="11.7320508076,9!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+110 [shape="none", label="110", pos="12.5,8!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+111 [shape="none", label="111", pos="13.7320508076,9!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+       000:sw -> 000:nw [arrowhead="vee"];
+       001 -> 101 [arrowhead="vee"];
+       001:sw -> 001:nw [arrowhead="vee"];
+       010 -> 010 [arrowhead="vee"];
+       010 -> 011 [arrowhead="vee"];
+       010 -> 000 [arrowhead="vee"];
+       011 -> 011 [arrowhead="vee"];
+       011 -> 111 [arrowhead="vee"];
+       011 -> 001 [arrowhead="vee"];
+       100 -> 000 [arrowhead="vee"]; 
+       100 -> 101 [arrowhead="vee"]; 
+       100:sw -> 100:nw [arrowhead="vee"]; 
+       101 -> 111 [arrowhead="vee"];
+       101 -> 101:nw [arrowhead="vee"];
+       110 -> 111 [arrowhead="vee"]; 
+       110 -> 010 [arrowhead="vee"]; 
+       110 -> 100 [arrowhead="vee"]; 
+       111 -> 111 [arrowhead="vee"];
+       111 -> 011 [arrowhead="vee"];
+
+}

diff --git a/images/faig.pdf b/images/faig.pdf
new file mode 100644 (file)
index 0000000..ec58ecf
Binary files /dev/null and b/images/faig.pdf differ

diff --git a/images/fgig.dot b/images/fgig.dot
new file mode 100644 (file)
index 0000000..1e59628
--- /dev/null
+++ b/images/fgig.dot
@@ -0,0 +1,41 @@
+digraph  {
+000 [shape="none"label="000", pos="10.5,10!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+001 [shape="none"label="001", pos="11.7320508076,11!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+010 [shape="none", label="010", pos="12.5,10!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+011 [shape="none", label="011", pos="13.7320508076,11!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+100 [shape="none", label="100", pos="10.5,8!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+101 [shape="none", label="101", pos="11.7320508076,9!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+110 [shape="none", label="110", pos="12.5,8!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+111 [shape="none", label="111", pos="13.7320508076,9!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+       000:sw -> 000:nw [arrowhead="vee"];
+       001 -> 101[arrowhead="vee"];
+       001:sw -> 001:nw[arrowhead="vee"];
+       010 -> 010[arrowhead="vee"];
+       010 -> 011[arrowhead="vee"];
+       010 -> 000[arrowhead="vee"];
+       010 -> 001[arrowhead="vee"];
+
+       011 -> 011[arrowhead="vee"];
+       011 -> 001[arrowhead="vee"];
+       011 -> 111[arrowhead="vee"];
+       011 -> 101[arrowhead="vee"];
+       100:sw -> 100:nw[arrowhead="vee"]; 
+       100 -> 000[arrowhead="vee"]; 
+       100 -> 001[arrowhead="vee"]; 
+       100 -> 101[arrowhead="vee"]; 
+       101 -> 101:nw[arrowhead="vee"];
+       101 -> 111[arrowhead="vee"];
+
+       110 -> 000[arrowhead="vee"]; 
+       110 -> 110[arrowhead="vee"]; 
+       110 -> 001[arrowhead="vee"]; 
+       110 -> 010[arrowhead="vee"]; 
+       110 -> 011[arrowhead="vee"]; 
+       110 -> 100[arrowhead="vee"]; 
+       110 -> 101[arrowhead="vee"]; 
+       110 -> 111[arrowhead="vee"]; 
+
+       111 -> 111[arrowhead="vee"];
+       111 -> 011[arrowhead="vee"];
+
+}

diff --git a/images/fgig.pdf b/images/fgig.pdf
new file mode 100644 (file)
index 0000000..b518eff
Binary files /dev/null and b/images/fgig.pdf differ

diff --git a/images/fsig.dot b/images/fsig.dot
new file mode 100644 (file)
index 0000000..a6ba548
--- /dev/null
+++ b/images/fsig.dot
@@ -0,0 +1,19 @@
+digraph  {
+
+000 [shape="none"label="000", pos="10.5,10!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+001 [shape="none"label="001", pos="11.7320508076,11!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+010 [shape="none", label="010", pos="12.5,10!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+011 [shape="none", label="011", pos="13.7320508076,11!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+100 [shape="none", label="100", pos="10.5,8!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+101 [shape="none", label="101", pos="11.7320508076,9!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+110 [shape="none", label="110", pos="12.5,8!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+111 [shape="none", label="111", pos="13.7320508076,9!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+       000:sw -> 000:nw [arrowhead="vee"];
+       010 -> 001 [arrowhead="vee"];
+       100 -> 001 [arrowhead="vee"]; 
+       110 -> 001 [arrowhead="vee"]; 
+       001 -> 101 [arrowhead="vee"];
+       101 -> 111 [arrowhead="vee"];
+       111 -> 011 [arrowhead="vee"];
+       011 -> 101 [arrowhead="vee"];
+}

diff --git a/images/fsig.pdf b/images/fsig.pdf
new file mode 100644 (file)
index 0000000..b3d1de8
Binary files /dev/null and b/images/fsig.pdf differ

diff --git a/images/gf.dot b/images/gf.dot
new file mode 100644 (file)
index 0000000..c8937f3
--- /dev/null
+++ b/images/gf.dot
@@ -0,0 +1,10 @@
+digraph  { rankdir="LR"
+1 -> 1 [label=" - "]
+1 -> 3 [label="+"]
+3 -> 3 [label="+"]
+3 -> 2 [label="+"] 
+3 -> 1 [label="+"] 
+2 -> 3 [label="+"] 
+2 -> 1  [label="-"]
+1 -> 2  [label="+"]
+}

diff --git a/images/gf.pdf b/images/gf.pdf
new file mode 100644 (file)
index 0000000..6d588d4
Binary files /dev/null and b/images/gf.pdf differ

diff --git a/images/gfp.pdf b/images/gfp.pdf
new file mode 100644 (file)
index 0000000..3facf65
Binary files /dev/null and b/images/gfp.pdf differ

diff --git a/main.glsdefs b/main.glsdefs
deleted file mode 100644 (file)
index 334ef46..0000000
--- a/main.glsdefs
+++ /dev/null
@@ -1,330 +0,0 @@
-\ifglsentryexists{graphoriente}{}%
-{%
-\gls@defglossaryentry{graphoriente}%
-{%
-name={graphe orienté},%
-sort={graphe orienté},%
-type={main},%
-first={graphe orient\IeC {\'e}},%
-firstplural={graphe orient\IeC {\'e}s},%
-text={graphe orient\IeC {\'e}},%
-plural={graphe orient\IeC {\'e}s},%
-description={Un graphe orienté $G=(S,A)$ est défini par la donnée d'un ensemble de sommets $S$ et d'un ensemble d'arcs $A$, chaque arc étant représenté par un couple de sommets. Si $x$ et $y$ sont des sommets de $S$, le couple $(x,y)$ représente l'arc orienté allant du sommet \emph {origine} $x$ au sommet \emph {extremité} $y$.},%
-descriptionplural={Un graphe orienté $G=(S,A)$ est défini par la donnée d'un ensemble de sommets $S$ et d'un ensemble d'arcs $A$, chaque arc étant représenté par un couple de sommets. Si $x$ et $y$ sont des sommets de $S$, le couple $(x,y)$ représente l'arc orienté allant du sommet \emph {origine} $x$ au sommet \emph {extremité} $y$.},%
-symbol={\relax },%
-symbolplural={\relax },%
-user1={},%
-user2={},%
-user3={},%
-user4={},%
-user5={},%
-user6={},%
-long={},%
-longplural={},%
-short={},%
-shortplural={},%
-counter={page},%
-parent={},%
-%
-}%
-}%
-\ifglsentryexists{graphfortementconnexe}{}%
-{%
-\gls@defglossaryentry{graphfortementconnexe}%
-{%
-name={graphe fortement connexe},%
-sort={graphe fortement connexe},%
-type={main},%
-first={graphe fortement connexe},%
-firstplural={graphe fortement connexes},%
-text={graphe fortement connexe},%
-plural={graphe fortement connexes},%
-description={Un graphe orienté $G=(S,A)$ est fortement connexe si pour tout couple de sommets $x$, $y$ de $S$ il existe un chemin reliant $x$ à $y$ et $y$ à $x$.},%
-descriptionplural={Un graphe orienté $G=(S,A)$ est fortement connexe si pour tout couple de sommets $x$, $y$ de $S$ il existe un chemin reliant $x$ à $y$ et $y$ à $x$.},%
-symbol={\relax },%
-symbolplural={\relax },%
-user1={},%
-user2={},%
-user3={},%
-user4={},%
-user5={},%
-user6={},%
-long={},%
-longplural={},%
-short={},%
-shortplural={},%
-counter={page},%
-parent={},%
-%
-}%
-}%
-\ifglsentryexists{distributionuniforme}{}%
-{%
-\gls@defglossaryentry{distributionuniforme}%
-{%
-name={distribution uniforme},%
-sort={distribution uniforme},%
-type={main},%
-first={distribution uniforme},%
-firstplural={distribution uniformes},%
-text={distribution uniforme},%
-plural={distribution uniformes},%
-description={Les lois de distribution uniforme (ou loi uniformes continues) forment une famille de lois à densité caractérisées par la propriété suivante: tous les intervalles de même longueur inclus dans le support de la loi ont la même probabilité.},%
-descriptionplural={Les lois de distribution uniforme (ou loi uniformes continues) forment une famille de lois à densité caractérisées par la propriété suivante: tous les intervalles de même longueur inclus dans le support de la loi ont la même probabilité.},%
-symbol={\relax },%
-symbolplural={\relax },%
-user1={},%
-user2={},%
-user3={},%
-user4={},%
-user5={},%
-user6={},%
-long={},%
-longplural={},%
-short={},%
-shortplural={},%
-counter={page},%
-parent={},%
-%
-}%
-}%
-\ifglsentryexists{partieentiere}{}%
-{%
-\gls@defglossaryentry{partieentiere}%
-{%
-name={partie entière},%
-sort={partie entière},%
-type={main},%
-first={partie enti\IeC {\`e}re},%
-firstplural={partie enti\IeC {\`e}res},%
-text={partie enti\IeC {\`e}re},%
-plural={partie enti\IeC {\`e}res},%
-description={La partie entière d'un nombre réel est l'entier qui lui est immédiatement inférieur ou égal. Pour un nombre réel $x$, on la note $\lfloor x \rfloor $.},%
-descriptionplural={La partie entière d'un nombre réel est l'entier qui lui est immédiatement inférieur ou égal. Pour un nombre réel $x$, on la note $\lfloor x \rfloor $.},%
-symbol={\ensuremath {\lfloor x \rfloor }},%
-symbolplural={\ensuremath {\lfloor x \rfloor }},%
-user1={},%
-user2={},%
-user3={},%
-user4={},%
-user5={},%
-user6={},%
-long={},%
-longplural={},%
-short={},%
-shortplural={},%
-counter={page},%
-parent={},%
-%
-}%
-}%
-\ifglsentryexists{distanceHamming}{}%
-{%
-\gls@defglossaryentry{distanceHamming}%
-{%
-name={distance de Hamming},%
-sort={distance de Hamming},%
-type={main},%
-first={distance de Hamming},%
-firstplural={distance de Hammings},%
-text={distance de Hamming},%
-plural={distance de Hammings},%
-description={La distance de Hamming entre deux éléments $x=(x_1,\ldots ,x_n)$ et $y=(y_1,\ldots ,y_n)$ dans $\Bool ^n$ est le nombre d'indices $i$, $1 \le i \le n$ tels que $x_i$ diffère de $y_i$.},%
-descriptionplural={La distance de Hamming entre deux éléments $x=(x_1,\ldots ,x_n)$ et $y=(y_1,\ldots ,y_n)$ dans $\Bool ^n$ est le nombre d'indices $i$, $1 \le i \le n$ tels que $x_i$ diffère de $y_i$.},%
-symbol={\relax },%
-symbolplural={\relax },%
-user1={},%
-user2={},%
-user3={},%
-user4={},%
-user5={},%
-user6={},%
-long={},%
-longplural={},%
-short={},%
-shortplural={},%
-counter={page},%
-parent={},%
-%
-}%
-}%
-\ifglsentryexists{decalageDeBits}{}%
-{%
-\gls@defglossaryentry{decalageDeBits}%
-{%
-name={décalage de bits},%
-sort={décalage de bits},%
-type={main},%
-first={d\IeC {\'e}calage de bits},%
-firstplural={d\IeC {\'e}calages de bits},%
-text={d\IeC {\'e}calage de bits},%
-plural={d\IeC {\'e}calages de bits},%
-description={Soit $x$ un nombre binaire de $n$ bits et $b$ un entier. Le nombre binaire de $n$ bits $x \ll b$ (respectivement $x \gg b$) est obtenu en décalant les bits de $x$ de $b$ bits vers la gauche (resp. vers la droite) et en complétant avec des zéros à droite (resp. à gauche).},%
-descriptionplural={Soit $x$ un nombre binaire de $n$ bits et $b$ un entier. Le nombre binaire de $n$ bits $x \ll b$ (respectivement $x \gg b$) est obtenu en décalant les bits de $x$ de $b$ bits vers la gauche (resp. vers la droite) et en complétant avec des zéros à droite (resp. à gauche).},%
-symbol={\relax },%
-symbolplural={\relax },%
-user1={},%
-user2={},%
-user3={},%
-user4={},%
-user5={},%
-user6={},%
-long={},%
-longplural={},%
-short={},%
-shortplural={},%
-counter={page},%
-parent={},%
-%
-}%
-}%
-\ifglsentryexists{chaineDeMarkov}{}%
-{%
-\gls@defglossaryentry{chaineDeMarkov}%
-{%
-name={chaîne de Markov},%
-sort={chaîne de Markov},%
-type={main},%
-first={cha\IeC {\^\i }ne de Markov},%
-firstplural={cha\IeC {\^\i }nes de Markov},%
-text={cha\IeC {\^\i }ne de Markov},%
-plural={cha\IeC {\^\i }nes de Markov},%
-description={On se restreint à la définition d'une chaîne de Markov homogène. Celle-ci désigne une suite de variables aléatoires $(X_n)_{n \in \Nats }$ à temps discret, à espace d'états discret, sans mémoire et dont le mécanisme de transition ne change pas au cours du temps. Formellement la propriété suivante doit être établie:\newline $ \forall n \ge 0, \forall (i_0, \ldots , i_{n-1}, i,j),\\ \textrm { }P(X_{n+1}=j\mid X_0=i_0, X_1=i_1, X_2=i_2, \ldots , X_{n-1}=i_{n-1}, X_{n}=i) \\ \textrm { }= P(X_{1}=j\mid X_n=i). $},%
-descriptionplural={On se restreint à la définition d'une chaîne de Markov homogène. Celle-ci désigne une suite de variables aléatoires $(X_n)_{n \in \Nats }$ à temps discret, à espace d'états discret, sans mémoire et dont le mécanisme de transition ne change pas au cours du temps. Formellement la propriété suivante doit être établie:\newline $ \forall n \ge 0, \forall (i_0, \ldots , i_{n-1}, i,j),\\ \textrm { }P(X_{n+1}=j\mid X_0=i_0, X_1=i_1, X_2=i_2, \ldots , X_{n-1}=i_{n-1}, X_{n}=i) \\ \textrm { }= P(X_{1}=j\mid X_n=i). $},%
-symbol={\relax },%
-symbolplural={\relax },%
-user1={},%
-user2={},%
-user3={},%
-user4={},%
-user5={},%
-user6={},%
-long={},%
-longplural={},%
-short={},%
-shortplural={},%
-counter={page},%
-parent={},%
-%
-}%
-}%
-\ifglsentryexists{vecteurDeProbabilite}{}%
-{%
-\gls@defglossaryentry{vecteurDeProbabilite}%
-{%
-name={vecteur de probabilités},%
-sort={vecteur de probabilités},%
-type={main},%
-first={vecteur de probabilit\IeC {\'e}s},%
-firstplural={vecteurs de probabilit\IeC {\'e}s},%
-text={vecteur de probabilit\IeC {\'e}s},%
-plural={vecteurs de probabilit\IeC {\'e}s},%
-description={Un vecteur de probabilités est un vecteur tel que toutes ses composantes sont positives ou nulles et leur somme vaut 1.},%
-descriptionplural={Un vecteur de probabilités est un vecteur tel que toutes ses composantes sont positives ou nulles et leur somme vaut 1.},%
-symbol={\relax },%
-symbolplural={\relax },%
-user1={},%
-user2={},%
-user3={},%
-user4={},%
-user5={},%
-user6={},%
-long={},%
-longplural={},%
-short={},%
-shortplural={},%
-counter={page},%
-parent={},%
-%
-}%
-}%
-\ifglsentryexists{matriceDAdjacence}{}%
-{%
-\gls@defglossaryentry{matriceDAdjacence}%
-{%
-name={matrice d'adjacence},%
-sort={matrice d'adjacence},%
-type={main},%
-first={matrice d'adjacence},%
-firstplural={matrice d'adjacences},%
-text={matrice d'adjacence},%
-plural={matrice d'adjacences},%
-description={La matrice d'adjacence du graphe orienté $G=(S,A)$ à $n$ sommets est la matrice $\check {M}$ de dimension $n \times n$ dont l'élément $\check {M}_{ij}$ représente le nombre d'arcs d'origine $i$ et d'extrémité $j$.},%
-descriptionplural={La matrice d'adjacence du graphe orienté $G=(S,A)$ à $n$ sommets est la matrice $\check {M}$ de dimension $n \times n$ dont l'élément $\check {M}_{ij}$ représente le nombre d'arcs d'origine $i$ et d'extrémité $j$.},%
-symbol={\relax },%
-symbolplural={\relax },%
-user1={},%
-user2={},%
-user3={},%
-user4={},%
-user5={},%
-user6={},%
-long={},%
-longplural={},%
-short={},%
-shortplural={},%
-counter={page},%
-parent={},%
-%
-}%
-}%
-\ifglsentryexists{xor}{}%
-{%
-\gls@defglossaryentry{xor}%
-{%
-name={ou exclusif},%
-sort={ou exclusif},%
-type={main},%
-first={ou exclusif},%
-firstplural={ou exclusifs},%
-text={ou exclusif},%
-plural={ou exclusifs},%
-description={La fonction \og ou exclusif\fg {}, XOR, est l'opérateur de $\Bool ^2$ dans $\Bool $ qui prend la valeur 1 si seulement si les deux opérandes ont des valeurs distinctes.},%
-descriptionplural={La fonction \og ou exclusif\fg {}, XOR, est l'opérateur de $\Bool ^2$ dans $\Bool $ qui prend la valeur 1 si seulement si les deux opérandes ont des valeurs distinctes.},%
-symbol={\ensuremath {\oplus }},%
-symbolplural={\ensuremath {\oplus }},%
-user1={},%
-user2={},%
-user3={},%
-user4={},%
-user5={},%
-user6={},%
-long={},%
-longplural={},%
-short={},%
-shortplural={},%
-counter={page},%
-parent={},%
-%
-}%
-}%
-\ifglsentryexists{matriceDeTransitions}{}%
-{%
-\gls@defglossaryentry{matriceDeTransitions}%
-{%
-name={matrice de transitions},%
-sort={matrice de transitions},%
-type={main},%
-first={matrice de transitions},%
-firstplural={matrice de transitionss},%
-text={matrice de transitions},%
-plural={matrice de transitionss},%
-description={Le nombre $p_{ij}= P(X_1=j \mid X_0 =i)$ est appelé probabilité de transition de l'état $i$ à l'état $j$ en un pas. La matrice composée des $p_{ij}$ est la matrice de transitions associée à la chaine de Markov $X$.},%
-descriptionplural={Le nombre $p_{ij}= P(X_1=j \mid X_0 =i)$ est appelé probabilité de transition de l'état $i$ à l'état $j$ en un pas. La matrice composée des $p_{ij}$ est la matrice de transitions associée à la chaine de Markov $X$.},%
-symbol={\relax },%
-symbolplural={\relax },%
-user1={},%
-user2={},%
-user3={},%
-user4={},%
-user5={},%
-user6={},%
-long={},%
-longplural={},%
-short={},%
-shortplural={},%
-counter={page},%
-parent={},%
-%
-}%
-}%

diff --git a/main.pdf b/main.pdf
index 5c4e3bd6ab43cffd20423f4a563c2d93d99b152b..5ee54b773f66abdba39983cc386dbb88660d4309 100644 (file)
Binary files a/main.pdf and b/main.pdf differ

diff --git a/main.tex b/main.tex
index e12726aff13f73705cec5f2ed529588dd7297fb0..c16595e1021448ae0d1d8b2bf9e38216e02b5a83 100644 (file)
--- a/main.tex
+++ b/main.tex
@@ -11,18 +11,16 @@
 
 \documentclass[french]{spimufchdr}
 \usepackage{dsfont}
 
 \documentclass[french]{spimufchdr}
 \usepackage{dsfont}

-\usepackage{glossaries}

 \usepackage{graphicx}
 \usepackage{listings}
 \usepackage{graphicx}
 \usepackage{listings}

-\usepackage{verbatim}
- 
-% The TeX code is entering with UTF8
-% character encoding (Linux and MacOS standards)
+%\usepackage[font=footnotesize]{subfig}

 \usepackage[utf8]{inputenc}
 \usepackage[utf8]{inputenc}

+\usepackage{thmtools, thm-restate}
+%\declaretheorem{theorem}

 
 %%--------------------
 %% Search path for pictures
 
 %%--------------------
 %% Search path for pictures

-%\graphicspath{{path1/},{path2/}}
+\graphicspath{{images/},{path2/}}

 
 %%--------------------
 %% Definition of the bibliography entries
 
 %%--------------------
 %% Definition of the bibliography entries


@@ -130,13 +128,6 @@
 \newtheorem{Def}{Définition}
 
 \begin{document}
 \newtheorem{Def}{Définition}
 
 \begin{document}

-\input{glossaire.tex}
-
-% \chapter*{Remerciements}
-
-% Blabla blabla.
-
-% \tableofcontents

 
  
 
 
  
 


@@ -151,22 +142,29 @@ Blabla blabla.
 \part{Système Booléens}
 
 \chapter{Iterations discrètes de Systèmes Dynamiques booléens}
 \part{Système Booléens}
 
 \chapter{Iterations discrètes de Systèmes Dynamiques booléens}

-
-\JFC{Chapeau chapitre à faire}
+\section{Formalisation}

 \input{sdd}
 
 
 \input{sdd}
 
 

-\chapter{Combinaisons Synchrones et Asynchrones de Systèmes Booléens}
+\section{Combinaisons synchrones et asynchrones}

 \input{mixage}
 
 
 \input{mixage}
 
 

+\section{Conclusion}
+Introduire de l'asynchronisme peut permettre de réduire le temps 
+d'exécution global, mais peut aussi introduire de la divergence. 
+Dans ce chapitre, nous avons exposé comment construire un mode combinant les
+avantage du synchronisme en terme de convergence avec les avantages 
+de l'asynchronisme en terme de vitesse de convergence.
+
+
+

 
 \chapter[Preuve de convergence de systèmes booléens]{Preuve automatique de  convergence de systèmes booléens}\label{chap:promela}
 \input{modelchecking}
 
 
 
 
 \chapter[Preuve de convergence de systèmes booléens]{Preuve automatique de  convergence de systèmes booléens}\label{chap:promela}
 \input{modelchecking}
 
 
 

-

 \JFC{Mixage}
 
 
 \JFC{Mixage}
 
 

diff --git a/mixage.tex b/mixage.tex
index a499409656f0ddabdc97a69d5fdc6bd53b3a5aca..d5f1981d43478f293e5ea98fdf53ca9b1e274a02 100644 (file)
--- a/mixage.tex
+++ b/mixage.tex
@@ -1,8 +1,19 @@
-\JFC{Refaire le châpeau}
-\section{Généralisation au cadre asynchrone}
-Dans ce chapitre une stratégie $s=(s^{t})^{t \in \Nats}$ est une séquence
-\emph{des éléments} qui sont mis à jour au temps $t$. Pratiquement, 
-on représente ceci comme un nombre décimal dont la représentation en 
+
+Pour être exécuté, 
+le mode des itérations généralisées nécessite que chaque élément 
+connaisse la valeur de chaque autre élément dont il dépend.
+Pratiquement, cela se réalise en diffusant les valeurs des éléments de 
+proche en proche à tous les composants.
+Dans le mode généralisé 
+\emph{asynchrone}, le composant n'attend pas: il met à jour sa 
+valeur avec les dernières valeurs dont il dispose, même si celles-ci 
+ne sont pas à jour.
+Cette section vise l'étude de ce mode.
+
+
+%\subsection{Généralisation au cadre asynchrone}
+Pratiquement, chaque stratégie du mode généralisé peut être 
+mémorisée  comme un nombre décimal dont la représentation en 

 binaire donne la liste des éléments modifiés. Par exemple, pour un système 
 à 5 éléments la stratégie définie par 
 \begin{equation}\label{eq:pseudo}
 binaire donne la liste des éléments modifiés. Par exemple, pour un système 
 à 5 éléments la stratégie définie par 
 \begin{equation}\label{eq:pseudo}


@@ -46,7 +57,7 @@ fonction des dernières valeurs qu'il connaît des autre composants.
 Obtenir où non les valeurs les plus à jours dépend du temps de calcul et 
 du temps d'acheminement de celles-ci. On parle de latence, de délai.
 
 Obtenir où non les valeurs les plus à jours dépend du temps de calcul et 
 du temps d'acheminement de celles-ci. On parle de latence, de délai.
 

-Formalisons le mode les itérations asynchrones.
+Formalisons le mode les itérations asynchrone.

 Soit $x^0 =(x_1^0, \ldots, x_n^0)$ une configuration initiale.
 Soit $(D^{t})^{t \in  \Nats}$ la suite de matrice de taille $n  \times n$  
 dont chaque élément $D_{ij}^{t}$ représente la date (inférieure ou égale à $t$) 
 Soit $x^0 =(x_1^0, \ldots, x_n^0)$ une configuration initiale.
 Soit $(D^{t})^{t \in  \Nats}$ la suite de matrice de taille $n  \times n$  
 dont chaque élément $D_{ij}^{t}$ représente la date (inférieure ou égale à $t$) 


@@ -54,7 +65,8 @@ dont chaque élément $D_{ij}^{t}$ représente la date (inférieure ou égale à
 disponible au composant $i$. 
 On considère que le délai entre l'émission par $j$ et la réception par $i$, 
 défini par $\delta_{ij}^t  = t  - D_{ij}^{t}$ est borné par une constante $\delta_0$ pour tous les $i$, $j$.
 disponible au composant $i$. 
 On considère que le délai entre l'émission par $j$ et la réception par $i$, 
 défini par $\delta_{ij}^t  = t  - D_{ij}^{t}$ est borné par une constante $\delta_0$ pour tous les $i$, $j$.

-Le \emph{mode des itérations asynchrones} est défini pour chaque  $i
+Le \emph{mode des itérations généralisées sans attente} 
+est défini pour chaque  $i

 \in \{1,\ldots,n\}$ et chaque  $t=0,1,2,...$ par:
 
 \vspace{-.5em}
 \in \{1,\ldots,n\}$ et chaque  $t=0,1,2,...$ par:
 
 \vspace{-.5em}


@@ -87,13 +99,15 @@ $(D^{(t)})^{t  \in \Nats}$, alors les itérations de  $f$ sont
 \emph{universellement convergentes}.
 
 
 \emph{universellement convergentes}.
 
 

-\section{Exemple jouet}
+\subsection{Exemple jouet}

 On considère cinq éléments prenant à valeurs dans $\Bool$. 
 Une configuration dans $\Bool^5$ est représentée par un entier entre 
 0 et 31. La~\Fig{fig:mix:map} donne la fonction définissant la dynamique du 
 système. La~\Fig{fig:mix:xplgraph} donne le graphe d'interaction associé à cette fonction.
 On note que le graphe d'interaction contient cinq cycles. Les résultats 
 On considère cinq éléments prenant à valeurs dans $\Bool$. 
 Une configuration dans $\Bool^5$ est représentée par un entier entre 
 0 et 31. La~\Fig{fig:mix:map} donne la fonction définissant la dynamique du 
 système. La~\Fig{fig:mix:xplgraph} donne le graphe d'interaction associé à cette fonction.
 On note que le graphe d'interaction contient cinq cycles. Les résultats 

-connus~\cite{Bah00} de conditions suffisantes établissant la convergence du système pour les itérations synchrones et asynchrones sont basés sur l'absence de cycles. Ils ne peuvent donc pas être appliqués ici.
+connus~\cite{Bah00} de conditions suffisantes établissant la convergence
+du système pour les itérations généralisées sont
+basés sur l'absence de cycles. Ils ne peuvent donc pas être appliqués ici.

 
 \begin{figure}[ht]
 \begin{minipage}[b]{0.55\linewidth}
 
 \begin{figure}[ht]
 \begin{minipage}[b]{0.55\linewidth}


@@ -112,7 +126,7 @@ connus~\cite{Bah00} de conditions suffisantes établissant la convergence du sys
 \end{minipage}\hfill
 \begin{minipage}[b]{.40\linewidth}
   \begin{center}
 \end{minipage}\hfill
 \begin{minipage}[b]{.40\linewidth}
   \begin{center}

-    \includegraphics[scale=0.55]{images/xplgraphmix.eps}
+    \includegraphics[scale=0.55]{xplgraphmix}

   \end{center}
   \caption{Graphe d'interaction associé à $f$.}
   \label{fig:mix:xplgraph}
   \end{center}
   \caption{Graphe d'interaction associé à $f$.}
   \label{fig:mix:xplgraph}


@@ -122,12 +136,12 @@ connus~\cite{Bah00} de conditions suffisantes établissant la convergence du sys
 
 \begin{figure}
 \begin{minipage}{0.56\linewidth}
 
 \begin{figure}
 \begin{minipage}{0.56\linewidth}

-  \includegraphics[scale=0.55]{images/para_iterate_dec.eps}
+  \includegraphics[scale=0.55]{para_iterate_dec}

   \caption{Itérations parallèles de $f$.}\label{fig:mix:xplparaFig}
 \end{minipage}
 \hfill
 \begin{minipage}{0.39\linewidth}
   \caption{Itérations parallèles de $f$.}\label{fig:mix:xplparaFig}
 \end{minipage}
 \hfill
 \begin{minipage}{0.39\linewidth}

-  \includegraphics[scale=0.55]{images/chao_iterate_excerpt.eps}
+  \includegraphics[scale=0.55]{chao_iterate_excerpt}

   \caption{Extrait d'itérations chaotiques.}
   \label{fig:mix:xplchaoFig}
 \end{minipage}
   \caption{Extrait d'itérations chaotiques.}
   \label{fig:mix:xplchaoFig}
 \end{minipage}


@@ -160,17 +174,17 @@ $$
 \noindent sinon. 
 En démarrant de $x^0=00011$, le système atteint $x^1 = 01011$ et boucle entre 
 ces deux configurations. Pour une même stratégies, les itérations 
 \noindent sinon. 
 En démarrant de $x^0=00011$, le système atteint $x^1 = 01011$ et boucle entre 
 ces deux configurations. Pour une même stratégies, les itérations 

-asynchrones divergent alors que les synchrones convergent.
+asynhrones divergent alors que les synchrones convergent.

 Les sections suivantes de ce chapitre montrent comment résoudre ce problème.
 
 Les sections suivantes de ce chapitre montrent comment résoudre ce problème.
 

-\section{Itérations Mixes}
+\subsection{Itérations Mixes}

 Introduit dans~\cite{abcvs05}  
 le mode d'\emph{itérations mixes} combine synchronisme et asynchronisme.
 Intuitivement, les n{\oe}uds qui pourraient introduire des cycles dans 
 les itérations asynchrones sont regroupés. 
 Les noeuds à l'intérieur de chaque groupe seront itérés de manière 
 synchrone. 
 Introduit dans~\cite{abcvs05}  
 le mode d'\emph{itérations mixes} combine synchronisme et asynchronisme.
 Intuitivement, les n{\oe}uds qui pourraient introduire des cycles dans 
 les itérations asynchrones sont regroupés. 
 Les noeuds à l'intérieur de chaque groupe seront itérés de manière 
 synchrone. 

-L'asynchronisme est conservé entre les groupes.
+Les itérations asynchrones sont conservées entre les groupes.

 
 \begin{Def}[Relation de Synchronisation]\label{def:eqrel}
   Soit une fonction $f$ et  $\Gamma(f)$ son  graphe d'interaction. 
 
 \begin{Def}[Relation de Synchronisation]\label{def:eqrel}
   Soit une fonction $f$ et  $\Gamma(f)$ son  graphe d'interaction. 


@@ -234,7 +248,7 @@ La preuve de ce théorème est donnée en section~\ref{anx:mix}.
 
 
 
 
 
 

-\section{Durées de convergence} 
+\subsection{Durées de convergence} 

 Cette section donne des bornes supérieures et inférieures des durées 
 globales de convergence pour les modes synchrones, mixes et asynchrones.
 Pour simplifier le discours, on considère que les itérations 
 Cette section donne des bornes supérieures et inférieures des durées 
 globales de convergence pour les modes synchrones, mixes et asynchrones.
 Pour simplifier le discours, on considère que les itérations 


@@ -246,7 +260,7 @@ de communication, ce depuis l'initialisation et jusqu'à la stabilisation.
 Pour simplifier l'évaluation, nous considérons que le temps de calcul d'une 
 itération sur un composant ainsi que celui de communication entre deux 
 composants est constant. Ceci implique en particulier que, dans 
 Pour simplifier l'évaluation, nous considérons que le temps de calcul d'une 
 itération sur un composant ainsi que celui de communication entre deux 
 composants est constant. Ceci implique en particulier que, dans 

-le mode asynchrone, les délais  sont bornés. En d'autres mots, il existe 
+le mode asynchrone, ces derniers  sont bornés. En d'autres mots, il existe 

 un entier $\delta_0$ tel que $0 \le t-D_{ij}^t \le \delta_0$ est établi 
 pour tout couple de n{\oe}uds $(i,j)$. 
 Les notations utilisées sont les suivantes:
 un entier $\delta_0$ tel que $0 \le t-D_{ij}^t \le \delta_0$ est établi 
 pour tout couple de n{\oe}uds $(i,j)$. 
 Les notations utilisées sont les suivantes:


@@ -294,13 +308,13 @@ graphe d'interaction, le temps global de convergence est
 \begin{figure}
   \centering
   \begin{minipage}{1\linewidth}
 \begin{figure}
   \centering
   \begin{minipage}{1\linewidth}

-    \includegraphics[scale=0.4]{images/eval_sync.eps}
+    \includegraphics[scale=0.4]{eval_sync}

     \caption{Itérations parallèles}
     \label{fig:evalsync}
   \end{minipage}
   
   \begin{minipage}{1\textwidth}
     \caption{Itérations parallèles}
     \label{fig:evalsync}
   \end{minipage}
   
   \begin{minipage}{1\textwidth}

-    \includegraphics[scale=0.4]{images/eval_mixte.pdf}
+    \includegraphics[scale=0.4]{eval_mixte}

     \caption{Itérations mixes avec
       \class{1} $=\{1,2\}$, \class{3} $=\{3\}$,
       \class{4} $=\{4,5\}$.}
     \caption{Itérations mixes avec
       \class{1} $=\{1,2\}$, \class{3} $=\{3\}$,
       \class{4} $=\{4,5\}$.}


@@ -308,7 +322,7 @@ graphe d'interaction, le temps global de convergence est
   \end{minipage}
   
   \begin{minipage}{1\textwidth}
   \end{minipage}
   
   \begin{minipage}{1\textwidth}

-    \includegraphics[scale=0.4]{images/eval_async.pdf}
+    \includegraphics[scale=0.4]{eval_async}

     \caption{Itérations asynchrones}
     \label{fig:evalasync}
   \end{minipage}
     \caption{Itérations asynchrones}
     \label{fig:evalasync}
   \end{minipage}


@@ -366,7 +380,7 @@ graphe d'interaction, le temps global de convergence est
 %   \begin{figure}%[h]
 %     \centering
 %     % \includegraphics[width=\textwidth]{eval_siac.eps}
 %   \begin{figure}%[h]
 %     \centering
 %     % \includegraphics[width=\textwidth]{eval_siac.eps}

-%     \includegraphics[width=\textwidth]{images/eval_siac.eps}
+%     \includegraphics[width=\textwidth]{eval_siac.eps}

 %     \caption{Execution  of  the \textit{SIAC}  iterations  starting  from state  4
 %       (00100).}
 %     \label{fig:evalsiac}
 %     \caption{Execution  of  the \textit{SIAC}  iterations  starting  from state  4
 %       (00100).}
 %     \label{fig:evalsiac}


@@ -435,7 +449,7 @@ ascendants pour converger. On a dans ce cas:
   mode parallèle.
 \end{xpl}
 
   mode parallèle.
 \end{xpl}
 

-\subsection{Le mode asynchrone}
+\subsection{Le mode généralisé asynchrone}

 \label{sec:evalasync}
 En terme de durée de convergence, ce mode peut être vu comme un 
 cas particulier du mode mixe où toutes les classes sont des singletons.
 \label{sec:evalasync}
 En terme de durée de convergence, ce mode peut être vu comme un 
 cas particulier du mode mixe où toutes les classes sont des singletons.


@@ -472,12 +486,6 @@ ne recouvrent nullement les communications.
 
 
 
 
 
 

-\section{Conclusion}
-Introduire de l'asynchronisme peut permettre de réduire le temps 
-d'exécution global, mais peut aussi introduire de la divergence. 
-Dans ce chapitre, nous avons exposé comment construire un mode combinant les
-avantage du synchronisme en terme de convergence avec les avantages 
-de l'asynchronisme en terme de vitesse de convergence.

  
 
 
  
 
 

diff --git a/modelchecking.tex b/modelchecking.tex
index ca223fb4c35e3d68d7293805aac76cbf8ca14b74..1b8843d80ea820bd7b3f7d49a11b636d5ead2bed 100644 (file)
--- a/modelchecking.tex
+++ b/modelchecking.tex
@@ -572,20 +572,25 @@ Toutes les preuves sont déplacées en
 annexes~\ref{anx:promela}.
 
 
 annexes~\ref{anx:promela}.
 
 

-\begin{theorem}[Correction]\label{Theo:sound}
+\begin{restatable}[Correction de la traduction vers Promela]{theorem}{promelasound}
+\label{Theo:sound}
+%

   Soit $\phi$ un modèle de système dynamique discret et $\psi$ sa traduction PROMELA.  
   Si $\psi$ vérifie
   la propriété  LTL  (\ref{eq:ltl:conv})  sous hypothèse d'équité faible,  alors
   les itérations de $\phi$ sont universellement convergentes.
   Soit $\phi$ un modèle de système dynamique discret et $\psi$ sa traduction PROMELA.  
   Si $\psi$ vérifie
   la propriété  LTL  (\ref{eq:ltl:conv})  sous hypothèse d'équité faible,  alors
   les itérations de $\phi$ sont universellement convergentes.

-\end{theorem}
-
+\end{restatable}

 
 
 
 

-\begin{theorem}[Complétude]\label{Theo:completeness}
+\begin{restatable}[Complétude de la traduction vers Promela]{theorem}{promelacomplete}
+\label{Theo:completeness}
+%

   Soit $\phi$ un modèle de système dynamique discret et $\psi$ sa traduction.  Si $\psi$ ne vérifie pas 
   la propriété LTL (\ref{eq:ltl:conv}) sous hypothèse d'équité faible,
   alors les itérations de  $\phi$ ne sont pas universellement convergentes.
   Soit $\phi$ un modèle de système dynamique discret et $\psi$ sa traduction.  Si $\psi$ ne vérifie pas 
   la propriété LTL (\ref{eq:ltl:conv}) sous hypothèse d'équité faible,
   alors les itérations de  $\phi$ ne sont pas universellement convergentes.

-\end{theorem}
+\end{restatable}
+
+

 
 
 
 
 
 

diff --git a/plan.tex b/plan.tex
index 1c13c17b9a6c44e28a9add59ff8cb95b3251f0e0..36ef8560d1adef6543dff338960f6365c5c3458e 100644 (file)
--- a/plan.tex
+++ b/plan.tex
@@ -1,6 +1,6 @@
 \chapter{Iterations discrètes}
 
 \chapter{Iterations discrètes}
 

-Formalisation: TIPE 
+Formalisation: TIPE1 et 2 

 
 Model cheking
 
 
 Model cheking
 


@@ -11,13 +11,13 @@ Mixage
 Olivier Grasset
 
 
 Olivier Grasset
 
 

-PArtie FCT11 chaos
+Partie TIPE PRNG

 
 \chapter{Rendre le chaos alléatoire}
 
 partie FCT11 random
 
 
 \chapter{Rendre le chaos alléatoire}
 
 partie FCT11 random
 

-Secrypt 14/ Mons14
+15Rairo

 
 
 
 
 
 


@@ -38,13 +38,17 @@ Oxford 11
 
 Etude de robustesse :  IIHMSP 13
 
 
 Etude de robustesse :  IIHMSP 13
 

-
+\section{Tatouage ds les pdf}
+Avec Bittar

 
 \section{Stéganographie}
 
 Stabylo
 
 
 
 \section{Stéganographie}
 
 Stabylo
 
 

+
+
+

 \chapter{Application aux fonctions de hachage}
 
 Journal Fonctions de hachage
 \chapter{Application aux fonctions de hachage}
 
 Journal Fonctions de hachage

diff --git a/sdd.tex b/sdd.tex
index f86c5448c5d0e9a87f4eb12ad69d568afae11b58..37552951ecc85d033d2eddf4a966a7f12fcc59af 100644 (file)
--- a/sdd.tex
+++ b/sdd.tex
@@ -1,184 +1,476 @@
 
 

-
-

 \JFC{Chapeau chapitre à faire}
 
 
 
 \JFC{Chapeau chapitre à faire}
 
 
 

-Cette section énonce quelques notions suffisantes 
-à la compréhension de ce document.
-Elle commence par formaliser ce que sont les systèmes dynamiques booléens 
-(section \ref{sub:sdd}) 
-et montre comment en extraire leur graphe d'itérations (section~\ref{sub:grIter})
-et d'interactions (section~\ref{sub:sdd:inter}). 
-Elle se termine en définissant une distance sur l'espace 
-$\llbracket 1;n\rrbracket^{\Nats}\times \Bool^n$ (section~\ref{sub:metric}).
-
-
-
-
-
-
-\section{Système dynamique booléen}\label{sub:sdd}
-
-Soit $n$ un entier naturel. Un système dynamique booléen est 
+% Cette section énonce quelques notions suffisantes 
+% à la compréhension de ce document.
+% Elle commence par formaliser ce que sont les systèmes dynamiques booléens 
+% (section \ref{sub:sdd}) 
+% et montre comment en extraire leur graphe d'itérations (section~\ref{sub:grIter})
+% et d'interactions (section~\ref{sub:sdd:inter}). 
+% Elle se termine en définissant une distance sur l'espace 
+% $\llbracket 1;n\rrbracket^{\Nats}\times \Bool^n$ (section~\ref{sub:metric}).
+
+
+
+
+On considère l'espace booléen 
+$\Bool=\{0,1\}$
+muni des opérateurs binaires 
+de disjonction \og +\fg{},
+de conjonction \og . \fg{} et
+unaire de négation \og $\overline{\mathstrut\enskip}$ \fg{}.
+
+
+Soit $n$ un entier naturel.
+On introduit quelques notations à propos d'éléments de $\Bool^n$. 
+L'ensemble $\{1,\dots, n\}$ sera par la suite noté $[n]$.
+Le $i^{\textrm{ème}}$ composant d'un élément 
+$x \in \Bool^n$ s'écrit  $x_i$.
+Si l'ensemble $I$ est une partie de $[n]$, alors 
+$\overline{x}^I$ est l'élément $y\in  \Bool^n$
+tel que $y_i = 1 - x_i$ si $i\in I$ et  
+$y_i = x_i$ sinon. 
+On considère les deux abréviations $\overline{x}$ pour $\overline{x}^{[n]}$ 
+(chaque composant de $\overline{x}$ est nié:
+c'est une négation composante à composante)
+et $\overline{x}^i$ pour $\overline{x}^{\{i\}}$ pour $i \in [n]$
+(seul $x_i$ est nié dans $\overline{x}$).
+Pour tout $x$ et  $y$ dans  $\Bool^n$, l'ensemble 
+$\Delta(x, y)$,  contient les $i \in [n]$
+tels que $x_i \neq y_i$.
+Soit enfin $f : \Bool^n \rightarrow \Bool^n$. Son $i^{\textrm{ème}}$ composant
+est nommé $f_i$ qui est une fonction de $\Bool^n$ dans $\Bool$.
+Pour chaque 
+$x$ dans $\Bool^n$, l'ensemble 
+$\Delta f(x)$ est défini par $\Delta f(x) = \Delta(x,f(x))$.
+On peut admettre que $f (x) = \overline{x}^{\Delta f(x)}$ .
+
+\begin{xpl}\label{xpl:1}
+On considère $n= 3$ et $f:\Bool^3 \rightarrow \Bool^3$ telle que
+$f(x)=(f_1(x),f_2(x),f_3(x))$ avec  
+$$\begin{array}{rcl}
+f_1(x_1, x_2, x_3) &=& (\overline{x_1} + \overline{x_2}).x_3 \textrm{, }\\
+f_2(x_1, x_2, x_3) &= &x_1.x_3 \textrm{ et }\\
+f_3(x_1, x_2, x_3) &=& x_1 + x_2 + x_3.
+\end{array}
+$$
+
+\begin{table}[ht]
+$$
+\begin{array}{|l|l|l||c|c|c|}
+\hline
+\multicolumn{3}{|c||}{x} & 
+\multicolumn{3}{|c|}{f(x)} \\
+\hline
+x_1 & x_2 & x_3 & 
+f_1(x) & f_2(x) & f_3(x) \\
+\hline
+0& 0 & 0 & 0 & 0  & 0 \\
+\hline 
+0& 0 & 1 & 1 &  0 & 1\\
+\hline 
+0& 1 & 0 & 0 & 0& 1\\
+\hline 
+0& 1 & 1 & 1 & 0& 1\\
+\hline 
+1& 0 & 0 & 0 & 0& 1\\
+\hline 
+1& 0 & 1 & 1 & 1& 1\\
+\hline 
+1& 1 & 0 & 0 & 0& 1\\
+\hline 
+1& 1 & 1 & 0 & 1& 1\\
+\hline 
+\end{array}
+$$
+\caption{Images de 
+$(x_1, x_2, x_3) \mapsto 
+((\overline{x_1} + \overline{x_2}).x_3,
+x_1.x_3,
+x_1 + x_2 + x_3)$ \label{table:xpl:images}}
+\end{table}
+
+La \textsc{Table}~\ref{table:xpl:images} donne l'image de chaque élément
+$x \in \Bool^3$.
+Pour $x=(0,1,0)$ les assertions suivantes se déduisent directement du tableau:
+\begin{itemize}
+\item $f(x)=(0,0,1)$;
+\item pour $I=\{1,3\}$, $\overline{x}^{I} = (1,1,1)$ et 
+  $\overline{x} = (1,0,1)$; 
+\item $\Delta(x,f(x)) = \{2,3\}$.
+\end{itemize}
+
+\end{xpl}
+
+\subsection{Réseau booléen}
+Soit $n$ un entier naturel représentant le nombre 
+d'éléments étudiés (gènes, protéines,\ldots).
+Un réseau booléen  est 

 défini à partir d'une fonction booléenne:
 \[
 f:\Bool^n\to\Bool^n,\qquad x=(x_1,\dots,x_n)\mapsto f(x)=(f_1(x),\dots,f_n(x)),
 \]
 défini à partir d'une fonction booléenne:
 \[
 f:\Bool^n\to\Bool^n,\qquad x=(x_1,\dots,x_n)\mapsto f(x)=(f_1(x),\dots,f_n(x)),
 \]

-et un {\emph{schéma des itérations}} qui peuvent être 
-parallèles, séquentielles, chaotiques, asynchrones \ldots 
-Le schéma des itérations parallèles est défini comme suit:
-à partir d'une configuration initiale $x^0\in\Bool^n$, la suite 
-$(x^{t})^{t \in \Nats}$ 
-des configurations du système est construite à partir de la relation de récurrence
-$x^{t+1}=f(x^t)$. Tous les $x_i$, $1 \le i \le n$ 
-sont ainsi mis à jour à chaque itération. 
-Le  schéma qui ne modifie qu'un élément
-$i$, $1 \le i \le n$ à chaque itération 
-est le schéma \emph{chaotique}. 
-Plus formellement, à la  $t^{\textrm{ème}}$ itération, seul le  $s_{t}^{\textrm{ème}}$ 
-composant (entre 1 et $n$) est mis à jour.
-La suite $s = \left(s_t\right)_{t \in \mathds{N}}$ est une séquence d'indices
-de $\llbracket 1;n \rrbracket$ appelée \emph{stratégie}. Formellement, dans 
-ce mode opératoire,
-soit $F_f: \llbracket1;n\rrbracket\times \Bool^{n}$ vers $\Bool^n$ définie par 
-\[
-F_f(i,x)=(x_1,\dots,x_{i-1},f_i(x),x_{i+1},\dots,x_n).
-\]
-
-Dans le schéma des itérations chaotiques pour une configuration initiale
-$x^0\in\Bool^n$ et une stratégie $s\in
-\llbracket1;n\rrbracket^\Nats$, les configurations $x^t$
-sont définies par la récurrence
-\begin{equation}\label{eq:asyn}
-x^{t+1}=F_f(s_t,x^t).
-\end{equation}
-
-Soit alors $G_f$ une fonction de $\llbracket1;n\rrbracket^\Nats\times\Bool^n$ 
-dans lui même définie par 
-\[
-G_f(s,x)=(\sigma(s),F_f(s_0,x)),
-\] 
-où $\forall t\in\Nats,\sigma(s)_t=s_{t+1}$.
-En d'autres termes la fonction $\sigma$ décale
-la stratégie fournie en argument d'un élément vers la gauche en supprimant 
-l'élément de tête. 
-Les itérations parallèles de $G_f$ depuis un point initial
-$X^0=(s,x^0)$ décrivent la même orbite que les  
-itérations chaotiques de $f$ induites par $x^0$ et la  stratégie
-$s$.
-
-\section{Graphe d'itérations}\label{sub:grIter}
-
-Soit $f$ une fonction de $\Bool^n$ dans lui-même. 
-Le {\emph{graphe des itérations chaotiques}} associé à $f$ est le 
-graphe orienté $\Gamma(f)$ défini ainsi: 
-l'ensemble de ses sommets est $\Bool^n$ et pour chaque $x\in\Bool^n$ et  
-$i\in \llbracket1;n\rrbracket$, le graphe $\Gamma(f)$ 
-contient un arc de $x$ vers $F_f(i,x)$. 
-La relation entre $\Gamma(f)$ et $G_f$ est claire: il  existe un 
-chemin  de $x$ à  $x'$ dans $\Gamma(f)$ si et seulement s'il existe une 
-stratégie  $s$ telle que les itérations  parallèles $G_f$ à partir 
-du point $(s,x)$ mènent au point $x'$.
-
-
-Dans ce qui suit, et par souci de concision, le terme \emph{graphe des itérations}
-est une abréviation de  graphe des itérations chaotiques.
-La figure~\ref{fig:xplgraphIter} donne deux exemples de graphes d'itérations 
-pour les fonctions $g$ et $h$ définies dans $\Bool^2$ qui seront reprises dans la suite.
-
-
-
-\begin{figure}%
-\centering
-\begin{minipage}{0.40\textwidth}
-  \begin{center}
-    \includegraphics[scale=0.4]{images/g.pdf}
-  \end{center}
-\caption{$g(x_1,x_2)=(\overline{x_1},x_1\overline{x_2}) $}%
-\label{fig:g:iter}%
-\end{minipage}
-\qquad
-\begin{minipage}{0.40\textwidth}%
+et un  {\emph{schéma itératif}} ou  encore \emph{mode de  mise à jour}. À  partir d'une configuration initiale $x^0\in\Bool^n$,  la suite $(x^{t})^{t
+  \in  \Nats}$ des  configurations  du  système est  construite  selon l'un  des
+schémas suivants :
+\begin{itemize}
+\item \textbf{Schéma parallèle  synchrone :} basé sur la  relation de récurrence
+  $x^{t+1}=f(x^t)$. Tous  les $x_i$, $1 \le  i \le n$,  sont ainsi mis à  jour à
+  chaque itération en utilisant l'état global précédent du système $x^t$.
+\item \textbf{Schéma  unaire :} cette terminologie  a plusieurs 
+  interprétations
+  dans  la littérature,  mais celle  que  nous
+  retenons ici  consiste à modifier la valeur 
+  d'un unique élément $i$,  $1 \le i \le  n$, à
+  chaque itération. Le choix de l'élément qui est modifié à chaque itération est
+  défini  par une  suite 
+  $S  = \left(s^t\right)^{t \in  \mathds{N}}$ qui est  une séquence
+  d'indices dans $[n]$. Cette suite est appelée \emph{stratégie unaire}. 
+%  Lorsque  cette  suite est  strictement cyclique  (sans
+  % occurrences multiples  dans le motif) sur l'ensemble  des éléments $\{1,\ldots
+  % n\}$, alors on retrouve le comportement du mode séquentiel synchrone.
+\item \textbf{Schéma généralisé:}  dans ce schéma, ce sont les valeurs  
+  d'un ensemble d'éléments de $[n]$ qui sont modifiées à  chaque  itération.
+  Dans  le  cas  particulier où  c'est la valeur d'un  singleton
+  $\{k\}$, $1 \le k  \le n$, qui est modifiée à
+  chaque  itération, on retrouve le
+  mode unaire. Dans le second cas particulier où ce sont les valeurs de 
+  tous les éléments de $\{1, \ldots,  n\}$ qui sont  modifiées
+  à chaque  itération, on retrouve  le mode
+  parallèle.  Ce mode généralise donc les deux modes précédents.  
+  Plus formellement,  à  la  $t^{\textrm{ème}}$
+  itération, seuls les éléments de la partie 
+  $s^{t} \in \mathcal{P}([n])$ sont mis à
+  jour.  La  suite $S  = \left(s^t\right)^{t \in  \mathds{N}}$ est  une séquence
+  de sous-ensembles 
+  de   $[n]$   appelée   \emph{stratégie généralisée}.
+  \end{itemize}
+
+
+ 
+ 
+
+La section suivante détaille comment représenter graphiquement les évolutions de tels réseaux.
+\subsection{Graphes des itérations}
+
+
+
+Pour un entier naturel $n$ et une 
+fonction $f : B^n \rightarrow B^n$, plusieurs évolutions sont possibles
+en fonction du schéma itératif retenu. 
+Celles-ci sont représentées par un graphe orienté dont les noeuds 
+sont les éléments de $\Bool^n$ (voir \textsc{Figure}~\ref{fig:xpl:graphs}).
+
+
+\begin{itemize}
+\item Le \emph{graphe des itérations synchrones} de $f$, noté $\textsc{gis}(f)$ 
+est le graphe orienté de $\Bool^n$ qui contient un arc $x \rightarrow y$ si 
+et seulement si $y=f(x)$.
+\item Le \emph{graphe des itérations unaires} de $f$, noté $\textsc{gia}(f)$
+est le graphe orienté de $\Bool^n$ qui contient un arc $x \rightarrow y$ si 
+et seulement s'il existe $x \in \Delta f(x)$ tel que $y = \overline{x}^i$.
+\item Le \emph{graphe des itérations généralisées} de $f$, noté $\textsc{gig}(f)$
+est le graphe orienté de $\Bool^n$ qui contient un arc $x \rightarrow y$ si 
+et seulement s'il existe un ensemble $I\subseteq \Delta f(x)$ tel que 
+$y = \overline{x}^I$. On peut remarquer que ce graphe contient comme 
+sous-graphe à la fois celui des itérations synchrones et celui 
+des itérations unaires.
+
+
+\end{itemize}
+
+
+
+\begin{xpl}
+On reprend notre exemple illustratif
+détaillé à la page~\pageref{xpl:1} avec sa table
+d'images (\textsc{Table}~\ref{table:xpl:images}).
+La \textsc{Figure}~\ref{fig:xpl:graphs} donne les trois graphes d'itérations 
+associés à $f$.
+
+\begin{figure}[ht]

   \begin{center}
   \begin{center}

-    \includegraphics[scale=0.4]{images/h.pdf}
+    \subfigure[$\textsc{gis}(f)$]{
+      \begin{minipage}{0.33\textwidth}
+        \begin{center}
+          \includegraphics[scale=0.4]{fsig}
+        \end{center}
+      \end{minipage}
+      \label{fig:fsig}
+    }
+    \subfigure[$\textsc{gia}(f)$]{
+      \begin{minipage}{0.33\textwidth}
+        \begin{center}
+          \includegraphics[scale=0.4]{faig}
+        \end{center}
+      \end{minipage}
+      \label{fig:faig}
+    }   
+    \subfigure[$\textsc{gig}(f)$]{
+      \begin{minipage}{0.33\textwidth}
+        \begin{center}
+          \includegraphics[scale=0.4]{fgig}
+        \end{center}
+      \end{minipage}
+      \label{fig:fgig}
+    }

   \end{center}
   \end{center}

-\caption{$h(x_1,x_2)=(\overline{x_1},x_1\overline{x_2}+\overline{x_1}x_2)$}%
-\label{fig:h:iter}%
-\end{minipage}%
-\caption{Graphes d'itérations de fonctions booléennes dans $\Bool^2$}
-\label{fig:xplgraphIter} 
-\end{figure}%
-
-
-
-
-
-\section{Graphe d'interactions}\label{sub:sdd:inter}
-
-Pour $x\in\Bool^n$ et $i\in\llbracket 1;n\rrbracket$, on nomme  
-$\overline{x}^i$ la configuration obtenue en niant le 
-$i^{\textrm{ème}}$ composant de $x$. En d'autres termes
-$\overline{x}^i=(x_1,\dots,\overline{x_i},\dots,x_n)$.
-Des interactions entre les composants du 
+  \caption{Graphes des itérations de la fonction 
+$f:\Bool^3 \rightarrow \Bool^3$ telle que  
+$(x_1, x_2, x_3) \mapsto 
+((\overline{x_1} + \overline{x_2}).x_3,
+x_1.x_3,
+x_1 + x_2 + x_3)$.\label{fig:xpl:graphs}
+On remarque le cycle $((101,111),(111,011),(011,101))$ 
+ à la \textsc{Figure}~(\ref{fig:fsig}).}
+\end{figure}
+\end{xpl} 
+
+
+\subsection{Attracteurs}
+
+On dit que le point 
+$x \in \Bool^n$ est un \emph{point fixe} de $f$ si  $x = f (x)$.
+Les points fixes sont particulièrement intéressants car ils correspondent 
+aux états stables:
+dans chaque graphe d'itérations, le point $x$ est un point fixe 
+si et seulement si il est son seul successeur.
+Dans le contexte des réseaux de régulation de gènes,
+ces points fixes correspondent aux configurations stables pour l'expression de
+gènes.
+
+
+
+Soit $\Gamma$ un graphe d'itérations (synchrones, unaires ou généralisées)
+de $f$. 
+Les \emph{attracteurs}  de $\Gamma$ sont les 
+plus petits sous-ensembles (au sens de l'inclusion) non vides
+$A \subseteq \Bool^n$ tels que pour tout arc
+$x \rightarrow y$ de $\Gamma$, si $x$ est un élément de $A$, alors 
+$y$ aussi.
+Un attracteur qui contient au moins deux éléments  est dit \emph{cyclique}.
+On en déduit qu'un attracteur cyclique ne contient pas de point fixe.
+En d'autres termes, lorsqu'un système entre dans un attracteur cyclique, 
+il ne peut pas atteindre un point fixe.
+
+
+On a la proposition suivante:
+
+
+\begin{theorem}\label{Prop:attracteur}
+Le point $x$ est un point fixe si et seulement si 
+$\{x\}$ est un attracteur de $\Gamma$.
+En d'autres termes, les attracteurs non cycliques de $\Gamma$ 
+sont les points fixes de $f$.
+Ainsi pour chaque $x\in \Bool^n$, il existe au moins un chemin 
+depuis $x$ qui atteint un attracteur.
+Ainsi $\Gamma$ contient toujours au moins un attracteur.
+\end{theorem}
+
+
+
+\begin{xpl}
+Les attracteurs de $\textsc{gia}(f)$ et de $\textsc{gig}(f)$ sont 
+le point fixe $000$ et l'attracteur cyclique 
+$\{001, 101,111, 011  \}$. 
+Les attracteurs de $\textsc{gis}(f)$ sont le point fixe $000$
+et l'attracteur cyclique $\{011, 101, 111\}$.
+\end{xpl}
+
+\subsection{Graphe d'interaction}
+Les interactions entre les composants du 

 système peuvent être mémorisées 
 système peuvent être mémorisées 

-dans la {\emph{matrice Jacobienne discrète}} $f'$.
+dans la {\emph{matrice jacobienne discrète}} $f'$.

 Celle-ci est définie comme étant la fonction  qui  à chaque 
 configuration $x\in\Bool^n$ associe la matrice de taille 
 Celle-ci est définie comme étant la fonction  qui  à chaque 
 configuration $x\in\Bool^n$ associe la matrice de taille 

-$n\times n$ 
-\[
-f'(x)=(f_{ij}(x)),\qquad 
-f_{ij}(x)=\frac{f_i(\overline{x}^j)-f_i(x)}{\overline{x}^j_j-x_j}\qquad (i,j\in\llbracket1;n\rrbracket).
-\]
-On note que dans l'équation donnant la valeur de $f_{ij}(x)$, 
+$n\times n$ telle que 
+\begin{equation}
+f'(x)=(f'_{ij}(x)),\qquad 
+f'_{ij}(x)=\frac{f_i(\overline{x}^j){-}f_i(x)}{\overline{x_j}{-}x_j}\qquad (i,j\in[n]).
+\label{eq:jacobienne}
+\end{equation}
+On note que dans l'équation donnant la valeur de $f'_{ij}(x)$, 

 les termes $f_i(\overline{x}^j)$, $f_i(x)$, 
 $\overline{x}^j_j$ et $x_j$ sont considérés comme des entiers naturels 
 les termes $f_i(\overline{x}^j)$, $f_i(x)$, 
 $\overline{x}^j_j$ et $x_j$ sont considérés comme des entiers naturels 

-égaux à $0$ ou à $1$ et que le calcul est effectué dans $\Z$.
-On a le lien suivant avec la \emph{matrice d'adjacence} $A$ de $f$ dans $\Bool^{n^2}$:
-le booléen $A_{ij}$ vaut 1 si et seulement s'il existe $x\in \Bool^{n}$ tel que 
-$f_{ij}(x)$ est différent de 0.
+égaux à $0$ ou à $1$ et que la différence est effectuée
+ dans $\Z$.
+Lorsqu'on supprime les signes dans la matrice jacobienne discrète, 
+on obtient une matrice notée $B(f)$ aussi de taille 
+$n\times n$.
+Celle-ci mémorise uniquement 
+l'existence d'une dépendance de tel élément vis à vis de 
+ tel élément.
+Elle ne mémorise pas \emph{comment} dépendent les éléments 
+les uns par rapport aux autres. Cette matrice est nommée 
+\emph{matrice d'incidence}.  
+
+\begin{theorem}
+Si $f_i$ ne dépend pas de $x_j$, alors pour tout $x\in [n]$, 
+$f_i(\overline{x}^j)$ est égal à  $f_i(x)$, \textit{i.e}, 
+$f'_{ij}(x)=0$. Ainsi $B(f)_{ij}$ est nulle. La réciproque est aussi vraie.
+\end{theorem} 
+
+

 
 
 En outre, les interactions peuvent se  représenter à l'aide d'un 
 graphe $G(f)$ orienté et signé défini ainsi: 
 l'ensemble des sommets est 
 
 
 En outre, les interactions peuvent se  représenter à l'aide d'un 
 graphe $G(f)$ orienté et signé défini ainsi: 
 l'ensemble des sommets est 

-$\llbracket1;n\rrbracket$ et il existe un arc de $j$ à $i$ de signe
+$[n]$ et il existe un arc de $j$ à $i$ de signe

  $s\in\{-1,1\}$, noté $(j,s,i)$, si $f_{ij}(x)=s$ pour au moins
 un $x\in\Bool^n$. 
  $s\in\{-1,1\}$, noté $(j,s,i)$, si $f_{ij}(x)=s$ pour au moins
 un $x\in\Bool^n$. 

+

 On note que la présence de 
 deux arcs de signes opposés entre deux sommets donnés 
 est possible.
 On note que la présence de 
 deux arcs de signes opposés entre deux sommets donnés 
 est possible.

-
-
-
-
-
-\begin{figure}%
-\centering
-\begin{minipage}{0.40\textwidth}
+% Dans la suite, le graphe signé $G$ sera qualifié de 
+% \emph{simple} si, pour chaque  $i$, $j$ dans $[n]$,
+% il existe au plus un arc de $j$ à $i$ dans $G$.
+Un cycle \emph{positif} (resp. négatif) de $G$
+est un cycle \emph{élémentaire} qui contient un nombre 
+pair (resp. impair) d'arcs négatifs. 
+La \emph{longueur}
+d'un cycle est le nombre d'arcs qu'il contient.
+
+\begin{xpl}
+Pour exprimer la jacobienne discrète de la fonction donnée en exemple,
+pour chaque $i$, $j$ dans
+$[3]$ on exprime 
+$f'_{ij}(x)=
+\frac
+{f_i(\overline{x}^j){-}f_i(x)}
+{\overline{x_j}{-}x_j}$
+d'après l'équation~(\ref{eq:jacobienne}).
+% Ainsi 
+% $$
+% f'_{12} (x_1,x_2,x_3)=  
+% \frac
+% { ((\overline{x_1} + \overline{\overline{x_2}}).x_3)
+% {-}  
+% ((\overline{x_1} + \overline{x_2}).x_3) 
+% }
+% {\overline{x_2}{-}x_2} =  \frac{   
+% ((\overline{x_1} + x_2).x_3)
+% {-}  
+% ((\overline{x_1} + \overline{x_2}).x_3) 
+% }{\overline{x_2}{-}x_2} .
+% $$
+% Évaluons cette fonction de $\Bool^3$ dans $\Z$ en construisant le tableau de toutes ses valeurs.
+% $$
+% \begin{array}{|c|c|c|c|c|c|c|c|}
+% \hline
+% x_1 &   x_2 &  x_3 &  
+% (\overline{x_1} + {x_2}).x_3 & (\overline{x_1} + \overline{x_2}).x_3 &   
+% (\overline{x_1} + {x_2}).x_3 {-} (\overline{x_1} + \overline{x_2}).x_3 & \overline{x_2} {-} x_2  &  
+% f'_{12} (x_1,x_2,x_3)\\
+% \hline
+% 0   &  0    &  0   &  0  & 0 & 0 & 1   & 0 \\\hline
+% 0   &  0    &  1   &  1  & 1 & 0 & 1   & 0 \\\hline
+% 0   &  1    &  0   &  0  & 0 & 0 & -1  & 0 \\\hline
+% 0   &  1    &  1   &  1  & 1 & 0 & -1  & 0 \\\hline
+% 1   &  0    &  0   &  0  & 0 & 0 & 1   & 0 \\\hline
+% 1   &  0    &  1   &  0  & 1 & -1 & 1   & -1 \\\hline
+% 1   &  1    &  0   &  0  & 0 & 0 & -1  & 0 \\\hline
+% 1   &  1    &  1   &  1  & 0 & 1& -1  & -1 \\\hline
+% \end{array}
+% $$
+% La seule valeur de $f'_{12}$ qui n'est pas nulle est -1, qui est négative.
+% Le graphe d'interaction contiendra ainsi un arc négatif entre le n{\oe}ud 2 et le n{\oe}ud 1.
+La \textsc{Figure}~(\ref{fig:f:jacobienne}) explicite la matrice jacobienne discrète de cette fonction.
+
+Le graphe d'interaction de $f$ s'en déduit directement. Il est donné à la 
+\textsc{Figure}~(\ref{fig:f:interaction}). 
+Il possède 
+un cycle négatif de longueur 1 et 
+un cycle négatif de longueur 3. 
+Concernant les cycles positifs, il en possède 
+un de longueur 1, 
+deux de longueur 2 
+et un de longueur 3.
+
+La matrice d'incidence peut se déduire de la matrice d'interaction en supprimant les signes ou bien 
+en constatant que $f_1$ dépend des trois éléments $x_1$, $x_2$ et $x_3$ et donc que la première ligne de $B(f)$ 
+est égale à $1~1~1$. De manière similaire,  $f_2$ (resp. $f_3$) dépend  de 
+$x_1$ et  de $x_3$ 
+(resp. dépend de $x_1$, $x_2$ et $x_3$).
+Ainsi la seconde ligne (resp. la troisième ligne) de $B(f)$ est $1~0~1$ (resp. est $1~1~1$). 
+La \textsc{Figure}~(\ref{fig:f:incidence}) donne la matrice d'incidence complète. 
+
+\begin{figure}[ht]

   \begin{center}
   \begin{center}

-    \includegraphics[scale=0.4]{images/gp.pdf}
-  \end{center}
-\caption{$g(x_1,x_2)=(\overline{x_1},x_1\overline{x_2}) $}%
-\label{fig:g:inter}%
-\end{minipage}
-\qquad
-\begin{minipage}{0.40\textwidth}
-  \begin{center}
-    \includegraphics[scale=0.4]{images/hp.pdf}
-  \end{center}
-\caption{$h(x_1,x_2)=(\overline{x_1},x_1\overline{x_2}+\overline{x_1}x_2)$}%
-\label{fig:h:inter}%
-\end{minipage}%
-\caption{Graphes d'interactions de fonctions booléennes dans $\Bool^2$}
-\label{fig:xplgraphInter}
-\end{figure}%
-
-
-
-
-
+     \subfigure[Matrice jacobienne de $f$.]{
+       \begin{minipage}{0.90\textwidth}
+         \begin{center}
+        $
+        \left(
+          \begin{array}{ccc}
+            \frac{   
+              ((x_1 + \overline{x_2}).x_3)
+              {-}  
+              ((\overline{x_1} + \overline{x_2}).x_3) 
+            }{\overline{x_1}{-}x_1}
+            &
+            \frac{   
+              ((\overline{x_1} + x_2).x_3)
+              {-}  
+              ((\overline{x_1} + \overline{x_2}).x_3) 
+            }{\overline{x_2}{-}x_2}
+            &
+            \frac{   
+              ((\overline{x_1} + \overline{x_2}).\overline{x_3})
+              {-}  
+              ((\overline{x_1} + \overline{x_2}).x_3) 
+            }{\overline{x_3}{-}x_3} 
+\\
+\\
+            \frac{\overline{x_1}.x_3 {-} x_1.x_3}{\overline{x_1}{-}x_1}
+             & 0 & 
+\frac{{x_1}.\overline{x_3} {-} x_1.x_3}{\overline{x_3}{-}x_3}
+ \\
+\\
+            \frac{(\overline{x_1}+x_2+x_3){-}(x_1+x_2+x_3)}{\overline{x_1}{-}{x_1}} &
+            \frac{(x_1+\overline{x_2}+x_3){-}(x_1+x_2+x_3)}{\overline{x_2}{-}{x_2}} &
+            \frac{(x_1+x_2+\overline{x_3}){-}(x_1+x_2+x_3)}{\overline{x_3}{-}{x_3}} 
+          \end{array}
+        \right)
+        $
+         \end{center}
+       \end{minipage}
+       \label{fig:f:jacobienne}
+     } 
+     
+    \subfigure[Graphe d'interaction de $f$.]{
+      \begin{minipage}{0.45\textwidth}
+      \begin{center}
+        \includegraphics[scale=0.5]{gf}
+      \end{center}
+      \label{fig:f:interaction}
+    \end{minipage}
+    }
+    
+    \subfigure[Matrice d'incidence de $f$.]{
+      \begin{minipage}{0.45\textwidth}
+        \begin{center}
+          $
+          B(f) =
+          \left(
+            \begin{array}{ccc}
+              1 & 1 & 1 \\
+              1 & 0 & 1 \\
+              1 & 1 & 1 
+            \end{array}
+          \right)
+          $
+        \end{center}
+        \label{fig:f:incidence}
+    \end{minipage}
+  }
+\end{center}  
+\caption{Représentations des dépendances entre les éléments de la fonction $f$ de l'exemple illustratif.}
+\end{figure}
+\end{xpl}

 
 
 
 
 
 


@@ -198,38 +490,88 @@ arc positif (resp. un arc négatif) de $i$ vers lui-même.
 
 
 
 
 
 

-
-
-\section{Distance sur l'espace $\llbracket 1;n\rrbracket^{\Nats}\times \Bool^n$}\label{sub:metric}
-On considère l'espace $\mathcal{X}=\llbracket 1;n\rrbracket^{\Nats}\times
-\Bool^n$ et
-on définit la distance $d$ entre les points $X=(s,x)$ et
-$X'=(s',x')$ de $\mathcal{X}$ par 
-\[
-d(X,X')= d_H(x,x')+d_S(s,s'),~\textrm{où}~
-\left\{
-\begin{array}{l}
-\displaystyle{d_H(x,x')=\sum_{i=1}^n |x_i-x'_i|}\\[5mm] 
-\displaystyle{d_S(s,s')=\frac{9}{n}\sum_{t\in\Nats}\frac{|s_t-s'_t|}{10^{t+1}}}.
-\end{array}
-\right.\,.
-\]
-On note que dans le calcul de $d_H(x,x')$-- 
-appelée \gls{distanceHamming} (cf. glossaire) entre $x$ et $x'$-- 
-les termes $x_i$ et $x'_i$ sont considérés comme des entiers naturels 
-égaux à $0$ ou à $1$ et que le calcul est effectué dans $\Z$.
-De plus, la \gls{partieentiere} (cf. glossaire) 
-$\lfloor d(X,X')\rfloor$ est égale à $d_H(x,x')$ soit la distance 
-de Hamming entre $x$ et $x'$. 
-%D'autre part, $d(X,X')-\lfloor d(X,X')\rfloor=d_S(s,s')$ 
-%mesure la différence entre $s$ et $s'$.
-On remarque que la partie décimale est inférieure à $10^{-l}$ si
-et seulement si les $l$ premiers termes des deux stratégies sont égaux. 
-De plus, si la 
-$(l+1)^{\textrm{ème}}$ décimale  
-de $d_S(s,s')$ 
-n'est pas nulle, alors $s_l$ est différent de  $s'_l$. 
-
-On a  démontré que pour toute fonction booléenne $f$, 
-$G_f$ est continue sur $\mathcal{X}$ (cf annexe~\ref{anx:cont}).   
+\subsection{Conditions de convergence}\label{sec:Robert:async}
+
+Parmi les itérations unaires caractérisées par leurs stratégies
+$S=(s^t)^{t \in \Nats}$ d'éléments appartenant à $[n]$,
+sont jugées intéressantes 
+celles qui activent au moins une fois
+chacun des $i\in[n]$. Dans le cas contraire, un élément n'est jamais modifié. 
+
+Plus formellement, une séquence finie $S=(s^t)^{t \in \Nats}$
+est dite \emph{complète} relativement à $[n]$ si 
+tout indice de $[n]$
+s'y retrouve au moins une fois.
+
+Parmi toutes les stratégies unaires de 
+$[n]^{\Nats}$, on qualifie de:
+\begin{itemize}
+\item \emph{périodiques} celles 
+qui sont constituées par une répétition indéfinie 
+d'une même séquence $S$ complète relativement à $[n]$.
+En particulier toute séquence périodique est complète.
+\item \emph{pseudo-périodiques} celles 
+qui sont constituées par une succession indéfinie de séquences 
+(de longueur éventuellement variable non supposée bornée) complètes.
+Autrement dit dans chaque stratégie pseudo-périodique, chaque indice de
+$1$ à $n$ revient indéfiniment.
+\end{itemize}
+
+
+François Robert~\cite{Rob95}
+a énoncé en 1995 le théorème suivant de convergence 
+dans le mode des itérations unaires.
+
+\begin{theorem}\label{Th:conv:GIA}
+Si le graphe $G(f)$ n'a pas de cycle et si la stratégie unaire est
+pseudo-périodique, alors tout chemin de $\textsc{GIA}(f)$ atteint 
+l'unique point fixe $\zeta$ en au plus $n$ pseudo-périodes.
+\end{theorem}
+
+Le qualificatif \emph{pseudo-périodique} peut aisément 
+s'étendre aux stratégies généralisées comme suit.
+Lorsqu'une stratégie généralisée est constituée d'une 
+succession indéfinie de séquences de parties de $[n]$ 
+dont l'union est $[n]$, cette stratégie est {pseudo-périodique}.
+J. Bahi~\cite{Bah00} a démontré le théorème suivant:
+
+\begin{theorem}\label{Th:Bahi}
+Si le graphe $G(f)$ n'a pas de cycle et si la stratégie généralisée
+est pseudo-périodique alors
+tout chemin de $\textsc{gig}(f)$ finit par atteindre
+l'unique point fixe $\zeta$. 
+\end{theorem}
+
+% \section{Distance sur l'espace $\llbracket 1;n\rrbracket^{\Nats}\times \Bool^n$}\label{sub:metric}
+% On considère l'espace $\mathcal{X}=\llbracket 1;n\rrbracket^{\Nats}\times
+% \Bool^n$ et
+% on définit la distance $d$ entre les points $X=(s,x)$ et
+% $X'=(s',x')$ de $\mathcal{X}$ par 
+% \[
+% d(X,X')= d_H(x,x')+d_S(s,s'),~\textrm{où}~
+% \left\{
+% \begin{array}{l}
+% \displaystyle{d_H(x,x')=\sum_{i=1}^n |x_i-x'_i|}\\[5mm] 
+% \displaystyle{d_S(s,s')=\frac{9}{n}\sum_{t\in\Nats}\frac{|s_t-s'_t|}{10^{t+1}}}.
+% \end{array}
+% \right.\,.
+% \]
+% On note que dans le calcul de $d_H(x,x')$-- 
+% appelée \gls{distanceHamming} (cf. glossaire) entre $x$ et $x'$-- 
+% les termes $x_i$ et $x'_i$ sont considérés comme des entiers naturels 
+% égaux à $0$ ou à $1$ et que le calcul est effectué dans $\Z$.
+% De plus, la \gls{partieentiere} (cf. glossaire) 
+% $\lfloor d(X,X')\rfloor$ est égale à $d_H(x,x')$ soit la distance 
+% de Hamming entre $x$ et $x'$. 
+% %D'autre part, $d(X,X')-\lfloor d(X,X')\rfloor=d_S(s,s')$ 
+% %mesure la différence entre $s$ et $s'$.
+% On remarque que la partie décimale est inférieure à $10^{-l}$ si
+% et seulement si les $l$ premiers termes des deux stratégies sont égaux. 
+% De plus, si la 
+% $(l+1)^{\textrm{ème}}$ décimale  
+% de $d_S(s,s')$ 
+% n'est pas nulle, alors $s_l$ est différent de  $s'_l$. 
+
+% On a  démontré que pour toute fonction booléenne $f$, 
+% $G_f$ est continue sur $\mathcal{X}$ (cf annexe~\ref{anx:cont}).