fsfd

[hdrcouchot.git] / modelchecking.tex

diff --git a/modelchecking.tex b/modelchecking.tex
index ca223fb4c35e3d68d7293805aac76cbf8ca14b74..1b8843d80ea820bd7b3f7d49a11b636d5ead2bed 100644 (file)
--- a/modelchecking.tex
+++ b/modelchecking.tex
@@ -572,20 +572,25 @@ Toutes les preuves sont déplacées en
 annexes~\ref{anx:promela}.
 
 
 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.
   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.
   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}
+
+