talk/sdd2promela.tex

   1 \begin{itemize}
   2 \item Points clefs de la traduction:
   3 \begin{itemize}
   4 \item Stratégie: pseudo périodicité garantie par le choix indéterministe de
   5   SPIN.
   6 \item Délais(bornés par construction): oubli de certaines valeurs grâce à l'indéterminisme de SPIN.
   7 \end{itemize}
   8 \item Convergence universelle:   $\diamond  (\Box  \verb+Xp+ = \verb+X+)$.
   9 \end{itemize}
  10
  11 \begin{theorem}[Correction et complétude de la traduction vers Promela~\cite{Cou10:ir}]
  12   Soit $\phi$ un modèle de système dynamique discret et $\psi$ sa traduction PROMELA.
  13   Les itérations de $\phi$ sont universellement convergentes si et
  14   seulement si
  15   $\psi$ vérifie
  16   la propriété  LTL  sous hypothèse d'équité faible.
  17 \end{theorem}