From: Jean-François Couchot Date: Fri, 22 May 2015 08:26:03 +0000 (+0200) Subject: azerazerzer X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/commitdiff_plain/714ce29544c8cc7bf8b4530d28352fb1a5306991?ds=sidebyside;hp=-c azerazerzer Merge branch 'master' of ssh://bilbo.iut-bm.univ-fcomte.fr/hdrcouchot --- 714ce29544c8cc7bf8b4530d28352fb1a5306991 diff --combined main.tex index 0893d3b,a31f0bd..27c159c --- a/main.tex +++ b/main.tex @@@ -111,7 -111,7 +111,7 @@@ \newcommand{\Bool}[0]{\ensuremath{\mathds{B}}} \newcommand{\rel}[0]{\ensuremath{{\mathcal{R}}}} \newcommand{\Gall}[0]{\ensuremath{\mathcal{G}}} -\newcommand{\Sec}[1]{Sect\,\ref{#1}} +\newcommand{\Sec}[1]{Section\,\ref{#1}} \newcommand{\Fig}[1]{{\sc Figure}~\ref{#1}} \newcommand{\Alg}[1]{Algorithme~\ref{#1}} \newcommand{\Tab}[1]{Tableau~\ref{#1}} @@@ -139,12 -139,9 +139,12 @@@ Blabla blabla \mainmatter -\part{Système Booléens} +\part{Réseaux Discrets} -\chapter{Iterations discrètes de Systèmes Dynamiques booléens} + + +\chapter{Iterations discrètes de réseaux booléens} +\JFC{chapeau à refaire} \section{Formalisation} \input{sdd} @@@ -154,8 -151,6 +154,8 @@@ \section{Conclusion} +\JFC{Conclusion à refaire} + Introduire de l'asynchronisme peut permettre de réduire le temps d'exécution global, mais peut aussi introduire de la divergence. Dans ce chapitre, nous avons exposé comment construire un mode combinant les @@@ -165,7 -160,7 +165,7 @@@ de l'asynchronisme en terme de vitesse -\chapter[Preuve de convergence de systèmes booléens]{Preuve automatique de convergence de systèmes booléens}\label{chap:promela} +\chapter[Preuve de convergence de systèmes booléens]{Preuve automatique de convergence}\label{chap:promela} \input{modelchecking} @@@ -178,14 -173,23 +178,23 @@@ au chaos \chapter{Characterisation des systèmes discrets chaotiques} + + 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), généralisée (TSI). Pour chacune d'elle, on introduit une distance différente. On montre qu'on a des résultats similaires. + \section{Systèmes dynamiques chaotiques selon Devaney} + \label{subsec:Devaney} + \input{devaney} + + \section{Schéma unaire} \input{12TIPE} + \section{Schéma généralisé} + \input{15TSI} générer des fonctions vérifiant ceci (TIPE12 juste sur le résultat d'adrien). @@@ -202,21 -206,7 +211,21 @@@ -% \part{Conclusion et Perspectives} + + \part{Conclusion et Perspectives} + +\JFC{Perspectives pour SDD->Promela} +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}. + % \chapter{Conclusion} @@@ -244,11 -234,18 +253,18 @@@ \input{annexecontinuite.tex} + + \section{Caractérisation des fonctions $f$ rendant chaotique $G_f$ dans $(\mathcal{X},d)$}\label{anx:chaos:unaire} \input{caracunaire.tex} + \section{Preuve que $d$ est une distance sur $\mathcal{X}$}\label{anx:distance:generalise} + \input{preuveDistanceGeneralisee} + + \section{Caractérisation des fonctions $f$ rendant chaotique $G_f$ dans $(\mathcal{X},d)$}\label{anx:chaos:generalise} + \input{caracgeneralise.tex} diff --combined sdd.tex index c165102,eb51e97..2352fad --- a/sdd.tex +++ b/sdd.tex @@@ -23,32 -23,32 +23,32 @@@ de conjonction \og . \fg{} e unaire de négation \og $\overline{\mathstrut\enskip}$ \fg{}. - Soit $n$ un entier naturel. - On introduit quelques notations à propos d'éléments de $\Bool^n$. - L'ensemble $\{1,\dots, n\}$ sera par la suite noté $[n]$. + Soit ${\mathsf{N}}$ un entier naturel. + On introduit quelques notations à propos d'éléments de $\Bool^{\mathsf{N}}$. + L'ensemble $\{1,\dots, {\mathsf{N}}\}$ sera par la suite noté $[{\mathsf{N}}]$. Le $i^{\textrm{ème}}$ composant d'un élément - $x \in \Bool^n$ s'écrit $x_i$. - Si l'ensemble $I$ est une partie de $[n]$, alors - $\overline{x}^I$ est l'élément $y\in \Bool^n$ + $x \in \Bool^{\mathsf{N}}$ s'écrit $x_i$. + Si l'ensemble $I$ est une partie de $[{\mathsf{N}}]$, alors + $\overline{x}^I$ est l'élément $y\in \Bool^{\mathsf{N}}$ tel que $y_i = 1 - x_i$ si $i\in I$ et $y_i = x_i$ sinon. - On considère les deux abréviations $\overline{x}$ pour $\overline{x}^{[n]}$ + On considère les deux abréviations $\overline{x}$ pour $\overline{x}^{[{\mathsf{N}}]}$ (chaque composant de $\overline{x}$ est nié: c'est une négation composante à composante) - et $\overline{x}^i$ pour $\overline{x}^{\{i\}}$ pour $i \in [n]$ + et $\overline{x}^i$ pour $\overline{x}^{\{i\}}$ pour $i \in [{\mathsf{N}}]$ (seul $x_i$ est nié dans $\overline{x}$). - Pour tout $x$ et $y$ dans $\Bool^n$, l'ensemble - $\Delta(x, y)$, contient les $i \in [n]$ + Pour tout $x$ et $y$ dans $\Bool^{\mathsf{N}}$, l'ensemble + $\Delta(x, y)$, contient les $i \in [{\mathsf{N}}]$ tels que $x_i \neq y_i$. - Soit enfin $f : \Bool^n \rightarrow \Bool^n$. Son $i^{\textrm{ème}}$ composant - est nommé $f_i$ qui est une fonction de $\Bool^n$ dans $\Bool$. + Soit enfin $f : \Bool^n \rightarrow \Bool^{\mathsf{N}}$. Son $i^{\textrm{ème}}$ composant + est nommé $f_i$ qui est une fonction de $\Bool^{\mathsf{N}}$ dans $\Bool$. Pour chaque - $x$ dans $\Bool^n$, l'ensemble + $x$ dans $\Bool^{\mathsf{N}}$, l'ensemble $\Delta f(x)$ est défini par $\Delta f(x) = \Delta(x,f(x))$. On peut admettre que $f (x) = \overline{x}^{\Delta f(x)}$ . \begin{xpl}\label{xpl:1} - On considère $n= 3$ et $f:\Bool^3 \rightarrow \Bool^3$ telle que + On considère ${\mathsf{N}}= 3$ et $f:\Bool^3 \rightarrow \Bool^3$ telle que $f(x)=(f_1(x),f_2(x),f_3(x))$ avec $$\begin{array}{rcl} f_1(x_1, x_2, x_3) &=& (\overline{x_1} + \overline{x_2}).x_3 \textrm{, }\\ @@@ -110,58 -110,64 +110,64 @@@ d'éléments étudiés (gènes, protéi Un réseau booléen est défini à partir d'une fonction booléenne: \[ - f:\Bool^n\to\Bool^n,\qquad x=(x_1,\dots,x_n)\mapsto f(x)=(f_1(x),\dots,f_n(x)), + f:\Bool^{\mathsf{N}}\to\Bool^{\mathsf{N}},\qquad x=(x_1,\dots,x_{\mathsf{N}})\mapsto f(x)=(f_1(x),\dots,f_{\mathsf{N}}(x)), \] - et un {\emph{schéma itératif}} ou encore \emph{mode de mise à jour}. À partir d'une configuration initiale $x^0\in\Bool^n$, la suite $(x^{t})^{t + et un {\emph{schéma itératif}} ou encore \emph{mode de mise à jour}. À partir d'une configuration initiale $x^0\in\Bool^{\mathsf{N}}$, la suite $(x^{t})^{t \in \Nats}$ des configurations du système est construite selon l'un des schémas suivants : \begin{itemize} \item \textbf{Schéma parallèle synchrone :} basé sur la relation de récurrence - $x^{t+1}=f(x^t)$. Tous les $x_i$, $1 \le i \le n$, sont ainsi mis à jour à + $x^{t+1}=f(x^t)$. Tous les $x_i$, $1 \le i \le {\mathsf{N}}$, sont ainsi mis à jour à chaque itération en utilisant l'état global précédent du système $x^t$. \item \textbf{Schéma unaire :} ce schéma est parfois qualifié de chaotique dans la littérature. Il consiste à modifier la valeur - d'un unique élément $i$, $1 \le i \le n$, à + d'un unique élément $i$, $1 \le i \le {\mathsf{N}}$, à chaque itération. Le choix de l'élément qui est modifié à chaque itération est défini par une suite $S = \left(s^t\right)^{t \in \mathds{N}}$ qui est une séquence - d'indices dans $[n]$. Cette suite est appelée \emph{stratégie unaire}. - Il est basé sur la relation définie pour tout $i \in [n]$ par - $$ + d'indices dans $[{\mathsf{N}}]$. Cette suite est appelée \emph{stratégie unaire}. + Il est basé sur la relation définie pour tout $i \in [{\mathsf{N}}]$ par + + \begin{equation} x^{t+1}_i= \left\{ \begin{array}{l} f_i(x^t) \textrm{ si } i=s^t, \\ x^t_i\textrm{ sinon.} \end{array} - \right.$$ + \right. + \label{eq:schema:unaire} + \end{equation} \item \textbf{Schéma généralisé:} dans ce schéma, ce sont les valeurs - d'un ensemble d'éléments de $[n]$ qui sont modifiées à chaque itération. + d'un ensemble d'éléments de $[{\mathsf{N}}]$ qui sont modifiées à chaque itération. Dans le cas particulier où c'est la valeur d'un singleton - $\{k\}$, $1 \le k \le n$, qui est modifiée à + $\{k\}$, $1 \le k \le {\mathsf{N}}$, qui est modifiée à chaque itération, on retrouve le mode unaire. Dans le second cas particulier où ce sont les valeurs de - tous les éléments de $\{1, \ldots, n\}$ qui sont modifiées + tous les éléments de $\{1, \ldots, {\mathsf{N}}\}$ qui sont modifiées à chaque itération, on retrouve le mode parallèle. Ce mode généralise donc les deux modes précédents. Plus formellement, à la $t^{\textrm{ème}}$ itération, seuls les éléments de la partie - $s^{t} \in \mathcal{P}([n])$ sont mis à + $s^{t} \in \mathcal{P}([{\mathsf{N}}])$ sont mis à jour. La suite $S = \left(s^t\right)^{t \in \mathds{N}}$ est une séquence de sous-ensembles - de $[n]$ appelée \emph{stratégie généralisée}. - Il est basé sur la relation définie pour tout $i \in [n]$ par - $$ + de $[{\mathsf{N}}]$ appelée \emph{stratégie généralisée}. + Il est basé sur la relation définie pour tout $i \in [{\mathsf{N}}]$ par + \begin{equation} x^{t+1}_i= \left\{ \begin{array}{l} f_i(x^t) \textrm{ si } i \in s^t, \\ x^t_i\textrm{ sinon.} \end{array} - \right.$$ + \right. + \label{eq:schema:generalise} + \end{equation} + @@@ -176,22 -182,22 +182,22 @@@ La section suivante détaille comment r - Pour un entier naturel $n$ et une - fonction $f : B^n \rightarrow B^n$, plusieurs évolutions sont possibles + Pour un entier naturel ${\mathsf{N}}$ et une + fonction $f : B^{\mathsf{N}} \rightarrow B^{\mathsf{N}}$, plusieurs évolutions sont possibles en fonction du schéma itératif retenu. Celles-ci sont représentées par un graphe orienté dont les noeuds - sont les éléments de $\Bool^n$ (voir \textsc{Figure}~\ref{fig:xpl:graphs}). + sont les éléments de $\Bool^{\mathsf{N}}$ (voir \textsc{Figure}~\ref{fig:xpl:graphs}). \begin{itemize} \item Le \emph{graphe des itérations synchrones} de $f$, noté $\textsc{gis}(f)$ - est le graphe orienté de $\Bool^n$ qui contient un arc $x \rightarrow y$ si + est le graphe orienté de $\Bool^{\mathsf{N}}$ qui contient un arc $x \rightarrow y$ si et seulement si $y=f(x)$. \item Le \emph{graphe des itérations unaires} de $f$, noté $\textsc{giu}(f)$ - est le graphe orienté de $\Bool^n$ qui contient un arc $x \rightarrow y$ si + est le graphe orienté de $\Bool^{\mathsf{N}}$ qui contient un arc $x \rightarrow y$ si et seulement s'il existe $x \in \Delta f(x)$ tel que $y = \overline{x}^i$. \item Le \emph{graphe des itérations généralisées} de $f$, noté $\textsc{gig}(f)$ - est le graphe orienté de $\Bool^n$ qui contient un arc $x \rightarrow y$ si + est le graphe orienté de $\Bool^{\mathsf{N}}$ qui contient un arc $x \rightarrow y$ si et seulement s'il existe un ensemble $I\subseteq \Delta f(x)$ tel que $y = \overline{x}^I$. On peut remarquer que ce graphe contient comme sous-graphe à la fois celui des itérations synchrones et celui @@@ -209,7 -215,7 +215,7 @@@ d'images (\textsc{Table}~\ref{table:xpl La \textsc{Figure}~\ref{fig:xpl:graphs} donne les trois graphes d'itérations associés à $f$. -\begin{figure}[ht] +\begin{figure}%[ht] \begin{center} \subfigure[$\textsc{gis}(f)$]{ \begin{minipage}{0.33\textwidth} @@@ -251,7 -257,7 +257,7 @@@ On remarque le cycle $((101,111),(111,0 \subsection{Attracteurs} On dit que le point - $x \in \Bool^n$ est un \emph{point fixe} de $f$ si $x = f (x)$. + $x \in \Bool^{\mathsf{N}}$ est un \emph{point fixe} de $f$ si $x = f (x)$. Les points fixes sont particulièrement intéressants car ils correspondent aux états stables: dans chaque graphe d'itérations, le point $x$ est un point fixe @@@ -259,12 -265,12 +265,12 @@@ si et seulement si il est son seul succ - Soit $\Gamma$ un graphe d'itérations (synchrones, unaires ou généralisées) + Soit un graphe d'itérations (synchrones, unaires ou généralisées) de $f$. - Les \emph{attracteurs} de $\Gamma$ sont les + Les \emph{attracteurs} de ce graphe sont les plus petits sous-ensembles (au sens de l'inclusion) non vides - $A \subseteq \Bool^n$ tels que pour tout arc - $x \rightarrow y$ de $\Gamma$, si $x$ est un élément de $A$, alors + $A \subseteq \Bool^{\mathsf{N}}$ tels que pour tout arc + $x \rightarrow y$, si $x$ est un élément de $A$, alors $y$ aussi. Un attracteur qui contient au moins deux éléments est dit \emph{cyclique}. On en déduit qu'un attracteur cyclique ne contient pas de point fixe. @@@ -277,12 -283,12 +283,12 @@@ On a la proposition suivante \begin{theorem}\label{Prop:attracteur} Le point $x$ est un point fixe si et seulement si - $\{x\}$ est un attracteur de $\Gamma$. - En d'autres termes, les attracteurs non cycliques de $\Gamma$ + $\{x\}$ est un attracteur du graphe d'itération (synchrone, unaire, généralisé). + En d'autres termes, les attracteurs non cycliques de celui-ci sont les points fixes de $f$. - Ainsi pour chaque $x\in \Bool^n$, il existe au moins un chemin + Ainsi pour chaque $x\in \Bool^{\mathsf{N}}$, il existe au moins un chemin depuis $x$ qui atteint un attracteur. - Ainsi $\Gamma$ contient toujours au moins un attracteur. + Ainsi tout graphe d'itérations contient toujours au moins un attracteur. \end{theorem} @@@ -300,7 -306,7 +306,7 @@@ Les interactions entre les composants d système peuvent être mémorisées dans la {\emph{matrice jacobienne discrète}} $f'$. Celle-ci est définie comme étant la fonction qui à chaque - configuration $x\in\Bool^n$ associe la matrice de taille + configuration $x\in\Bool^{\mathsf{N}}$ associe la matrice de taille $n\times n$ telle que \begin{equation} f'(x)=(f'_{ij}(x)),\qquad @@@ -314,7 -320,7 +320,7 @@@ $\overline{x}^j_j$ et $x_j$ sont consid dans $\Z$. Lorsqu'on supprime les signes dans la matrice jacobienne discrète, on obtient une matrice notée $B(f)$ aussi de taille - $n\times n$. + ${\mathsf{N}}\times {\mathsf{N}}$. Celle-ci mémorise uniquement l'existence d'une dépendance de tel élément vis à vis de tel élément. @@@ -323,7 -329,7 +329,7 @@@ les uns par rapport aux autres. Cette m \emph{matrice d'incidence}. \begin{theorem} - Si $f_i$ ne dépend pas de $x_j$, alors pour tout $x\in [n]$, + Si $f_i$ ne dépend pas de $x_j$, alors pour tout $x\in [{\mathsf{N}}]$, $f_i(\overline{x}^j)$ est égal à $f_i(x)$, \textit{i.e}, $f'_{ij}(x)=0$. Ainsi $B(f)_{ij}$ est nulle. La réciproque est aussi vraie. \end{theorem} @@@ -333,10 -339,10 +339,10 @@@ En outre, les interactions peuvent se représenter à l'aide d'un graphe $\Gamma(f)$ orienté et signé défini ainsi: - l'ensemble des sommets est - $[n]$ et il existe un arc de $j$ à $i$ de signe + l'ensemble des sommet %s est + $[{\mathsf{N}}]$ et il existe un arc de $j$ à $i$ de signe $s\in\{-1,1\}$, noté $(j,s,i)$, si $f_{ij}(x)=s$ pour au moins - un $x\in\Bool^n$. + un $x\in\Bool^{\mathsf{N}}$. On note que la présence de deux arcs de signes opposés entre deux sommets donnés @@@ -414,7 -420,7 +420,7 @@@ $x_1$ et de $x_3 Ainsi la seconde ligne (resp. la troisième ligne) de $B(f)$ est $1~0~1$ (resp. est $1~1~1$). La \textsc{Figure}~(\ref{fig:f:incidence}) donne la matrice d'incidence complète. -\begin{figure}[ht] +\begin{figure}%[ht] \begin{center} \subfigure[Matrice jacobienne]{ \begin{minipage}{0.90\textwidth} @@@ -515,28 -521,28 +521,28 @@@ arc positif (resp. un arc négatif) de \subsection{Conditions de convergence}\label{sec:Robert:async} Parmi les itérations unaires caractérisées par leurs stratégies - $S=(s^t)^{t \in \Nats}$ d'éléments appartenant à $[n]$, + $S=(s^t)^{t \in \Nats}$ d'éléments appartenant à $[{\mathsf{N}}]$, sont jugées intéressantes celles qui activent au moins une fois - chacun des $i\in[n]$. Dans le cas contraire, un élément n'est jamais modifié. + chacun des $i\in[{\mathsf{N}}]$. Dans le cas contraire, un élément n'est jamais modifié. Plus formellement, une séquence finie $S=(s^t)^{t \in \Nats}$ - est dite \emph{complète} relativement à $[n]$ si - tout indice de $[n]$ + est dite \emph{complète} relativement à $[{\mathsf{N}}]$ si + tout indice de $[{\mathsf{N}}]$ s'y retrouve au moins une fois. Parmi toutes les stratégies unaires de - $[n]^{\Nats}$, on qualifie de: + $[{\mathsf{N}}]^{\Nats}$, on qualifie de: \begin{itemize} \item \emph{périodiques} celles qui sont constituées par une répétition indéfinie - d'une même séquence $S$ complète relativement à $[n]$. + d'une même séquence $S$ complète relativement à $[{\mathsf{N}}]$. En particulier toute séquence périodique est complète. \item \emph{pseudo-périodiques} celles qui sont constituées par une succession indéfinie de séquences (de longueur éventuellement variable non supposée bornée) complètes. Autrement dit dans chaque stratégie pseudo-périodique, chaque indice de - $1$ à $n$ revient indéfiniment. + $1$ à ${\mathsf{N}}$ revient indéfiniment. \end{itemize} @@@ -547,14 -553,14 +553,14 @@@ dans le mode des itérations unaires \begin{theorem}\label{Th:conv:GIU} Si le graphe $\Gamma(f)$ n'a pas de cycle et si la stratégie unaire est pseudo-périodique, alors tout chemin de $\textsc{giu}(f)$ atteint - l'unique point fixe $\zeta$ en au plus $n$ pseudo-périodes. + l'unique point fixe $\zeta$ en au plus ${\mathsf{N}}$ pseudo-périodes. \end{theorem} Le qualificatif \emph{pseudo-périodique} peut aisément s'étendre aux stratégies généralisées comme suit. Lorsqu'une stratégie généralisée est constituée d'une - succession indéfinie de séquences de parties de $[n]$ - dont l'union est $[n]$, cette stratégie est {pseudo-périodique}. + succession indéfinie de séquences de parties de $[{\mathsf{N}}]$ + dont l'union est $[{\mathsf{N}}]$, cette stratégie est {pseudo-périodique}. J. Bahi~\cite{Bah00} a démontré le théorème suivant: \begin{theorem}\label{Th:Bahi}