X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/f4dd79b2c3181cb26ec94555b62ed77dcb0a4200..148e6fe3fc164ce0c37454354e0815c398cdea62:/modelchecking.tex?ds=inline

diff --git a/modelchecking.tex b/modelchecking.tex
index ca223fb..1b8843d 100644
--- a/modelchecking.tex
+++ b/modelchecking.tex
@@ -572,20 +572,25 @@ Toutes les preuves sont dÃ©placÃ©es en
 annexes~\ref{anx:promela}.
 
 
-\begin{theorem}[Correction]\label{Theo:sound}
+\begin{restatable}[Correction de la traduction vers Promela]{theorem}{promelasound}
+\label{Theo:sound}
+%
   Soit $\phi$ un modÃ¨le de systÃ¨me dynamique discret et $\psi$ sa traduction PROMELA.  
   Si $\psi$ vÃ©rifie
   la propriÃ©tÃ©  LTL  (\ref{eq:ltl:conv})  sous hypothÃ¨se d'Ã©quitÃ© faible,  alors
   les itÃ©rations de $\phi$ sont universellement convergentes.
-\end{theorem}
-
+\end{restatable}
 
 
-\begin{theorem}[ComplÃ©tude]\label{Theo:completeness}
+\begin{restatable}[ComplÃ©tude de la traduction vers Promela]{theorem}{promelacomplete}
+\label{Theo:completeness}
+%
   Soit $\phi$ un modÃ¨le de systÃ¨me dynamique discret et $\psi$ sa traduction.  Si $\psi$ ne vÃ©rifie pas 
   la propriÃ©tÃ© LTL (\ref{eq:ltl:conv}) sous hypothÃ¨se d'Ã©quitÃ© faible,
   alors les itÃ©rations de  $\phi$ ne sont pas universellement convergentes.
-\end{theorem}
+\end{restatable}
+
+
 
 
 
