X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/d31be79de69d9af9371a3b1fcb3df81246c5928a..refs/heads/master:/talk/preuveconvmotiv.tex?ds=inline

diff --git a/talk/preuveconvmotiv.tex b/talk/preuveconvmotiv.tex
index b3e38d4..0e8c621 100644
--- a/talk/preuveconvmotiv.tex
+++ b/talk/preuveconvmotiv.tex
@@ -1,16 +1,16 @@
 
 \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 Non exhaustives pour les schémas unaires, généralisés, asynchrones\ldots
 \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.