X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/d31be79de69d9af9371a3b1fcb3df81246c5928a..HEAD:/talk/sdd2promela.tex

diff --git a/talk/sdd2promela.tex b/talk/sdd2promela.tex
index 4676dfa..9389fc3 100644
--- a/talk/sdd2promela.tex
+++ b/talk/sdd2promela.tex
@@ -3,10 +3,10 @@
 \begin{itemize}
 \item StratÃ©gie: pseudo pÃ©riodicitÃ© garantie par le choix indÃ©terministe de 
   SPIN.
-\item DÃ©lais(bornÃ©s par construction): oubli de certaines valeurs grÃ¢ce Ã  l'indÃ©terminisme de SPIN.
+\item DÃ©lais (bornÃ©s par construction): oubli de certaines valeurs grÃ¢ce Ã  l'indÃ©terminisme de SPIN.
 \end{itemize}
 \item Convergence universelle:   $\diamond  (\Box  \verb+Xp+ = \verb+X+)$.
-\end{itemize}
+
 
 \begin{theorem}[Correction et complÃ©tude de la traduction vers Promela~\cite{Cou10:ir}]
   Soit $\phi$ un modÃ¨le de systÃ¨me dynamique discret et $\psi$ sa traduction PROMELA.  
@@ -15,3 +15,16 @@
   $\psi$ vÃ©rifie
   la propriÃ©tÃ©  LTL  sous hypothÃ¨se d'Ã©quitÃ© faible.
 \end{theorem}
+
+% \item EquitÃ© faible grantie uniquement entre processus:
+% \begin{itemize}
+% \item L'imposer pour chaque choix oÃ¹
+% \item Filtrer les traces non Ã©quitables retournÃ©e.
+% \end{itemize}
+\item Bilan: 
+\begin{itemize}
+\item Preuve automatique de convergence de modÃ¨les indpt. schÃ©ma/mode.
+\item A pu dÃ©cider de la convergence d'exemples simples.
+\item Ne passe pas Ã  l'Ã©chelle.
+\end{itemize}
+\end{itemize}
