X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/3759a997c005ffb313be135f98820410cb6061b4..ac26aa33009d503bf9c04a2b00244c5bf723e694:/annexePromelaProof.tex

diff --git a/annexePromelaProof.tex b/annexePromelaProof.tex
index ade9df0..3c0724c 100644
--- a/annexePromelaProof.tex
+++ b/annexePromelaProof.tex
@@ -14,7 +14,7 @@ du chapitre~\ref{chap:promela}.
 \begin{proof}
   La preuve est directe pour $t=0$.
   Supposons qu'elle est Ã©tablie jusqu'en $t$ valant un certain $t_0$. 
-  On considÃ¨re des stratÃ©gies pseudo pÃ©riodiques.
+  On considÃ¨re des stratÃ©gies pseudo-pÃ©riodiques.
   GrÃ¢ce Ã  l'hypothÃ¨se d'Ã©quitÃ© faible, \verb+update_elems+ modifie 
   les Ã©lÃ©ments de $S^t$ Ã  l'itÃ©ration $t$.
 \end{proof}
@@ -287,7 +287,7 @@ GrÃ¢ce Ã ~\Equ{eq:correct_retrieve} dÃ©jÃ  prouvÃ©e, on peut conclure la preuve.
   Pour chaque  modÃ¨le  $\psi$ 
   qui ne vÃ©rifie pas la propriÃ©tÃ©  LTL  (\ref{eq:ltl:conv}), 
   il est immÃ©diat de construire les itÃ©rations correspondantes du
-  systÃ¨me dynamique, dont la stratÃ©gie est pseudo pÃ©riodique en raison 
+  systÃ¨me dynamique, dont la stratÃ©gie est pseudo-pÃ©riodique en raison 
   de la propriÃ©tÃ© d'Ã©quitÃ© faible..
 
 %   i.e. iterations that  are divergent.   Executions are
