
\begin{itemize}
\item Conditions suffisantes de convergence: facile à appliquer, 
  domaine restreint
\item Recherche d'une métrique decroissante minorée: difficile
\item Simulations:  
\begin{itemize}
\item Non exhaustives pour les schémas généralisés et asynchrones.
\item Verdict $\leftrightarrow$ vérité ssi divergence (contre-exemple).
\end{itemize}
\item Souhait: exploiter un outil qui traiterait toutes les transitions 
\begin{itemize}
\item explosion combinatoire: par abstraction,
  quotientage, ordre partiel\ldots
\item Model checker: SPIN~\cite{Hol03}.
\item Correction et complétude de la démarche.
  \end{itemize}
\end{itemize}
