fin chap FCT11 juste la génération

diff --git a/11FCT.tex b/11FCT.tex
index 5c7747a5a9b005bd86b99cb9a5ab816b635e3302..8ab511ed51018c6923b80a45a1d48d801543aefd 100644 (file)
--- a/11FCT.tex
+++ b/11FCT.tex
@@ -59,15 +59,35 @@ $f$ dont le  graphe d'itérations
 Soit $f$ une fonction de $\Bool^{\mathsf{N}}$ vers lui-même telle que:
 \begin{enumerate}
 \item 
 Soit $f$ une fonction de $\Bool^{\mathsf{N}}$ vers lui-même telle que:
 \begin{enumerate}
 \item 

-$G(f)$ n'a pas de cycle de longueur supérieure ou égale à deux;
+$\Gamma(f)$ n'a pas de cycle de longueur supérieure ou égale à deux;

 \item 
 \item 

-chaque sommet de  $G(f)$ qui possède une boucle 
+chaque sommet de  $\Gamma(f)$ qui possède une boucle 

 positive a aussi une boucle négative;
 \item
 positive a aussi une boucle négative;
 \item

-chaque sommet de $G(f)$ est accessible depuis un sommet qui possède 
+chaque sommet de $\Gamma(f)$ est accessible depuis un sommet qui possède 

 une boucle négative.
 \end{enumerate}
 Alors, $\textsc{giu}(f)$ est fortement connexe.
 \end{theorem}
 
 La preuve de ce théorème est donnée en annexe~\ref{anx:sccg}.
 une boucle négative.
 \end{enumerate}
 Alors, $\textsc{giu}(f)$ est fortement connexe.
 \end{theorem}
 
 La preuve de ce théorème est donnée en annexe~\ref{anx:sccg}.

