\end{Proof}
-\begin{theorem}[Soundness wrt universal convergence property]\label{Theo:sound}
- Let $\phi$ be a DDN model and $\psi$ be its translation. If $\psi$ verifies
- the LTL property (\ref{eq:ltl:conv}) under weak fairness property, then
- iterations of $\phi$ are universally convergent.
-\end{theorem}
+\promelasound*
\begin{Proof}
% For the case where the strategy is finite, one notice that property
% verification is achieved under weak fairness property. Instructions that
% \end{Corol}
+\promelacomplete*
-\begin{theorem}[Completeness wrt universal convergence property]\label{Theo:completeness}
- Let $\phi$ be a DDN model and $\psi$ be its translation. If $\psi$ does not
- verify the LTL property (\ref{eq:ltl:conv}) under weak fairness property then
- the iterations of $\phi$ are divergent.
-\end{theorem}
\begin{Proof}
For models $\psi$ that do not verify the LTL property (\ref{eq:ltl:conv}) it
is easy to construct corresponding iterations of the DDN, whose strategy is
--- /dev/null
+digraph {
+000 [shape="none"label="000", pos="10.5,10!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+001 [shape="none"label="001", pos="11.7320508076,11!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+010 [shape="none", label="010", pos="12.5,10!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+011 [shape="none", label="011", pos="13.7320508076,11!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+100 [shape="none", label="100", pos="10.5,8!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+101 [shape="none", label="101", pos="11.7320508076,9!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+110 [shape="none", label="110", pos="12.5,8!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+111 [shape="none", label="111", pos="13.7320508076,9!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+ 000:sw -> 000:nw [arrowhead="vee"];
+ 001 -> 101 [arrowhead="vee"];
+ 001:sw -> 001:nw [arrowhead="vee"];
+ 010 -> 010 [arrowhead="vee"];
+ 010 -> 011 [arrowhead="vee"];
+ 010 -> 000 [arrowhead="vee"];
+ 011 -> 011 [arrowhead="vee"];
+ 011 -> 111 [arrowhead="vee"];
+ 011 -> 001 [arrowhead="vee"];
+ 100 -> 000 [arrowhead="vee"];
+ 100 -> 101 [arrowhead="vee"];
+ 100:sw -> 100:nw [arrowhead="vee"];
+ 101 -> 111 [arrowhead="vee"];
+ 101 -> 101:nw [arrowhead="vee"];
+ 110 -> 111 [arrowhead="vee"];
+ 110 -> 010 [arrowhead="vee"];
+ 110 -> 100 [arrowhead="vee"];
+ 111 -> 111 [arrowhead="vee"];
+ 111 -> 011 [arrowhead="vee"];
+
+}
--- /dev/null
+digraph {
+000 [shape="none"label="000", pos="10.5,10!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+001 [shape="none"label="001", pos="11.7320508076,11!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+010 [shape="none", label="010", pos="12.5,10!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+011 [shape="none", label="011", pos="13.7320508076,11!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+100 [shape="none", label="100", pos="10.5,8!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+101 [shape="none", label="101", pos="11.7320508076,9!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+110 [shape="none", label="110", pos="12.5,8!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+111 [shape="none", label="111", pos="13.7320508076,9!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+ 000:sw -> 000:nw [arrowhead="vee"];
+ 001 -> 101[arrowhead="vee"];
+ 001:sw -> 001:nw[arrowhead="vee"];
+ 010 -> 010[arrowhead="vee"];
+ 010 -> 011[arrowhead="vee"];
+ 010 -> 000[arrowhead="vee"];
+ 010 -> 001[arrowhead="vee"];
+
+ 011 -> 011[arrowhead="vee"];
+ 011 -> 001[arrowhead="vee"];
+ 011 -> 111[arrowhead="vee"];
+ 011 -> 101[arrowhead="vee"];
+ 100:sw -> 100:nw[arrowhead="vee"];
+ 100 -> 000[arrowhead="vee"];
+ 100 -> 001[arrowhead="vee"];
+ 100 -> 101[arrowhead="vee"];
+ 101 -> 101:nw[arrowhead="vee"];
+ 101 -> 111[arrowhead="vee"];
+
+ 110 -> 000[arrowhead="vee"];
+ 110 -> 110[arrowhead="vee"];
+ 110 -> 001[arrowhead="vee"];
+ 110 -> 010[arrowhead="vee"];
+ 110 -> 011[arrowhead="vee"];
+ 110 -> 100[arrowhead="vee"];
+ 110 -> 101[arrowhead="vee"];
+ 110 -> 111[arrowhead="vee"];
+
+ 111 -> 111[arrowhead="vee"];
+ 111 -> 011[arrowhead="vee"];
+
+}
--- /dev/null
+digraph {
+
+000 [shape="none"label="000", pos="10.5,10!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+001 [shape="none"label="001", pos="11.7320508076,11!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+010 [shape="none", label="010", pos="12.5,10!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+011 [shape="none", label="011", pos="13.7320508076,11!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+100 [shape="none", label="100", pos="10.5,8!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+101 [shape="none", label="101", pos="11.7320508076,9!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+110 [shape="none", label="110", pos="12.5,8!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+111 [shape="none", label="111", pos="13.7320508076,9!",fontsize=20,fixedsize=true,width=0.5,height=0.3];
+ 000:sw -> 000:nw [arrowhead="vee"];
+ 010 -> 001 [arrowhead="vee"];
+ 100 -> 001 [arrowhead="vee"];
+ 110 -> 001 [arrowhead="vee"];
+ 001 -> 101 [arrowhead="vee"];
+ 101 -> 111 [arrowhead="vee"];
+ 111 -> 011 [arrowhead="vee"];
+ 011 -> 101 [arrowhead="vee"];
+}
--- /dev/null
+digraph { rankdir="LR"
+1 -> 1 [label=" - "]
+1 -> 3 [label="+"]
+3 -> 3 [label="+"]
+3 -> 2 [label="+"]
+3 -> 1 [label="+"]
+2 -> 3 [label="+"]
+2 -> 1 [label="-"]
+1 -> 2 [label="+"]
+}
+++ /dev/null
-\ifglsentryexists{graphoriente}{}%
-{%
-\gls@defglossaryentry{graphoriente}%
-{%
-name={graphe orienté},%
-sort={graphe orienté},%
-type={main},%
-first={graphe orient\IeC {\'e}},%
-firstplural={graphe orient\IeC {\'e}s},%
-text={graphe orient\IeC {\'e}},%
-plural={graphe orient\IeC {\'e}s},%
-description={Un graphe orienté $G=(S,A)$ est défini par la donnée d'un ensemble de sommets $S$ et d'un ensemble d'arcs $A$, chaque arc étant représenté par un couple de sommets. Si $x$ et $y$ sont des sommets de $S$, le couple $(x,y)$ représente l'arc orienté allant du sommet \emph {origine} $x$ au sommet \emph {extremité} $y$.},%
-descriptionplural={Un graphe orienté $G=(S,A)$ est défini par la donnée d'un ensemble de sommets $S$ et d'un ensemble d'arcs $A$, chaque arc étant représenté par un couple de sommets. Si $x$ et $y$ sont des sommets de $S$, le couple $(x,y)$ représente l'arc orienté allant du sommet \emph {origine} $x$ au sommet \emph {extremité} $y$.},%
-symbol={\relax },%
-symbolplural={\relax },%
-user1={},%
-user2={},%
-user3={},%
-user4={},%
-user5={},%
-user6={},%
-long={},%
-longplural={},%
-short={},%
-shortplural={},%
-counter={page},%
-parent={},%
-%
-}%
-}%
-\ifglsentryexists{graphfortementconnexe}{}%
-{%
-\gls@defglossaryentry{graphfortementconnexe}%
-{%
-name={graphe fortement connexe},%
-sort={graphe fortement connexe},%
-type={main},%
-first={graphe fortement connexe},%
-firstplural={graphe fortement connexes},%
-text={graphe fortement connexe},%
-plural={graphe fortement connexes},%
-description={Un graphe orienté $G=(S,A)$ est fortement connexe si pour tout couple de sommets $x$, $y$ de $S$ il existe un chemin reliant $x$ à $y$ et $y$ à $x$.},%
-descriptionplural={Un graphe orienté $G=(S,A)$ est fortement connexe si pour tout couple de sommets $x$, $y$ de $S$ il existe un chemin reliant $x$ à $y$ et $y$ à $x$.},%
-symbol={\relax },%
-symbolplural={\relax },%
-user1={},%
-user2={},%
-user3={},%
-user4={},%
-user5={},%
-user6={},%
-long={},%
-longplural={},%
-short={},%
-shortplural={},%
-counter={page},%
-parent={},%
-%
-}%
-}%
-\ifglsentryexists{distributionuniforme}{}%
-{%
-\gls@defglossaryentry{distributionuniforme}%
-{%
-name={distribution uniforme},%
-sort={distribution uniforme},%
-type={main},%
-first={distribution uniforme},%
-firstplural={distribution uniformes},%
-text={distribution uniforme},%
-plural={distribution uniformes},%
-description={Les lois de distribution uniforme (ou loi uniformes continues) forment une famille de lois à densité caractérisées par la propriété suivante: tous les intervalles de même longueur inclus dans le support de la loi ont la même probabilité.},%
-descriptionplural={Les lois de distribution uniforme (ou loi uniformes continues) forment une famille de lois à densité caractérisées par la propriété suivante: tous les intervalles de même longueur inclus dans le support de la loi ont la même probabilité.},%
-symbol={\relax },%
-symbolplural={\relax },%
-user1={},%
-user2={},%
-user3={},%
-user4={},%
-user5={},%
-user6={},%
-long={},%
-longplural={},%
-short={},%
-shortplural={},%
-counter={page},%
-parent={},%
-%
-}%
-}%
-\ifglsentryexists{partieentiere}{}%
-{%
-\gls@defglossaryentry{partieentiere}%
-{%
-name={partie entière},%
-sort={partie entière},%
-type={main},%
-first={partie enti\IeC {\`e}re},%
-firstplural={partie enti\IeC {\`e}res},%
-text={partie enti\IeC {\`e}re},%
-plural={partie enti\IeC {\`e}res},%
-description={La partie entière d'un nombre réel est l'entier qui lui est immédiatement inférieur ou égal. Pour un nombre réel $x$, on la note $\lfloor x \rfloor $.},%
-descriptionplural={La partie entière d'un nombre réel est l'entier qui lui est immédiatement inférieur ou égal. Pour un nombre réel $x$, on la note $\lfloor x \rfloor $.},%
-symbol={\ensuremath {\lfloor x \rfloor }},%
-symbolplural={\ensuremath {\lfloor x \rfloor }},%
-user1={},%
-user2={},%
-user3={},%
-user4={},%
-user5={},%
-user6={},%
-long={},%
-longplural={},%
-short={},%
-shortplural={},%
-counter={page},%
-parent={},%
-%
-}%
-}%
-\ifglsentryexists{distanceHamming}{}%
-{%
-\gls@defglossaryentry{distanceHamming}%
-{%
-name={distance de Hamming},%
-sort={distance de Hamming},%
-type={main},%
-first={distance de Hamming},%
-firstplural={distance de Hammings},%
-text={distance de Hamming},%
-plural={distance de Hammings},%
-description={La distance de Hamming entre deux éléments $x=(x_1,\ldots ,x_n)$ et $y=(y_1,\ldots ,y_n)$ dans $\Bool ^n$ est le nombre d'indices $i$, $1 \le i \le n$ tels que $x_i$ diffère de $y_i$.},%
-descriptionplural={La distance de Hamming entre deux éléments $x=(x_1,\ldots ,x_n)$ et $y=(y_1,\ldots ,y_n)$ dans $\Bool ^n$ est le nombre d'indices $i$, $1 \le i \le n$ tels que $x_i$ diffère de $y_i$.},%
-symbol={\relax },%
-symbolplural={\relax },%
-user1={},%
-user2={},%
-user3={},%
-user4={},%
-user5={},%
-user6={},%
-long={},%
-longplural={},%
-short={},%
-shortplural={},%
-counter={page},%
-parent={},%
-%
-}%
-}%
-\ifglsentryexists{decalageDeBits}{}%
-{%
-\gls@defglossaryentry{decalageDeBits}%
-{%
-name={décalage de bits},%
-sort={décalage de bits},%
-type={main},%
-first={d\IeC {\'e}calage de bits},%
-firstplural={d\IeC {\'e}calages de bits},%
-text={d\IeC {\'e}calage de bits},%
-plural={d\IeC {\'e}calages de bits},%
-description={Soit $x$ un nombre binaire de $n$ bits et $b$ un entier. Le nombre binaire de $n$ bits $x \ll b$ (respectivement $x \gg b$) est obtenu en décalant les bits de $x$ de $b$ bits vers la gauche (resp. vers la droite) et en complétant avec des zéros à droite (resp. à gauche).},%
-descriptionplural={Soit $x$ un nombre binaire de $n$ bits et $b$ un entier. Le nombre binaire de $n$ bits $x \ll b$ (respectivement $x \gg b$) est obtenu en décalant les bits de $x$ de $b$ bits vers la gauche (resp. vers la droite) et en complétant avec des zéros à droite (resp. à gauche).},%
-symbol={\relax },%
-symbolplural={\relax },%
-user1={},%
-user2={},%
-user3={},%
-user4={},%
-user5={},%
-user6={},%
-long={},%
-longplural={},%
-short={},%
-shortplural={},%
-counter={page},%
-parent={},%
-%
-}%
-}%
-\ifglsentryexists{chaineDeMarkov}{}%
-{%
-\gls@defglossaryentry{chaineDeMarkov}%
-{%
-name={chaîne de Markov},%
-sort={chaîne de Markov},%
-type={main},%
-first={cha\IeC {\^\i }ne de Markov},%
-firstplural={cha\IeC {\^\i }nes de Markov},%
-text={cha\IeC {\^\i }ne de Markov},%
-plural={cha\IeC {\^\i }nes de Markov},%
-description={On se restreint à la définition d'une chaîne de Markov homogène. Celle-ci désigne une suite de variables aléatoires $(X_n)_{n \in \Nats }$ à temps discret, à espace d'états discret, sans mémoire et dont le mécanisme de transition ne change pas au cours du temps. Formellement la propriété suivante doit être établie:\newline $ \forall n \ge 0, \forall (i_0, \ldots , i_{n-1}, i,j),\\ \textrm { }P(X_{n+1}=j\mid X_0=i_0, X_1=i_1, X_2=i_2, \ldots , X_{n-1}=i_{n-1}, X_{n}=i) \\ \textrm { }= P(X_{1}=j\mid X_n=i). $},%
-descriptionplural={On se restreint à la définition d'une chaîne de Markov homogène. Celle-ci désigne une suite de variables aléatoires $(X_n)_{n \in \Nats }$ à temps discret, à espace d'états discret, sans mémoire et dont le mécanisme de transition ne change pas au cours du temps. Formellement la propriété suivante doit être établie:\newline $ \forall n \ge 0, \forall (i_0, \ldots , i_{n-1}, i,j),\\ \textrm { }P(X_{n+1}=j\mid X_0=i_0, X_1=i_1, X_2=i_2, \ldots , X_{n-1}=i_{n-1}, X_{n}=i) \\ \textrm { }= P(X_{1}=j\mid X_n=i). $},%
-symbol={\relax },%
-symbolplural={\relax },%
-user1={},%
-user2={},%
-user3={},%
-user4={},%
-user5={},%
-user6={},%
-long={},%
-longplural={},%
-short={},%
-shortplural={},%
-counter={page},%
-parent={},%
-%
-}%
-}%
-\ifglsentryexists{vecteurDeProbabilite}{}%
-{%
-\gls@defglossaryentry{vecteurDeProbabilite}%
-{%
-name={vecteur de probabilités},%
-sort={vecteur de probabilités},%
-type={main},%
-first={vecteur de probabilit\IeC {\'e}s},%
-firstplural={vecteurs de probabilit\IeC {\'e}s},%
-text={vecteur de probabilit\IeC {\'e}s},%
-plural={vecteurs de probabilit\IeC {\'e}s},%
-description={Un vecteur de probabilités est un vecteur tel que toutes ses composantes sont positives ou nulles et leur somme vaut 1.},%
-descriptionplural={Un vecteur de probabilités est un vecteur tel que toutes ses composantes sont positives ou nulles et leur somme vaut 1.},%
-symbol={\relax },%
-symbolplural={\relax },%
-user1={},%
-user2={},%
-user3={},%
-user4={},%
-user5={},%
-user6={},%
-long={},%
-longplural={},%
-short={},%
-shortplural={},%
-counter={page},%
-parent={},%
-%
-}%
-}%
-\ifglsentryexists{matriceDAdjacence}{}%
-{%
-\gls@defglossaryentry{matriceDAdjacence}%
-{%
-name={matrice d'adjacence},%
-sort={matrice d'adjacence},%
-type={main},%
-first={matrice d'adjacence},%
-firstplural={matrice d'adjacences},%
-text={matrice d'adjacence},%
-plural={matrice d'adjacences},%
-description={La matrice d'adjacence du graphe orienté $G=(S,A)$ à $n$ sommets est la matrice $\check {M}$ de dimension $n \times n$ dont l'élément $\check {M}_{ij}$ représente le nombre d'arcs d'origine $i$ et d'extrémité $j$.},%
-descriptionplural={La matrice d'adjacence du graphe orienté $G=(S,A)$ à $n$ sommets est la matrice $\check {M}$ de dimension $n \times n$ dont l'élément $\check {M}_{ij}$ représente le nombre d'arcs d'origine $i$ et d'extrémité $j$.},%
-symbol={\relax },%
-symbolplural={\relax },%
-user1={},%
-user2={},%
-user3={},%
-user4={},%
-user5={},%
-user6={},%
-long={},%
-longplural={},%
-short={},%
-shortplural={},%
-counter={page},%
-parent={},%
-%
-}%
-}%
-\ifglsentryexists{xor}{}%
-{%
-\gls@defglossaryentry{xor}%
-{%
-name={ou exclusif},%
-sort={ou exclusif},%
-type={main},%
-first={ou exclusif},%
-firstplural={ou exclusifs},%
-text={ou exclusif},%
-plural={ou exclusifs},%
-description={La fonction \og ou exclusif\fg {}, XOR, est l'opérateur de $\Bool ^2$ dans $\Bool $ qui prend la valeur 1 si seulement si les deux opérandes ont des valeurs distinctes.},%
-descriptionplural={La fonction \og ou exclusif\fg {}, XOR, est l'opérateur de $\Bool ^2$ dans $\Bool $ qui prend la valeur 1 si seulement si les deux opérandes ont des valeurs distinctes.},%
-symbol={\ensuremath {\oplus }},%
-symbolplural={\ensuremath {\oplus }},%
-user1={},%
-user2={},%
-user3={},%
-user4={},%
-user5={},%
-user6={},%
-long={},%
-longplural={},%
-short={},%
-shortplural={},%
-counter={page},%
-parent={},%
-%
-}%
-}%
-\ifglsentryexists{matriceDeTransitions}{}%
-{%
-\gls@defglossaryentry{matriceDeTransitions}%
-{%
-name={matrice de transitions},%
-sort={matrice de transitions},%
-type={main},%
-first={matrice de transitions},%
-firstplural={matrice de transitionss},%
-text={matrice de transitions},%
-plural={matrice de transitionss},%
-description={Le nombre $p_{ij}= P(X_1=j \mid X_0 =i)$ est appelé probabilité de transition de l'état $i$ à l'état $j$ en un pas. La matrice composée des $p_{ij}$ est la matrice de transitions associée à la chaine de Markov $X$.},%
-descriptionplural={Le nombre $p_{ij}= P(X_1=j \mid X_0 =i)$ est appelé probabilité de transition de l'état $i$ à l'état $j$ en un pas. La matrice composée des $p_{ij}$ est la matrice de transitions associée à la chaine de Markov $X$.},%
-symbol={\relax },%
-symbolplural={\relax },%
-user1={},%
-user2={},%
-user3={},%
-user4={},%
-user5={},%
-user6={},%
-long={},%
-longplural={},%
-short={},%
-shortplural={},%
-counter={page},%
-parent={},%
-%
-}%
-}%
\documentclass[french]{spimufchdr}
\usepackage{dsfont}
-\usepackage{glossaries}
\usepackage{graphicx}
\usepackage{listings}
-\usepackage{verbatim}
-
-% The TeX code is entering with UTF8
-% character encoding (Linux and MacOS standards)
+%\usepackage[font=footnotesize]{subfig}
\usepackage[utf8]{inputenc}
+\usepackage{thmtools, thm-restate}
+%\declaretheorem{theorem}
%%--------------------
%% Search path for pictures
-%\graphicspath{{path1/},{path2/}}
+\graphicspath{{images/},{path2/}}
%%--------------------
%% Definition of the bibliography entries
\newtheorem{Def}{Définition}
\begin{document}
-\input{glossaire.tex}
-
-% \chapter*{Remerciements}
-
-% Blabla blabla.
-
-% \tableofcontents
\part{Système Booléens}
\chapter{Iterations discrètes de Systèmes Dynamiques booléens}
-
-\JFC{Chapeau chapitre à faire}
+\section{Formalisation}
\input{sdd}
-\chapter{Combinaisons Synchrones et Asynchrones de Systèmes Booléens}
+\section{Combinaisons synchrones et asynchrones}
\input{mixage}
+\section{Conclusion}
+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
+avantage du synchronisme en terme de convergence avec les avantages
+de l'asynchronisme en terme de vitesse de convergence.
+
+
+
\chapter[Preuve de convergence de systèmes booléens]{Preuve automatique de convergence de systèmes booléens}\label{chap:promela}
\input{modelchecking}
-
\JFC{Mixage}
-\JFC{Refaire le châpeau}
-\section{Généralisation au cadre asynchrone}
-Dans ce chapitre une stratégie $s=(s^{t})^{t \in \Nats}$ est une séquence
-\emph{des éléments} qui sont mis à jour au temps $t$. Pratiquement,
-on représente ceci comme un nombre décimal dont la représentation en
+
+Pour être exécuté,
+le mode des itérations généralisées nécessite que chaque élément
+connaisse la valeur de chaque autre élément dont il dépend.
+Pratiquement, cela se réalise en diffusant les valeurs des éléments de
+proche en proche à tous les composants.
+Dans le mode généralisé
+\emph{asynchrone}, le composant n'attend pas: il met à jour sa
+valeur avec les dernières valeurs dont il dispose, même si celles-ci
+ne sont pas à jour.
+Cette section vise l'étude de ce mode.
+
+
+%\subsection{Généralisation au cadre asynchrone}
+Pratiquement, chaque stratégie du mode généralisé peut être
+mémorisée comme un nombre décimal dont la représentation en
binaire donne la liste des éléments modifiés. Par exemple, pour un système
à 5 éléments la stratégie définie par
\begin{equation}\label{eq:pseudo}
Obtenir où non les valeurs les plus à jours dépend du temps de calcul et
du temps d'acheminement de celles-ci. On parle de latence, de délai.
-Formalisons le mode les itérations asynchrones.
+Formalisons le mode les itérations asynchrone.
Soit $x^0 =(x_1^0, \ldots, x_n^0)$ une configuration initiale.
Soit $(D^{t})^{t \in \Nats}$ la suite de matrice de taille $n \times n$
dont chaque élément $D_{ij}^{t}$ représente la date (inférieure ou égale à $t$)
disponible au composant $i$.
On considère que le délai entre l'émission par $j$ et la réception par $i$,
défini par $\delta_{ij}^t = t - D_{ij}^{t}$ est borné par une constante $\delta_0$ pour tous les $i$, $j$.
-Le \emph{mode des itérations asynchrones} est défini pour chaque $i
+Le \emph{mode des itérations généralisées sans attente}
+est défini pour chaque $i
\in \{1,\ldots,n\}$ et chaque $t=0,1,2,...$ par:
\vspace{-.5em}
\emph{universellement convergentes}.
-\section{Exemple jouet}
+\subsection{Exemple jouet}
On considère cinq éléments prenant à valeurs dans $\Bool$.
Une configuration dans $\Bool^5$ est représentée par un entier entre
0 et 31. La~\Fig{fig:mix:map} donne la fonction définissant la dynamique du
système. La~\Fig{fig:mix:xplgraph} donne le graphe d'interaction associé à cette fonction.
On note que le graphe d'interaction contient cinq cycles. Les résultats
-connus~\cite{Bah00} de conditions suffisantes établissant la convergence du système pour les itérations synchrones et asynchrones sont basés sur l'absence de cycles. Ils ne peuvent donc pas être appliqués ici.
+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{minipage}[b]{0.55\linewidth}
\end{minipage}\hfill
\begin{minipage}[b]{.40\linewidth}
\begin{center}
- \includegraphics[scale=0.55]{images/xplgraphmix.eps}
+ \includegraphics[scale=0.55]{xplgraphmix}
\end{center}
\caption{Graphe d'interaction associé à $f$.}
\label{fig:mix:xplgraph}
\begin{figure}
\begin{minipage}{0.56\linewidth}
- \includegraphics[scale=0.55]{images/para_iterate_dec.eps}
+ \includegraphics[scale=0.55]{para_iterate_dec}
\caption{Itérations parallèles de $f$.}\label{fig:mix:xplparaFig}
\end{minipage}
\hfill
\begin{minipage}{0.39\linewidth}
- \includegraphics[scale=0.55]{images/chao_iterate_excerpt.eps}
+ \includegraphics[scale=0.55]{chao_iterate_excerpt}
\caption{Extrait d'itérations chaotiques.}
\label{fig:mix:xplchaoFig}
\end{minipage}
\noindent sinon.
En démarrant de $x^0=00011$, le système atteint $x^1 = 01011$ et boucle entre
ces deux configurations. Pour une même stratégies, les itérations
-asynchrones divergent alors que les synchrones convergent.
+asynhrones divergent alors que les synchrones convergent.
Les sections suivantes de ce chapitre montrent comment résoudre ce problème.
-\section{Itérations Mixes}
+\subsection{Itérations Mixes}
Introduit dans~\cite{abcvs05}
le mode d'\emph{itérations mixes} combine synchronisme et asynchronisme.
Intuitivement, les n{\oe}uds qui pourraient introduire des cycles dans
les itérations asynchrones sont regroupés.
Les noeuds à l'intérieur de chaque groupe seront itérés de manière
synchrone.
-L'asynchronisme est conservé entre les groupes.
+Les itérations asynchrones sont conservées entre les groupes.
\begin{Def}[Relation de Synchronisation]\label{def:eqrel}
Soit une fonction $f$ et $\Gamma(f)$ son graphe d'interaction.
-\section{Durées de convergence}
+\subsection{Durées de convergence}
Cette section donne des bornes supérieures et inférieures des durées
globales de convergence pour les modes synchrones, mixes et asynchrones.
Pour simplifier le discours, on considère que les itérations
Pour simplifier l'évaluation, nous considérons que le temps de calcul d'une
itération sur un composant ainsi que celui de communication entre deux
composants est constant. Ceci implique en particulier que, dans
-le mode asynchrone, les délais sont bornés. En d'autres mots, il existe
+le mode asynchrone, ces derniers sont bornés. En d'autres mots, il existe
un entier $\delta_0$ tel que $0 \le t-D_{ij}^t \le \delta_0$ est établi
pour tout couple de n{\oe}uds $(i,j)$.
Les notations utilisées sont les suivantes:
\begin{figure}
\centering
\begin{minipage}{1\linewidth}
- \includegraphics[scale=0.4]{images/eval_sync.eps}
+ \includegraphics[scale=0.4]{eval_sync}
\caption{Itérations parallèles}
\label{fig:evalsync}
\end{minipage}
\begin{minipage}{1\textwidth}
- \includegraphics[scale=0.4]{images/eval_mixte.pdf}
+ \includegraphics[scale=0.4]{eval_mixte}
\caption{Itérations mixes avec
\class{1} $=\{1,2\}$, \class{3} $=\{3\}$,
\class{4} $=\{4,5\}$.}
\end{minipage}
\begin{minipage}{1\textwidth}
- \includegraphics[scale=0.4]{images/eval_async.pdf}
+ \includegraphics[scale=0.4]{eval_async}
\caption{Itérations asynchrones}
\label{fig:evalasync}
\end{minipage}
% \begin{figure}%[h]
% \centering
% % \includegraphics[width=\textwidth]{eval_siac.eps}
-% \includegraphics[width=\textwidth]{images/eval_siac.eps}
+% \includegraphics[width=\textwidth]{eval_siac.eps}
% \caption{Execution of the \textit{SIAC} iterations starting from state 4
% (00100).}
% \label{fig:evalsiac}
mode parallèle.
\end{xpl}
-\subsection{Le mode asynchrone}
+\subsection{Le mode généralisé asynchrone}
\label{sec:evalasync}
En terme de durée de convergence, ce mode peut être vu comme un
cas particulier du mode mixe où toutes les classes sont des singletons.
-\section{Conclusion}
-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
-avantage du synchronisme en terme de convergence avec les avantages
-de l'asynchronisme en terme de vitesse de convergence.
annexes~\ref{anx:promela}.
-\begin{theorem}[Correction]\label{Theo:sound}
+\begin{restatable}[Correction de la traduction vers Promela]{theorem}{promelasound}
+\label{Theo:sound}
+%
Soit $\phi$ un modèle de système dynamique discret et $\psi$ sa traduction PROMELA.
Si $\psi$ vérifie
la propriété LTL (\ref{eq:ltl:conv}) sous hypothèse d'équité faible, alors
les itérations de $\phi$ sont universellement convergentes.
-\end{theorem}
-
+\end{restatable}
-\begin{theorem}[Complétude]\label{Theo:completeness}
+\begin{restatable}[Complétude de la traduction vers Promela]{theorem}{promelacomplete}
+\label{Theo:completeness}
+%
Soit $\phi$ un modèle de système dynamique discret et $\psi$ sa traduction. Si $\psi$ ne vérifie pas
la propriété LTL (\ref{eq:ltl:conv}) sous hypothèse d'équité faible,
alors les itérations de $\phi$ ne sont pas universellement convergentes.
-\end{theorem}
+\end{restatable}
+
+
\chapter{Iterations discrètes}
-Formalisation: TIPE
+Formalisation: TIPE1 et 2
Model cheking
Olivier Grasset
-PArtie FCT11 chaos
+Partie TIPE PRNG
\chapter{Rendre le chaos alléatoire}
partie FCT11 random
-Secrypt 14/ Mons14
+15Rairo
Etude de robustesse : IIHMSP 13
-
+\section{Tatouage ds les pdf}
+Avec Bittar
\section{Stéganographie}
Stabylo
+
+
+
\chapter{Application aux fonctions de hachage}
Journal Fonctions de hachage
-
-
\JFC{Chapeau chapitre à faire}
-Cette section énonce quelques notions suffisantes
-à la compréhension de ce document.
-Elle commence par formaliser ce que sont les systèmes dynamiques booléens
-(section \ref{sub:sdd})
-et montre comment en extraire leur graphe d'itérations (section~\ref{sub:grIter})
-et d'interactions (section~\ref{sub:sdd:inter}).
-Elle se termine en définissant une distance sur l'espace
-$\llbracket 1;n\rrbracket^{\Nats}\times \Bool^n$ (section~\ref{sub:metric}).
-
-
-
-
-
-
-\section{Système dynamique booléen}\label{sub:sdd}
-
-Soit $n$ un entier naturel. Un système dynamique booléen est
+% Cette section énonce quelques notions suffisantes
+% à la compréhension de ce document.
+% Elle commence par formaliser ce que sont les systèmes dynamiques booléens
+% (section \ref{sub:sdd})
+% et montre comment en extraire leur graphe d'itérations (section~\ref{sub:grIter})
+% et d'interactions (section~\ref{sub:sdd:inter}).
+% Elle se termine en définissant une distance sur l'espace
+% $\llbracket 1;n\rrbracket^{\Nats}\times \Bool^n$ (section~\ref{sub:metric}).
+
+
+
+
+On considère l'espace booléen
+$\Bool=\{0,1\}$
+muni des opérateurs binaires
+de disjonction \og +\fg{},
+de conjonction \og . \fg{} et
+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]$.
+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$
+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]}$
+(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]$
+(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]$
+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$.
+Pour chaque
+$x$ dans $\Bool^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
+$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{, }\\
+f_2(x_1, x_2, x_3) &= &x_1.x_3 \textrm{ et }\\
+f_3(x_1, x_2, x_3) &=& x_1 + x_2 + x_3.
+\end{array}
+$$
+
+\begin{table}[ht]
+$$
+\begin{array}{|l|l|l||c|c|c|}
+\hline
+\multicolumn{3}{|c||}{x} &
+\multicolumn{3}{|c|}{f(x)} \\
+\hline
+x_1 & x_2 & x_3 &
+f_1(x) & f_2(x) & f_3(x) \\
+\hline
+0& 0 & 0 & 0 & 0 & 0 \\
+\hline
+0& 0 & 1 & 1 & 0 & 1\\
+\hline
+0& 1 & 0 & 0 & 0& 1\\
+\hline
+0& 1 & 1 & 1 & 0& 1\\
+\hline
+1& 0 & 0 & 0 & 0& 1\\
+\hline
+1& 0 & 1 & 1 & 1& 1\\
+\hline
+1& 1 & 0 & 0 & 0& 1\\
+\hline
+1& 1 & 1 & 0 & 1& 1\\
+\hline
+\end{array}
+$$
+\caption{Images de
+$(x_1, x_2, x_3) \mapsto
+((\overline{x_1} + \overline{x_2}).x_3,
+x_1.x_3,
+x_1 + x_2 + x_3)$ \label{table:xpl:images}}
+\end{table}
+
+La \textsc{Table}~\ref{table:xpl:images} donne l'image de chaque élément
+$x \in \Bool^3$.
+Pour $x=(0,1,0)$ les assertions suivantes se déduisent directement du tableau:
+\begin{itemize}
+\item $f(x)=(0,0,1)$;
+\item pour $I=\{1,3\}$, $\overline{x}^{I} = (1,1,1)$ et
+ $\overline{x} = (1,0,1)$;
+\item $\Delta(x,f(x)) = \{2,3\}$.
+\end{itemize}
+
+\end{xpl}
+
+\subsection{Réseau booléen}
+Soit $n$ un entier naturel représentant le nombre
+d'éléments étudiés (gènes, protéines,\ldots).
+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)),
\]
-et un {\emph{schéma des itérations}} qui peuvent être
-parallèles, séquentielles, chaotiques, asynchrones \ldots
-Le schéma des itérations parallèles est défini comme suit:
-à partir d'une configuration initiale $x^0\in\Bool^n$, la suite
-$(x^{t})^{t \in \Nats}$
-des configurations du système est construite à partir de la relation de récurrence
-$x^{t+1}=f(x^t)$. Tous les $x_i$, $1 \le i \le n$
-sont ainsi mis à jour à chaque itération.
-Le schéma qui ne modifie qu'un élément
-$i$, $1 \le i \le n$ à chaque itération
-est le schéma \emph{chaotique}.
-Plus formellement, à la $t^{\textrm{ème}}$ itération, seul le $s_{t}^{\textrm{ème}}$
-composant (entre 1 et $n$) est mis à jour.
-La suite $s = \left(s_t\right)_{t \in \mathds{N}}$ est une séquence d'indices
-de $\llbracket 1;n \rrbracket$ appelée \emph{stratégie}. Formellement, dans
-ce mode opératoire,
-soit $F_f: \llbracket1;n\rrbracket\times \Bool^{n}$ vers $\Bool^n$ définie par
-\[
-F_f(i,x)=(x_1,\dots,x_{i-1},f_i(x),x_{i+1},\dots,x_n).
-\]
-
-Dans le schéma des itérations chaotiques pour une configuration initiale
-$x^0\in\Bool^n$ et une stratégie $s\in
-\llbracket1;n\rrbracket^\Nats$, 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).
-\end{equation}
-
-Soit alors $G_f$ une fonction de $\llbracket1;n\rrbracket^\Nats\times\Bool^n$
-dans lui même définie par
-\[
-G_f(s,x)=(\sigma(s),F_f(s_0,x)),
-\]
-où $\forall t\in\Nats,\sigma(s)_t=s_{t+1}$.
-En d'autres termes la fonction $\sigma$ décale
-la stratégie fournie en argument d'un élément vers la gauche en supprimant
-l'élément de tête.
-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 chaotiques de $f$ induites par $x^0$ et la stratégie
-$s$.
-
-\section{Graphe d'itérations}\label{sub:grIter}
-
-Soit $f$ une fonction de $\Bool^n$ dans lui-même.
-Le {\emph{graphe des itérations chaotiques}} associé à $f$ est le
-graphe orienté $\Gamma(f)$ défini ainsi:
-l'ensemble de ses sommets est $\Bool^n$ et pour chaque $x\in\Bool^n$ et
-$i\in \llbracket1;n\rrbracket$, le graphe $\Gamma(f)$
-contient un arc de $x$ vers $F_f(i,x)$.
-La relation entre $\Gamma(f)$ et $G_f$ est claire: il existe un
-chemin de $x$ à $x'$ dans $\Gamma(f)$ si et seulement s'il existe une
-stratégie $s$ telle que les itérations parallèles $G_f$ à partir
-du point $(s,x)$ mènent au point $x'$.
-
-
-Dans ce qui suit, et par souci de concision, le terme \emph{graphe des itérations}
-est une abréviation de graphe des itérations chaotiques.
-La figure~\ref{fig:xplgraphIter} donne deux exemples de graphes d'itérations
-pour les fonctions $g$ et $h$ définies dans $\Bool^2$ qui seront reprises dans la suite.
-
-
-
-\begin{figure}%
-\centering
-\begin{minipage}{0.40\textwidth}
- \begin{center}
- \includegraphics[scale=0.4]{images/g.pdf}
- \end{center}
-\caption{$g(x_1,x_2)=(\overline{x_1},x_1\overline{x_2}) $}%
-\label{fig:g:iter}%
-\end{minipage}
-\qquad
-\begin{minipage}{0.40\textwidth}%
+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
+ \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 à
+ chaque itération en utilisant l'état global précédent du système $x^t$.
+\item \textbf{Schéma unaire :} cette terminologie a plusieurs
+ interprétations
+ dans la littérature, mais celle que nous
+ retenons ici consiste à modifier la valeur
+ d'un unique élément $i$, $1 \le i \le 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}.
+% Lorsque cette suite est strictement cyclique (sans
+ % occurrences multiples dans le motif) sur l'ensemble des éléments $\{1,\ldots
+ % n\}$, alors on retrouve le comportement du mode séquentiel synchrone.
+\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.
+ Dans le cas particulier où c'est la valeur d'un singleton
+ $\{k\}$, $1 \le k \le 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
+ à 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 à
+ 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}.
+ \end{itemize}
+
+
+
+
+
+La section suivante détaille comment représenter graphiquement les évolutions de tels réseaux.
+\subsection{Graphes des itérations}
+
+
+
+Pour un entier naturel $n$ et une
+fonction $f : B^n \rightarrow B^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}).
+
+
+\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
+et seulement si $y=f(x)$.
+\item Le \emph{graphe des itérations unaires} de $f$, noté $\textsc{gia}(f)$
+est le graphe orienté de $\Bool^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
+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
+des itérations unaires.
+
+
+\end{itemize}
+
+
+
+\begin{xpl}
+On reprend notre exemple illustratif
+détaillé à la page~\pageref{xpl:1} avec sa table
+d'images (\textsc{Table}~\ref{table:xpl:images}).
+La \textsc{Figure}~\ref{fig:xpl:graphs} donne les trois graphes d'itérations
+associés à $f$.
+
+\begin{figure}[ht]
\begin{center}
- \includegraphics[scale=0.4]{images/h.pdf}
+ \subfigure[$\textsc{gis}(f)$]{
+ \begin{minipage}{0.33\textwidth}
+ \begin{center}
+ \includegraphics[scale=0.4]{fsig}
+ \end{center}
+ \end{minipage}
+ \label{fig:fsig}
+ }
+ \subfigure[$\textsc{gia}(f)$]{
+ \begin{minipage}{0.33\textwidth}
+ \begin{center}
+ \includegraphics[scale=0.4]{faig}
+ \end{center}
+ \end{minipage}
+ \label{fig:faig}
+ }
+ \subfigure[$\textsc{gig}(f)$]{
+ \begin{minipage}{0.33\textwidth}
+ \begin{center}
+ \includegraphics[scale=0.4]{fgig}
+ \end{center}
+ \end{minipage}
+ \label{fig:fgig}
+ }
\end{center}
-\caption{$h(x_1,x_2)=(\overline{x_1},x_1\overline{x_2}+\overline{x_1}x_2)$}%
-\label{fig:h:iter}%
-\end{minipage}%
-\caption{Graphes d'itérations de fonctions booléennes dans $\Bool^2$}
-\label{fig:xplgraphIter}
-\end{figure}%
-
-
-
-
-
-\section{Graphe d'interactions}\label{sub:sdd:inter}
-
-Pour $x\in\Bool^n$ et $i\in\llbracket 1;n\rrbracket$, on nomme
-$\overline{x}^i$ la configuration obtenue en niant le
-$i^{\textrm{ème}}$ composant de $x$. En d'autres termes
-$\overline{x}^i=(x_1,\dots,\overline{x_i},\dots,x_n)$.
-Des interactions entre les composants du
+ \caption{Graphes des itérations de la fonction
+$f:\Bool^3 \rightarrow \Bool^3$ telle que
+$(x_1, x_2, x_3) \mapsto
+((\overline{x_1} + \overline{x_2}).x_3,
+x_1.x_3,
+x_1 + x_2 + x_3)$.\label{fig:xpl:graphs}
+On remarque le cycle $((101,111),(111,011),(011,101))$
+ à la \textsc{Figure}~(\ref{fig:fsig}).}
+\end{figure}
+\end{xpl}
+
+
+\subsection{Attracteurs}
+
+On dit que le point
+$x \in \Bool^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
+si et seulement si il est son seul successeur.
+Dans le contexte des réseaux de régulation de gènes,
+ces points fixes correspondent aux configurations stables pour l'expression de
+gènes.
+
+
+
+Soit $\Gamma$ un graphe d'itérations (synchrones, unaires ou généralisées)
+de $f$.
+Les \emph{attracteurs} de $\Gamma$ 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
+$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.
+En d'autres termes, lorsqu'un système entre dans un attracteur cyclique,
+il ne peut pas atteindre un point fixe.
+
+
+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$
+sont les points fixes de $f$.
+Ainsi pour chaque $x\in \Bool^n$, il existe au moins un chemin
+depuis $x$ qui atteint un attracteur.
+Ainsi $\Gamma$ contient toujours au moins un attracteur.
+\end{theorem}
+
+
+
+\begin{xpl}
+Les attracteurs de $\textsc{gia}(f)$ et de $\textsc{gig}(f)$ sont
+le point fixe $000$ et l'attracteur cyclique
+$\{001, 101,111, 011 \}$.
+Les attracteurs de $\textsc{gis}(f)$ sont le point fixe $000$
+et l'attracteur cyclique $\{011, 101, 111\}$.
+\end{xpl}
+
+\subsection{Graphe d'interaction}
+Les interactions entre les composants du
système peuvent être mémorisées
-dans la {\emph{matrice Jacobienne discrète}} $f'$.
+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
-$n\times n$
-\[
-f'(x)=(f_{ij}(x)),\qquad
-f_{ij}(x)=\frac{f_i(\overline{x}^j)-f_i(x)}{\overline{x}^j_j-x_j}\qquad (i,j\in\llbracket1;n\rrbracket).
-\]
-On note que dans l'équation donnant la valeur de $f_{ij}(x)$,
+$n\times n$ telle que
+\begin{equation}
+f'(x)=(f'_{ij}(x)),\qquad
+f'_{ij}(x)=\frac{f_i(\overline{x}^j){-}f_i(x)}{\overline{x_j}{-}x_j}\qquad (i,j\in[n]).
+\label{eq:jacobienne}
+\end{equation}
+On note que dans l'équation donnant la valeur de $f'_{ij}(x)$,
les termes $f_i(\overline{x}^j)$, $f_i(x)$,
$\overline{x}^j_j$ et $x_j$ sont considérés comme des entiers naturels
-égaux à $0$ ou à $1$ et que le calcul est effectué dans $\Z$.
-On a le lien suivant avec la \emph{matrice d'adjacence} $A$ de $f$ dans $\Bool^{n^2}$:
-le booléen $A_{ij}$ vaut 1 si et seulement s'il existe $x\in \Bool^{n}$ tel que
-$f_{ij}(x)$ est différent de 0.
+égaux à $0$ ou à $1$ et que la différence est effectuée
+ 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$.
+Celle-ci mémorise uniquement
+l'existence d'une dépendance de tel élément vis à vis de
+ tel élément.
+Elle ne mémorise pas \emph{comment} dépendent les éléments
+les uns par rapport aux autres. Cette matrice est nommée
+\emph{matrice d'incidence}.
+
+\begin{theorem}
+Si $f_i$ ne dépend pas de $x_j$, alors pour tout $x\in [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 $G(f)$ orienté et signé défini ainsi:
l'ensemble des sommets est
-$\llbracket1;n\rrbracket$ et il existe un arc de $j$ à $i$ de signe
+$[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$.
+
On note que la présence de
deux arcs de signes opposés entre deux sommets donnés
est possible.
-
-
-
-
-
-\begin{figure}%
-\centering
-\begin{minipage}{0.40\textwidth}
+% Dans la suite, le graphe signé $G$ sera qualifié de
+% \emph{simple} si, pour chaque $i$, $j$ dans $[n]$,
+% il existe au plus un arc de $j$ à $i$ dans $G$.
+Un cycle \emph{positif} (resp. négatif) de $G$
+est un cycle \emph{élémentaire} qui contient un nombre
+pair (resp. impair) d'arcs négatifs.
+La \emph{longueur}
+d'un cycle est le nombre d'arcs qu'il contient.
+
+\begin{xpl}
+Pour exprimer la jacobienne discrète de la fonction donnée en exemple,
+pour chaque $i$, $j$ dans
+$[3]$ on exprime
+$f'_{ij}(x)=
+\frac
+{f_i(\overline{x}^j){-}f_i(x)}
+{\overline{x_j}{-}x_j}$
+d'après l'équation~(\ref{eq:jacobienne}).
+% Ainsi
+% $$
+% f'_{12} (x_1,x_2,x_3)=
+% \frac
+% { ((\overline{x_1} + \overline{\overline{x_2}}).x_3)
+% {-}
+% ((\overline{x_1} + \overline{x_2}).x_3)
+% }
+% {\overline{x_2}{-}x_2} = \frac{
+% ((\overline{x_1} + x_2).x_3)
+% {-}
+% ((\overline{x_1} + \overline{x_2}).x_3)
+% }{\overline{x_2}{-}x_2} .
+% $$
+% Évaluons cette fonction de $\Bool^3$ dans $\Z$ en construisant le tableau de toutes ses valeurs.
+% $$
+% \begin{array}{|c|c|c|c|c|c|c|c|}
+% \hline
+% x_1 & x_2 & x_3 &
+% (\overline{x_1} + {x_2}).x_3 & (\overline{x_1} + \overline{x_2}).x_3 &
+% (\overline{x_1} + {x_2}).x_3 {-} (\overline{x_1} + \overline{x_2}).x_3 & \overline{x_2} {-} x_2 &
+% f'_{12} (x_1,x_2,x_3)\\
+% \hline
+% 0 & 0 & 0 & 0 & 0 & 0 & 1 & 0 \\\hline
+% 0 & 0 & 1 & 1 & 1 & 0 & 1 & 0 \\\hline
+% 0 & 1 & 0 & 0 & 0 & 0 & -1 & 0 \\\hline
+% 0 & 1 & 1 & 1 & 1 & 0 & -1 & 0 \\\hline
+% 1 & 0 & 0 & 0 & 0 & 0 & 1 & 0 \\\hline
+% 1 & 0 & 1 & 0 & 1 & -1 & 1 & -1 \\\hline
+% 1 & 1 & 0 & 0 & 0 & 0 & -1 & 0 \\\hline
+% 1 & 1 & 1 & 1 & 0 & 1& -1 & -1 \\\hline
+% \end{array}
+% $$
+% La seule valeur de $f'_{12}$ qui n'est pas nulle est -1, qui est négative.
+% Le graphe d'interaction contiendra ainsi un arc négatif entre le n{\oe}ud 2 et le n{\oe}ud 1.
+La \textsc{Figure}~(\ref{fig:f:jacobienne}) explicite la matrice jacobienne discrète de cette fonction.
+
+Le graphe d'interaction de $f$ s'en déduit directement. Il est donné à la
+\textsc{Figure}~(\ref{fig:f:interaction}).
+Il possède
+un cycle négatif de longueur 1 et
+un cycle négatif de longueur 3.
+Concernant les cycles positifs, il en possède
+un de longueur 1,
+deux de longueur 2
+et un de longueur 3.
+
+La matrice d'incidence peut se déduire de la matrice d'interaction en supprimant les signes ou bien
+en constatant que $f_1$ dépend des trois éléments $x_1$, $x_2$ et $x_3$ et donc que la première ligne de $B(f)$
+est égale à $1~1~1$. De manière similaire, $f_2$ (resp. $f_3$) dépend de
+$x_1$ et de $x_3$
+(resp. dépend de $x_1$, $x_2$ et $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{center}
- \includegraphics[scale=0.4]{images/gp.pdf}
- \end{center}
-\caption{$g(x_1,x_2)=(\overline{x_1},x_1\overline{x_2}) $}%
-\label{fig:g:inter}%
-\end{minipage}
-\qquad
-\begin{minipage}{0.40\textwidth}
- \begin{center}
- \includegraphics[scale=0.4]{images/hp.pdf}
- \end{center}
-\caption{$h(x_1,x_2)=(\overline{x_1},x_1\overline{x_2}+\overline{x_1}x_2)$}%
-\label{fig:h:inter}%
-\end{minipage}%
-\caption{Graphes d'interactions de fonctions booléennes dans $\Bool^2$}
-\label{fig:xplgraphInter}
-\end{figure}%
-
-
-
-
-
+ \subfigure[Matrice jacobienne de $f$.]{
+ \begin{minipage}{0.90\textwidth}
+ \begin{center}
+ $
+ \left(
+ \begin{array}{ccc}
+ \frac{
+ ((x_1 + \overline{x_2}).x_3)
+ {-}
+ ((\overline{x_1} + \overline{x_2}).x_3)
+ }{\overline{x_1}{-}x_1}
+ &
+ \frac{
+ ((\overline{x_1} + x_2).x_3)
+ {-}
+ ((\overline{x_1} + \overline{x_2}).x_3)
+ }{\overline{x_2}{-}x_2}
+ &
+ \frac{
+ ((\overline{x_1} + \overline{x_2}).\overline{x_3})
+ {-}
+ ((\overline{x_1} + \overline{x_2}).x_3)
+ }{\overline{x_3}{-}x_3}
+\\
+\\
+ \frac{\overline{x_1}.x_3 {-} x_1.x_3}{\overline{x_1}{-}x_1}
+ & 0 &
+\frac{{x_1}.\overline{x_3} {-} x_1.x_3}{\overline{x_3}{-}x_3}
+ \\
+\\
+ \frac{(\overline{x_1}+x_2+x_3){-}(x_1+x_2+x_3)}{\overline{x_1}{-}{x_1}} &
+ \frac{(x_1+\overline{x_2}+x_3){-}(x_1+x_2+x_3)}{\overline{x_2}{-}{x_2}} &
+ \frac{(x_1+x_2+\overline{x_3}){-}(x_1+x_2+x_3)}{\overline{x_3}{-}{x_3}}
+ \end{array}
+ \right)
+ $
+ \end{center}
+ \end{minipage}
+ \label{fig:f:jacobienne}
+ }
+
+ \subfigure[Graphe d'interaction de $f$.]{
+ \begin{minipage}{0.45\textwidth}
+ \begin{center}
+ \includegraphics[scale=0.5]{gf}
+ \end{center}
+ \label{fig:f:interaction}
+ \end{minipage}
+ }
+
+ \subfigure[Matrice d'incidence de $f$.]{
+ \begin{minipage}{0.45\textwidth}
+ \begin{center}
+ $
+ B(f) =
+ \left(
+ \begin{array}{ccc}
+ 1 & 1 & 1 \\
+ 1 & 0 & 1 \\
+ 1 & 1 & 1
+ \end{array}
+ \right)
+ $
+ \end{center}
+ \label{fig:f:incidence}
+ \end{minipage}
+ }
+\end{center}
+\caption{Représentations des dépendances entre les éléments de la fonction $f$ de l'exemple illustratif.}
+\end{figure}
+\end{xpl}
-
-
-\section{Distance sur l'espace $\llbracket 1;n\rrbracket^{\Nats}\times \Bool^n$}\label{sub:metric}
-On considère l'espace $\mathcal{X}=\llbracket 1;n\rrbracket^{\Nats}\times
-\Bool^n$ et
-on définit la distance $d$ entre les points $X=(s,x)$ et
-$X'=(s',x')$ de $\mathcal{X}$ par
-\[
-d(X,X')= d_H(x,x')+d_S(s,s'),~\textrm{où}~
-\left\{
-\begin{array}{l}
-\displaystyle{d_H(x,x')=\sum_{i=1}^n |x_i-x'_i|}\\[5mm]
-\displaystyle{d_S(s,s')=\frac{9}{n}\sum_{t\in\Nats}\frac{|s_t-s'_t|}{10^{t+1}}}.
-\end{array}
-\right.\,.
-\]
-On note que dans le calcul de $d_H(x,x')$--
-appelée \gls{distanceHamming} (cf. glossaire) entre $x$ et $x'$--
-les termes $x_i$ et $x'_i$ sont considérés comme des entiers naturels
-égaux à $0$ ou à $1$ et que le calcul est effectué dans $\Z$.
-De plus, la \gls{partieentiere} (cf. glossaire)
-$\lfloor d(X,X')\rfloor$ est égale à $d_H(x,x')$ soit la distance
-de Hamming entre $x$ et $x'$.
-%D'autre part, $d(X,X')-\lfloor d(X,X')\rfloor=d_S(s,s')$
-%mesure la différence entre $s$ et $s'$.
-On remarque que la partie décimale est inférieure à $10^{-l}$ si
-et seulement si les $l$ premiers termes des deux stratégies sont égaux.
-De plus, si la
-$(l+1)^{\textrm{ème}}$ décimale
-de $d_S(s,s')$
-n'est pas nulle, alors $s_l$ est différent de $s'_l$.
-
-On a démontré que pour toute fonction booléenne $f$,
-$G_f$ est continue sur $\mathcal{X}$ (cf annexe~\ref{anx:cont}).
+\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]$,
+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é.
+
+Plus formellement, une séquence finie $S=(s^t)^{t \in \Nats}$
+est dite \emph{complète} relativement à $[n]$ si
+tout indice de $[n]$
+s'y retrouve au moins une fois.
+
+Parmi toutes les stratégies unaires de
+$[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]$.
+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.
+\end{itemize}
+
+
+François Robert~\cite{Rob95}
+a énoncé en 1995 le théorème suivant de convergence
+dans le mode des itérations unaires.
+
+\begin{theorem}\label{Th:conv:GIA}
+Si le graphe $G(f)$ n'a pas de cycle et si la stratégie unaire est
+pseudo-périodique, alors tout chemin de $\textsc{GIA}(f)$ atteint
+l'unique point fixe $\zeta$ en au plus $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}.
+J. Bahi~\cite{Bah00} a démontré le théorème suivant:
+
+\begin{theorem}\label{Th:Bahi}
+Si le graphe $G(f)$ n'a pas de cycle et si la stratégie généralisée
+est pseudo-périodique alors
+tout chemin de $\textsc{gig}(f)$ finit par atteindre
+l'unique point fixe $\zeta$.
+\end{theorem}
+
+% \section{Distance sur l'espace $\llbracket 1;n\rrbracket^{\Nats}\times \Bool^n$}\label{sub:metric}
+% On considère l'espace $\mathcal{X}=\llbracket 1;n\rrbracket^{\Nats}\times
+% \Bool^n$ et
+% on définit la distance $d$ entre les points $X=(s,x)$ et
+% $X'=(s',x')$ de $\mathcal{X}$ par
+% \[
+% d(X,X')= d_H(x,x')+d_S(s,s'),~\textrm{où}~
+% \left\{
+% \begin{array}{l}
+% \displaystyle{d_H(x,x')=\sum_{i=1}^n |x_i-x'_i|}\\[5mm]
+% \displaystyle{d_S(s,s')=\frac{9}{n}\sum_{t\in\Nats}\frac{|s_t-s'_t|}{10^{t+1}}}.
+% \end{array}
+% \right.\,.
+% \]
+% On note que dans le calcul de $d_H(x,x')$--
+% appelée \gls{distanceHamming} (cf. glossaire) entre $x$ et $x'$--
+% les termes $x_i$ et $x'_i$ sont considérés comme des entiers naturels
+% égaux à $0$ ou à $1$ et que le calcul est effectué dans $\Z$.
+% De plus, la \gls{partieentiere} (cf. glossaire)
+% $\lfloor d(X,X')\rfloor$ est égale à $d_H(x,x')$ soit la distance
+% de Hamming entre $x$ et $x'$.
+% %D'autre part, $d(X,X')-\lfloor d(X,X')\rfloor=d_S(s,s')$
+% %mesure la différence entre $s$ et $s'$.
+% On remarque que la partie décimale est inférieure à $10^{-l}$ si
+% et seulement si les $l$ premiers termes des deux stratégies sont égaux.
+% De plus, si la
+% $(l+1)^{\textrm{ème}}$ décimale
+% de $d_S(s,s')$
+% n'est pas nulle, alors $s_l$ est différent de $s'_l$.
+
+% On a démontré que pour toute fonction booléenne $f$,
+% $G_f$ est continue sur $\mathcal{X}$ (cf annexe~\ref{anx:cont}).
