\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.
+\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.
$\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}
