+
+
+
+L'étude de convergence de systèmes dynamiques discrets est simple à vérifier
+pratiquement pour le mode synchrone. Lorsqu'on introduit des stratégies
+pseudo périodiques pour les modes unaires et généralisées, le problème
+se complexifie. C'est pire encore lorsqu'on traite des itérations asynchrones
+et mixes prenant de plus en compte les délais.
+
+Des méthodes de simulation basées sur des stratégies et des délais générés aléatoirement
+ont déjà été présentées~\cite{BM99,BCV02}.
+Cependant, comme ces implantations ne sont pas exhaustives, elles ne donnent un résultat
+formel que lorsqu'elles fournissent un contre-exemple. Lorsqu'elles exhibent une convergence,
+cela ne permet que donner une intuition de convergence, pas une preuve.
+Autant que nous sachions, aucune démarche de preuve formelle automatique
+de convergence n'a jamais été établie.
+Dans le travail théorique~\cite{Cha06}, Chandrasekaran a montré que les itérations asynchrones sont convergentes
+si et seulement si on peut construire une fonction de Lyaponov décroissante, mais il ne donne pas de méthode
+automatique pour construire cette fonction.
+
+Un outil qui construirait automatiquement toutes
+les transitons serait le bienvenu.
+Pour peu qu'on établisse la preuve de correction et de complétude de la
+démarche, la convergence du réseau discret ne repose alors que sur le verdict
+donné par l'outil.
+Cependant, même pour des réseaux discrets à peu d'éléments,
+le nombre de configurations induites explose rapidement.
+Les \emph{Model-Checkers}~\cite{Hol03,nusmv02,Blast07,MCErlang07,Bogor03}
+sont des classes d'outils qui adressent le problème de vérifier automatiquement
+qu'un modèle vérifie une propriété donnée. Pour traiter le problème d'explosion
+combinatoire, ces outils appliquent des méthodes d'ordre partiel, d'abstraction,
+de quotientage selon une relation d'équivalence.
+
+Ce chapitre montre comment nous simulons
+des réseaux discrets selon toutes les sortes d'itérations pour établir
+formellement leur convergence (ou pas).
+Nous débutons par un exemple et faisons quelques rappels sur
+le langage PROMELA qui est le langage du model-checker
+SPIN~\cite{Hol03} (\Sec{sec:spin:promela}).
+Nous présentons ensuite la démarche de traduction
+de réseaux discrets dans PROMELA (\Sec{sec:spin:translation}).
+Les théorèmes de correction et de complétude de la démarche
+sont ensuite donnés à la (\Sec{sec:spin:proof}).
+Des données pratiques comme la complexité et des synthèses d'expérimentation
+sont ensuite fournies (\Sec{sec:spin:practical}).
+
+
+
+
+
+
+
+%\section{Exemple jouet}
+
+
+\begin{figure}[ht]
+ \begin{center}
+ \subfigure[Fonction à itérer]{
+ $ F(x)= \left \{
+ \begin{array}{rcl}
+ f_1(x_1,x_2,x_3) & = & x_1.\overline{x_2} + x_3 \\
+ f_2(x_1,x_2,x_3) & = & x_1 + \overline{x_3} \\
+ f_3(x_1,x_2,x_3) & = & x_2.x_3
+ \end{array}
+ \right.
+ $
+ \label{fig:map}
+ }
+ \hfill
+ \subfigure[Graphe d'intéraction]{
+ \includegraphics[width=4cm]{images/xplCnxMc.eps}
+ \label{fig:xplgraph:inter:mc}
+ }
+ \end{center}
+ \caption{Exemple pour SDD $\approx$ SPIN.}
+\end{figure}
+
+
+
+\begin{xpl}
+ On considère un exemple à trois éléments dans $\Bool$.
+ Chaque configuration est ainsi un élément de $\Bool^3$, \textit{i.e.},
+ un nombre entre 0 et 7.
+ La \Fig{fig:map} précise la fonction $f$ considérée et
+ la \Fig{fig:xplgraph:inter:mc} donne son graphe d'intéraction.
+
+
+
+
+
+
+
+On peut facilement vérifier que toutes les itérations synchrones initialisées
+avec $x^0 \neq 7$ soit $(111)$
+convergent vers $2$ soit $(010)$; celles initialisées avec
+$x^0=7$ restent en 7.
+Pour les mode unaires ou généralisés avec une
+stratégie pseudo périodique, on a des comportements qui dépendent
+de la configuration initiale:
+\begin{itemize}
+\item initialisée avec 7, les itérations restent en 7;
+\item initialisée avec 0, 2, 4 ou 6 les itérations convergent vers 2;
+\item initialisées avec 1, 3 ou 5, les itérations convergent vers un des
+deux points fixes 2 ou 7.
+\end{itemize}
+\end{xpl}
+
+
+