+
+Illustrons ce théorème par un exemple. On considère par le graphe d'interactions 
+$\Gamma(f)$ donné en figure~\ref{fig:G}. 
+Il vérifie le théorème~\ref{th:Adrien}: 
+toutes les fonctions $f$ possédant un tel graphe d'interactions
+ont un graphe d'itérations  $\textsc{giu}(f)$ fortement connexe.
+Pratiquement, il existe 34226 fonctions de $\Bool^4$ dans lui même qui 
+vérifient ce graphe d'intéraction. 
+Cependant, nombreuses sont celles qui possèdent un comportement équivalent.
+Deux fonctions sont equivalentes si leurs \textsc{giu} sont isomorphes 
+(au sens de l'isomorphisme de graphes). Il ne reste alors plus que 
+520 fonctions $f$ non équivalentes de graphe d'interactions $\Gamma(f)$.
+
+\begin{figure}%[h]
+  \begin{center}
+    \includegraphics[scale=0.5]{images/Gi.pdf}
+  \end{center}
+\caption{Exemple de graphe d'interactions vérifiant le théorème~\ref{th:Adrien}} \label{fig:G}
+\end{figure}
+

diff --git a/12TIPE.tex b/12TIPE.tex
index e735c46917e905315ab4cab8a63b42f1742aaaa4..4f9fa9b93687b46740c11992161fe6360c1ce714 100644 (file)
--- a/12TIPE.tex
+++ b/12TIPE.tex
@@ -9,38 +9,32 @@ $\Bool^{{\mathsf{N}}}$ dans lui-même.
 Dans le schéma unaire, à la  $t^{\textrm{ème}}$ itération, 
 seul le  $s_{t}^{\textrm{ème}}$ 
 composant (entre 1 et $n$) est mis à jour.
 Dans le schéma unaire, à la  $t^{\textrm{ème}}$ itération, 
 seul le  $s_{t}^{\textrm{ème}}$ 
 composant (entre 1 et $n$) est mis à jour.

-
-Formellement, pour une stratégie $s = \left(s_t\right)_{t \in \mathds{N}}$ 
+Pour une stratégie $s = \left(s_t\right)_{t \in \mathds{N}}$ 

 (\textit{i.e.}, une séquence d'indices
 (\textit{i.e.}, une séquence d'indices

-de $\llbracket 1;\mathsf{N} \rrbracket$), on définit
-la fonction $F_f: \Bool^{\mathsf{N}} \times \llbracket1;\mathsf{N}\rrbracket$
+de $\llbracket 1;\mathsf{N} \rrbracket$), on peut définir
+la fonction $F_{f_u}: \Bool^{\mathsf{N}} \times \llbracket1;\mathsf{N}\rrbracket$

 vers $\Bool^\mathsf{N}$ par 
 \[
 vers $\Bool^\mathsf{N}$ par 
 \[

-F_f(x,i)=(x_1,\dots,x_{i-1},f_i(x),x_{i+1},\dots,x_\mathsf{N}).
+F_{f_u}(x,i)=(x_1,\dots,x_{i-1},f_i(x),x_{i+1},\dots,x_\mathsf{N}).

 \]
 
 Dans le schéma des itérations unaires pour une configuration initiale
 $x^0\in\Bool^\mathsf{N}$ et une stratégie $s\in
 \llbracket1;\mathsf{N}\rrbracket^\Nats$, les configurations $x^t$
 sont définies par la récurrence
 \]
 
 Dans le schéma des itérations unaires pour une configuration initiale
 $x^0\in\Bool^\mathsf{N}$ et une stratégie $s\in
 \llbracket1;\mathsf{N}\rrbracket^\Nats$, les configurations $x^t$
 sont définies par la récurrence

-x\begin{equation}\label{eq:asyn}
-x^{t+1}=F_f(x^t,s_t).
+\begin{equation}\label{eq:asyn}
+x^{t+1}=F_{f_u}(x^t,s_t).

 \end{equation}
 
 \end{equation}
 

-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 asynchrones de $f$ induites par $x^0$ et la  stratégie
-$s$.
-

 
 On peut alors construire l'espace 
 
 On peut alors construire l'espace 

-$\mathcal{X} =
+$\mathcal{X}_u =

 \Bool^{{\mathsf{N}}} \times \llbracket1;{\mathsf{N}}\rrbracket^{\Nats}$ 
 \Bool^{{\mathsf{N}}} \times \llbracket1;{\mathsf{N}}\rrbracket^{\Nats}$ 

-et la fonction d'iteration $G_f$ définie  de 
-$\mathcal{X}$ 
+et la fonction d'iteration $G_{f_u}$ définie  de 
+$\mathcal{X}_u$ 

 dans lui-même par 
 \[
 dans lui-même par 
 \[

-G_f(x,s)=(F_f(x,s_0),\sigma(s)).
+G_{f_u}(x,s)=(F_{f_u}(x,s_0),\sigma(s)).

 \] 
 
 Dans cette définition, la fonction 
 \] 
 
 Dans cette définition, la fonction 


@@ -57,14 +51,13 @@ $$
 
 Ainsi, effectuer des itérations unaires sur la fonction 
 $f$ selon une stratégie $s$ revient à effectuer des itérations
 
 Ainsi, effectuer des itérations unaires sur la fonction 
 $f$ selon une stratégie $s$ revient à effectuer des itérations

-parallèles de la fonctions $G_f$ dans  $\mathcal{X}$.
+parallèles de la fonctions $G_{f_u}$ dans  $\mathcal{X}_u$.
+La section suivante introduit une métrique sur $\mathcal{X}_u$.

 
 

-La section suivante introduit une métrique sur $\mathcal{X}$.
-
-\subsection{Une métrique pour $\mathcal{X}$}
-Sur $\mathcal{X}$, 
+\subsection{Une métrique pour $\mathcal{X}_u$}
+Sur $\mathcal{X}_u$, 

 on définit la distance $d$ entre les points $X=(x,s)$ et
 on définit la distance $d$ entre les points $X=(x,s)$ et

-$X'=(x',s')$ de $\mathcal{X}$ par 
+$X'=(x',s')$ de $\mathcal{X}_u$ par 

 \[
 d(X,X')= d_H(x,x')+d_S(s,s'),~\textrm{où}~
 \left\{
 \[
 d(X,X')= d_H(x,x')+d_S(s,s'),~\textrm{où}~
 \left\{


@@ -88,40 +81,40 @@ $(l+1)^{\textrm{ème}}$ décimale
 de $d_S(s,s')$ 
 n'est pas nulle, alors $s_l$ est différent de  $s'_l$. 
 
 de $d_S(s,s')$ 
 n'est pas nulle, alors $s_l$ est différent de  $s'_l$. 
 

-La section fournit quelques résultats de caractérisation de fonctions 
-chaotiques pour le schéma unaire.
+Se pose la question de caractériser les fonctions $f$ telles que 
+les itérations de $G_{f_u}$ associées à leurs itérations unaires 
+sont chaotiques dans $\mathcal{X}_u$. La section suivante 
+apporte une réponse à cette question. 
+

 
 

+\subsection{Caractérisation des fonctions rendant 
+chaotiques $G_{f_u}$ sur $\mathcal{X}_u$}

 
 

-\subsection{Caractérisation des fonctions chaotiques 
-pour le schéma unaire}

 
 On peut tout d'abord démontrer que pour toute fonction booléenne $f$, 
 
 On peut tout d'abord démontrer que pour toute fonction booléenne $f$, 

-$G_f$ est continue sur $\mathcal{X}$ (cf annexe~\ref{anx:cont}).   
+$G_{f_u}$ est continue sur $\mathcal{X}_u$ (cf annexe~\ref{anx:cont}).   

 
 

-Pour charactérister les fonctions rendant chaotiques dans $
-\mathcal{X}$ les itérations de $G_f$ 
-on se focalise donc que sur la régularité et 
-sur la transitivité de $G_f$.
- 
+Pour charactérister les fonctions rendant chaotiques dans $\mathcal{X}_u$ les itérations de $G_{f_u}$ 
+on se focalise donc que sur la régularité et sur la transitivité de $G_{f_u}$.

 Ceci se réalise en établissant les relations d'inclusion entre 
 les ensembles $\mathcal{T}$ des fonctions topologiquement transitives, 
 $\mathcal{R}$ des fonctions régulières  
 et $\mathcal{C}$ des fonctions chaotiques définis respectivement ci-dessous:
 \begin{itemize}
 \item   $\mathcal{T}   =    \left\{f   :   \mathds{B}^n   \to
 Ceci se réalise en établissant les relations d'inclusion entre 
 les ensembles $\mathcal{T}$ des fonctions topologiquement transitives, 
 $\mathcal{R}$ des fonctions régulières  
 et $\mathcal{C}$ des fonctions chaotiques définis respectivement ci-dessous:
 \begin{itemize}
 \item   $\mathcal{T}   =    \left\{f   :   \mathds{B}^n   \to

-\mathds{B}^n \big/ G_f \textrm{ est transitive} \right\}$,
+\mathds{B}^n \big/ G_{f_u} \textrm{ est transitive} \right\}$,

 \item   $\mathcal{R}   =    \left\{f   :   \mathds{B}^n   \to
 \item   $\mathcal{R}   =    \left\{f   :   \mathds{B}^n   \to

-\mathds{B}^n \big/ G_f \textrm{ est régulière} \right\}$,
+\mathds{B}^n \big/ G_{f_u} \textrm{ est régulière} \right\}$,

 \item   $\mathcal{C}   =    \left\{f   :   \mathds{B}^n   \to
 \item   $\mathcal{C}   =    \left\{f   :   \mathds{B}^n   \to

-\mathds{B}^n  \big/  G_f  \textrm{  est chaotique} \right\}$.
+\mathds{B}^n  \big/  G_{f_u}  \textrm{  est chaotique} \right\}$.

 \end{itemize}
 
 
 On énnonce les théorèmes successifs suivants.
 Leur preuve est donnée en annexe~\ref{anx:chaos:unaire}.
 
 \end{itemize}
 
 
 On énnonce les théorèmes successifs suivants.
 Leur preuve est donnée en annexe~\ref{anx:chaos:unaire}.
 

-\begin{theorem} $G_f$  est transitive si et seulement si 
- $\Gamma(f)$ est fortement connexe.
+\begin{theorem} $G_{f_u}$  est transitive si et seulement si 
+ $\textsc{giu}(f)$ est fortement connexe.

 \end{theorem}
 
 \begin{theorem}
 \end{theorem}
 
 \begin{theorem}


@@ -133,8 +126,8 @@ On peut conclure  que $\mathcal{C} = \mathcal{R} \cap \mathcal{T}
 
 \begin{theorem}%[Characterization of $\mathcal{C}$]
 \label{Th:CaracIC}  
 
 \begin{theorem}%[Characterization of $\mathcal{C}$]
 \label{Th:CaracIC}  

-Soit $f:\Bool^n\to\Bool^n$. La fonction $G_f$ est chaotique  
-si et seulement si $\Gamma(f)$ est fortement connexe.
+Soit $f:\Bool^n\to\Bool^n$. La fonction $G_{f_u}$ est chaotique  
+si et seulement si $\textsc{giu}(f)$ est fortement connexe.

 \end{theorem}
 
 
 \end{theorem}
 
 

diff --git a/15TSI.tex b/15TSI.tex
index 47ecd366f94f7b130fe1c9cac8693bddf6f50817..7d1d8429d9b21e6015aad11847303cc23aac668e 100644 (file)
--- a/15TSI.tex
+++ b/15TSI.tex
@@ -1,7 +1,6 @@
 On reprend ici le même plan que dans la section précédente.
 
 On reprend ici le même plan que dans la section précédente.
 

-Soit ${\mathsf{N}}$ un entier naturel et $f$ une fonction de 
-$\Bool^{{\mathsf{N}}}$ dans lui-même.
+

 
 
 \subsection{Des itérations généralisées aux itérations parallèles}
 
 
 \subsection{Des itérations généralisées aux itérations parallèles}


@@ -11,10 +10,10 @@ c'est l'ensemble
 des $s_{t}^{\textrm{ème}}$ éléments (inclus dans $[n]$) qui 
 sont  mis à jour (c.f. équation~(\ref{eq:schema:generalise})).
 On redéfinit la fonction la fonction
 des $s_{t}^{\textrm{ème}}$ éléments (inclus dans $[n]$) qui 
 sont  mis à jour (c.f. équation~(\ref{eq:schema:generalise})).
 On redéfinit la fonction la fonction

-  $F_f:  \Bool^{\mathsf{N}} \times \mathcal{P}(\{1, \ldots, \mathsf{N}\}) 
+  $F_{f_g}:  \Bool^{\mathsf{N}} \times \mathcal{P}(\{1, \ldots, \mathsf{N}\}) 

   \rightarrow \Bool^{\mathsf{N}}$  par
   \[
   \rightarrow \Bool^{\mathsf{N}}$  par
   \[

-  F_f(x,s)_i=\left\{
+  F_{f_g}(x,s)_i=\left\{

     \begin{array}{l}
       f_i(x) \textrm{ si $i \in s$;}\\   
       x_i \textrm{ sinon.}
     \begin{array}{l}
       f_i(x) \textrm{ si $i \in s$;}\\   
       x_i \textrm{ sinon.}


@@ -28,28 +27,26 @@ $x^0\in\Bool^{\mathsf{N}}$ et une stratégie $S = \left(s_t\right)_{t \in  \math
 les
 configurations $x^t$ sont définies par la récurrence
 \begin{equation}\label{eq:asyn}
 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).
+    x^{t+1}=F_{f_g}(s_t,x^t).

   \end{equation}
   \end{equation}

-  Soit alors $G_f$ une fonction de $\Bool^{\mathsf{N}}  \times  \mathcal{P}(\{1, \ldots, {\mathsf{N}}\})^{\Nats}$ 
+  Soit alors $G_{f_g}$ une fonction de $\Bool^{\mathsf{N}}  \times  \mathcal{P}(\{1, \ldots, {\mathsf{N}}\})^{\Nats}$ 

   dans lui-même définie par 
   \[
   dans lui-même définie par 
   \[

-  G_f(S,x)=(\sigma(S),F_f(s_0,x)),
+  G_{f_g}(S,x)=(\sigma(S),F_{f_g}(s_0,x)),

   \] 
   \] 

-  où la fonction $\sigma$ est définit comme à la section précédente.
+  où la fonction $\sigma$ est définie comme à la section précédente.

   A nouveau, les itérations généralisées 
   de $f$ induites par $x^0$ et la  stratégie $S$.
   décrivent la même orbite que les 
   A nouveau, les itérations généralisées 
   de $f$ induites par $x^0$ et la  stratégie $S$.
   décrivent la même orbite que les 

-  itérations parallèles de $G_f$ depuis un point initial
+  itérations parallèles de $G_{f_g}$ depuis un point initial

   $X^0=(x^0,S)$ 
   
   
   $X^0=(x^0,S)$ 
   
   

-
-%%%%%%%%%%%%%%%%%%%%
-On peut alors construire l'espace 
-$\mathcal{X} = \Bool^{\mathsf{N}} \times
+On onstruit cette fois-ci l'espace 
+$\mathcal{X}_g = \Bool^{\mathsf{N}} \times

 \mathcal{P}(\{1, \ldots, {\mathsf{N}}\})^{\Nats}$
 
 \mathcal{P}(\{1, \ldots, {\mathsf{N}}\})^{\Nats}$
 

-\subsection{Une métrique pour $\mathcal{X}$}
+\subsection{Une métrique pour $\mathcal{X}_g$}

 
 Cette nouvelle distance va comparer des ensembles. 
 On rappelle pour quelques notions ensemblistes. 
 
 Cette nouvelle distance va comparer des ensembles. 
 On rappelle pour quelques notions ensemblistes. 


@@ -61,10 +58,10 @@ A \Delta B = (A \cap \overline{B}) \cup (\overline{A} \cap B)
 \]  
 où $\overline{B}$ désigne le complémentaire de $B$ dans $\Omega$.
 
 \]  
 où $\overline{B}$ désigne le complémentaire de $B$ dans $\Omega$.
 

-On considère l'espace $\mathcal{X}=\mathcal{P}(\{1, \ldots, {\mathsf{N}}\})^{\Nats}\times
+On considère l'espace $\mathcal{X}_g=\mathcal{P}(\{1, \ldots, {\mathsf{N}}\})^{\Nats}\times

 \Bool^{\mathsf{N}}$ et
 on définit la distance $d$ entre les points $X=(S,x)$ et
 \Bool^{\mathsf{N}}$ et
 on définit la distance $d$ entre les points $X=(S,x)$ et

-$X'=(S',x')$ de $\mathcal{X}$ par 
+$X'=(S',x')$ de $\mathcal{X}_g$ par 

 \[
 d(X,X')= d_H(x,x')+d_S(S,S'),~\textrm{où}~
 \left\{
 \[
 d(X,X')= d_H(x,x')+d_S(S,S'),~\textrm{où}~
 \left\{


@@ -84,14 +81,15 @@ de montrer que $d_S$ en une aussi, ce qui est fait en annexe~\ref{anx:distance:g
 La section suivante caractérise les fonctions $f$ qui sont  
 chaotiques pour le schéma généralisées.
 
 La section suivante caractérise les fonctions $f$ qui sont  
 chaotiques pour le schéma généralisées.
 

-
-\subsection{Caractérisation des fonctions chaotiques 
-pour le schéma généralisé}
+\subsection{Caractérisation des fonctions rendant 
+chaotiques $G_{f_g}$ sur $\mathcal{X}_g$}
+On reprend les définitions des ensembles $\mathcal{T}$, $\mathcal{R}$ et $\mathcal{C}$
+en les adaptant à  $G_{f_g}$.

 On a les théorèmes suivants dont les preuves sont données en 
 annexe~\ref{anx:chaos:generalise}.
 
 On a les théorèmes suivants dont les preuves sont données en 
 annexe~\ref{anx:chaos:generalise}.
 

-\begin{theorem} $G_f$  est transitive si et seulement si 
- $\Gamma(f)$ est fortement connexe.
+\begin{theorem} $G_{f_g}$  est transitive si et seulement si 
+ $\textsc{gig}(f)$ est fortement connexe.

 \end{theorem}
 
 \begin{theorem}
 \end{theorem}
 
 \begin{theorem}


@@ -101,8 +99,8 @@ annexe~\ref{anx:chaos:generalise}.
 
 \begin{theorem}%[Characterization of $\mathcal{C}$]
 \label{Th:CaracIC}  
 
 \begin{theorem}%[Characterization of $\mathcal{C}$]
 \label{Th:CaracIC}  

-Soit $f:\Bool^{\mathsf{N}}\to\Bool^{\mathsf{N}}$. La fonction $G_f$ est chaotique  
-si et seulement si $\Gamma(f)$ est fortement connexe.
+Soit $f:\Bool^{\mathsf{N}}\to\Bool^{\mathsf{N}}$. La fonction $G_{f_g}$ est chaotique  
+si et seulement si $\textsc{gig}(f)$ est fortement connexe.

 \end{theorem}
 
 
 \end{theorem}
 
 

diff --git a/annexesccg.tex b/annexesccg.tex
index 3db4320a045f548e37f9320592b1c12b14e8b7b6..9d32b2236fe3e6ba698471e0c8688586ecf9adb0 100644 (file)
--- a/annexesccg.tex
+++ b/annexesccg.tex
@@ -1,13 +1,13 @@
 Soit $\alpha\in\Bool$. 
 Soit $\alpha\in\Bool$. 

-On nomme $f^{\alpha}$ la fonction de $\Bool^{n-1}$ 
+On nomme $f^{\alpha}$ la fonction de $\Bool^{{\mathsf{N}}-1}$ 

 dans lui-même définie pour 
 dans lui-même définie pour 

-chaque $x\in\Bool^{n-1}$ par 
+chaque $x\in\Bool^{{\mathsf{N}}-1}$ par 

 \[
 \[

-f^{\alpha}(x)=(f_1(x,\alpha),\dots,f_{n-1}(x,\alpha)).
+f^{\alpha}(x)=(f_1(x,\alpha),\dots,f_{{\mathsf{N}}-1}(x,\alpha)).

 \]
 \]

-On nomme $\Gamma(f)^\alpha$ le sous-graphe
-de $\Gamma(f)$ engendré par le sous-ensemble
-$\Bool^{n-1} \times \{\alpha\}$ de $\Bool^n$.
+On nomme $\textsc{giu}(f)^\alpha$ le sous-graphe
+de $\textsc{giu}(f)$ engendré par le sous-ensemble
+$\Bool^{{\mathsf{N}}-1} \times \{\alpha\}$ de $\Bool^{\mathsf{N}}$.

 
 
 
 
 
 


@@ -16,27 +16,27 @@ $\Bool^{n-1} \times \{\alpha\}$ de $\Bool^n$.
 
 \begin{lemma}\label{lemma:subgraph}
 $G(f^\alpha)$ est un sous-graphe de $G(f)$: chaque arc de $G(f^\alpha)$ est
 
 \begin{lemma}\label{lemma:subgraph}
 $G(f^\alpha)$ est un sous-graphe de $G(f)$: chaque arc de $G(f^\alpha)$ est

-un arc de $G(f)$. De plus si $G(f)$ n'a pas d'arc de $n$ vers un autre 
-sommet $i\neq n$, alors on déduit
-$G(f^\alpha)$ de $G(f)$ en supprimant le sommet $n$ ainsi que tous les 
-arcs dont $n$ est soit l'extrémité, soit l'origine (et dans ce dernier  
-cas, les arcs sont des boucles sur $n$).
+un arc de $G(f)$. De plus si $G(f)$ n'a pas d'arc de ${\mathsf{N}}$ vers un autre 
+sommet $i\neq {\mathsf{N}}$, alors on déduit
+$G(f^\alpha)$ de $G(f)$ en supprimant le sommet ${\mathsf{N}}$ ainsi que tous les 
+arcs dont ${\mathsf{N}}$ est soit l'extrémité, soit l'origine (et dans ce dernier  
+cas, les arcs sont des boucles sur ${\mathsf{N}}$).

 \end{lemma}
 
 \begin{Proof}
 Supposons que $G(f^{\alpha})$ possède un arc de  $j$ vers $i$ de signe 
 \end{lemma}
 
 \begin{Proof}
 Supposons que $G(f^{\alpha})$ possède un arc de  $j$ vers $i$ de signe 

-$s$. Par définition, il existe un sommet $x\in\Bool^{n-1}$ tel que
+$s$. Par définition, il existe un sommet $x\in\Bool^{{\mathsf{N}}-1}$ tel que

 $f^{\alpha}_{ij}(x)=s$, et puisque 
 $f^{\alpha}_{ij}(x)=f_{ij}(x,\alpha)$, on en déduit que $G(f)$ possède un arc
 de $j$ à $i$ de signe $s$. Ceci prouve la première assertion. 
 Pour démontrer la seconde, il suffit de  prouver que si
 $f^{\alpha}_{ij}(x)=s$, et puisque 
 $f^{\alpha}_{ij}(x)=f_{ij}(x,\alpha)$, on en déduit que $G(f)$ possède un arc
 de $j$ à $i$ de signe $s$. Ceci prouve la première assertion. 
 Pour démontrer la seconde, il suffit de  prouver que si

-$G(f)$ a un arc de $j$ vers $i$ de signe $s$, avec $i,j\neq n$, alors
+$G(f)$ a un arc de $j$ vers $i$ de signe $s$, avec $i,j\neq {\mathsf{N}}$, alors

 $G(f^\alpha)$ contient aussi cet arc. Ainsi, supposons que $G(f)$ a un 
 $G(f^\alpha)$ contient aussi cet arc. Ainsi, supposons que $G(f)$ a un 

-arc de $j$ vers $i$ de signe $s$, avec $i,j\neq n$.
+arc de $j$ vers $i$ de signe $s$, avec $i,j\neq {\mathsf{N}}$.

 Alors, il existe
 Alors, il existe

-$x\in\Bool^{n-1}$ et $\beta\in\Bool$ tels que
+$x\in\Bool^{{\mathsf{N}}-1}$ et $\beta\in\Bool$ tels que

 $f_{ij}(x,\beta)=s$. Si $f_{ij}(x,\beta)\neq f_{ij}(x,\alpha)$, alors
 $f_{ij}(x,\beta)=s$. Si $f_{ij}(x,\beta)\neq f_{ij}(x,\alpha)$, alors

-$f_i$ dépend du  $n^{\textrm{ème}}$ composant, ce qui est en contradiction 
+$f_i$ dépend du  ${\mathsf{N}}^{\textrm{ème}}$ composant, ce qui est en contradiction 

 avec les hypothèses.
 Ainsi $f_{ij}(x,\alpha)$ est égal à $s$.
 On a donc aussi
 avec les hypothèses.
 Ainsi $f_{ij}(x,\alpha)$ est égal à $s$.
 On a donc aussi


@@ -45,80 +45,80 @@ arc de $j$ vers $i$ de signe $s$.
 \end{Proof}
 
 \begin{lemma}\label{lemma:iso}
 \end{Proof}
 
 \begin{lemma}\label{lemma:iso}

-Les graphes $\Gamma(f^\alpha)$ et $\Gamma(f)^\alpha$ sont isomorphes.
+Les graphes $\textsc{giu}(f^\alpha)$ et $\textsc{giu}(f)^\alpha$ sont isomorphes.

 \end{lemma}
 
 \begin{Proof}
 \end{lemma}
 
 \begin{Proof}

-Soit $h$ la bijection de $\Bool^{n-1}$ vers
-$\Bool^{n-1}\times \{\alpha\}$ définie par $h(x)=(x,\alpha)$ pour chaque
-$x\in\Bool^{n-1}$.
+Soit $h$ la bijection de $\Bool^{{\mathsf{N}}-1}$ vers
+$\Bool^{{\mathsf{N}}-1}\times \{\alpha\}$ définie par $h(x)=(x,\alpha)$ pour chaque
+$x\in\Bool^{{\mathsf{N}}-1}$.

 On voit facilement que $h$ permet de définir un isomorphisme
 On voit facilement que $h$ permet de définir un isomorphisme

-entre $\Gamma(f^\alpha)$ et $\Gamma(f)^\alpha$: 
-$\Gamma(f^\alpha)$ possède un arc de $x$ vers $y$ si et seulement si 
-$\Gamma(f)^\alpha$ a un  arc de $h(x)$ vers $h(y)$.
+entre $\textsc{giu}(f^\alpha)$ et $\textsc{giu}(f)^\alpha$: 
+$\textsc{giu}(f^\alpha)$ possède un arc de $x$ vers $y$ si et seulement si 
+$\textsc{giu}(f)^\alpha$ a un  arc de $h(x)$ vers $h(y)$.

 \end{Proof}
 
 
 \begin{Proof}
 du Théorème~\ref{th:Adrien}.
 \end{Proof}
 
 
 \begin{Proof}
 du Théorème~\ref{th:Adrien}.

-La preuve se fait par induction sur $n$. 
-Soit $f$ une fonction de $\Bool^n$ dans lui-même et qui vérifie les hypothèses 
+La preuve se fait par induction sur ${\mathsf{N}}$. 
+Soit $f$ une fonction de $\Bool^{\mathsf{N}}$ dans lui-même et qui vérifie les hypothèses 

 du théorème.
 du théorème.

-Si $n=1$ la démonstration est élémentaire:
+Si ${\mathsf{N}}=1$ la démonstration est élémentaire:

 en raison du troisième point du théorème, $G(f)$ a une boucle négative;
 en raison du troisième point du théorème, $G(f)$ a une boucle négative;

-ainsi $f(x)=\overline{x}$ et $\Gamma(f)$ est un cycle de longueur 2.
-On suppose donc que $n>1$ et que le théorème est valide pour toutes les 
-fonctions de $\Bool^{n-1}$ dans lui-même. 
+ainsi $f(x)=\overline{x}$ et $\textsc{giu}(f)$ est un cycle de longueur 2.
+On suppose donc que ${\mathsf{N}}>1$ et que le théorème est valide pour toutes les 
+fonctions de $\Bool^{{\mathsf{N}}-1}$ dans lui-même. 

 En raison du premier point du théorème, $G(f)$
 contient au moins un sommet $i$ tel qu'il n'existe pas dans $G(f)$
 d'arc de $i$ vers un autre sommet $j\neq i$.
 Sans perte de généralité, on peut considérer que 
 En raison du premier point du théorème, $G(f)$
 contient au moins un sommet $i$ tel qu'il n'existe pas dans $G(f)$
 d'arc de $i$ vers un autre sommet $j\neq i$.
 Sans perte de généralité, on peut considérer que 

-ce sommet est  $n$.
+ce sommet est  ${\mathsf{N}}$.

 Alors, d'après le lemme~\ref{lemma:subgraph}, 
 $f^0$ et $f^1$ vérifient les conditions de l'hypothèse.
 Alors, d'après le lemme~\ref{lemma:subgraph}, 
 $f^0$ et $f^1$ vérifient les conditions de l'hypothèse.

-Alors, par hypothèse d'induction $\Gamma(f^0)$ et
-$\Gamma(f^1)$ sont fortement connexes. 
+Alors, par hypothèse d'induction $\textsc{giu}(f^0)$ et
+$\textsc{giu}(f^1)$ sont fortement connexes. 

 Ainsi, d'après le lemme~\ref{lemma:iso}, 
 Ainsi, d'après le lemme~\ref{lemma:iso}, 

-$\Gamma(f)^0$ et $\Gamma(f)^1$ sont fortement 
+$\textsc{giu}(f)^0$ et $\textsc{giu}(f)^1$ sont fortement 

 connexes. 
 connexes. 

-Pour prouver que $\Gamma(f)$ est fortement connexe, il suffit 
-de prouver que $\Gamma(f)$ contient un arc $x\to y$ avec 
-$x_n=0<y_n$ et un arc $x\to y$ avec $x_n=1>y_n$. 
+Pour prouver que $\textsc{giu}(f)$ est fortement connexe, il suffit 
+de prouver que $\textsc{giu}(f)$ contient un arc $x\to y$ avec 
+$x_{\mathsf{N}}=0<y_{\mathsf{N}}$ et un arc $x\to y$ avec $x_{\mathsf{N}}=1>y_{\mathsf{N}}$. 

 En d'autres mots, il suffit de prouver que:
 \begin{equation}\tag{$*$}
 En d'autres mots, il suffit de prouver que:
 \begin{equation}\tag{$*$}

-\forall \alpha\in\Bool,~\exists x\in\Bool^n,\qquad  x_n=\alpha\neq f_n(x).
+\forall \alpha\in\Bool,~\exists x\in\Bool^{\mathsf{N}},\qquad  x_{\mathsf{N}}=\alpha\neq f_{\mathsf{N}}(x).

 \end{equation}
 
 \end{equation}
 

-On suppose tout d'abord que $n$ a une boucle 
+On suppose tout d'abord que ${\mathsf{N}}$ a une boucle 

 négative.
 Alors, d'après la définition de 
 négative.
 Alors, d'après la définition de 

-$G(f)$, il existe $x\in\Bool^n$ tel que $f_{nn}(x)<0$. 
-Ainsi si $x_n=0$, on a  $f_n(x)>f_n(\overline{x}^n)$, et donc 
-$x_n=0\neq f_n(x)$ et
-$\overline{x}^n_n=1\neq f_n(\overline{x}^n)$; 
-et si  $x_n=1$, on a 
-$f_n(x)<f_n(\overline{x}^n)$, donc $x_n=1\neq f_n(x)$ et $\overline{x}^n_n=0\neq
-f_n(\overline{x}^n)$. 
+$G(f)$, il existe $x\in\Bool^{\mathsf{N}}$ tel que $f_{{\mathsf{N}}{\mathsf{N}}}(x)<0$. 
+Ainsi si $x_{\mathsf{N}}=0$, on a  $f_{\mathsf{N}}(x)>f_{\mathsf{N}}(\overline{x}^{\mathsf{N}})$, et donc 
+$x_{\mathsf{N}}=0\neq f_{\mathsf{N}}(x)$ et
+$\overline{x}^{\mathsf{N}}_{\mathsf{N}}=1\neq f_{\mathsf{N}}(\overline{x}^{\mathsf{N}})$; 
+et si  $x_{\mathsf{N}}=1$, on a 
+$f_{\mathsf{N}}(x)<f_{\mathsf{N}}(\overline{x}^{\mathsf{N}})$, donc $x_{\mathsf{N}}=1\neq f_{\mathsf{N}}(x)$ et $\overline{x}^{\mathsf{N}}_{\mathsf{N}}=0\neq
+f_{\mathsf{N}}(\overline{x}^{\mathsf{N}})$. 

 Dans les deux cas, la condition ($*$) est établie.
 
 Dans les deux cas, la condition ($*$) est établie.
 

-Supposons maintenant que  $n$ n'a pas de boucle négative.
+Supposons maintenant que  ${\mathsf{N}}$ n'a pas de boucle négative.

 D'après la seconde hypothèse, 
 D'après la seconde hypothèse, 

-$n$ n'a pas de boucle, \emph{i.e.}, la valeur de $f_n(x)$
-ne dépend pas de la valeur de $x_n$. 
+${\mathsf{N}}$ n'a pas de boucle, \emph{i.e.}, la valeur de $f_{\mathsf{N}}(x)$
+ne dépend pas de la valeur de $x_{\mathsf{N}}$. 

 D'après la troisième hypothèse, 
 D'après la troisième hypothèse, 

-il existe $i\in \llbracket 1;n \rrbracket$ tel que $G(f)$ a un arc de 
-$i$ vers $n$.
-Ainsi, il existe $x \in \Bool^n$ tel que $f_{ni}(x) \neq 0$ et donc 
+il existe $i\in \llbracket 1;{\mathsf{N}} \rrbracket$ tel que $G(f)$ a un arc de 
+$i$ vers ${\mathsf{N}}$.
+Ainsi, il existe $x \in \Bool^{\mathsf{N}}$ tel que $f_{{\mathsf{N}}i}(x) \neq 0$ et donc 

 %$n$ n'est donc pas de degré zéro dans $G(f)$, \emph{i.e.} 
 %$n$ n'est donc pas de degré zéro dans $G(f)$, \emph{i.e.} 

-$f_n$ n'est pas constante.
-Ainsi, il existe $x,y\in \Bool^n$ tel que
-$f_n(x)=1$ et $f_n(y)=0$. 
-Soit  $x'=(x_1,\dots,x_{n-1},0)$ et
-$y'=(y_1,\dots,y_{n-1},1)$. 
-Puisque la valeur de $f_n(x)$
-(resp. de $f_n(y)$) ne dépend pas de la  valeur de  $x_n$ (resp. de  $y_n$),
-on a $f_n(x')=f_n(x)=1\neq x'_n$ (resp. $f_n(y')=f_n(y)=0\neq
-y'_n$). 
+$f_{\mathsf{N}}$ n'est pas constante.
+Ainsi, il existe $x,y\in \Bool^{\mathsf{N}}$ tel que
+$f_{\mathsf{N}}(x)=1$ et $f_{\mathsf{N}}(y)=0$. 
+Soit  $x'=(x_1,\dots,x_{{\mathsf{N}}-1},0)$ et
+$y'=(y_1,\dots,y_{{\mathsf{N}}-1},1)$. 
+Puisque la valeur de $f_{\mathsf{N}}(x)$
+(resp. de $f_{\mathsf{N}}(y)$) ne dépend pas de la  valeur de  $x_{\mathsf{N}}$ (resp. de  $y_{\mathsf{N}}$),
+on a $f_{\mathsf{N}}(x')=f_{\mathsf{N}}(x)=1\neq x'_{\mathsf{N}}$ (resp. $f_{\mathsf{N}}(y')=f_{\mathsf{N}}(y)=0\neq
+y'_{\mathsf{N}}$). 

 Ainsi la  condition ($*$) est établie, et le théorème est prouvé.
 \end{Proof}
 
 Ainsi la  condition ($*$) est établie, et le théorème est prouvé.
 \end{Proof}
 

diff --git a/caracgeneralise.tex b/caracgeneralise.tex
index e1c825a65782271dc0d11cb9aeed7a4c0b5aba26..0427db87648bac22bf28aab93b5943f6f6cb4475 100644 (file)
--- a/caracgeneralise.tex
+++ b/caracgeneralise.tex
@@ -1,54 +1,54 @@
 
 Commençons par caractériser l'ensemble $\mathcal{T}$ des fonctions transitives:
 
 
 Commençons par caractériser l'ensemble $\mathcal{T}$ des fonctions transitives:
 

-\begin{theorem} $G_f$  est transitive si et seulement si 
- $\Gamma(f)$ est fortement connexe.
+\begin{theorem} $G_{f_g}$  est transitive si et seulement si 
+ $\textsc{gig}(f)$ est fortement connexe.

 \end{theorem}
 
 \begin{Proof} 
 
 \end{theorem}
 
 \begin{Proof} 
 

-$\Longleftarrow$ Supposons que $\Gamma(f)$ soit fortement connexe.
-Soient $(x,S)$ et $(x',S')$ deux points de $\mathcal{X}$ et  $\varepsilon >0$. 
+$\Longleftarrow$ Supposons que $\textsc{gig}(f)$ soit fortement connexe.
+Soient $(x,S)$ et $(x',S')$ deux points de $\mathcal{X}_g$ et  $\varepsilon >0$. 

 On construit la stratégie $\tilde S$ telle que la distance 
 entre $(x,\tilde S)$ et  $(x,S)$ est inférieure à 
 On construit la stratégie $\tilde S$ telle que la distance 
 entre $(x,\tilde S)$ et  $(x,S)$ est inférieure à 

-$\varepsilon$ et telle que les  itérations parallèles de $G_f$ depuis
+$\varepsilon$ et telle que les  itérations parallèles de $G_{f_g}$ depuis

 $(x,\tilde S)$ mènent au point $(x',S')$.
 
 Pour cela, on pose $t_1 =-\lfloor\log_{10}(\varepsilon)\rfloor$ et   $x''$ la 
 configuration de $\Bool^{\mathsf{N}}$ obtenue depuis $(x,S)$
 après $t_1$ itérations
 $(x,\tilde S)$ mènent au point $(x',S')$.
 
 Pour cela, on pose $t_1 =-\lfloor\log_{10}(\varepsilon)\rfloor$ et   $x''$ la 
 configuration de $\Bool^{\mathsf{N}}$ obtenue depuis $(x,S)$
 après $t_1$ itérations

-parallèles de $G_f$. 
-Comme $\Gamma(f)$ est fortement connexe, il existe une 
+parallèles de $G_{f_g}$. 
+Comme $\textsc{gig}(f)$ est fortement connexe, il existe une 

 stratégie $S''$ et un entier  $t_2$ tels que $x'$ est atteint depuis 
 stratégie $S''$ et un entier  $t_2$ tels que $x'$ est atteint depuis 

-$(x'',S'')$ après $t_2$ itérations de $G_f$.
+$(x'',S'')$ après $t_2$ itérations de $G_{f_g}$.

 
 Considérons à présent la stratégie 
 $\tilde S=(s_0,\dots,s_{t_1-1},s''_0,\dots,s''_{t_2-1},s'_0,s'_1,s'_2,s'_3\dots)$.
 Il est évident que $(x',s')$ est atteint depuis  $(x,\tilde S)$ après 
 
 Considérons à présent la stratégie 
 $\tilde S=(s_0,\dots,s_{t_1-1},s''_0,\dots,s''_{t_2-1},s'_0,s'_1,s'_2,s'_3\dots)$.
 Il est évident que $(x',s')$ est atteint depuis  $(x,\tilde S)$ après 

-$t_1+t_2$ itérations parallèles de $G_f$. Puisque 
+$t_1+t_2$ itérations parallèles de $G_{f_g}$. Puisque 

 $\tilde s_t=s_t$ pour $t<t_1$, grâce au choix de $t_1$,
 on a $d((x,S),(x,\tilde S))<\epsilon$. 
 $\tilde s_t=s_t$ pour $t<t_1$, grâce au choix de $t_1$,
 on a $d((x,S),(x,\tilde S))<\epsilon$. 

-Par conséquent, $G_f$ est transitive.
+Par conséquent, $G_{f_g}$ est transitive.

 
 $\Longrightarrow$ Démontrons la contraposée.
 
 $\Longrightarrow$ Démontrons la contraposée.

-Si $\Gamma(f)$ n'est pas  fortement connexe, alors 
+Si $\textsc{gig}(f)$ n'est pas  fortement connexe, alors 

 il existe deux configurations $x$  et $x'$ telles qu'aucun chemin de 
 il existe deux configurations $x$  et $x'$ telles qu'aucun chemin de 

-$\Gamma(f)$ ne mène de $x$ à $x'$. 
+$\textsc{gig}(f)$ ne mène de $x$ à $x'$. 

 Soient $S$ et $S'$ deux stratégies et $\varepsilon \in ]0;1[$.
 Alors, pour tout $(x'',S'')$ tel que 
 $d((x'',S''),(x,S))<\varepsilon$ on a $x''$ qui est égal à $x$.
 Soient $S$ et $S'$ deux stratégies et $\varepsilon \in ]0;1[$.
 Alors, pour tout $(x'',S'')$ tel que 
 $d((x'',S''),(x,S))<\varepsilon$ on a $x''$ qui est égal à $x$.

-Comme il n'existe aucun chemin de $\Gamma(f)$ 
+Comme il n'existe aucun chemin de $\textsc{gig}(f)$ 

 qui mène de $x$ à $x'$, 
 qui mène de $x$ à $x'$, 

-les itérations de $G_f$ à partir de 
+les itérations de $G_{f_g}$ à partir de 

 $(x'',S'') = (x,S'')$ ne peuvent atteindre que des points 
 $(x'',S'') = (x,S'')$ ne peuvent atteindre que des points 

-$(x''',S''')$ de $\mathcal{X}$ tels que $x''' \neq x'$, 
+$(x''',S''')$ de $\mathcal{X}_g$ tels que $x''' \neq x'$, 

 et donc ne peuvent pas atteindre $(x',S')$. 
 On peut remarquer que, du fait que $x''' \neq x'$, 
 et donc ne peuvent pas atteindre $(x',S')$. 
 On peut remarquer que, du fait que $x''' \neq x'$, 

-elles n'atteignent que des points de $\mathcal{X}$
+elles n'atteignent que des points de $\mathcal{X}_g$

 dont la distance à $(x',S')$ est supérieure à 1.
 Pour tout entier naturel $t$, on a 
 dont la distance à $(x',S')$ est supérieure à 1.
 Pour tout entier naturel $t$, on a 

-$G_f^t(x'',S'') \neq (x',S')$.
-Ainsi $G_f$ n'est pas transitive et 
+$G_{f_g}^t(x'',S'') \neq (x',S')$.
+Ainsi $G_{f_g}$ n'est pas transitive et 

 par contraposée, on a la démonstration souhaitée.
 \end{Proof}
 
 par contraposée, on a la démonstration souhaitée.
 \end{Proof}
 


@@ -61,19 +61,19 @@ Prouvons à présent le théorème suivant:
 
 
 \begin{Proof}  
 
 
 \begin{Proof}  

-Soit $f:\Bool^{\mathsf{N}}\to\Bool^{\mathsf{N}}$ telle que  $G_f$ est transitive (\textit{i.e.}
+Soit $f:\Bool^{\mathsf{N}}\to\Bool^{\mathsf{N}}$ telle que  $G_{f_g}$ est transitive (\textit{i.e.}

 $f$ appartient à $\mathcal{T}$). 
 $f$ appartient à $\mathcal{T}$). 

-Soit $(x,S) \in\mathcal{X}$ et $\varepsilon >0$. Pour 
+Soit $(x,S) \in\mathcal{X}_g$ et $\varepsilon >0$. Pour 

 prouver que $f$ appartient à  $\mathcal{R}$, il suffit de prouver 
 qu'il existe une stratégie $\tilde S$ telle que la distance entre
 $(x,\tilde S)$ et $(x,S)$ est inférieure à  $\varepsilon$ et telle que 
 $(x,\tilde S)$ est un  point périodique.
 
 Soit $t_1=-\lfloor \log_{10}(\varepsilon)\rfloor$  et soit $x'$ la 
 prouver que $f$ appartient à  $\mathcal{R}$, il suffit de prouver 
 qu'il existe une stratégie $\tilde S$ telle que la distance entre
 $(x,\tilde S)$ et $(x,S)$ est inférieure à  $\varepsilon$ et telle que 
 $(x,\tilde S)$ est un  point périodique.
 
 Soit $t_1=-\lfloor \log_{10}(\varepsilon)\rfloor$  et soit $x'$ la 

-configuration obtenue après $t_1$ itérations de $G_f$ depuis  $(x,S)$. 
-D'après la proposition précédente, $\Gamma(f)$ est fortement connexe.
+configuration obtenue après $t_1$ itérations de $G_{f_g}$ depuis  $(x,S)$. 
+D'après la proposition précédente, $\textsc{gig}(f)$ est fortement connexe.

 Ainsi, il existe une stratégie $S'$ et un nombre $t_2\in\Nats$ tels
 Ainsi, il existe une stratégie $S'$ et un nombre $t_2\in\Nats$ tels

-que $x$ est atteint depuis $(x',S')$ après $t_2$ itérations de $G_f$.
+que $x$ est atteint depuis $(x',S')$ après $t_2$ itérations de $G_{f_g}$.

 
 Soit alors la  stratégie $\tilde S$ qui alterne les $t_1$ premiers termes
 de $S$ avec les $t_2$ premiers termes de $S'$. 
 
 Soit alors la  stratégie $\tilde S$ qui alterne les $t_1$ premiers termes
 de $S$ avec les $t_2$ premiers termes de $S'$. 


@@ -82,7 +82,7 @@ Ainsi $\tilde S$ est définie par
 (s_0,\dots,s_{t_1-1},s'_0,\dots,s'_{t_2-1},s_0,\dots,s_{t_1-1},s'_0,\dots,s'_{t_2-1},s_0,\dots).
 \end{equation*}
 Il est évident que  $(x,\tilde S)$ s'obtient à partir de  $(x,\tilde S)$ après
 (s_0,\dots,s_{t_1-1},s'_0,\dots,s'_{t_2-1},s_0,\dots,s_{t_1-1},s'_0,\dots,s'_{t_2-1},s_0,\dots).
 \end{equation*}
 Il est évident que  $(x,\tilde S)$ s'obtient à partir de  $(x,\tilde S)$ après

-$t_1+t_2$ itérations parallèles de $G_f$. Ainsi $(x,\tilde S)$ est un point 
+$t_1+t_2$ itérations parallèles de $G_{f_g}$. Ainsi $(x,\tilde S)$ est un point 

 périodique. Puisque $\tilde s_t$ est égal à $s_t$ pour $t<t_1$, d'après le 
 choix de  $t_1$, on a  $d((x,S),(x,\tilde S))<\epsilon$.
 \end{Proof}
 périodique. Puisque $\tilde s_t$ est égal à $s_t$ pour $t<t_1$, d'après le 
 choix de  $t_1$, on a  $d((x,S),(x,\tilde S))<\epsilon$.
 \end{Proof}


@@ -92,6 +92,6 @@ On peut conclure  que $\mathcal{C} = \mathcal{R} \cap \mathcal{T}
 
 \begin{theorem}%[Characterization of $\mathcal{C}$]
 \label{Th:CaracIC}  
 
 \begin{theorem}%[Characterization of $\mathcal{C}$]
 \label{Th:CaracIC}  

-Soit $f:\Bool^{\mathsf{N}}\to\Bool^{\mathsf{N}}$. La fonction $G_f$ est chaotique  
-si et seulement si $\Gamma(f)$ est fortement connexe.
+Soit $f:\Bool^{\mathsf{N}}\to\Bool^{\mathsf{N}}$. La fonction $G_{f_g}$ est chaotique  
+si et seulement si $\textsc{gig}(f)$ est fortement connexe.

 \end{theorem}
 \end{theorem}

diff --git a/caracunaire.tex b/caracunaire.tex
index d21e7c10f58ebf174bb9d30723d92d9295b766aa..c74aaf063e463c156d6342829e7e9ceca306731c 100644 (file)
--- a/caracunaire.tex
+++ b/caracunaire.tex
@@ -1,8 +1,8 @@
 On prouve les théorèmes suivants
 
 
 On prouve les théorèmes suivants
 
 

-\begin{theorem} $G_f$  est transitive si et seulement si 
- $\Gamma(f)$ est fortement connexe.
+\begin{theorem} $G_{f_u}$  est transitive si et seulement si 
+ $\textsc{giu}(f)$ est fortement connexe.

 \end{theorem}
 
 
 \end{theorem}
 
 


@@ -10,48 +10,48 @@ On prouve les théorèmes suivants
 
 \begin{Proof} 
 
 
 \begin{Proof} 
 

-$\Longleftarrow$ Supposons que $\Gamma(f)$ soit fortement connexe.
-Soient $(x,S)$ et $(x',S')$ deux points de $\mathcal{X}$ et  $\varepsilon >0$. 
+$\Longleftarrow$ Supposons que $\textsc{giu}(f)$ soit fortement connexe.
+Soient $(x,S)$ et $(x',S')$ deux points de $\mathcal{X}_u$ et  $\varepsilon >0$. 

 On construit la stratégie $\tilde S$ telle que la distance 
 entre $(x,\tilde S)$ et  $(x,S)$ est inférieure à 
 On construit la stratégie $\tilde S$ telle que la distance 
 entre $(x,\tilde S)$ et  $(x,S)$ est inférieure à 

-$\varepsilon$ et telle que les  itérations parallèles de $G_f$ depuis
+$\varepsilon$ et telle que les  itérations parallèles de $G_{f_u}$ depuis

 $(x,\tilde S)$ mènent au point $(x',S')$.
 
 Pour cela, on pose $t_1 =-\lfloor\log_{10}(\varepsilon)\rfloor$ et   $x''$ la 
 configuration de $\Bool^{\mathsf{N}}$ obtenue depuis $(x,S)$ après $t_1$ 
 itérations
 $(x,\tilde S)$ mènent au point $(x',S')$.
 
 Pour cela, on pose $t_1 =-\lfloor\log_{10}(\varepsilon)\rfloor$ et   $x''$ la 
 configuration de $\Bool^{\mathsf{N}}$ obtenue depuis $(x,S)$ après $t_1$ 
 itérations

-parallèles de $G_f$. 
-Comme $\Gamma(f)$ est fortement connexe, il existe une 
+parallèles de $G_{f_u}$. 
+Comme $\textsc{giu}(f)$ est fortement connexe, il existe une 

 stratégie $S''$ et un entier  $t_2$ tels que $x'$ est atteint depuis 
 stratégie $S''$ et un entier  $t_2$ tels que $x'$ est atteint depuis 

-$(x'',S'')$ après $t_2$ itérations de $G_f$.
+$(x'',S'')$ après $t_2$ itérations de $G_{f_u}$.

 
 Considérons à présent la stratégie 
 $\tilde S=(s_0,\dots,s_{t_1-1},s''_0,\dots,s''_{t_2-1},s'_0,s'_1,s'_2,s'_3\dots)$.
 Il est évident que $(x',s')$ est atteint depuis  $(x,\tilde S)$ après 
 
 Considérons à présent la stratégie 
 $\tilde S=(s_0,\dots,s_{t_1-1},s''_0,\dots,s''_{t_2-1},s'_0,s'_1,s'_2,s'_3\dots)$.
 Il est évident que $(x',s')$ est atteint depuis  $(x,\tilde S)$ après 

-$t_1+t_2$ itérations parallèles de $G_f$. Puisque 
+$t_1+t_2$ itérations parallèles de $G_{f_u}$. Puisque 

 $\tilde s_t=s_t$ pour $t<t_1$, grâce au choix de $t_1$,
 on a $d((x,S),(x,\tilde S))<\epsilon$. 
 $\tilde s_t=s_t$ pour $t<t_1$, grâce au choix de $t_1$,
 on a $d((x,S),(x,\tilde S))<\epsilon$. 

-Par conséquent, $G_f$ est transitive.
+Par conséquent, $G_{f_u}$ est transitive.

 
 $\Longrightarrow$ Démontrons la contraposée.
 
 $\Longrightarrow$ Démontrons la contraposée.

-Si $\Gamma(f)$ n'est pas  fortement connexe, alors 
+Si $\textsc{giu}(f)$ n'est pas  fortement connexe, alors 

 il existe deux configurations $x$  et $x'$ telles qu'aucun chemin de 
 il existe deux configurations $x$  et $x'$ telles qu'aucun chemin de 

-$\Gamma(f)$ ne mène de $x$ à $x'$. 
+$\textsc{giu}(f)$ ne mène de $x$ à $x'$. 

 Soient $S$ et $S'$ deux stratégies et $\varepsilon \in ]0;1[$.
 Alors, pour tout $(x'',S'')$ tel que 
 $d((x'',S''),(x,S))<\varepsilon$ on a $x''$ qui est égal à $x$.
 Soient $S$ et $S'$ deux stratégies et $\varepsilon \in ]0;1[$.
 Alors, pour tout $(x'',S'')$ tel que 
 $d((x'',S''),(x,S))<\varepsilon$ on a $x''$ qui est égal à $x$.

-Comme il n'existe aucun chemin de $\Gamma(f)$ 
+Comme il n'existe aucun chemin de $\textsc{giu}(f)$ 

 qui mène de $x$ à $x'$, 
 qui mène de $x$ à $x'$, 

-les itérations de $G_f$ à partir de 
+les itérations de $G_{f_u}$ à partir de 

 $(x'',S'') = (x,S'')$ ne peuvent atteindre que des points 
 $(x'',S'') = (x,S'')$ ne peuvent atteindre que des points 

-$(x''',S''')$ de $\mathcal{X}$ tels que $x''' \neq x'$, 
+$(x''',S''')$ de $\mathcal{X}_u$ tels que $x''' \neq x'$, 

 et donc ne peuvent pas atteindre $(x',S')$. 
 On peut remarquer que, du fait que $x''' \neq x'$, 
 et donc ne peuvent pas atteindre $(x',S')$. 
 On peut remarquer que, du fait que $x''' \neq x'$, 

-elles n'atteignent que des points de $\mathcal{X}$
+elles n'atteignent que des points de $\mathcal{X}_u$

 dont la distance à $(x',S')$ est supérieure à 1.
 Pour tout entier naturel $t$, on a 
 dont la distance à $(x',S')$ est supérieure à 1.
 Pour tout entier naturel $t$, on a 

-$G_f^t(x'',S'') \neq (x',S')$.
-Ainsi $G_f$ n'est pas transitive et 
+$G_{f_u}^t(x'',S'') \neq (x',S')$.
+Ainsi $G_{f_u}$ n'est pas transitive et 

 par contraposée, on a la démonstration souhaitée.
 \end{Proof}
 
 par contraposée, on a la démonstration souhaitée.
 \end{Proof}
 


@@ -64,19 +64,19 @@ Prouvons à présent le théorème suivant:
 
 
 \begin{Proof}  
 
 
 \begin{Proof}  

-Soit $f:\Bool^{\mathsf{N}}\to\Bool^{\mathsf{N}}$ telle que  $G_f$ est transitive (\textit{i.e.}
+Soit $f:\Bool^{\mathsf{N}}\to\Bool^{\mathsf{N}}$ telle que  $G_{f_u}$ est transitive (\textit{i.e.}

 $f$ appartient à $\mathcal{T}$). 
 $f$ appartient à $\mathcal{T}$). 

-Soit $(x,S) \in\mathcal{X}$ et $\varepsilon >0$. Pour 
+Soit $(x,S) \in\mathcal{X}_u$ et $\varepsilon >0$. Pour 

 prouver que $f$ appartient à  $\mathcal{R}$, il suffit de prouver 
 qu'il existe une stratégie $\tilde S$ telle que la distance entre
 $(x,\tilde S)$ et $(x,S)$ est inférieure à  $\varepsilon$ et telle que 
 $(x,\tilde S)$ est un  point périodique.
 
 Soit $t_1=-\lfloor \log_{10}(\varepsilon)\rfloor$  et soit $x'$ la 
 prouver que $f$ appartient à  $\mathcal{R}$, il suffit de prouver 
 qu'il existe une stratégie $\tilde S$ telle que la distance entre
 $(x,\tilde S)$ et $(x,S)$ est inférieure à  $\varepsilon$ et telle que 
 $(x,\tilde S)$ est un  point périodique.
 
 Soit $t_1=-\lfloor \log_{10}(\varepsilon)\rfloor$  et soit $x'$ la 

-configuration obtenue après $t_1$ itérations de $G_f$ depuis  $(x,S)$. 
-D'après la proposition précédente, $\Gamma(f)$ est fortement connexe.
+configuration obtenue après $t_1$ itérations de $G_{f_u}$ depuis  $(x,S)$. 
+D'après la proposition précédente, $\textsc{giu}(f)$ est fortement connexe.

 Ainsi, il existe une stratégie $S'$ et un nombre $t_2\in\Nats$ tels
 Ainsi, il existe une stratégie $S'$ et un nombre $t_2\in\Nats$ tels

-que $x$ est atteint depuis $(x',S')$ après $t_2$ itérations de $G_f$.
+que $x$ est atteint depuis $(x',S')$ après $t_2$ itérations de $G_{f_u}$.

 
 Soit alors la  stratégie $\tilde S$ qui alterne les $t_1$ premiers termes
 de $S$ avec les $t_2$ premiers termes de $S'$. 
 
 Soit alors la  stratégie $\tilde S$ qui alterne les $t_1$ premiers termes
 de $S$ avec les $t_2$ premiers termes de $S'$. 


@@ -85,7 +85,7 @@ Ainsi $\tilde S$ est définie par
 (s_0,\dots,s_{t_1-1},s'_0,\dots,s'_{t_2-1},s_0,\dots,s_{t_1-1},s'_0,\dots,s'_{t_2-1},s_0,\dots).
 \end{equation*}
 Il est évident que  $(x,\tilde S)$ s'obtient à partir de  $(x,\tilde S)$ après
 (s_0,\dots,s_{t_1-1},s'_0,\dots,s'_{t_2-1},s_0,\dots,s_{t_1-1},s'_0,\dots,s'_{t_2-1},s_0,\dots).
 \end{equation*}
 Il est évident que  $(x,\tilde S)$ s'obtient à partir de  $(x,\tilde S)$ après

-$t_1+t_2$ itérations parallèles de $G_f$. Ainsi $(x,\tilde S)$ est un point 
+$t_1+t_2$ itérations parallèles de $G_{f_u}$. Ainsi $(x,\tilde S)$ est un point 

 périodique. Puisque $\tilde s_t$ est égal à $s_t$ pour $t<t_1$, d'après le 
 choix de  $t_1$, on a  $d((x,S),(x,\tilde S))<\epsilon$.
 \end{Proof}
 périodique. Puisque $\tilde s_t$ est égal à $s_t$ pour $t<t_1$, d'après le 
 choix de  $t_1$, on a  $d((x,S),(x,\tilde S))<\epsilon$.
 \end{Proof}


@@ -95,7 +95,7 @@ On peut conclure  que $\mathcal{C} = \mathcal{R} \cap \mathcal{T}
 
 \begin{theorem}%[Characterization of $\mathcal{C}$]
 \label{Th:CaracIC}  
 
 \begin{theorem}%[Characterization of $\mathcal{C}$]
 \label{Th:CaracIC}  

-Soit $f:\Bool^{\mathsf{N}}\to\Bool^{\mathsf{N}}$. La fonction $G_f$ est chaotique  
-si et seulement si $\Gamma(f)$ est fortement connexe.
+Soit $f:\Bool^{\mathsf{N}}\to\Bool^{\mathsf{N}}$. La fonction $G_{f_u}$ est chaotique  
+si et seulement si $\textsc{giu}(f)$ est fortement connexe.

 \end{theorem}
 
 \end{theorem}
 

diff --git a/devaney.tex b/devaney.tex
index 1291793d6ff9c3ba12fe2626d8c55b34061ff708..2a2a167b3c7a4b6d6b732fb7fb561f5ca06043c6 100644 (file)
--- a/devaney.tex
+++ b/devaney.tex
@@ -1,80 +1,60 @@
 
 

-Dans  cette  partie, les  définitions  fondamentales  liées  au chaos
-dans  les systèmes booléens sont rappelées.

 
 

+Dans  cette  partie, les  définitions  fondamentales  liées  au chaos  dans  les
+systèmes booléens sont rappelées et plusieurs résultats théoriques sont montrés.

 
 

-
-Soit un espace topologique $(\mathcal{X},\tau)$ et une fonction continue $f :
-\mathcal{X} \rightarrow \mathcal{X}$.
-
-
-
-
-\begin{Def}[Chaos selon Devaney~\cite{Devaney}]
-La fonction $f$  \emph{chaotique} sur $(\mathcal{X},\tau)$ 
-si elles est régulière et topologiquement transitive.
+\begin{Def}[Chaos (Devaney)]
+Une fonction $k$ continue sur un espace métrique $(\mathcal{X},d)$ est \textbf{chaotique}
+si elle est transitive,
+régulière et fortement sensible aux conditions initiales.

 \end{Def}
 
 \end{Def}
 

-
-
-\begin{Def}[Transitivite topologique]
-La fonction  $f$ est dite  \emph{topologiquement transitive} si, 
-pour chaque paire d'ensembles ouverts
-$U,V \subset \mathcal{X}$, 
-il existe  $k>0$ tel que $f^k(U) \cap V \neq
-\varnothing$.
+\begin{Def}[Transitivité]
+Une fonction $k$ est  \textbf{transitive} sur $(\mathcal{X},d)$ si  la propriété suivante est établie:
+\[
+\forall X, Y\in \mathcal{X},
+\forall \epsilon > 0,
+\exists  Z \in \mathcal{X},
+\exists  t \in \Nats,
+d(X,Z) < \epsilon  \land k^t(Z) = Y
+\] 

 \end{Def}
 
 \begin{Def}[Point périodique]
 \end{Def}
 
 \begin{Def}[Point périodique]

-  Un point $P  \in \mathcal{X}$ est dit \emph{périodique}  de période $t$ pour
+  Un point $P  \in \mathcal{X}$ est dit \textbf{périodique}  de période $t$ pour

   une fonction $k$ si $t$ est un entier  naturel non nul tel que $k^t(P) = P$ et
   pour tout $n$, $0 < n \le t-1$, on a $k^n(P) \neq P$.
   une fonction $k$ si $t$ est un entier  naturel non nul tel que $k^t(P) = P$ et
   pour tout $n$, $0 < n \le t-1$, on a $k^n(P) \neq P$.

-  Par la  suite, $\emph{Per(k)}$ dénote  l'ensemble des points  périodiques de
+  Par la  suite, $\textbf{Per(k)}$ dénote  l'ensemble des points  périodiques de

   $k$ dans $\mathcal{X}$ de période quelconque.
 \end{Def}
 
   $k$ dans $\mathcal{X}$ de période quelconque.
 \end{Def}
 

-
-

 \begin{Def}[Régularité]
 \begin{Def}[Régularité]

-La fonction $f$ est dite \emph{régulière} 
-sur $(\mathcal{X}, \tau)$ si l'ensemble des points périodiques 
- de $f$ is dense in $\mathcal{X}$: 
-pour chaque point $x \in \mathcal{X}$, chaque voisin 
-de $x$ contient au moins un point périodique 
-(sans que la période soit nécessairement constante).
+Une fonction $k$  est dite \textbf{régulière} dans $(\mathcal{X},d)$ 
+si l'ensemble des points périodiques de $k$ est dense dans $\mathcal{X}$, 
+c'est-à-dire  si la propriété suivante est établie: 
+\[
+\forall X \in \mathcal{X}, \forall \epsilon > 0, \exists Y \in \textit{Per}(k) 
+ \textrm{ tel que } d(X,Y) < \epsilon.
+\]

 \end{Def}
 
 \end{Def}
 

-
-
-
-
-
-
-
-
-La propriété de chaos est souvent associée à la notion de 
-\og sensibilité aux conditions initiales\fg{}, notion définie elle 
-sur un espace métrique $(\mathcal{X},d)$ par:
-
-

 \begin{Def}[Forte sensibilité aux conditions initiales]
 \begin{Def}[Forte sensibilité aux conditions initiales]

-Une fonction $k$ définie sur $(\mathcal{X},\tau)$ 
-est  \emph{fortement sensible aux conditions initiales} 
+Une fonction $k$ définie sur $(\mathcal{X},d)$ 
+est  \textbf{fortement sensible aux conditions initiales} 

 s'il existe une valeur $\epsilon> 0$ telle que
 pour tout $X \in \mathcal{X}$ et pour tout 
  $\delta > 0$, il existe  $Y \in  \mathcal{X}$ et  
 $t \in \Nats$ qui vérifient  $d(X,Y) < \delta$ et 
 $d(k^t(X) , k^t(Y)) > \epsilon$.
 s'il existe une valeur $\epsilon> 0$ telle que
 pour tout $X \in \mathcal{X}$ et pour tout 
  $\delta > 0$, il existe  $Y \in  \mathcal{X}$ et  
 $t \in \Nats$ qui vérifient  $d(X,Y) < \delta$ et 
 $d(k^t(X) , k^t(Y)) > \epsilon$.

-
-La constante $\delta$ est appelée \emph{constante de sensibilité} de $f$.

 \end{Def}
 
 \end{Def}
 

+

 John Banks et ses collègues ont cependant
 démontré que la sensibilité aux conditions initiales est une conséquence
 de la régularité et de la transitivité topologique~\cite{Banks92}. 
 John Banks et ses collègues ont cependant
 démontré que la sensibilité aux conditions initiales est une conséquence
 de la régularité et de la transitivité topologique~\cite{Banks92}. 

-
-
-
+On ne se focalise donc dans la suite que sur ces deux dernières
+propriétés pour caractériser les fonctions booléennes $f$ 
+rendant chaotique la fonction engendrée $G_f$.

 
 
 
 
 
 

diff --git a/main.pdf b/main.pdf
index 8210825f8bf5ff2da646b5c0d7320411a05ca9d3..23c1a19083fd78c669723f475935022aaad3a973 100644 (file)
Binary files a/main.pdf and b/main.pdf differ

diff --git a/main.tex b/main.tex
index 27c159c8017829f0a7909829d1402375a90a4494..6887ceca45aa7b5742604918e5cfb1fa59769b6b 100644 (file)
--- a/main.tex
+++ b/main.tex
@@ -177,7 +177,7 @@ de l'asynchronisme en terme de vitesse de convergence.
 au chaos} 
 
 \chapter{Characterisation des systèmes 
 au chaos} 
 
 \chapter{Characterisation des systèmes 

-  discrets chaotiques}
+  discrets chaotiques pour les schémas unaires et généralisés}

 
 La première section  rappelle ce que sont les systèmes dynamiques chaotiques.
 Dire que cette caractérisation dépend du type de stratégie : unaire (TIPE), 
 
 La première section  rappelle ce que sont les systèmes dynamiques chaotiques.
 Dire que cette caractérisation dépend du type de stratégie : unaire (TIPE), 


@@ -197,7 +197,9 @@ On montre qu'on a des résultats similaires.
 \input{15TSI}
 
 
 \input{15TSI}
 
 

-générer des fonctions vérifiant ceci (TIPE12 juste sur le résultat d'adrien).
+\section{Générer des fonctions chaotiques}
+\input{11FCT} 
+

 
 \chapter{Prédiction des systèmes chaotiques}
 
 
 \chapter{Prédiction des systèmes chaotiques}
 


@@ -249,26 +251,22 @@ to discharge proofs notably by deductive analysis~\cite{CGK05}.
 \chapter{Preuves sur les systèmes chaotiques}
 
 
 \chapter{Preuves sur les systèmes chaotiques}
 
 

-\section{Continuité de $G_f$ dans $(\mathcal{X},d)$}\label{anx:cont}
+\section{Continuité de $G_f$ dans $(\mathcal{X}_u,d)$}\label{anx:cont}

 \input{annexecontinuite.tex}
 
 
 \input{annexecontinuite.tex}
 
 

-
-
-\section{Caractérisation des fonctions $f$ rendant chaotique $G_f$ dans $(\mathcal{X},d)$}\label{anx:chaos:unaire}
+\section{Caractérisation des fonctions $f$ rendant chaotique $G_{f_u}$ dans $(\mathcal{X}_u,d)$}\label{anx:chaos:unaire}

 \input{caracunaire.tex}
 
 
 \input{caracunaire.tex}
 
 

-\section{Preuve que $d$ est une distance sur $\mathcal{X}$}\label{anx:distance:generalise}
+\section{Preuve que $d$ est une distance sur $\mathcal{X}_g$}\label{anx:distance:generalise}

 \input{preuveDistanceGeneralisee}
 
 
 \input{preuveDistanceGeneralisee}
 
 

-\section{Caractérisation des fonctions $f$ rendant chaotique $G_f$ dans $(\mathcal{X},d)$}\label{anx:chaos:generalise}
+\section{Caractérisation des fonctions $f$ rendant chaotique $G_{f_g}$ dans $(\mathcal{X}_g,d)$}\label{anx:chaos:generalise}

 \input{caracgeneralise.tex}
 
 
 \input{caracgeneralise.tex}
 
 

-
-

 \section{Théorème~\ref{th:Adrien}}\label{anx:sccg}
 \input{annexesccg}
 
 \section{Théorème~\ref{th:Adrien}}\label{anx:sccg}
 \input{annexesccg}
 

diff --git a/mixage.tex b/mixage.tex
index a71a36d25735bb68daecf2a65e16e2dbe0a5d1fb..0b24636263588e3ec9a4fb3386f96ae18e67a10f 100644 (file)
--- a/mixage.tex
+++ b/mixage.tex
@@ -110,7 +110,7 @@ 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.
 
 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{figure}%[ht]

   \begin{center}
     $$ f(x)= \left \{
     \begin{array}{lll}
   \begin{center}
     $$ f(x)= \left \{
     \begin{array}{lll}

diff --git a/modelchecking.tex b/modelchecking.tex
index 1b8843d80ea820bd7b3f7d49a11b636d5ead2bed..6f968bbc292d48a37a491762ff62e7b812fed92b 100644 (file)
--- a/modelchecking.tex
+++ b/modelchecking.tex
@@ -1,21 +1,61 @@
-\JFC{donner dans les rappels les délais et les propriétés de convergence universelle}

 
 

-\JFC{Statuer sur la taille des exemples traitables par la démarche, cf données pratiques}

 
 

-\section{Exemple jouet}

 
 

-\begin{xpl}
-  On considère dans ce chapitre l'exemple où trois éléments dans $\Bool$. 
-  Chaque configuration est ainsi un élement de $\{0,1\}^3$, \textit{i.e.}, 
-  un nombre entre 0 et 7. 
-  La \Fig{fig:map} précise la fonction $f$ considérée et 
-  la \Fig{fig:xplgraph} donne son graphe d'intéraction.
-  
+L'étude de convergence de systèmes dynamiques discrets est simple à vérifier 
+pratiquement pour le mode synchrone. Lorsqu'on introduit des stratégies 
+pseudo périodiques pour les modes unaires et généralisées, le problème 
+se complexifie. C'est pire encore lorsqu'on traite des itérations asynchrones 
+et mixes prenant de plus en compte les délais. 
+
+Des méthodes de simulation basées sur des stratégies et des délais générés aléatoirement 
+ont déjà été présentées~\cite{BM99,BCV02}.
+Cependant, comme ces implantations ne sont pas exhaustives, elles ne donnent un résultat 
+formel que lorsqu'elles fournissent un contre-exemple. Lorsqu'elles exhibent une convergence,  
+cela ne permet que donner une intuition de convergence, pas  une preuve.
+Autant que nous sachions, aucune démarche de preuve formelle automatique 
+de convergence n'a jamais été établie. 
+Dans le travail théorique~\cite{Cha06}, Chandrasekaran a montré que les itérations asynchrones sont convergentes 
+si et seulement si on peut construire une fonction de Lyaponov décroissante, mais il ne donne pas de méthode 
+automatique pour construire cette fonction.
+
+Un outil qui construirait automatiquement toutes 
+les transitons serait le bienvenu. 
+Pour peu qu'on établisse la preuve de correction et de complétude de la 
+démarche, la convergence du réseau discret ne repose alors que sur le verdict 
+donné par l'outil. 
+Cependant, même pour des réseaux discrets à peu d'éléments, 
+le nombre de configurations induites explose rapidement.
+Les \emph{Model-Checkers}~\cite{Hol03,nusmv02,Blast07,MCErlang07,Bogor03}  
+sont des classes d'outils qui addressent le problème de vérifier automatiquement
+qu'un modèle vérifie une propriété donnée. Pour traiter le problème d'explosion 
+combinatoire, ces outils appliquent des méthodes d'ordre partiel, d'abstraction,
+de quotientage selon une relation d'équivalence.
+
+Ce chapitre montre comment nous simulons 
+des réseaux discrets selon toutes les sortes d'itérations pour établir 
+formellement leur convergence (ou pas).
+Nous débutons par un exemple et faisons quelques rappels sur 
+le langage PROMELA qui est le langage du model-checker 
+SPIN~\cite{Hol03} (\Sec{sec:spin:promela}).
+Nous présentons ensuite la démarche de traduction 
+de réseaux discrets dans PROMELA (\Sec{sec:spin:translation}).   
+Les théorèmes de correction et de complétude de la démarche
+sont ensuite donnés à la (\Sec{sec:spin:proof}). 
+Des données pratiques comme la complexité et des synthèses d'expérimentation
+sont ensuite fournies (\Sec{sec:spin:practical}). 
+
+
+
+
+
+
+
+%\section{Exemple jouet}
+
+

 \begin{figure}[ht]
 \begin{figure}[ht]

-  \centering
-  \begin{minipage}%[h]
-    {.6\linewidth}
-    \begin{center}
+  \begin{center}
+    \subfigure[Fonction à itérer]{

       $ F(x)= \left \{
         \begin{array}{rcl}
           f_1(x_1,x_2,x_3) & = & x_1.\overline{x_2} + x_3  \\
       $ F(x)= \left \{
         \begin{array}{rcl}
           f_1(x_1,x_2,x_3) & = & x_1.\overline{x_2} + x_3  \\


@@ -24,31 +64,39 @@
         \end{array}
       \right.
       $        
         \end{array}
       \right.
       $        

-    \end{center}
-    \caption{Fonction à itérer}    \label{fig:map}
-  \end{minipage}
-  \begin{minipage}%[h]
-    {.35\linewidth}
-    \begin{center}
+      \label{fig:map}
+    }
+    \hfill
+    \subfigure[Graphe d'intéraction]{

       \includegraphics[width=4cm]{images/xplCnxMc.eps}
       \includegraphics[width=4cm]{images/xplCnxMc.eps}

-    \end{center}
-    \caption{Graphe d'intéraction}
-    \label{fig:xplgraph}
-    \end{minipage}
+      \label{fig:xplgraph}
+    }
+  \end{center}

   \caption{Exemple pour SDD $\approx$ SPIN.}
 \end{figure}
 
 
 
   \caption{Exemple pour SDD $\approx$ SPIN.}
 \end{figure}
 
 
 

+\begin{xpl}
+  On considère un exemple à trois éléments dans $\Bool$. 
+  Chaque configuration est ainsi un élement de $\Bool^3$, \textit{i.e.}, 
+  un nombre entre 0 et 7. 
+  La \Fig{fig:map} précise la fonction $f$ considérée et 
+  la \Fig{fig:xplgraph} donne son graphe d'intéraction.
+  
+
+
+

 
 
 
 
 
 

-On peut facilement vérifier que toutes les itérations parallèles initialisées 
+On peut facilement vérifier que toutes les itérations synchrones initialisées 

 avec $x^0 \neq 7$ soit $(111)$ 
 convergent vers $2$ soit $(010)$; celles initialisées avec 
 $x^0=7$ restent en 7.
 avec $x^0 \neq 7$ soit $(111)$ 
 convergent vers $2$ soit $(010)$; celles initialisées avec 
 $x^0=7$ restent en 7.

-Pour les autres modes synchrones avec  une 
-stratégie pseudo périodique, les comportements selon la configuration initiale:
+Pour les  mode unaires ou généralisés  avec  une 
+stratégie pseudo périodique, on a des comportements qui dépendent 
+de la configuration initiale:

 \begin{itemize}
 \item initialisée avec 7, les itérations restent en 7;
 \item initialisée avec 0, 2, 4 ou 6 les itérations convergent vers 2;
 \begin{itemize}
 \item initialisée avec 7, les itérations restent en 7;
 \item initialisée avec 0, 2, 4 ou 6 les itérations convergent vers 2;


@@ -92,47 +140,50 @@ chan sync_mutex=[1] of {bool};
 \end{figure}
 
 
 \end{figure}
 
 

-Les types primaires de PROMELA sont \texttt{bool}, \texttt{byte},
-\texttt{short} et  \texttt{int}. Comme dans le langage C par exemple,
-on peut déclarer des tableaux à une dimension de taille constante 
+% Les types primaires de PROMELA sont \texttt{bool}, \texttt{byte},
+% \texttt{short} et  \texttt{int}.
+Comme en C,
+on peut déclarer des tableaux à une dimension 

 ou des nouveaux types de données (introduites par le mot clef 
 ou des nouveaux types de données (introduites par le mot clef 

-\verb+typedef+). Ces derniers sont utilisés pour définir des tableaux à deux
-dimensions.
+\verb+typedef+). % Ces derniers sont utilisés
+% pour définir des tableaux à deux
+% dimensions.

 
 \begin{xpl}
 Le programme donné à la {\sc Figure}~\ref{fig:arrayofchannels} correspond à des 
 
 \begin{xpl}
 Le programme donné à la {\sc Figure}~\ref{fig:arrayofchannels} correspond à des 

-déclarations de variables qui serviront dans l'exemple jouet de ce chapitre. 
-Il définit tout d'abord:
+déclarations de variables qui servent dans l'exemple de ce chapitre. 
+Il définit:

 \begin{itemize}
 \item les constantes \verb+N+ et \verb+d_0+ qui précisent respectivement le nombre
  $n$ d'éléments et le délais maximum $\delta_0$;
 \item les deux tableaux  (\verb+X+ et \verb+Xp+) de \verb+N+ variables booléennes; 
 les cellules \verb+X[i]+ et \verb+Xp[i]+ sont associées à la variables $x_{i+1}$
 \begin{itemize}
 \item les constantes \verb+N+ et \verb+d_0+ qui précisent respectivement le nombre
  $n$ d'éléments et le délais maximum $\delta_0$;
 \item les deux tableaux  (\verb+X+ et \verb+Xp+) de \verb+N+ variables booléennes; 
 les cellules \verb+X[i]+ et \verb+Xp[i]+ sont associées à la variables $x_{i+1}$

-d'un système dynamique discret 
-(le décalages d'un entier est dû à l'indexation à partir de zéro des cellules d'un tableau);
-Elles  mémorisent les  valeurs de $X_{i+1}$ respectivement avant et après sa mise à jour; 
+d'un système dynamique discret;
+elles  mémorisent les  valeurs de $X_{i+1}$ respectivement avant et après sa mise à jour; 

 il suffit ainsi de comparer  \verb+X+ et \verb+Xp+ pour constater si $x$ à changé ou pas;
 \item le tableau \verb+mods+ contient les éléments qui doivent être modifiés lors de l'itération 
 en cours; cela correspond naturellement à l'ensemble des éléments $s^t$;
 \item le type de données structurées \verb+vals+ et le tableau de tableaux 
  \verb+Xd[+$i$\verb+].v[+$j$\verb+]+ qui vise à mémoriser $x_{j+1}^{D^{t-1}_{i+1j+1}}$
 il suffit ainsi de comparer  \verb+X+ et \verb+Xp+ pour constater si $x$ à changé ou pas;
 \item le tableau \verb+mods+ contient les éléments qui doivent être modifiés lors de l'itération 
 en cours; cela correspond naturellement à l'ensemble des éléments $s^t$;
 \item le type de données structurées \verb+vals+ et le tableau de tableaux 
  \verb+Xd[+$i$\verb+].v[+$j$\verb+]+ qui vise à mémoriser $x_{j+1}^{D^{t-1}_{i+1j+1}}$

- pour l'itération au temps $t$ (en d'autres termes, utile lors du calcul de $x^{t}$).
+ pour l'itération au temps $t$. 
+%(en d'autres termes, utile lors du calcul de $x^{t}$).

 \end{itemize}
 
 
 \end{itemize}
 
 

-Puisque le décalage d'un indices ne change pas fondamentalement 
-le comportement de la version PROMELA par rapport au modèle initial
-et pour des raisons de clarté, on utilisera par la suite la même 
-lettre d'indice entre les deux niveaux (pour le modèle: $x_i$ et pour  PROMELA: 
-\texttt{X[i]}). Cependant, ce décalage devra être conservé mémoire.
+% Puisque le décalage d'un indices ne change pas fondamentalement 
+% le comportement de la version PROMELA par rapport au modèle initial
+% et pour des raisons de clarté, on utilisera par la suite la même 
+% lettre d'indice entre les deux niveaux (pour le modèle: $x_i$ et pour  PROMELA: 
+% \texttt{X[i]}). Cependant, ce décalage devra être conservé mémoire.

 
 

-Une donnée de type \texttt{channel} permet le 
+Déclarée avec le mot clef \verb+chan+, 
+une donnée de type \texttt{channel} permet le 

 transfert de messages entre processus dans un ordre FIFO.
 transfert de messages entre processus dans un ordre FIFO.

-Elles serait déclarée avec le mot clef \verb+chan+ suivi par sa capacité 
-(qui est constante), son nom et le type des messages qui sont stockés dans ce canal.
+% Elles serait  suivi par sa capacité 
+% (qui est constante), son nom et le type des messages qui sont stockés dans ce canal.

 Dans l'exemple précédent, on déclare successivement:
 \begin{itemize}
 Dans l'exemple précédent, on déclare successivement:
 \begin{itemize}

-\item un canal \verb+sent+ qui vise à mémoriser\verb+d_0+ messages de type
+\item un canal \verb+sent+ qui vise à mémoriser \verb+d_0+ messages de type

  \verb+bool+; le tableau nommé \verb+channels+ de \verb+N+*\verb+N+
  éléments de type \verb+a_send+ est utilisé pour mémoriser les valeurs intermédiaires $x_j$;
  Il permet donc de temporiser leur emploi par d'autres elements $i$.
  \verb+bool+; le tableau nommé \verb+channels+ de \verb+N+*\verb+N+
  éléments de type \verb+a_send+ est utilisé pour mémoriser les valeurs intermédiaires $x_j$;
  Il permet donc de temporiser leur emploi par d'autres elements $i$.


@@ -143,8 +194,8 @@ chacun un message booléen et utilisé ensuite comme des sémaphores.
 
 %\subsection{PROMELA Processes} 
 Le langage PROMELA exploite la notion de \emph{process} pour modéliser la concurrence
 
 %\subsection{PROMELA Processes} 
 Le langage PROMELA exploite la notion de \emph{process} pour modéliser la concurrence

-au sein de systèmes. Un process est déclaré avec le mot-clé
-\verb+proctype+  et est  instancié soit immédiatement (lorsque sa déclaration est préfixée 
+au sein de systèmes. Un process est  instancié soit immédiatement
+(lorsque sa déclaration est préfixée 

  par le mot-clef  \verb+active+) ou bien au moment de l'exécution de l'instruction 
 \texttt{run}.
 Parmi tous les process,  \verb+init+ est le process  initial qui permet 
  par le mot-clef  \verb+active+) ou bien au moment de l'exécution de l'instruction 
 \texttt{run}.
 Parmi tous les process,  \verb+init+ est le process  initial qui permet 


@@ -304,7 +355,7 @@ suivi par des mises à jour: ceci est réalisé grâce à la modification de la
 La mise à jour de l'ensemble  $s^t=\{s_1,\ldots, s_m\}$  des éléments qui constituent la stratégie
 $(s^t)^{t \in \Nats}$ est implantée à l'aide du process  \verb+update_elems+ fourni à la 
 {\sc Figure}~\ref{fig:proc}.  
 La mise à jour de l'ensemble  $s^t=\{s_1,\ldots, s_m\}$  des éléments qui constituent la stratégie
 $(s^t)^{t \in \Nats}$ est implantée à l'aide du process  \verb+update_elems+ fourni à la 
 {\sc Figure}~\ref{fig:proc}.  

-Ce process actif attend jusqu'à ce qu'il soit débloqué par le process
+Ce processus actif attend jusqu'à ce qu'il soit débloqué par le process

 \verb+scheduler+  à l'aide du sémaphore \verb+unlock_elements_update+.
 L'implantation se déroule en cinq étapes:
 
 \verb+scheduler+  à l'aide du sémaphore \verb+unlock_elements_update+.
 L'implantation se déroule en cinq étapes:
 


@@ -514,7 +565,7 @@ n'y a pas d'arc de $j$ à $i$ dans le graphe d'incidence;
 
 L'introduction de l'indéterminisme  à la fois dans les fonctions \verb+fetch_values+ 
 et \verb+diffuse_values+ est nécessaire dans notre contexte. Si celui-ci n'était 
 
 L'introduction de l'indéterminisme  à la fois dans les fonctions \verb+fetch_values+ 
 et \verb+diffuse_values+ est nécessaire dans notre contexte. Si celui-ci n'était 

-présent que dans la fonction \verb+fetch_values+, nous ne pourrions pas par exemple récupérer *
+présent que dans la fonction \verb+fetch_values+, nous ne pourrions pas par exemple récupérer 

 la valeur $x_i^{(t)}$ sans considérer la valeur $x_i^{(t-1)}$.  
 De manière duale, si le  non déterminisme  était uniquement
 utilisé dans la fonction \verb+diffuse_values+, alors chaque fois qu'une valeur serait 
 la valeur $x_i^{(t)}$ sans considérer la valeur $x_i^{(t-1)}$.  
 De manière duale, si le  non déterminisme  était uniquement
 utilisé dans la fonction \verb+diffuse_values+, alors chaque fois qu'une valeur serait 


@@ -620,11 +671,11 @@ puis présente ensuite les expérimentations issues de ce travail.
   Le nombre de configurations est donc borné par $2^{m(\delta_0+1)+n(n+2)}$.
   On remarque que cette borne est traitable par SPIN pour des valeurs raisonnables de  $n$, 
   $m$ et $\delta_0$.
   Le nombre de configurations est donc borné par $2^{m(\delta_0+1)+n(n+2)}$.
   On remarque que cette borne est traitable par SPIN pour des valeurs raisonnables de  $n$, 
   $m$ et $\delta_0$.

-  \JFC{Donner un ordre de grandeur de cet ordre de grandeur}
+  %\JFC{Donner un ordre de grandeur de cet ordre de grandeur}

   
 \end{Proof}
 
   
 \end{Proof}
 

-La méthode détaillée ici a pu être appliquée sur l'exemple jouet
+La méthode détaillée ici a pu être appliquée sur l'exemple

 pour prouver formellement sa convergence universelle.
 
 On peut remarquer que SPIN n'impose l'équité faible qu'entre les process
 pour prouver formellement sa convergence universelle.
 
 On peut remarquer que SPIN n'impose l'équité faible qu'entre les process


@@ -645,7 +696,7 @@ Cependant en raison de l'explosion de la taille du produit entre
 l'automate de Büchi issu de cette formule et celui issu du programme  PROMELA,
 SPIN n'arrive pas à vérifier si la convergence universelle est établie 
 ou non sur des exemples 
 l'automate de Büchi issu de cette formule et celui issu du programme  PROMELA,
 SPIN n'arrive pas à vérifier si la convergence universelle est établie 
 ou non sur des exemples 

-simples\JFC{faire référence à un tel exemple}. 
+simples.%\JFC{faire référence à un tel exemple}. 

 
 Ce problème a été pratiquement résolu en laissant SPIN 
 générer toutes les traces d'exécution,
 
 Ce problème a été pratiquement résolu en laissant SPIN 
 générer toutes les traces d'exécution,


@@ -669,7 +720,8 @@ Dans le cas contraire on doit analyser le contre exemple produit par SPIN.
 
 
 La méthode détaillée ici a été appliquée sur des exemples pour prouver formellement 
 
 
 La méthode détaillée ici a été appliquée sur des exemples pour prouver formellement 

-leur convergence ou leur divergence (\Fig{fig:async:exp}).
+leur convergence ou leur divergence (\Fig{fig:exp:promela}) 
+avec ou sans délais.

 Dans ces expériences, les délais ont été bornés par $\delta_0=10$.
 Dans ce tableau,  $P$ est vrai ($\top$) si et seulement si la convergence 
 universelle 
 Dans ces expériences, les délais ont été bornés par $\delta_0=10$.
 Dans ce tableau,  $P$ est vrai ($\top$) si et seulement si la convergence 
 universelle 


@@ -679,95 +731,93 @@ $T$ est le temps d'exécution sur un  Intel Centrino Dual Core 2 Duo @1.8GHz ave
 pour établir un verdict.
 
 
 pour établir un verdict.
 
 

-\begin{figure}
-\begin{center}
-\begin{tiny}
-\begin{tabular}{|*{7}{c|}}
-\cline{2-7}
-\multicolumn{1}{c|}{ }
-&\multicolumn{3}{|c|}{Parallèles} & \multicolumn{3}{|c|}{Chaotiques} \\
-\cline{2-7}
-\multicolumn{1}{c|}{ }& 
-P & M & T&
-P & M & T \\
-\hline %\cline{2-7}
-\textit{RE}  &
-$\top$ & 2.7 & 0.01s & 
-$\bot$ & 369.371 & 0.509s \\ 
-\hline %\cline{2-7}
-\cite{RC07} &
-$\bot$ & 2.5 & 0.001s & % RC07_sync.spin
-$\bot$ & 2.5 & 0.01s \\ % RC07_sync_chao_all.spin
-\hline
-\cite{BM99} &
-$\top$ & 36.7 & 12s & % BM99_sync_para.spin
-$\top$ &  &  \\ % BM99_sync_chao.spin
-\hline
-\end{tabular}
-\end{tiny}
-\end{center}
-\caption{Expérimentations avec des itérations synchrones}\label{fig:sync:exp}
-\end{figure} 
-
-
-
-\begin{figure}
-\begin{center}
-\tiny
-\begin{tabular}{|*{13}{c|}}
-\cline{2-13}
-\multicolumn{1}{c|}{ }
-&\multicolumn{6}{|c|}{Mixed Mode} & \multicolumn{6}{|c|}{Only Bounded} \\
-\cline{2-13}
-\multicolumn{1}{c|}{ }
-&\multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} &
-\multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} \\
-\cline{2-13}
-\multicolumn{1}{c|}{ }
-&P & M & T &
-P & M & T &
-P & M & T&
-P & M & T \\
-\hline %cline{2-13}
-\textit{RE} & 
-$\top$ & 409 & 1m11s&
-$\bot$ & 370 & 0.54 &
-$\bot$ & 374 & 7.7s&
-$\bot$ & 370 & 0.51s \\
-\hline %\cline{2-13}
-AC2D 
-&$\bot$ & 2.5 & 0.001s  % RC07_async_mixed.spin
-&$\bot$ & 2.5 & 0.01s   % RC07_async_mixed_all.spin
-&$\bot$ & 2.5 & 0.01s   % RC07_async.spin
-&$\bot$ & 2.5 & 0.01s  \\ % RC07_async_all.spin 
-\hline %\cline{2-13}
-\cite{BM99}
-&$\top$ &  &   %BM99_mixed_para.spin 
-&$\top$ &  &    % RC07_async_mixed_all.spin
-&$\bot$ &  &    % RC07_async.spin
-&$\bot$ &  &   \\ % RC07_async_all.spin 
-\hline %\cline{2-13}
-\end{tabular}
-\end{center}
-\caption{Expérimentations avec des itérations asynchrones}\label{fig:async:exp}
+\begin{figure}[ht]
+  \begin{center}
+    \begin{tiny}
+      \subfigure[Sans délais]{
+        \begin{tabular}{|*{7}{c|}}
+          \cline{2-7}
+          \multicolumn{1}{c|}{ }
+          &\multicolumn{3}{|c|}{Synchrones} & \multicolumn{3}{|c|}{Généralisées} \\
+          \cline{2-7}
+          \multicolumn{1}{c|}{ }& 
+          P & M & T&
+          P & M & T \\
+          \hline %\cline{2-7}
+          \textit{RE}  &
+          $\top$ & 2.7 & 0.01s & 
+          $\bot$ & 369.371 & 0.509s \\ 
+          \hline %\cline{2-7}
+          \cite{RC07} &
+          $\bot$ & 2.5 & 0.001s & % RC07_sync.spin
+          $\bot$ & 2.5 & 0.01s \\ % RC07_sync_chao_all.spin
+          \hline
+          \cite{BM99} &
+          $\top$ & 36.7 & 12s & % BM99_sync_para.spin
+          $\top$ &  &  \\ % BM99_sync_chao.spin
+          \hline
+        \end{tabular}
+        \label{fig:sync:exp}  
+      }
+    
+      \subfigure[Avec délais]{
+        \begin{tabular}{|*{13}{c|}}
+          \cline{2-13}
+          \multicolumn{1}{c|}{ }
+          &\multicolumn{6}{|c|}{Mode Mixe} & \multicolumn{6}{|c|}{Seulement borné} \\
+          \cline{2-13}
+          \multicolumn{1}{c|}{ }
+          &\multicolumn{3}{|c|}{Synchrones} & \multicolumn{3}{|c|}{Pseudo-Périodique} &
+          \multicolumn{3}{|c|} {Synchrones} & \multicolumn{3}{|c|}{Pseudo-Périodique} \\
+          \cline{2-13}
+          \multicolumn{1}{c|}{ }
+          &P & M & T &
+          P & M & T &
+          P & M & T&
+          P & M & T \\
+          \hline %cline{2-13}
+          \textit{RE} & 
+          $\top$ & 409 & 1m11s&
+          $\bot$ & 370 & 0.54 &
+          $\bot$ & 374 & 7.7s&
+          $\bot$ & 370 & 0.51s \\
+          \hline %\cline{2-13}
+          AC2D 
+          &$\bot$ & 2.5 & 0.001s  % RC07_async_mixed.spin
+          &$\bot$ & 2.5 & 0.01s   % RC07_async_mixed_all.spin
+          &$\bot$ & 2.5 & 0.01s   % RC07_async.spin
+          &$\bot$ & 2.5 & 0.01s  \\ % RC07_async_all.spin 
+          \hline %\cline{2-13}
+          \cite{BM99}
+          &$\top$ &  &   %BM99_mixed_para.spin 
+          &$\top$ &  &    % RC07_async_mixed_all.spin
+          &$\bot$ &  &    % RC07_async.spin
+          &$\bot$ &  &   \\ % RC07_async_all.spin 
+          \hline %\cline{2-13}
+        \end{tabular}
+        \label{fig:async:exp}
+      }
+    \end{tiny}
+  \end{center}
+  \caption{Résultats des simulations Promela des SDDs}\label{fig:exp:promela}

 \end{figure} 
 
 
 
 \end{figure} 
 
 
 

-L'exemple \textit{RE} est l'exemple jouet de ce chapitre,
+L'exemple \textit{RE} est l'exemple de ce chapitre,

 \cite{RC07} concerne un réseau composé de deux gènes
 à valeur dans $\{0,1,2\}$,
 AC2D est un automate cellulaire  avec 9 elements prenant des
 valeurs booléennes en fonction de 
 de 4 voisins et
 \cite{BM99} consiste en  10 process
 \cite{RC07} concerne un réseau composé de deux gènes
 à valeur dans $\{0,1,2\}$,
 AC2D est un automate cellulaire  avec 9 elements prenant des
 valeurs booléennes en fonction de 
 de 4 voisins et
 \cite{BM99} consiste en  10 process

-qui modifient leur valeur booléennes dans un graphe d'adjacence proche 
+qui modifient leurs valeurs booléennes dans un graphe d'adjacence proche 

 du graphe complet.
 
 
 du graphe complet.
 
 

-L'exemple jouet \textit{RE} a été prouvé comme universellement convergent.
+L'exemple  \textit{RE} a été prouvé comme universellement convergent.

 \JFC{statuer sur AC2D}
 \JFC{statuer sur AC2D}

-Comme la convergence n'est déjà pas établie pour les itérations parallèles
+Comme la convergence n'est déjà pas établie pour les itérations synchrones

 de~\cite{RC07}, il en est donc 
 de même pour les itérations asynchrones.
 La {\sc Figure}~\ref{fig:RC07CE} donne une trace de la sortie de SPIN de menant à la violation 
 de~\cite{RC07}, il en est donc 
 de même pour les itérations asynchrones.
 La {\sc Figure}~\ref{fig:RC07CE} donne une trace de la sortie de SPIN de menant à la violation 


@@ -817,28 +867,7 @@ lorsque pour $\delta_0$ vaut 1. Il ne peut donc y avoir convergence universelle.
  
 \section{Conclusion}
 \label{sec:spin:concl}
  
 \section{Conclusion}
 \label{sec:spin:concl}

-Des méthodes de simulation basées sur des stratégies et des délais générés aléatoirement 
-ont déjà été présentées~\cite{BM99,BCV02}.
-Cependant, comme ces implantations ne sont pas exhaustives, elles ne donnent un résultat 
-formel que lorsqu'elles fournissent un contre-exemple. Lorsqu'elles exhibent une convergence,  
-cela ne permet que donner une intuition de convergence, pas  une preuve.
-Autant que nous sachions, aucune démarche de preuve formelle automatique 
-de convergence n'a jamais été établie. 
-Dans le travail théorique~\cite{Cha06}, Chandrasekaran a montré que les itérations asynchrones sont convergentes 
-si et seulement si on peut construire une fonction de Lyaponov décroissante, mais il ne donne pas de méthode 
-automatique pour construire cette fonction.

 
 

-\JFC{Déplacer ceci dans les perspective}
-Among drawbacks of the method,  one can argue that bounded delays is only 
-realistic in practice for close systems. 
-However, in real large scale distributed systems where bandwidth is weak, 
-this restriction is too strong. In that case, one should only consider that 
-matrix $s^{t}$ follows the  iterations of the system, \textit{i.e.},
-for all $i$, $j$, $1 \le i \le j \le n$,  we have$
-\lim\limits_{t \to \infty} s_{ij}^t = + \infty$. 
-One challenge of this work should consist in weakening this constraint. 
-We plan as future work to take into account other automatic approaches 
-to discharge proofs notably by deductive analysis~\cite{CGK05}.