X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/e9bdff7e28e4cda1ffb71158afdcf44e3d656b6c..714ce29544c8cc7bf8b4530d28352fb1a5306991:/main.tex diff --git a/main.tex b/main.tex index 16de4a6..27c159c 100644 --- a/main.tex +++ b/main.tex @@ -111,7 +111,7 @@ \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}} @@ -139,9 +139,12 @@ Blabla blabla. \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} @@ -151,6 +154,8 @@ Blabla blabla. \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 @@ -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} @@ -173,14 +178,23 @@ au chaos} \chapter{Characterisation des systèmes discrets chaotiques} + +La première section rappelle ce que sont les systèmes dynamiques chaotiques. Dire que cette caractérisation dépend du type de stratégie : unaire (TIPE), généralisée (TSI). Pour chacune d'elle, on introduit une distance différente. On montre qu'on a des résultats similaires. +\section{Systèmes dynamiques chaotiques selon Devaney} +\label{subsec:Devaney} +\input{devaney} + +\section{Schéma unaire} \input{12TIPE} +\section{Schéma généralisé} +\input{15TSI} générer des fonctions vérifiant ceci (TIPE12 juste sur le résultat d'adrien). @@ -197,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} @@ -225,11 +253,18 @@ générer des fonctions vérifiant ceci (TIPE12 juste sur le résultat d'adrien) \input{annexecontinuite.tex} + + \section{Caractérisation des fonctions $f$ rendant chaotique $G_f$ dans $(\mathcal{X},d)$}\label{anx:chaos:unaire} \input{caracunaire.tex} +\section{Preuve que $d$ est une distance sur $\mathcal{X}$}\label{anx:distance:generalise} +\input{preuveDistanceGeneralisee} + +\section{Caractérisation des fonctions $f$ rendant chaotique $G_f$ dans $(\mathcal{X},d)$}\label{anx:chaos:generalise} +\input{caracgeneralise.tex}