From: Jean-François Couchot Date: Thu, 28 May 2015 12:51:39 +0000 (+0200) Subject: fin chap FCT11 juste la génération X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/commitdiff_plain/4e673fe23eacd3db39c4bc51610f1650c372b13c fin chap FCT11 juste la génération --- diff --git a/11FCT.tex b/11FCT.tex index 5c7747a..8ab511e 100644 --- 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 -$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} + diff --git a/12TIPE.tex b/12TIPE.tex index e735c46..4f9fa9b 100644 --- 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. - -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 @@ -57,14 +51,13 @@ $$ 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\{ @@ -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$. -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} @@ -133,8 +126,8 @@ On peut conclure que $\mathcal{C} = \mathcal{R} \cap \mathcal{T} \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} diff --git a/15TSI.tex b/15TSI.tex index 47ecd36..7d1d842 100644 --- a/15TSI.tex +++ b/15TSI.tex @@ -1,7 +1,6 @@ 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} @@ -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 - $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.} @@ -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} - 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. @@ -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$. -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\{ @@ -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. - -\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} @@ -101,8 +99,8 @@ annexe~\ref{anx:chaos:generalise}. \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} diff --git a/annexesccg.tex b/annexesccg.tex index 3db4320..9d32b22 100644 --- a/annexesccg.tex +++ b/annexesccg.tex @@ -1,13 +1,13 @@ 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}}$. @@ -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 -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 @@ -45,80 +45,80 @@ arc de $j$ vers $i$ de signe $s$. \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=0y_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}}=0y_{\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_{\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)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 $t0$. 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'$. @@ -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 -$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 $t0$. +$\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 $t0$. 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'$. @@ -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 -$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 $t0$ 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$. diff --git a/main.pdf b/main.pdf index 8210825..23c1a19 100644 Binary files a/main.pdf and b/main.pdf differ diff --git a/main.tex b/main.tex index 27c159c..6887cec 100644 --- 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 - 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), @@ -197,7 +197,9 @@ On montre qu'on a des résultats similaires. \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} @@ -249,26 +251,22 @@ to discharge proofs notably by deductive analysis~\cite{CGK05}. \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} diff --git a/mixage.tex b/mixage.tex index a71a36d..0b24636 100644 --- 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. -\begin{figure}[ht] +\begin{figure}%[ht] \begin{center} $$ f(x)= \left \{ \begin{array}{lll} diff --git a/modelchecking.tex b/modelchecking.tex index 1b8843d..6f968bb 100644 --- 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] - \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 \\ @@ -24,31 +64,39 @@ \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; @@ -92,47 +140,50 @@ chan sync_mutex=[1] of {bool}; \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$. @@ -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 -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 @@ -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}. -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: @@ -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 -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 @@ -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$. - \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 @@ -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 -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, @@ -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 -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 @@ -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. -\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 @@ -817,28 +867,7 @@ lorsque pour $\delta_0$ vaut 1. Il ne peut donc y avoir convergence universelle. \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}.