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
-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
-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}.
+
+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}
+
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
-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
\[
-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
-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}
-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
-$\mathcal{X} =
+$\mathcal{X}_u =
\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
\[
-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
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
-$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\{
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$,
-$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
-\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
-\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
-\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}.
-\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}
\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}
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}
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
\[
- 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.}
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}
- 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
\[
- 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
- 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)$
-
-%%%%%%%%%%%%%%%%%%%%
-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}$
-\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.
\]
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
-$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\{
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}.
-\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}
\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}
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
-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}}$.
\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
-$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
-$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
-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
-$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_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
\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}
-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
-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}.
-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.
-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;
-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
-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, 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},
-$\Gamma(f)^0$ et $\Gamma(f)^1$ sont fortement
+$\textsc{giu}(f)^0$ et $\textsc{giu}(f)^1$ sont fortement
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{$*$}
-\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}
-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
-$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.
-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,
-$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,
-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.}
-$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}
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}
-$\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 à
-$\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
-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
-$(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
-$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$.
-Par conséquent, $G_f$ est transitive.
+Par conséquent, $G_{f_g}$ est transitive.
$\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
-$\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$.
-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'$,
-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''')$ 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'$,
-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
-$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}
\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}$).
-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
-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
-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'$.
(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}
\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}
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}
\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 à
-$\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
-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
-$(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
-$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$.
-Par conséquent, $G_f$ est transitive.
+Par conséquent, $G_{f_u}$ est transitive.
$\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
-$\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$.
-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'$,
-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''')$ 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'$,
-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
-$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}
\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}$).
-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
-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
-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'$.
(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}
\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}
-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}
-
-
-\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]
- 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$.
- 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}
-
-
\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}
-
-
-
-
-
-
-
-
-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]
-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$.
-
-La constante $\delta$ est appelée \emph{constante de sensibilité} de $f$.
\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}.
-
-
-
+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$.
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),
\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{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}
-
-
-\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}
-\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}
-\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}
-
-
\section{Théorème~\ref{th:Adrien}}\label{anx:sccg}
\input{annexesccg}
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}
-\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]
- \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 \\
\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}
- \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}
+\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.
-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;
\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
-\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
-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}$
-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}}$
- 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}
-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.
-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}
-\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$.
%\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
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:
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
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}
-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
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,
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
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}
-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
-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.
-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}
-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
\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}.
