\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+)$.
\end{itemize}

\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}
