X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/d31be79de69d9af9371a3b1fcb3df81246c5928a..44a56c5eb4a1dfdf7dc67735c5c00f478cef2ede:/talk/preuveconvmotiv.tex?ds=inline diff --git a/talk/preuveconvmotiv.tex b/talk/preuveconvmotiv.tex index b3e38d4..f6540e9 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 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.