\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}}
\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}
\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
-\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}
\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).
-% \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}
\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}
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{, }\\
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}
+
- 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
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}
\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
- 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.
\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}
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
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.
\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}
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
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}
\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}
\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}
