X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/1b923f193392e3ce847882c24a128eff4bee9992..1863b8b84356fa645dafb42dc9fe4028d825e54f:/main.tex?ds=sidebyside diff --git a/main.tex b/main.tex index 79ec26a..fdcf059 100644 --- a/main.tex +++ b/main.tex @@ -11,18 +11,17 @@ \documentclass[french]{spimufchdr} \usepackage{dsfont} -\usepackage{glossaries} \usepackage{graphicx} \usepackage{listings} -\usepackage{verbatim} - -% The TeX code is entering with UTF8 -% character encoding (Linux and MacOS standards) +%\usepackage[font=footnotesize]{subfig} \usepackage[utf8]{inputenc} +\usepackage{thmtools, thm-restate} +\usepackage{multirow} +%\declaretheorem{theorem} %%-------------------- %% Search path for pictures -%\graphicspath{{path1/},{path2/}} +\graphicspath{{images/},{path2/}} %%-------------------- %% Definition of the bibliography entries @@ -113,29 +112,23 @@ \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{\Fig}[1]{Fig.\,\ref{#1}} -\newcommand{\Alg}[1]{Algorithm~\ref{#1}} -\newcommand{\Tab}[1]{Table~\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{\Equ}[1]{(\ref{#1})} \newcommand{\deriv}{\mathrm{d}} \newcommand{\class}[1]{\ensuremath{\langle #1\rangle}} \newcommand{\dom}[0]{\ensuremath{\textit{dom}}} - + \newcommand{\eqNode}[0]{\ensuremath{{\mathcal{R}}}} \newtheorem{theorem}{Théorème} \newtheorem{lemma}{Lemme} -\newtheorem{xpl}{Exemple} -\newtheorem{Proof}{Preuve} +\newtheorem*{xpl}{Exemple} +\newtheorem*{Proof}{Preuve} +\newtheorem{Def}{Définition} \begin{document} -\input{glossaire.tex} - -% \chapter*{Remerciements} - -% Blabla blabla. - -% \tableofcontents @@ -147,28 +140,92 @@ Blabla blabla. \mainmatter -\part{Système Booléens} - -\chapter{Iterations discrètes de Systèmes Dynamiques booléens} +\part{Réseaux Discrets} -\JFC{Chapeau chapitre à faire} +\chapter{Iterations discrètes de réseaux booléens} +\JFC{chapeau à refaire} +\section{Formalisation} \input{sdd} +\section{Combinaisons synchrones et asynchrones} +\input{mixage} -\chapter[Preuve de convergence de systèmes booléens]{Preuve automatique de convergence de systèmes booléens} +\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 +avantage du synchronisme en terme de convergence avec les avantages +de l'asynchronisme en terme de vitesse de convergence. + + + + +\chapter{Preuve automatique de convergence}\label{chap:promela} \input{modelchecking} -\JFC{Mixage} + + +\part{Des systèmes dynamiques discrets +au chaos} + +\chapter[Caracterisation des systèmes + discrets chaotiques]{Caracterisation des systèmes + discrets chaotiques pour les schémas unaires et généralisés} + +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}\label{sec:TIPE12} +\input{12TIPE} + +\section{Schéma généralisé} +\input{15TSI} + + +\section{Générer des fonctions chaotiques} +\input{11FCT} + + +\chapter{Prédiction des systèmes chaotiques} + +\input{chaosANN} + -% \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} @@ -179,15 +236,41 @@ Blabla blabla. \chapter{Preuves sur les SDD} -\section{Preuve du théorème~\ref{th:Adrien}}\label{anx:sccg} -\input{annexesccg} +\section{Convergence du mode mixe}\label{anx:mix} +\input{annexePreuveMixage} -\section{Preuve de continuité de $G_f$ dans $(\mathcal{X},d)$}\label{anx:cont} -\input{annexecontinuite.tex} -\section{Preuve de Correction et de complétude de l'approche de vérification de convergence à l'aide de SPIN} +\section{Correction et complétude de la + vérification de convergence par SPIN}\label{anx:promela} \input{annexePromelaProof} + + +\chapter{Preuves sur les systèmes chaotiques} + + +\section{Continuité de $G_f$ dans $(\mathcal{X}_u,d)$}\label{anx:cont} +\input{annexecontinuite.tex} + + +\section{Caractérisation des fonctions $f$ rendant chaotique $G_{f_u}$ dans $(\mathcal{X}_u,d)$}\label{anx:chaos:unaire} +\input{caracunaire.tex} + + +\section{Preuve que $d$ est une distance sur $\mathcal{X}_g$}\label{anx:distance:generalise} +\input{preuveDistanceGeneralisee} + + +\section{Caractérisation des fonctions $f$ rendant chaotique $G_{f_g}$ dans $(\mathcal{X}_g,d)$}\label{anx:chaos:generalise} +\input{caracgeneralise.tex} + + +\section{Théorème~\ref{th:Adrien}}\label{anx:sccg} +\input{annexesccg} + + + + \backmatter \bibliographystyle{apalike}