la veille

[hdrcouchot.git] / talk / preuveconvmotiv.tex

diff --git a/talk/preuveconvmotiv.tex b/talk/preuveconvmotiv.tex
index b3e38d438c226bb5957d622fa5f72b507c1a143e..0e8c6211e598b5c74b7b703622ccb8a3e072371d 100644 (file)
--- a/talk/preuveconvmotiv.tex
+++ b/talk/preuveconvmotiv.tex
@@ -1,16 +1,16 @@
 
 \begin{itemize}
 \item Conditions suffisantes de convergence: facile à appliquer, 
 
 \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 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 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}
 \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.
   quotientage, ordre partiel\ldots
 \item Model checker: SPIN~\cite{Hol03}.
 \item Correction et complétude de la démarche.