\begin{itemize}
\item Conditions suffisantes de convergence: facile à appliquer,
- domaine restreint
-\item Recherche d'une métrique decroissante minorée: difficile
+ 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
+\item Souhait: exploiter un outil qui traiterait toutes les transitions.
\begin{itemize}
-\item explosion combinatoire: par abstraction,
+\item Explosion combinatoire: par abstraction,
quotientage, ordre partiel\ldots
\item Model checker: SPIN~\cite{Hol03}.
\item Correction et complétude de la démarche.
