\begin{itemize}
\item Points clefs de la traduction:
\begin{itemize}
\item Stratégie: pseudo périodicité garantie par le choix indéterministe de 
  SPIN.
\item Délais (bornés par construction): oubli de certaines valeurs grâce à l'indéterminisme de SPIN.
\end{itemize}
\item Convergence universelle:   $\diamond  (\Box  \verb+Xp+ = \verb+X+)$.


\begin{theorem}[Correction et complétude de la traduction vers Promela~\cite{Cou10:ir}]
  Soit $\phi$ un modèle de système dynamique discret et $\psi$ sa traduction PROMELA.  
  Les itérations de $\phi$ sont universellement convergentes si et 
  seulement si
  $\psi$ vérifie
  la propriété  LTL  sous hypothèse d'équité faible.
\end{theorem}

% \item Equité faible grantie uniquement entre processus:
% \begin{itemize}
% \item L'imposer pour chaque choix où
% \item Filtrer les traces non équitables retournée.
% \end{itemize}
\item Bilan: 
\begin{itemize}
\item Preuve automatique de convergence de modèles indpt. schéma/mode.
\item A pu décider de la convergence d'exemples simples.
\item Ne passe pas à l'échelle.
\end{itemize}
\end{itemize}
