--- /dev/null
+digraph {
+1 -> 1 [label=" -"]
+1 -> 4 [label=" +-"]
+2 -> 2 [label=" -"]
+2 -> 4 [label=" +-"]
+3 -> 3 [label=" -"]
+3 -> 4 [label=" +-"]
+4 -> 4 [label=" +-"]
+}
\ No newline at end of file
--- /dev/null
+MAIN = main
+SOURCES = $(MAIN).tex abstract.tex intro.tex ddn.tex xpl.tex promela.tex translation.tex proof.tex complexity.tex exp.tex conclusion.tex abbrev.bib biblioand.bib
+LOG=logLatex
+
+pdf: $(MAIN).pdf
+
+$(MAIN).pdf: $(SOURCES)
+ @printf "***** Compilation 1 *****\n"
+ @pdflatex $(MAIN) > $(LOG)
+ @printf "***** Biblio *****\n"
+ @bibtex $(MAIN) >> $(LOG)
+ @printf "***** Compilation 2 *****\n"
+ @pdflatex $(MAIN) >> $(LOG)
+ @printf "***** Compilation 3 *****\n"
+ @pdflatex $(MAIN) >> $(LOG)
+
+all:
+ latex $(MAIN).tex > $(LOG)
+ latex $(MAIN).tex >> $(LOG)
+ bibtex $(MAIN) >> $(LOG)
+ latex $(MAIN).tex >> $(LOG)
+ dvips -t a4 $(MAIN).dvi -o >> $(LOG)
+ ps2pdf $(MAIN).ps >> $(LOG)
+
+fast:
+ latex $(MAIN).tex > $(LOG)
+ dvips -t a4 $(MAIN).dvi -o >> $(LOG)
+ ps2pdf $(MAIN).ps >> $(LOG)
+
+test:
+ acroread $(MAIN).pdf
+
+testr:
+ kghostview $(MAIN).ps
+
+clean:
+ rm -rf *~ *.aux *.log *.bbl *.blg *.dvi *.bak *.thm *.lof *.loe *.lot *.out *.toc
+
+
+# construit l'archive toute prete (pour Springer)
+TEXSOURCES = main.tex ddn.tex
+PACKAGES = mathpartir.sty synttree.sty bcprules.sty arydshln.sty
+CLSSTY = llncs.cls llncsdoc.sty splncs.bst sprmindx.sty
+UTIL = Makefile copyright.pdf CL07-CameraReady.pdf readme
+FILES = $(TEXSOURCES) $(PACKAGES) $(CLSSTY) $(UTIL)
+
+arch:
+ zip Archive.zip $(FILES)
+
--- /dev/null
+\JFC{Voir section~\ref{sec:spin:proof}}
+
--- /dev/null
+Montrons que pour toute fonction booléenne
+$f$ de $\Bool^n$ dans lui même, $G_f$ est continue sur $(\mathcal{X},d)$.
+
+Soit donc $(s_t,x^t)^{t \in \Nats}$ une suite de points de
+l'espace $\mathcal{X}$ qui converge vers $(s,x)$.
+Montrons que $(G_f (s_t,x^t))^{t \in \Nats}$ converge vers $G_f (s,x)$.
+
+La distance $d((s_t,x^t), (s,x))$ tend vers 0.
+Il en est donc de même pour $d_H(x^t, x)$ et $d_S(s_t, s)$.
+Or, $d_H(x^t, x)$ ne prend que des valeurs entières.
+Cette distance est donc nulle à partir d'un certain $t_0$.
+Ainsi, à partir de $t>t_0$, on a $x^t = x$ .
+De plus, $d_S(s_t, s)$ tend vers $0$ donc $d_S(s_t, s) < 10^{-1}$
+à partir d'un certain rang $t_1$.
+Ainsi, à partir de $t>t_1$, les suites $(s_t)_{t \in \Nats}$
+ont toutes le même premier terme, qui est celui
+de $s$ pour $t$ supérieur à $t_1$.
+Pour $t > \max(t_0,t_1)$, les configurations $x^t$ et $x$
+sont les mêmes,
+et les stratégies $s_t$ et $s$ ont le même premier terme
+($s_0^t = s_0$), donc les configurations
+de $F_f(s_0^t,x^t)$ et de $F_f (s_0,x)$ sont égales et donc la distance
+entre $G_f(s_t,x^t)$ et $G_f (s,x)$ est inférieure à 1.
+
+Montrons maintenant que la distance entre
+$G_f (s_t,x^t)$ et $G_f (s,x)$
+tend bien vers 0 quand $t$ tend vers $+\infty$. Soit $\epsilon > 0$.
+\begin{itemize}
+ \item Si $\epsilon \ge 1$. Comme la distance $d(G_f(s_t,x^t), G_f (s,x))<1$
+ pour $t > \max(t_0, t_1)$, alors
+ $d(G_f(s_t,x^t), G_f (s,x))<\epsilon$
+ \item Si $\epsilon < 1$, alors $\exists k \in \Nats \textrm{ tel que }
+ 10^{-k} > \epsilon > 10^{-(k+1)}$.
+ Comme $d_S(s_t, s)$ tend vers 0, il existe
+un rang $t_2$ à partir duquel
+$\forall t > t_2 , d_S(s_t, s) < 10^{-(k+2)}$:
+à partir de ce rang, les $k+2$ premiers termes de $s_t$ sont ceux de $s$.
+Donc les $k + 1$ premiers termes des stratégies de
+$G_f (s_t,x^t)$ et de
+$G_f (s,x)$ sont les mêmes (puisque $G_f$
+opère un décalage sur les stratégies), et vue la
+définition de $d_S$, la partie décimale de la distance entre les points
+$(s_t,x^t)$ et $(s,x)$ est
+inférieure à $10^{-(k+1)} \le \epsilon$.
+\end{itemize}
+Pour conclure, pour tout $\epsilon > 0$,
+$\exists~T_0 = \max(t_0, t_1, t_2) \in \Nats \textrm{ tel que }
+\forall t > T_0 , d (Gf (s_t,x^t),G_f (s,x))< \epsilon$.
--- /dev/null
+Soit $\alpha\in\Bool$.
+On nomme $f^{\alpha}$ la fonction de $\Bool^{n-1}$
+dans lui-même définie pour
+chaque $x\in\Bool^{n-1}$ par
+\[
+f^{\alpha}(x)=(f_1(x,\alpha),\dots,f_{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$.
+
+
+
+
+Énonçons et prouvons tout d'abord les lemmes techniques suivants:
+
+\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$).
+\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
+$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^\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$.
+Alors, il existe
+$x\in\Bool^{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
+avec les hypothèses.
+Ainsi $f_{ij}(x,\alpha)$ est égal à $s$.
+On a donc aussi
+$f^{\alpha}_{ij}(x)=s$. Ainsi $G(f^\alpha)$ possède un arc
+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.
+\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}$.
+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)$.
+\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
+du théorème.
+Si $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.
+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$.
+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.
+Ainsi, d'après le lemme~\ref{lemma:iso},
+$\Gamma(f)^0$ et $\Gamma(f)^1$ sont fortement
+connexes.
+Pour prouver que $\Gamma(f)$ est fortement connexe, il suffit
+de prouver que $\Gamma(f)$ contient un arc $x\to y$ avec
+$x_n=0<y_n$ et un arc $x\to y$ avec $x_n=1>y_n$.
+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).
+\end{equation}
+
+On suppose tout d'abord que $n$ a une boucle
+négative.
+Alors, d'après la définition de
+$G(f)$, il existe $x\in\Bool^n$ tel que $f_{nn}(x)<0$.
+Ainsi si $x_n=0$, on a $f_n(x)>f_n(\overline{x}^n)$, et donc
+$x_n=0\neq f_n(x)$ et
+$\overline{x}^n_n=1\neq f_n(\overline{x}^n)$;
+et si $x_n=1$, on a
+$f_n(x)<f_n(\overline{x}^n)$, donc $x_n=1\neq f_n(x)$ et $\overline{x}^n_n=0\neq
+f_n(\overline{x}^n)$.
+Dans les deux cas, la condition ($*$) est établie.
+
+Supposons maintenant que $n$ n'a pas de boucle négative.
+D'après la seconde hypothèse,
+$n$ n'a pas de boucle, \emph{i.e.}, la valeur de $f_n(x)$
+ne dépend pas de la valeur de $x_n$.
+D'après la troisième hypothèse,
+il existe $i\in \llbracket 1;n \rrbracket$ tel que $G(f)$ a un arc de
+$i$ vers $n$.
+Ainsi, il existe $x \in \Bool^n$ tel que $f_{ni}(x) \neq 0$ et donc
+%$n$ n'est donc pas de degré zéro dans $G(f)$, \emph{i.e.}
+$f_n$ n'est pas constante.
+Ainsi, il existe $x,y\in \Bool^n$ tel que
+$f_n(x)=1$ et $f_n(y)=0$.
+Soit $x'=(x_1,\dots,x_{n-1},0)$ et
+$y'=(y_1,\dots,y_{n-1},1)$.
+Puisque la valeur de $f_n(x)$
+(resp. de $f_n(y)$) ne dépend pas de la valeur de $x_n$ (resp. de $y_n$),
+on a $f_n(x')=f_n(x)=1\neq x'_n$ (resp. $f_n(y')=f_n(y)=0\neq
+y'_n$).
+Ainsi la condition ($*$) est établie, et le théorème est prouvé.
+\end{Proof}
+
+
+
--- /dev/null
+digraph {
+ 00 -> 00
+ 00 -> 10
+ 01 -> 00
+ 01 -> 11
+ 10 -> 11
+ 10 -> 00
+ 11 -> 10
+ 11 -> 01
+}
--- /dev/null
+\newglossaryentry{graphoriente}{name=graphe orienté, 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$.}}
+
+\newglossaryentry{graphfortementconnexe}{name=graphe fortement connexe, 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$.}
+}
+
+
+\newglossaryentry{distributionuniforme}{name=distribution uniforme, 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é.}
+}
+
+
+\newglossaryentry{partieentiere}{name=partie entière, 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$.
+},
+symbol={\ensuremath{\lfloor x \rfloor}}
+}
+
+
+\newglossaryentry{distanceHamming}{name=distance de Hamming, 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$.
+}}
+
+
+
+\newglossaryentry{decalageDeBits}{name=décalage de bits,
+plural=dé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).
+}}
+
+
+
+\newglossaryentry{chaineDeMarkov}{name=chaîne de Markov,
+plural=chaî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
+$
+%\begin{array}{l}
+\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).
+%\end{array}
+$
+}}
+
+
+\newglossaryentry{vecteurDeProbabilite}{name=vecteur de probabilités,
+plural=vecteurs de probabilités, description={
+Un vecteur de probabilités est un vecteur tel que toutes ses composantes
+sont positives ou nulles et leur somme vaut 1.}}
+
+\newglossaryentry{matriceDAdjacence}{name=matrice d'adjacence, 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$.}}
+
+
+\newglossaryentry{xor}{name=ou exclusif, 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.},
+symbol={\ensuremath{\oplus}}
+}
+
+\newglossaryentry{matriceDeTransitions}{name=matrice de transitions, 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$.}}
\ No newline at end of file
--- /dev/null
+digraph{
+ 1 -> 1 [label=" -"]
+ 1 -> 2 [label=" +"]
+ 2 -> 2 [label=" -"]
+}
\ No newline at end of file
--- /dev/null
+digraph {
+ 00 -> 00
+ 00 -> 10
+ 01 -> 11
+ 01 -> 01
+ 10 -> 11
+ 10 -> 00
+ 11 -> 10
+ 11 -> 01
+}
--- /dev/null
+digraph{
+ 1 -> 1 [label=" -"]
+ 1 -> 2 [label=" +-"]
+ 2 -> 2 [label=" +-"]
+}
\ No newline at end of file
--- /dev/null
+digraph {
+1 -> 1 [label=" -"]
+1 -> 4 [label=" +-"]
+2 -> 2 [label=" -"]
+2 -> 4 [label=" +-"]
+3 -> 3 [label=" -"]
+3 -> 4 [label=" +-"]
+4 -> 4 [label=" +-"]
+}
\ No newline at end of file
--- /dev/null
+digraph {
+ 00 -> 00
+ 00 -> 10
+ 01 -> 00
+ 01 -> 11
+ 10 -> 11
+ 10 -> 00
+ 11 -> 10
+ 11 -> 01
+}
--- /dev/null
+digraph{
+ 1 -> 1 [label=" -"]
+ 1 -> 2 [label=" +"]
+ 2 -> 2 [label=" -"]
+}
\ No newline at end of file
--- /dev/null
+digraph {
+ 00 -> 00
+ 00 -> 10
+ 01 -> 11
+ 01 -> 01
+ 10 -> 11
+ 10 -> 00
+ 11 -> 10
+ 11 -> 01
+}
--- /dev/null
+digraph{
+ 1 -> 1 [label=" -"]
+ 1 -> 2 [label=" +-"]
+ 2 -> 2 [label=" +-"]
+}
\ No newline at end of file
--- /dev/null
+This is pdfTeX, Version 3.1415926-1.40.10 (TeX Live 2009/Debian) (format=pdflatex 2010.9.1) 31 MAR 2011 21:10
+entering extended mode
+ restricted \write18 enabled.
+ %&-line parsing enabled.
+**main.tex
+
+! Emergency stop.
+<*> main.tex
+
+End of file on the terminal!
+
+
+Here is how much of TeX's memory you used:
+ 3 strings out of 495061
+ 105 string characters out of 1182622
+ 45108 words of memory out of 3000000
+ 3282 multiletter control sequences out of 15000+50000
+ 3640 words of font info for 14 fonts, out of 3000000 for 9000
+ 28 hyphenation exceptions out of 8191
+ 0i,0n,0p,1b,6s stack positions out of 5000i,500n,10000p,200000b,50000s
+! ==> Fatal error occurred, no output PDF file produced!
--- /dev/null
+Subproject commit 15fc32dafcfefd531b8e19721d3e66d22b269b8c
--- /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={},%
+%
+}%
+}%
--- /dev/null
+%% Use the standard UP-methodology class
+%% with French language.
+%%
+%% You may specify the option 'twoside' or 'oneside' for
+%% the document.
+%%
+%% See the documentation tex-upmethodology on
+%% http://www.arakhne.org/tex-upmethodology/
+%% for details about the macros that are provided by the class and
+%% to obtain the list of the packages that are already included.
+
+\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[utf8]{inputenc}
+
+%%--------------------
+%% Search path for pictures
+%\graphicspath{{path1/},{path2/}}
+
+%%--------------------
+%% Definition of the bibliography entries
+\declarebiblio{J}{Journaux internationaux avec comités de lecture}{mabiblio}
+
+%%--------------------
+%% Title of the document
+\declarehdr{Title}{XX Mois XXXX}
+
+%%--------------------
+%% Set the author of the HDR
+\addauthor[first.name@utbm.fr]{First}{Name}
+
+%%--------------------
+%% Add a member of the jury
+%% \addjury{Firstname}{Lastname}{Role in the jury}{Position}
+\addjury{First}{Name}{Rapporteur}{Professeur à l'Université de XXX}
+\addjury{First}{Name}{Examinateur}{Professeur à l'Université de XXX}
+
+%%--------------------
+%% Change the style of the text in the list of the members of the jury.
+%% \Set{jurystyle}{ style of the text}
+%\Set{jurystyle}{\small}
+
+%%--------------------
+%% Set the University where HDR was made
+\hdrpreparedin{Université de Technologie de Belfort-Montbéliard}
+
+%%--------------------
+%% Set the English abstract
+%\hdrabstract[english]{This is the abstract in English}
+
+%%--------------------
+%% Set the English keywords. They only appear if
+%% there is an English abstract
+%\hdrkeywords[english]{Keyword 1, Keyword 2}
+
+%%--------------------
+%% Set the French abstract
+\hdrabstract[french]{Blabla blabla.}
+
+%%--------------------
+%% Set the French keywords. They only appear if
+%% there is an French abstract
+%\hdrkeywords[french]{Mot-cl\'e 1, Mot-cl\'e 2}
+
+%%--------------------
+%% Change the layout and the style of the text of the "primary" abstract.
+%% If your document is written in French, the primary abstract is in French,
+%% otherwise it is in English.
+\Set{primaryabstractstyle}{\small}
+
+%%--------------------
+%% Change the layout and the style of the text of the "secondary" abstract.
+%% If your document is written in French, the secondary abstract is in English,
+%% otherwise it is in French.
+%\Set{secondaryabstractstyle}{\tiny}
+
+%%--------------------
+%% Change the layout and the style of the text of the "primary" keywords.
+%% If your document is written in French, the primary keywords are in French,
+%% otherwise they are in English.
+%\Set{primarykeywordstyle}{\tiny}
+
+%%--------------------
+%% Change the layout and the style of the text of the "secondary" keywords.
+%% If your document is written in French, the secondary keywords are in English,
+%% otherwise they are in French.
+%\Set{secondarykeywordstyle}{\tiny}
+
+%%--------------------
+%% Change the speciality of the PhD thesis
+%\Set{speciality}{Informatique}
+
+%%--------------------
+%% Change the institution
+%\Set{universityname}{Universit\'e de Technologie de Belfort-Montb\'eliard}
+
+%%--------------------
+%% Add the logo of a partner or a sponsor
+%\addpartner{partner_logo}
+\newcommand{\JFC}[1]{\begin{color}{green}\textit{#1}\end{color}}
+\newcommand{\vectornorm}[1]{\ensuremath{\left|\left|#1\right|\right|_2}}
+\newcommand{\ie}{\textit{i.e.}}
+\newcommand{\Nats}[0]{\ensuremath{\mathbb{N}}}
+\newcommand{\Reels}[0]{\ensuremath{\mathbb{R}}}
+\newcommand{\Zed}[0]{\ensuremath{\mathbb{Z}}}
+\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{\Fig}[1]{Fig.\,\ref{#1}}
+\newcommand{\Alg}[1]{Algorithm~\ref{#1}}
+\newcommand{\Tab}[1]{Table~\ref{#1}}
+\newcommand{\Equ}[1]{(\ref{#1})}
+\newcommand{\deriv}{\mathrm{d}}
+\newcommand{\class}[1]{\ensuremath{\langle #1\rangle}}
+\newcommand{\dom}[0]{\ensuremath{\textit{dom}}}
+
+
+\newtheorem{theorem}{Théorème}
+\newtheorem{lemma}{Lemme}
+\newtheorem{xpl}{Exemple}
+\newtheorem{Proof}{Preuve}
+
+\begin{document}
+\input{glossaire.tex}
+
+% \chapter*{Remerciements}
+
+% Blabla blabla.
+
+% \tableofcontents
+
+
+
+
+
+\chapter*{Introduction}
+
+Blabla blabla.
+
+\mainmatter
+
+\part{Système Booléens}
+
+\chapter{Iterations discrètes de Systèmes Dynamiques booléens}
+
+\JFC{Chapeau chapitre à faire}
+\input{sdd}
+
+
+\chapter[Preuve de convergence de systèmes booléens]{Preuve automatique de convergence de systèmes booléens}
+\input{modelchecking}
+
+
+
+
+\JFC{Mixage}
+
+
+
+
+
+
+% \part{Conclusion et Perspectives}
+
+% \chapter{Conclusion}
+
+% Blabla blabla.
+
+
+\appendix
+
+\chapter{Preuves sur les SDD}
+
+\section{Preuve du théorème~\ref{th:Adrien}}\label{anx:sccg}
+\input{annexesccg}
+
+\section{Preuve de continuité de $G_f$ dans $(\mathcal{X},d)$}\label{anx:cont}
+\input{annexecontinuite.tex}
+
+\section{Preuve de Correction et de complétude de l'approche de vérification de convergence à l'aide de SPIN}
+\input{annexePromelaProof}
+
+\backmatter
+
+\bibliographystyle{apalike}
+\bibliography{abbrev,biblioand}
+\listoffigures
+\listoftables
+\listofdefinitions
+
+\end{document}
+
+
+
+
+
--- /dev/null
+
+
+
+\section{Rappels sur le langage PROMELA}
+\label{sec:spin:promela}
+
+Cette section rappelle les éléments fondamentaux du langage PROMELA (Process Meta Language).
+On peut trouver davantage de détails dans~\cite{Hol03,Wei97}.
+
+
+
+
+\begin{figure}[ht]
+\begin{scriptsize}
+\begin{lstlisting}
+#define N 3
+#define d_0 5
+
+bool X [N]; bool Xp [N]; int mods [N];
+typedef vals{bool v [N]};
+vals Xd [N];
+
+typedef a_send{chan sent[N]=[d_0] of {bool}};
+a_send channels [N];
+
+chan unlock_elements_update=[1] of {bool};
+chan sync_mutex=[1] of {bool};
+\end{lstlisting}
+\end{scriptsize}
+\caption{Type declaration of the DDNs translation.}
+\label{fig:arrayofchannels}
+\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 declarer des tableaux à une dimension de taille constante
+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
+dimension.
+
+\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:
+\begin{itemize}
+\item les constantes \verb+N+ et \verb+d_0+ qui précisent respectivement le numbre
+ $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ène dynamique discret
+(le décallage d'un entier est dû à l'indexation à partir de zéro des cellules d'un tableau);
+Elles memorisent 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'iteration
+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}$).
+\end{itemize}
+
+
+Puisque le décallage d'un indices ne change pas fondamentalement
+le comportement de la version PROMELA par rapport au modèle initial
+et pour des raisons de clareté, 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écallage devra être conservé mémoire.
+
+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 cannal.
+Dans l'exemple précédent, on déclare successivement:
+\begin{itemize}
+\item un cannal \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$.
+\item les deux cannaux \verb+unlock_elements_update+ et \verb+sync_mutex+ contenant
+chacun un message booléen et utilisé ensuite comme des sémaphores.
+\end{itemize}
+\end{xpl}
+
+%\subsection{PROMELA Processes}
+Le langage PROMELA exploite la notion de \emph{process} pour modéliser la concurence
+au sein de systèmes. Un process est déclaréavec le mot-clef
+\verb+proctype+ et est instancié soit imé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
+d'initialiser les variables, lancer d'autres processes\ldots
+
+
+Les instructions d'affecatation sont interprétées usuellement.
+Les cannaux sont cernés par des instructions particulières d'envoi et de
+réception de messages. Pour un cannal
+\verb+ch+, ces instruction sont respectivement notées
+\verb+ch ! m+ et \verb+ch ? m+.
+L'instruction de réception consomme la valeur en tête du cannal \verb+ch+
+et l'affecte à la variable \verb+m+ (pour peu que \verb+ch+ soit initialisé et non vide).
+De manière similaire,l'instruction d'envoi ajoute la valeur de \verb+m+ à la queue du canal
+\verb+ch+ (pour peu que celui-ci soit initialisé et non rempli).
+Dans les cas problématiques, canal non initialisé et vide pour une reception ou bien rempli pour un envoi,
+le processus est blocké jusqu'à ce que les conditions soient remplies.
+
+La structures de contrôle \verb+if+ (resp. \verb+do+) définit un choix non déterministe
+ (resp. une boucle non déterministe). Que ce soit pour la conditionnelle ou la boucle,
+si plus d'une des conditions est établie, l'ensemble des instructions correspondantes
+sera choisi aléatoirement puis exécuté.
+
+Dans le process \verb+init+ détaillé à la {\sc Figure}~\ref{fig:spin:init},
+une boucle de taille $N$ initialise aléatoirement la variable globale de type tableau \verb+Xp+.
+Ceci permet par la suite de verifier si les itérations sont convergentes pour n'importe
+quelle configuration initiale $X^{(0)}$.
+
+
+
+Pour chaque élément $i$, si les itérations sont asynchrones
+\begin{itemize}
+\item on stocke d'abord la valeur de \verb+Xp[i]+ dans chaque \verb+Xd[j].v[i]+
+puisque la matrice $S^0$ est égale à $(0)$,
+\item puis, la valeur de $i$ (représentée par \verb+Xp[i]+) devrait être transmise
+ à $j$ s'il y a un arc de $i$ à $j$ dans le graphe d'incidence. Dans ce cas,
+ c'est la fonction \verb+hasnext+ (non détaillée ici)
+ \JFC{la détailler}
+ qui memorise ce graphe
+ en fixant à \texttt{true} la variable \verb+is_succ+, naturellement et à
+ \texttt{false} dans le cas contraire.
+ Cela permet d'envoyer la valeur de $i$ dans le canal au travers de \verb+channels[i].sent[j]+.
+\end{itemize}
+
+\begin{figure}[t]
+ \begin{minipage}[h]{.52\linewidth}
+\begin{scriptsize}
+\begin{lstlisting}
+init{
+ int i=0; int j=0; bool is_succ=0;
+ do
+ ::i==N->break;
+ ::i< N->{
+ if
+ ::Xp[i]=0;
+ ::Xp[i]=1;
+ fi;
+ j=0;
+ do
+ ::j==N -> break;
+ ::j< N -> Xd[j].v[i]=Xp[i]; j++;
+ od;
+ j=0;
+ do
+ ::j==N -> break;
+ ::j< N -> {
+ hasnext(i,j);
+ if
+ ::(i!=j && is_succ==1) ->
+ channels[i].sent[j] ! Xp[i];
+ ::(i==j || is_succ==0) -> skip;
+ fi;
+ j++;}
+ od;
+ i++;}
+ od;
+ sync_mutex ! 1;
+}
+\end{lstlisting}
+\end{scriptsize}
+\caption{PROMELA init process.}\label{fig:spin:init}
+\end{minipage}\hfill
+ \begin{minipage}[h]{.42\linewidth}
+\begin{scriptsize}
+\begin{lstlisting}
+active proctype scheduler(){
+ do
+ ::sync_mutex ? 1 -> {
+ int i=0; int j=0;
+ do
+ :: i==N -> break;
+ :: i< N -> {
+ if
+ ::skip;
+ ::mods[j]=i; j++;
+ fi;
+ i++;}
+ od;
+ ar_len=i;
+ unlock_elements_update ! 1;
+ }
+ od
+}
+\end{lstlisting}
+\end{scriptsize}
+\caption{Scheduler process for common pseudo-periodic strategy.
+ \label{fig:scheduler}}
+\end{minipage}
+\end{figure}
+
+
+
+\section{Du système booléen au modèle PROMELA}
+\label{sec:spin:translation}
+Les éléments principaux des itérations asynchrones rappelées à l'équation
+(\ref{eq:async}) sont la stratégie, la fonctions et la gestion des délais.
+Dans cette section, nous présentons successivement comment chacune de
+ces notions est traduite vers un modèle PROMELA.
+
+
+\subsection{La stratégie}\label{sub:spin:strat}
+Regardons comment une stratégie pseudo-périodique peut être représentée en PROMELA.
+Intuitivement, un process \verb+scheduler+ (comme représenté à la {\sc Figure}~\ref{fig:scheduler})
+est itérativement appelé pour construire chaque $S^t$ représentant
+les éléments possiblement mis à jour à l'itération $t$.
+
+Basiquement, le process est une boucle qui est débloquée lorsque la valeur du sémaphore
+\verb+sync_mutex+ est 1. Dans ce cas, les éléments à modifier sont choisis
+aléatoirement (grâce à $n$ choix successifs) et sont mémorisés dans le tableau
+\verb+mods+, dont la taille est \verb+ar_len+.
+Dans la séquence d'éxécution, le choix d'un élément mis à jour est directement
+suivi par des mis àjour: ceci est réalisé grace à la modification de la valeur du sémaphore
+ \verb+unlock_elements_updates+.
+
+\subsection{Applying the function $F$}\label{sub:spin:update}
+Updating a set $S^t=\{s_1,\ldots, s_m\}$ of elements that occur in the strategy
+$(S^t)^{t \in \Nats}$ is implemented by the \verb+update_elems+ process given
+in~\ref{fig:proc}. This active process waits until it is unlocked by the
+\verb+scheduler+ process through the semaphore \verb+unlock_elements_update+.
+The implementation is then fivefold:
+
+\begin{enumerate}
+\item it starts with updating the variable \texttt{X} with the values of \texttt{Xp}
+ thanks to the \texttt{update\_X} function (not detailed here);
+ %%we recall that the variable \texttt{X} is only defined as
+\item it stores in \texttt{Xd} the current available values of the elements thanks
+ to the function \texttt{fetch\_values} (see \Sec{sub:spin:vt});
+\item a loop over the number \texttt{ar\_len} of elements that have to evolve
+ iteratively updates the value of $j$ (through the function call \texttt{F(j)})
+ provided this has to evolve, \textit{i.e.}, it is referenced by
+ \texttt{mods[count]}; source code of \texttt{F} is given in~\ref{fig:p} and is a
+ direct translation of the map $F$;
+\item the new components values in \texttt{Xp} are symbolically sent to the other
+ components requiring them % for future access
+ thanks to the \texttt{diffuse\_values(Xp)} function (see \Sec{sub:spin:vt});
+\item finally, this process informs the scheduler about the end of the task
+ (through the semaphore \texttt{sync\_mutex}).
+\end{enumerate}
+
+
+\begin{figure}[t]
+ \begin{minipage}[h]{.475\linewidth}
+\begin{scriptsize}
+\begin{lstlisting}
+active proctype update_elems(){
+ do
+ ::unlock_elements_update ? 1 ->
+ {
+ atomic{
+ bool is_succ=0;
+ update_X();
+ fetch_values();
+ int count = 0;
+ int j = 0;
+ do
+ ::count == ar_len -> break;
+ ::count < ar_len ->
+ j = mods[count];
+ F(j);
+ count++;
+ od;
+ diffuse_values(Xp);
+ sync_mutex ! 1
+ }
+ }
+ od
+}
+\end{lstlisting}
+\end{scriptsize}
+\caption{Updatings of the elements.}\label{fig:proc}
+ \end{minipage}\hfill%
+%\end{figure}
+%\begin{figure}
+ \begin{minipage}[h]{.45\linewidth}
+\begin{scriptsize}
+\begin{lstlisting}
+inline F(){
+ if
+ ::j==0 -> Xp[0] =
+ (Xs[j].v[0] & !Xs[j].v[1])
+ |(Xs[j].v[2])
+ ::j==1 -> Xp[1] = Xs[j].v[0]
+ | !Xs[j].v[2]
+ ::j==2 -> Xp[2] = Xs[j].v[1]
+ & Xs[j].v[2]
+ fi
+}
+\end{lstlisting}
+\end{scriptsize}
+\caption{Application of function $F$.}\label{fig:p}
+ \end{minipage}
+\end{figure}
+
+% \subsection{Modifying Values of one Element}
+
+% Each element $i$ may modify its value through the coresponding
+% active process \verb+pi+.
+% In Fig.~\ref{fig:p4} that gives the translation of
+% modifying the element $4$, the process is waiting until it is unlocked
+% and then it computes the new value of $X_4$, represented by $X'_4$
+% and memorized as \verb+Xp[4]+.
+
+
+% \begin{ProofCr}
+
+% First of all, the second hypothesis of the previous proof is established.
+
+% In this part, we prove that for any time $t$,
+
+% The proof is achieved under the hypothesis that at current time $t$,
+
+% For $j$ in $J^t$, variables
+% \verb+v0+, \ldots \verb+vn-1+ are respectively
+% $X_0^{S_{j0}^t},\ldots, X_{n-1}^{S_{jn-1}^t}$.
+% Since \verb+F+ is the direct translation of $F$, rest of the proof is obvious.
+
+
+% \end{ProofCr}
+
+\subsection{Delays Handling}\label{sub:spin:vt}
+This section shows how delays are translated into PROMELA through the two
+functions \verb+fetch_values+ and \verb+diffuse_values+, given in~\ref{fig:val} and~\ref{fig:broadcast}, that respectively store and transmit the
+element values.
+
+\begin{figure}[t]
+ \begin{minipage}[h]{.475\linewidth}
+\begin{scriptsize}
+\begin{lstlisting}
+inline fetch_values(){
+ int countv = 0;
+ do
+ :: countv == ar_len -> break ;
+ :: countv < ar_len ->
+ j = mods[countv];
+ i = 0;
+ do
+ :: (i == N) -> break;
+ :: (i < N && i == j) -> {
+ Xd[j].v[i] = Xp[i] ;
+ i++ }
+ :: (i < N && i != j) -> {
+ hasnext(i,j);
+ if
+ :: skip
+ :: is_succ==1 &&
+ nempty(channels[i].sent[j]) ->
+ channels[i].sent[j] ?
+ Xd[j].v[i];
+ fi;
+ i++ }
+ od;
+ countv++
+ od
+}
+\end{lstlisting}
+\end{scriptsize}
+\caption{Fetching of the elements values\label{fig:val}}
+ \end{minipage}\hfill%
+ \begin{minipage}[h]{.475\linewidth}
+\begin{scriptsize}
+\begin{lstlisting}
+inline diffuse_values(values){
+ int countb=0;
+ do
+ :: countb == ar_len -> break ;
+ :: countb < ar_len ->
+ j = mods[countb];
+ i = 0 ;
+ do
+ :: (i == N) -> break;
+ :: (i < N && i == j) -> i++;
+ :: (i < N && i != j) -> {
+ hasnext(j,i);
+ if
+ :: skip
+ :: is_succ==1 &&
+ nfull(channels[j].sent[i]) ->
+ channels[j].sent[i] !
+ values[j];
+ fi;
+ i++ }
+ od;
+ countb++
+ od
+}
+\end{lstlisting}
+\end{scriptsize}
+\caption{Diffusion of the elements values}\label{fig:broadcast}
+ \end{minipage}
+\end{figure}
+
+The former potentially updates the array \verb+Xd+ needed by elements that have
+to be modified. For each element in \verb+mods+, identified by the variable
+$j$, the function retrieves the values of the other elements (labeled by $i$)
+whose $j$ depends on. There are two cases:
+\begin{itemize}
+\item since $i$ knows its last value (\textit{i.e.}, $D^t_{ii}$ is always $t$)
+ \verb+Xd[i].v[i]+ is then \verb+Xp[i]+.
+\item otherwise, there are two sub-cases which potentially update the value that
+ $j$ knows about $i$ (that may be chosen in a random way):
+ \begin{itemize}
+ \item from the viewpoint of $j$ the value of $i$ may not change (the
+ \verb+skip+ statement) or is not relevant; this latter case arises when
+ there is no edge from $i$ to $j$ in the incidence graph, \textit{i.e.}, when
+ the value of \verb+is_succ+ that is computed by \verb+hasnext(i,j)+ is 0;
+ then the value of \verb+Xd[j].v[i]+ is not modified;
+ \item otherwise, \verb+Xd[j].v[i]+ is assigned with the value stored in the
+ channel \verb+channels[i].sent[j]+ (provided this one is not empty).
+ Element values are added into this channel during the \verb+diffuse_values+
+ function as follows.
+ \end{itemize}
+\end{itemize}
+
+The \verb+diffuse_values+ function aims at storing the values of $X$ represented by
+\verb+Xp+ in the \verb+channels+. It allows the SPIN model-checker to execute
+the PROMELA model as if it allowed delays between processes.
+% as if computation mode were asynchronous.
+%For that reason, when an iteration has to synchronize the elements $i$ and
+%$j$ (\textit{i.e.} when \verb+sync[j] == sync[i]+ is true),
+% no delay emulation is performed.
+%In the asynchronous mode,
+There are two cases concerning the value of $X_{j}$:
+\begin{itemize}
+\item either it is left out to allow $i$ not to take into account all the values
+ of $j$; this case occurs either through the \verb+skip+ statement or when
+ there is no edge from $j$ to $i$ in the incidence graph;
+\item or it is stored in the channel \verb+channels[j].sent[i]+ (provided it is
+ not full).
+\end{itemize}
+
+Introducing non-determinism both in \verb+fetch_values+ and
+\verb+diffuse_values+ functions is necessary in our context. If the
+non-determinism would be used only in \verb+fetch_values+, then it would not be
+possible for instance to retrieve the value $X_i^{(t)}$ without taking into
+account the value $X_i^{(t-1)}$. On the other hand, if the non-determinism is
+only used in \verb+diffuse_values+, then each time a value is pushed into the
+channel, this value is immediately consumed, which contradicts the notion of
+delays.
+
+\subsection{Discussion}
+A coarse approach could consist in providing one process for each element.
+However, the distance with the mathematical model given in \Equ{eq:async} of
+such a translation would be larger than the method presented along these lines.
+It induces that it would be harder to prove the soundness and completeness of
+such a translation. For that reason we have developed a PROMELA model that is
+as close as possible to the mathematical one.
+
+Notice furthermore that PROMELA is an imperative language which
+often results in generating intermediate states
+(to execute a matrix assignment for
+instance).
+The use of the \verb+atomic+ keyword allows the grouping of
+instructions, making the PROMELA code and the DDN as closed as possible.
+
+\subsection{Universal Convergence Property}
+We are left to show how to formalize into the SPIN model-checker that iterations
+of a DDN with $n$ elements are universally convergent. We first recall that the
+variables \verb+X+ and \verb+Xp+ respectively contain the value of $X$ before
+and after an update. Then, by applying a non-deterministic initialization of
+\verb+Xp+ and applying a pseudo-periodic strategy, it is necessary and
+sufficient to establish the following Linear Temporal Logic (LTL) formula:
+\begin{equation}
+\diamond (\Box \verb+Xp+ = \verb+X+)
+\label{eq:ltl:conv}
+\end{equation}
+where $\diamond$ and $\Box$ have the usual meaning \textit{i.e.}, respectively
+{\em eventually} and {\em always} in the subsequent path. It is worth noticing
+that this property only ensures the stabilization of the system, but it does not
+provide any information over the way the system converges. In particular, some
+indeterminism may still be present under the form of multiple fixed points
+accessible from some initial states.
+
+
+
+\section{Proof of Translation Correctness}\label{sec:spin:proof}
+\JFC{Déplacer les preuves en annexes}
+
+This section establishes the soundness and completeness of the approach
+(Theorems~\ref{Theo:sound} and ~\ref{Theo:completeness}). Technical lemmas are
+first shown to ease the proof of the two theorems.
+
+
+% \begin{Lemma}[Absence of deadlock]\label{lemma:deadlock}
+% Let $\phi$ be a DDN model and $\psi$ be its translation. There is no deadlock
+% in any execution of $\psi$.
+% \end{Lemma}
+% \begin{Proof}
+% In current translation, deadlocks of PROMELA may only be introduced through
+% sending or receiving messages in channels. Sending (resp. receiving) a
+% message in the \verb+diffuse_values+ (resp. \verb+fetch_values+) function is
+% executed only if the channel is not full (resp. is not empty). In the
+% \verb+update_elems+ and \verb+scheduler+ processes, each time one adds a value
+% in any semaphore channel (\verb+unlock_elements_update+ and
+% \verb+sync_mutex+), the corresponding value is read; avoiding deadlocks by the
+% way.
+% \end{Proof}
+
+
+\begin{lemma}[Strategy Equivalence]\label{lemma:strategy}
+ Let $\phi$ be a DDN with strategy $(S^t)^{t \in \Nats}$ and $\psi$ be its
+ translation. There exists an execution of $\psi$ with weak fairness s.t. the
+ scheduler makes \verb+update_elems+ update elements of $S^t$ at iteration $t$.
+\end{lemma}
+\begin{Proof}
+ The proof is direct for $t=0$. Let us suppose it is established until $t$ is
+ some $t_0$. Let us consider pseudo-periodic strategies. Thanks to the weak
+ fairness equity property, \verb+update_elems+ will modify elements of $S^t$ at
+ iteration $t$.
+\end{Proof}
+
+In what follows, let $Xd^t_{ji}$ be the value of
+\verb+Xd[+$j$\verb+].v[+$i$\verb+]+ after the $t^{\text{th}}$ call to the
+function \verb+fetch_values+. Furthermore, let $Y^k_{ij}$ be the element at
+index $k$ in the channel \verb+channels[i].sent[j]+ of size $m$, $m \le
+\delta_0$; $Y^0_{ij}$ and $Y^{m-1}_{ij}$ are respectively the head and the tail
+of the channel. Secondly, let $(M_{ij}^t)^{t \in \{1, 1.5, 2, 2.5,\ldots\}}$ be a
+sequence such that $M_{ij}^t$ is the partial function that associates to each
+$k$, $0 \le k \le m-1$, the tuple $(Y^k_{ij},a^k_{ij},c^k_{ij})$ while entering
+into the \verb+update_elems+ at iteration $t$ where
+% \begin{itemize}
+% \item
+ $Y^k_{ij}$ is the value of the channel \verb+channels[i].sent[j]+
+ at index $k$,
+%\item
+$a^k_{ij}$ is the date (previous to $t$) when $Y^k_{ij}$ has been added and
+%\item
+$c^k_{ij}$ is the first date at which the value is available on $j$. So,
+ the value is removed from the channel $i\rightarrow j$ at date $c^k_{ij}+1$.
+%\end{itemize}
+$M_{ij}^t$ has the following signature:
+\begin{equation*}
+\begin{array}{rrcl}
+M_{ij}^t: &
+\{0,\ldots, \textit{max}-1\} &\rightarrow & E_i\times \Nats \times \Nats \\
+& k \in \{0,\ldots, m-1\} & \mapsto & M_{ij}(k)= (Y^k_{ij},a^k_{ij},c^k_{ij}).
+\end{array}
+\end{equation*}
+
+Intuitively, $M_{ij}^t$ is the memory of \verb+channels[i].sent[j]+ while
+starting the iteration $t$. Notice that the domain of any $M_{ij}^1$ is $\{0\}$
+and $M_{ij}^1(0)=(\verb+Xp[i]+,0,0)$: indeed, the \verb+init+ process
+initializes \verb+channels[i].sent[j]+ with \verb+Xp[i]+.
+
+Let us show how to make the indeterminism inside the two functions\linebreak
+\verb+fetch_values+ and \verb+diffuse_values+ compliant with \Equ{eq:async}.
+The function $M_{ij}^{t+1}$ is obtained by the successive updates of
+$M_{ij}^{t}$ through the two functions\linebreak \verb+fetch_values+ and
+\verb+diffuse_values+. Abusively, let $M_{ij}^{t+1/2}$ be the value of
+$M_{ij}^{t}$ after the former function during iteration $t$.
+
+In what follows, we consider elements $i$ and $j$ both in $\llbracket 1, n
+\rrbracket$ that are updated. At iteration $t$, $t \geq 1$, let
+$(Y^0_{ij},a^0_{ij},c^0_{ij})$ be the value of $M_{ij}^t(0)$ at the beginning of
+\verb+fetch_values+. If $t$ is equal to $c^0_{ij}+1$ then we execute the
+instruction that assigns $Y^0_{ij}$ (\textit{i.e.}, the head value of
+\verb+channels[i].sent[j]+) to $Xd_{ji}^t$. In that case, the function
+$M_{ij}^t$ is updated as follows: $M_{ij}^{t+1/2}(k) = M_{ij}^{t}(k+1)$ for each
+$k$, $0 \le k \le m-2$ and $m-1$ is removed from the domain of $M_{ij}^{t+1/2}$.
+Otherwise (\textit{i.e.}, when $t < c^0_{ij}+1$ or when the domain of $M_{ij}$
+is empty) the \verb+skip+ statement is executed and $M_{ij}^{t+1/2} =
+M_{ij}^{t}$.
+
+In the function \verb+diffuse_values+, if there exists some $\tau$, $\tau\ge t$
+such that \mbox{$D^{\tau}_{ji} = t$}, let $c_{ij}$ be defined by $ \min\{l \mid
+D^{l}_{ji} = t \} $. In that case, we execute the instruction that adds the
+value \verb+Xp[i]+ to the tail of \verb+channels[i].sent[j]+. Then,
+$M_{ij}^{t+1}$ is defined as an extension of $M_{ij}^{t+1/2}$ in $m$ such that
+$M_{ij}^{t+1}(m)$ is $(\verb+Xp[i]+,t,c_{ij})$. Otherwise (\textit{i.e.}, when $\forall l
+\, . \, l \ge t \Rightarrow D^{l}_{ji} \neq t$ is established) the \verb+skip+
+statement is executed and $M_{ij}^{t+1} = M_{ij}^{t+1/2}$.
+
+
+\begin{lemma}[Existence of SPIN Execution]\label{lemma:execution}
+ For any sequences $(S^t)^{t \in \Nats}$,\linebreak $(D^t)^{t \in \Nats}$, for
+ any map $F$ there exists a SPIN execution such that for any iteration $t$, $t
+ \ge 1$, for any $i$ and $j$ in $\llbracket 1, n \rrbracket$ we have the
+ following properties:
+
+\noindent If the domain of $M_{ij}^t$ is not empty, then
+\begin{equation}
+ \left\{
+ \begin{array}{rcl}
+ M_{ij}^1(0) & = & \left(X_i^{D_{ji}^{0}}, 0,0 \right) \\
+ \textrm{if $t \geq 2$ then }M_{ij}^t(0) & = &
+ \left(X_i^{D_{ji}^{c}},D_{ji}^{c},c \right) \textrm{, }
+ c = \min\{l | D_{ji}^l > D_{ji}^{t-2} \}
+ \end{array}
+ \right.
+ \label{eq:Mij0}
+\end{equation}
+\noindent Secondly we have:
+\begin{equation}
+ \forall t'\, .\, 1 \le t' \le t \Rightarrow Xd^{t'}_{ji} = X^{D^{t'-1}_{ji}}_i
+ \label{eq:correct_retrieve}
+\end{equation}
+\noindent Thirdly, for any $k\in S^t$. Then, the value of the computed variable
+\verb+Xp[k]+ at the end of the \verb+update_elems+ process is equal to
+$X_k^{t}$ \textit{i.e.}, $F_{k}\left( X_1^{D_{k\,1}^{t-1}},\ldots,
+ X_{n}^{D_{k\,{n}}^{t-1}}\right)$ at the end of the $t^{\text{th}}$ iteration.
+\end{lemma}
+\begin{Proof}
+The proof is done by induction on the number of iterations.
+
+\paragraph{Initial case:}
+
+For the first item, by definition of $M_{ij}^t$, we have $M_{ij}^1(0) = \left(
+ \verb+Xp[i]+, 0,0 \right)$ that is obviously equal to $\left(X_i^{D_{ji}^{0}},
+ 0,0 \right)$.
+
+Next, the first call to the function \verb+fetch_value+ either assigns the head
+of \verb+channels[i].sent[j]+ to \verb+Xd[j].v[i]+ or does not modify
+\verb+Xd[j].v[i]+. Thanks to the \verb+init+ process, both cases are equal to
+\verb+Xp[i]+, \textit{i.e.}, $X_i^0$. The equation (\ref{eq:correct_retrieve}) is then
+established.
+
+
+For the last item, let $k$, $0 \le k \le n-1$. At the end of the first
+execution\linebreak of the \verb+update_elems+ process, the value of
+\verb+Xp[k]+ is\linebreak $F(\verb+Xd[+k\verb+].v[0]+, \ldots,
+\verb+Xd[+k\verb+].v[+n-1\verb+]+)$. Thus, by definition of $Xd$, it is equal
+to $F(Xd^1_{k\,0}, \ldots,Xd^1_{k\,n-1})$. Thanks to \Equ{eq:correct_retrieve},
+we can conclude the proof.
+
+
+
+\paragraph{Inductive case:}
+
+Suppose now that lemma~\ref{lemma:execution} is established until iteration $l$.
+
+First, if domain of definition of the function $M_{ij}^l$ is not empty, by
+induction hypothesis $M_{ij}^{l}(0)$ is $\left(X_i^{D_{ji}^{c}}, D_{ji}^{c},c
+\right)$ where $c$ is $\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$.
+
+At iteration $l$, if $l < c + 1$ then the \verb+skip+ statement is executed in
+the \verb+fetch_values+ function. Thus, $M_{ij}^{l+1}(0)$ is equal to
+$M_{ij}^{l}(0)$. Since $c > l-1$ then $D_{ji}^c > D_{ji}^{l-1}$ and hence, $c$
+is $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$. Obviously, this implies also that
+$D_{ji}^c > D_{ji}^{l-2}$ and $c=\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$.
+
+We now consider that at iteration $l$, $l$ is $c + 1$. In other words, $M_{ij}$
+is modified depending on the domain $\dom(M^l_{ij})$ of $M^l_{ij}$:
+\begin{itemize}
+\item if $\dom(M_{ij}^{l})=\{0\}$ and $\forall k\, . \, k\ge l \Rightarrow
+ D^{k}_{ji} \neq l$ is established then $\dom(M_{ij}^{l+1})$ is empty and the
+ first item of the lemma is established;
+\item if $\dom(M_{ij}^{l})=\{0\}$ and $\exists k\, . \, k\ge l \land D^{k}_{ji}
+ = l$ is established then $M_{ij}^{l+1}(0)$ is $(\verb+Xp[i]+,l,c_{ij})$ that
+ is added in the \verb+diffuse_values+ function s.t.\linebreak $c_{ij} =
+ \min\{k \mid D^{k}_{ji} = l \} $. Let us prove that we can express
+ $M_{ij}^{l+1}(0)$ as $\left(X_i^{D_{ji}^{c'}},D_{ji}^{c'},c' \right)$ where
+ $c'$ is $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$. First, it is not hard to
+ establish that $D_{ji}^{c_{ij}}= l \geq D_{ji}^{l} > D_{ji}^{l-1}$ and thus
+ $c_{ij} \geq c'$. Next, since $\dom(M_{ij}^{l})=\{0\}$, then between
+ iterations $D_{ji}^{c}+1$ and $l-1$, the \texttt{diffuse\_values} function has
+ not updated $M_{ij}$. Formally we have
+$$
+\forall t,k \, .\, D_{ji}^c < t < l \land k \geq t \Rightarrow D_{ji}^k \neq
+t.$$
+
+Particularly, $D_{ji}^{c'} \not \in \{D_{ji}^{c}+1,\ldots,l-1\}$. We can apply
+the third item of the induction hypothesis to deduce
+$\verb+Xp[i]+=X_i^{D_{ji}^{c'}}$ and we can conclude.
+
+\item if $\{0,1\} \subseteq \dom(M_{ij}^{l})$ then $M_{ij}^{l+1}(0)$ is
+ $M_{ij}^{l}(1)$. Let $M_{ij}^{l}(1)= \left(\verb+Xp[i]+, a_{ij} , c_{ij}
+ \right)$. By construction $a_{ij}$ is $\min\{t' | t' > D_{ji}^c \land
+ (\exists k \, .\, k \geq t' \land D_{ji}^k = t')\}$ and $c_{ij}$ is $\min\{k |
+ D_{ji}^k = a_{ij}\}$. Let us show $c_{ij}$ is equal to $\min\{k | D_{ji}^k >
+ D_{ji}^{l-1} \}$ further referred as $c'$. First we have $D_{ji}^{c_{ij}} =
+ a_{ij} > D_{ji}^c$. Since $c$ by definition is greater or equal to $l-1$ ,
+ then $D_{ji}^{c_{ij}}> D_{ji}^{l-1}$ and then $c_{ij} \geq c'$. Next, since
+ $c$ is $l-1$, $c'$ is $\min\{k | D_{ji}^k > D_{ji}^{c} \}$ and then $a_{ij}
+ \leq D_{ji}^{c'}$. Thus, $c_{ij} \leq c'$ and we can conclude as in the
+ previous part.
+\end{itemize}
+
+
+The case where the domain $\dom(M^l_{ij})$ is empty but the formula $\exists k
+\, .\, k \geq l \land D_{ji}^k = l$ is established is equivalent to the second
+case given above and then is omitted.
+
+
+Secondly, let us focus on the formula~(\ref{eq:correct_retrieve}). At iteration
+$l+1$, let $c'$ be defined as $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$. Two cases
+have to be considered depending on whether $D_{ji}^{l}$ and $D_{ji}^{l-1}$ are
+equal or not.
+\begin{itemize}
+\item If $D_{ji}^{l} = D_{ji}^{l-1}$, since $D_{ji}^{c'} > D_{ji}^{l-1}$, then
+ $D_{ji}^{c'} > D_{ji}^{l}$ and then $c'$ is distinct from $l$. Thus, the SPIN
+ execution detailed above does not modify $Xd_{ji}^{l+1}$. It is obvious to
+ establish that $Xd_{ji}^{l+1} = Xd_{ji}^{l} = X_i^{D_{ji}^{l-1}} =
+ X_i^{D_{ji}^{l}}$.
+\item Otherwise $D_{ji}^{l}$ is greater than $D_{ji}^{l-1}$ and $c$ is thus $l$.
+ According to \Equ{eq:Mij0} we have proved, we have
+ $M_{ij}^{l+1}(0)=(X_i^{D_{ji}^{l}},D_{ji}^{l},l)$. Then the SPIN execution
+ detailed above assigns $X_i^{D_{ji}^{l}}$ to $Xd_{ji}^{l+1}$, which ends the
+ proof of (\ref{eq:correct_retrieve}).
+\end{itemize}
+
+We are left to prove the induction of the third part of the lemma. Let $k$, $k
+\in S^{l+1}$. % and $\verb+k'+ = k-1$.
+At the end of the first execution of the \verb+update_elems+ process, we have
+$\verb+Xp[+k\verb+]+= F(\verb+Xd[+k\verb+][0]+,
+\ldots,\verb+Xd[+k\verb+][+n\verb+-1]+)+$. By definition of $Xd$, it is equal
+to $F(Xd^{l+1}_{k\,0}, \ldots,Xd^{l+1}_{k\,n-1})$. Thanks to
+\Equ{eq:correct_retrieve} we have proved, we can conclude the proof.
+\end{Proof}
+
+
+\begin{lemma}
+ Bounding the size of channels to $\textit{max} = \delta_0$ is sufficient when
+ simulating a DDN where delays are bounded by $\delta_0$.
+\end{lemma}
+
+\begin{Proof}
+ For any $i$, $j$, at each iteration $t+1$, thanks to bounded delays (by
+ $\delta_0$), element $i$ has to know at worst $\delta_0$ values that are
+ $X_j^{t}$, \ldots, $X_j^{t-\delta_0+1}$. They can be stored into any channel
+ of size $\delta_0$.
+\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}
+\begin{Proof}
+% For the case where the strategy is finite, one notice that property
+% verification is achieved under weak fairness property. Instructions that
+% write or read into \verb+channels[j].sent[i]+ are continuously enabled leading
+% to convenient available dates $D_{ji}$. It is then easy to construct
+% corresponding iterations of the DDN that are convergent.
+% \ANNOT{quel sens donnes-tu a \emph{convenient} ici ?}
+
+ Let us show the contraposition of the theorem. The previous lemmas have shown
+ that for any sequence of iterations of the DDN, there exists an execution of
+ the PROMELA model that simulates them. If some iterations of the DDN are
+ divergent, then they prevent the PROMELA model from stabilizing, \textit{i.e.}, not
+ verifying the LTL property (\ref{eq:ltl:conv}).
+\end{Proof}
+
+
+% \begin{Corol}[Soundness wrt universall convergence property]\label{Theo:sound}
+% Let $\phi$ be a DDN model where strategy, $X^(0)$
+% are only constrained to be pseudo-periodic and
+% in $E$ respectively.
+% Let $\psi$ be its translation.
+% If all the executions of $\psi$ converge,
+% then iterations of $\phi$ are universally convergent.
+% \end{Corol}
+
+
+
+\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
+ pseudo-periodic since weak fairness property is taken into account.
+
+% i.e. iterations that are divergent. Executions are
+% performed under weak fairness property; we then detail what are continuously
+% enabled:
+% \begin{itemize}
+% \item if the strategy is not defined as periodic, elements $0$, \ldots, $n$ are
+% infinitely often updated leading to pseudo-periodic strategy;
+% \item instructions that write or read into \verb+channels[j].sent[i]+ are
+% continuously enabled leading to convenient available dates $D_{ji}$.
+% \end{itemize}
+% The simulated DDN does not stabilize and its iterations are divergent.
+ \end{Proof}
+
+
+
+\section{Practical Issues}
+\label{sec:spin:practical}
+This section first gives some notes about complexity and later presents
+experiments.
+%\subsection{Complexity Analysis}
+%\label{sub:spin:complexity}
+\begin{theorem}[Number of states]
+ Let $\phi$ be a DDN model with $n$ elements, $m$ edges in the incidence graph
+ and $\psi$ be its translation into PROMELA. The number of configurations of
+ the $\psi$ SPIN execution is bounded by $2^{m\times(\delta_0+1)+n(n+2)}$.
+\end{theorem}
+\begin{Proof}
+ A configuration is a valuation of global variables. Their number only depends
+ on those that are not constant.
+
+ The variables \verb+Xp+ \verb+X+ lead to $2^{2n}$ states. The variable
+ \verb+Xs+ leads to $2^{n^2}$ states. Each channel of \verb+array_of_channels+
+ may yield $1+2^1+\ldots+2^{\delta_0}= 2^{\delta_0+1}-1$ states. Since the
+ number of edges in the incidence graph is $m$, there are $m$ non-constant
+ channels, leading to approximately $2^{m\times(\delta_0+1)}$ states. The
+ number of configurations is then bounded by $2^{m\times(\delta_0+1)+n(n+2)}$.
+ Notice that this bound is tractable by SPIN for small values of $n$,
+ $m$ and $\delta_0$.
+\end{Proof}
+
+
+
+The method detailed along the line of this article has been applied on the
+running example to formally prove its universally convergence.
+
+First of all, SPIN only considers weak fairness property between processes
+whereas above proofs need such a behavior to be established each time a
+non-deterministic choice is done.
+
+
+A first attempt has consisted in building the following formula
+each time an undeterministic choice between $k$ elements
+respectively labeled $l1$, \ldots $lk$ occurs:
+$$
+[] <> (l == l0) \Rightarrow
+(([] <> (l== l1)) \land \ldots \land ([] <> (l == lk)))
+$$
+where label $l0$ denotes the line before the choice.
+This formula exactly translates the fairness property.
+The negation of such a LTL formula may then be efficiently translated
+into a Büchi automata with the tool ltl2ba~\cite{GO01}.
+However due to an explosion of the size of the product
+between this automata and the automata issued from the PROMELA program
+SPIN did not success to verify whether the property is established or not.
+
+This problem has been practically tackled by leaving spin generating all the (not necessarily fair) computations and verifying convergence property on them.
+We are then left to interpret its output with two issues.
+If property is established for all the computations,
+it is particularly established for fair ones and iterations are convergent.
+In the opposite case, when facing to a counter example, an analysis of the SPIN
+output is achieved.
+\begin{xpl}
+Experiments have shown that all the iterations of the running example are
+convergent for a delay equal to 1 in less than 10 min.
+The example presented in~\cite{abcvs05} with five elements taking boolean
+values has been verified with method presented in this article.
+Immediately, SPIN computes a counter example, that unfortunately does not
+fulfill fairness properties. Fair counter example is obtained
+after few minutes.
+All the experimentation have been realized in a classic desktop computer.
+\end{xpl}
+
+
+
+
+
+%However preliminary experiments have shown the interest of the approach.
+
+
+
+% The method detailed along the line of this article has been
+% applied on some examples to formally prove their convergence
+% (Fig.~\ref{fig:async:exp}).
+% In these experiments, Delays are supposed to be bounded by $\delta_0$ set to 10.
+% In these arrays,
+% $P$ is true ($\top$) provided the uniform convergence property is established, false ($\bot$) otherwise,
+% $M$ is the amount of memory usage (in MB) and
+% $T$ is the time needed on a Intel Centrino Dual Core 2 Duo @1.8GHz with 2GB of memory, both
+% to establish or refute the property.
+
+% RE is the running example of this article,
+% AC2D is a cellular automata with 9 elements taking boolean values
+% according their four neighbors
+% and BM99 is has been proposed in~\cite{BM99} and consists of 10 process
+% modifying their boolean values, but with many connected connection graph.
+
+
+
+
+
+% \begin{figure}
+% \begin{center}
+% \scriptsize
+% \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}
+% Running Example &
+% $\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}
+% 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{Experimentations with Asynchronous Iterations}\label{fig:async:exp}
+% \end{figure}
+
+
+
+% The example~\cite{RC07} deals with a network composed of two genes taking their
+% values into $\{0,1,2\}$. Since parallel iterations is already diverging,
+% the same behavior is observed for all other modes.
+% The Figure~\ref{fig:RC07CE} gives the trace leading to convergence property
+% violation output by SPIN.
+% It corresponds to peridic strategy that repeats $\{1,2\};\{1,2\};\{1\};\{1,2\};\{1,2\}$ and starts with $X=(0,0)$.
+
+
+% In the example extracted from~\cite{BM99},
+% we have 10 processors computing a binary value.
+% Due to the huge number of dependencies between these calculus,
+% $\delta_0$ is reduced to 1. It nevertheless leads to about $2^{100}$
+% configurations in asynchronous iterations.
+
+% Let us focus on checking universal convergence of asynchronous iterations
+% of example~\cite{BCVC10:ir}.
+% With a $\delta_0$ set to 5, SPIN generates an out of memory error.
+% However, it succeed to prove that the property is not established even
+% with $\delta_0$ set to 1 which is then sufficient.
+
+
+% \begin{figure}
+% \begin{center}
+% \begin{tiny}
+% \begin{tabular}{|*{7}{c|}}
+% \cline{2-7}
+% \multicolumn{1}{c|}{ }
+% &\multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} \\
+% \cline{2-7}
+% \multicolumn{1}{c|}{ }&
+% P & M & T&
+% P & M & T \\
+% \hline %\cline{2-7}
+% Running &
+% $\top$ & 2.7 & 0.01s &
+% $\bot$ & 369.371 & 0.509s \\
+% \hline %\cline{2-7}
+% \cite{RC07} example &
+% $\bot$ & 2.5 & 0.001s & % RC07_sync.spin
+% $\bot$ & 2.5 & 0.01s \\ % RC07_sync_chao_all.spin
+% \hline
+% \cite{BM99} example &
+% $\top$ & 36.7 & 12s & % BM99_sync_para.spin
+% $\top$ & & \\ % BM99_sync_chao.spin
+% \hline
+% \end{tabular}
+% \end{tiny}
+% \end{center}
+% \caption{Experimentations with Synchronous Iterations}\label{fig:sync:exp}
+% \end{figure}
+
+
+
+
+
+
+% \begin{tabular}{|*{}{c|}}
+% % \hline
+% % e \\
+% %
+% \hline
+% & \multicolumn{6}{|c|}{Synchronous} & \multicolumn{12}{|c|}{Asynchronous}\\
+% \cline{8-19}
+% Delay & \multicolumn{6}{|c|}{ }
+% & \multicolumn{6}{|c|}
+% {Only Bounded}
+% & \multicolumn{6}{|c|}
+% {Bounded+Mixed Mode}\\
+% Strategy&
+% \multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Chaotic} &
+% \multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Chaotic} &
+% \multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Chaotic} \\
+
+
+% \end{tabular}
+
+
+\section{Conclusion and Future Work}
+\label{sec:spin:concl}
+Stochastic based prototypes have been implemented to generate both
+strategies and delays for asynchronous iterations in first in~\cite{BM99,BCV02}.
+However, since these research softwares are not exhaustive, they really give an
+formal answer when they found a counterexample. When facing convergence, they only convince
+the user about this behavior without exhibiting a proof.
+
+As far as we know, no implemented formal method tackles the problem of
+proving asynchronous iterations convergence.
+In the theoretical work~\cite{Cha06} Chandrasekaran shows that asynchronous iterations
+are convergent iff we can build a decreasing Lyaponov function,
+but does not gives any automated method to compute it.
+
+In this work, we have shown how convergence proof for any asynchronous
+iterations of discrete dynamical networks with bounded delays
+can be automatically achieved.
+The key idea is to translate the network (map, strategy) into PROMELA and
+to leave the SPIN model checker establishing the validity
+of the temporal property corresponding to the convergence.
+The correctness and completeness of the approach have been proved, notably
+by computing a SPIN execution of the PROMELA model that have the same
+behaviors than initial network.
+The complexity of the problem is addressed. It shows that non trivial example
+may be addressed by this technique.
+
+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}.
+
+
+
+
+
+
--- /dev/null
+
+
+
+\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})
+qui permet ensuite (section~\ref{sec:charac}) d'établir la chaoticité des
+systèmes dynamiques booléens.
+
+
+
+
+
+\section{Système dynamique booléen}\label{sub:sdd}
+
+Soit $n$ un entier naturel. Un système dynamique 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 ou 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{asynchrone}.
+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 asynchrones 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 asynchrones 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 asynchrones}} 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 asynchrones.
+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 sont reprises tout au long
+de ce document.
+
+
+
+\begin{figure}%
+\centering
+\begin{minipage}{0.40\textwidth}
+ \begin{center}
+ \includegraphics[height=4cm]{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}%
+ \begin{center}
+ \includegraphics[height=4cm]{images/h.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:iter}%
+\end{minipage}%
+\end{figure}%
+
+% \begin{figure}%[t]
+% \begin{center}
+% \subfloat[$g(x_1,x_2)=(\overline{x_1},x_1\overline{x_2}) $]{
+% \begin{minipage}{0.40\textwidth}
+% \begin{center}
+% \includegraphics[height=4cm]{images/g.pdf}
+% \end{center}
+% \end{minipage}
+% \label{fig:g:iter}
+% }
+% \subfloat[$h(x_1,x_2)=(\overline{x_1},x_1\overline{x_2}+\overline{x_1}x_2)$]{
+% \begin{minipage}{0.40\textwidth}
+% \begin{center}
+% \includegraphics[height=4cm]{images/h.pdf}
+% \end{center}
+% \end{minipage}
+% \label{fig:h:iter}
+% } \end{center}
+% \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
+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
+$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)$,
+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$.
+
+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
+ $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}
+ \begin{center}
+ \includegraphics[height=3cm]{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[height=3cm]{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}%
+
+
+
+
+
+
+
+
+
+Soit $P$ une suite d'arcs de $G(f)$ de la forme
+\[
+(i_1,s_1,i_2),(i_2,s_2,i_3),\ldots,(i_r,s_r,i_{r+1}).
+\]
+Alors, $P$ est dit un chemin de $G(f)$ de longueur $r$ et de signe
+$\Pi_{i=1}^{r}s_i$ et $i_{r+1}$ est dit accessible depuis
+$i_1$.
+$P$ est un {\emph{circuit}} si $i_{r+1}=i_1$ et si les sommets
+$i_1$,\ldots $i_r$ sont deux à deux disjoints.
+Un sommet $i$ de $G(f)$ a une {\emph{boucle}}
+positive (resp. négative) , si $G(f)$ a un
+arc positif (resp. un arc négatif) de $i$ vers lui-même.
+
+
+
+
+
+\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 peut démontrer que pour toute fonction booléenne $f$,
+$G_f$ est continue sur $\mathcal{X}$ (cf annexe~\ref{anx:cont}).
+
--- /dev/null
+latexStyle/tex-templates/hdr/spimufchdr/spimufchdr-backpage.eps
\ No newline at end of file
--- /dev/null
+latexStyle/tex-templates/hdr/spimufchdr/spimufchdr-backpage.pdf
\ No newline at end of file
--- /dev/null
+latexStyle/tex-templates/hdr/spimufchdr/spimufchdr-frontpage.eps
\ No newline at end of file
--- /dev/null
+latexStyle/tex-templates/hdr/spimufchdr/spimufchdr-frontpage.pdf
\ No newline at end of file
--- /dev/null
+latexStyle/tex-templates/hdr/spimufchdr/spimufchdr-p3-head.eps
\ No newline at end of file
--- /dev/null
+latexStyle/tex-templates/hdr/spimufchdr/spimufchdr-p3-head.pdf
\ No newline at end of file
--- /dev/null
+latexStyle/tex-templates/hdr/spimufchdr/spimufchdr.cls
\ No newline at end of file
--- /dev/null
+latexStyle/tex-templates/hdr/spimufchdr/upmext-spimufchdr.cfg
\ No newline at end of file
