]> AND Private Git Repository - hdrcouchot.git/blobdiff - main.tex
Logo AND Algorithmique Numérique Distribuée

Private GIT Repository
azerazerzer
[hdrcouchot.git] / main.tex
index a31f0bd8962debdbd302597e10104ef33fd924cf..27c159c8017829f0a7909829d1402375a90a4494 100644 (file)
--- a/main.tex
+++ b/main.tex
 \newcommand{\Bool}[0]{\ensuremath{\mathds{B}}}
 \newcommand{\rel}[0]{\ensuremath{{\mathcal{R}}}}
 \newcommand{\Gall}[0]{\ensuremath{\mathcal{G}}}
 \newcommand{\Bool}[0]{\ensuremath{\mathds{B}}}
 \newcommand{\rel}[0]{\ensuremath{{\mathcal{R}}}}
 \newcommand{\Gall}[0]{\ensuremath{\mathcal{G}}}
-\newcommand{\Sec}[1]{Sect\,\ref{#1}}
+\newcommand{\Sec}[1]{Section\,\ref{#1}}
 \newcommand{\Fig}[1]{{\sc Figure}~\ref{#1}}
 \newcommand{\Alg}[1]{Algorithme~\ref{#1}}
 \newcommand{\Tab}[1]{Tableau~\ref{#1}}
 \newcommand{\Fig}[1]{{\sc Figure}~\ref{#1}}
 \newcommand{\Alg}[1]{Algorithme~\ref{#1}}
 \newcommand{\Tab}[1]{Tableau~\ref{#1}}
@@ -139,9 +139,12 @@ Blabla blabla.
 
 \mainmatter
 
 
 \mainmatter
 
-\part{Système Booléens}
+\part{Réseaux Discrets}
 
 
-\chapter{Iterations discrètes de Systèmes Dynamiques booléens}
+
+
+\chapter{Iterations discrètes de réseaux booléens}
+\JFC{chapeau à refaire}
 \section{Formalisation}
 \input{sdd}
 
 \section{Formalisation}
 \input{sdd}
 
@@ -151,6 +154,8 @@ Blabla blabla.
 
 
 \section{Conclusion}
 
 
 \section{Conclusion}
+\JFC{Conclusion à refaire}
+
 Introduire de l'asynchronisme peut permettre de réduire le temps 
 d'exécution global, mais peut aussi introduire de la divergence. 
 Dans ce chapitre, nous avons exposé comment construire un mode combinant les
 Introduire de l'asynchronisme peut permettre de réduire le temps 
 d'exécution global, mais peut aussi introduire de la divergence. 
 Dans ce chapitre, nous avons exposé comment construire un mode combinant les
@@ -160,7 +165,7 @@ de l'asynchronisme en terme de vitesse de convergence.
 
 
 
 
 
 
-\chapter[Preuve de convergence de systèmes booléens]{Preuve automatique de  convergence de systèmes booléens}\label{chap:promela}
+\chapter[Preuve de convergence de systèmes booléens]{Preuve automatique de  convergence}\label{chap:promela}
 \input{modelchecking}
 
 
 \input{modelchecking}
 
 
@@ -206,7 +211,21 @@ générer des fonctions vérifiant ceci (TIPE12 juste sur le résultat d'adrien)
 
 
 
 
 
 
-% \part{Conclusion et Perspectives}
+
+ \part{Conclusion et Perspectives}
+
+\JFC{Perspectives pour SDD->Promela}
+Among drawbacks of the method,  one can argue that bounded delays is only 
+realistic in practice for close systems. 
+However, in real large scale distributed systems where bandwidth is weak, 
+this restriction is too strong. In that case, one should only consider that 
+matrix $s^{t}$ follows the  iterations of the system, \textit{i.e.},
+for all $i$, $j$, $1 \le i \le j \le n$,  we have$
+\lim\limits_{t \to \infty} s_{ij}^t = + \infty$. 
+One challenge of this work should consist in weakening this constraint. 
+We plan as future work to take into account other automatic approaches 
+to discharge proofs notably by deductive analysis~\cite{CGK05}. 
+
 
 % \chapter{Conclusion}
 
 
 % \chapter{Conclusion}