+
+
+
+
+
+
+
+ \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}.
+
