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

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.
