1 %% Use the standard UP-methodology class
2 %% with French language.
4 %% You may specify the option 'twoside' or 'oneside' for
7 %% See the documentation tex-upmethodology on
8 %% http://www.arakhne.org/tex-upmethodology/
9 %% for details about the macros that are provided by the class and
10 %% to obtain the list of the packages that are already included.
12 \documentclass[french]{spimufchdr}
16 %\usepackage[font=footnotesize]{subfig}
17 \usepackage[utf8]{inputenc}
18 \usepackage{thmtools, thm-restate}
20 %\declaretheorem{theorem}
22 %%--------------------
23 %% Search path for pictures
24 \graphicspath{{images/},{path2/}}
26 %%--------------------
27 %% Definition of the bibliography entries
28 \declarebiblio{J}{Journaux internationaux avec comités de lecture}{mabiblio}
30 %%--------------------
31 %% Title of the document
32 \declarehdr{Title}{XX Mois XXXX}
34 %%--------------------
35 %% Set the author of the HDR
36 \addauthor[first.name@utbm.fr]{First}{Name}
38 %%--------------------
39 %% Add a member of the jury
40 %% \addjury{Firstname}{Lastname}{Role in the jury}{Position}
41 \addjury{First}{Name}{Rapporteur}{Professeur à l'Université de XXX}
42 \addjury{First}{Name}{Examinateur}{Professeur à l'Université de XXX}
44 %%--------------------
45 %% Change the style of the text in the list of the members of the jury.
46 %% \Set{jurystyle}{ style of the text}
47 %\Set{jurystyle}{\small}
49 %%--------------------
50 %% Set the University where HDR was made
51 \hdrpreparedin{Université de Technologie de Belfort-Montbéliard}
53 %%--------------------
54 %% Set the English abstract
55 %\hdrabstract[english]{This is the abstract in English}
57 %%--------------------
58 %% Set the English keywords. They only appear if
59 %% there is an English abstract
60 %\hdrkeywords[english]{Keyword 1, Keyword 2}
62 %%--------------------
63 %% Set the French abstract
64 \hdrabstract[french]{Blabla blabla.}
66 %%--------------------
67 %% Set the French keywords. They only appear if
68 %% there is an French abstract
69 %\hdrkeywords[french]{Mot-cl\'e 1, Mot-cl\'e 2}
71 %%--------------------
72 %% Change the layout and the style of the text of the "primary" abstract.
73 %% If your document is written in French, the primary abstract is in French,
74 %% otherwise it is in English.
75 \Set{primaryabstractstyle}{\small}
77 %%--------------------
78 %% Change the layout and the style of the text of the "secondary" abstract.
79 %% If your document is written in French, the secondary abstract is in English,
80 %% otherwise it is in French.
81 %\Set{secondaryabstractstyle}{\tiny}
83 %%--------------------
84 %% Change the layout and the style of the text of the "primary" keywords.
85 %% If your document is written in French, the primary keywords are in French,
86 %% otherwise they are in English.
87 %\Set{primarykeywordstyle}{\tiny}
89 %%--------------------
90 %% Change the layout and the style of the text of the "secondary" keywords.
91 %% If your document is written in French, the secondary keywords are in English,
92 %% otherwise they are in French.
93 %\Set{secondarykeywordstyle}{\tiny}
95 %%--------------------
96 %% Change the speciality of the PhD thesis
97 %\Set{speciality}{Informatique}
99 %%--------------------
100 %% Change the institution
101 %\Set{universityname}{Universit\'e de Technologie de Belfort-Montb\'eliard}
103 %%--------------------
104 %% Add the logo of a partner or a sponsor
105 %\addpartner{partner_logo}
106 \newcommand{\JFC}[1]{\begin{color}{green}\textit{#1}\end{color}}
107 \newcommand{\vectornorm}[1]{\ensuremath{\left|\left|#1\right|\right|_2}}
108 \newcommand{\ie}{\textit{i.e.}}
109 \newcommand{\Nats}[0]{\ensuremath{\mathbb{N}}}
110 \newcommand{\Reels}[0]{\ensuremath{\mathbb{R}}}
111 \newcommand{\Zed}[0]{\ensuremath{\mathbb{Z}}}
112 \newcommand{\Bool}[0]{\ensuremath{\mathds{B}}}
113 \newcommand{\rel}[0]{\ensuremath{{\mathcal{R}}}}
114 \newcommand{\Gall}[0]{\ensuremath{\mathcal{G}}}
115 \newcommand{\Sec}[1]{Section\,\ref{#1}}
116 \newcommand{\Fig}[1]{{\sc Figure}~\ref{#1}}
117 \newcommand{\Alg}[1]{Algorithme~\ref{#1}}
118 \newcommand{\Tab}[1]{Tableau~\ref{#1}}
119 \newcommand{\Equ}[1]{(\ref{#1})}
120 \newcommand{\deriv}{\mathrm{d}}
121 \newcommand{\class}[1]{\ensuremath{\langle #1\rangle}}
122 \newcommand{\dom}[0]{\ensuremath{\textit{dom}}}
123 \newcommand{\eqNode}[0]{\ensuremath{{\mathcal{R}}}}
125 \newtheorem{theorem}{Théorème}
126 \newtheorem{lemma}{Lemme}
127 \newtheorem*{xpl}{Exemple}
128 \newtheorem*{Proof}{Preuve}
129 \newtheorem{Def}{Définition}
137 \chapter*{Introduction}
143 \part{Réseaux Discrets}
145 \chapter{Iterations discrètes de réseaux booléens}
146 \JFC{chapeau à refaire}
147 \section{Formalisation}
150 \section{Combinaisons synchrones et asynchrones}
154 \JFC{Conclusion à refaire}
156 Introduire de l'asynchronisme peut permettre de réduire le temps
157 d'exécution global, mais peut aussi introduire de la divergence.
158 Dans ce chapitre, nous avons exposé comment construire un mode combinant les
159 avantage du synchronisme en terme de convergence avec les avantages
160 de l'asynchronisme en terme de vitesse de convergence.
165 \chapter{Preuve automatique de convergence}\label{chap:promela}
166 \input{modelchecking}
173 \part{Des systèmes dynamiques discrets
176 \chapter[Caracterisation des systèmes
177 discrets chaotiques]{Caracterisation des systèmes
178 discrets chaotiques pour les schémas unaires et généralisés}
180 La première section rappelle ce que sont les systèmes dynamiques chaotiques.
181 Dire que cette caractérisation dépend du type de stratégie : unaire (TIPE),
182 généralisée (TSI). Pour chacune d'elle,
183 on introduit une distance différente.
185 On montre qu'on a des résultats similaires.
187 \section{Systèmes dynamiques chaotiques selon Devaney}
188 \label{subsec:Devaney}
191 \section{Schéma unaire}\label{sec:TIPE12}
194 \section{Schéma généralisé}
198 \section{Générer des fonctions chaotiques}
202 \chapter{Prédiction des systèmes chaotiques}
215 \part{Conclusion et Perspectives}
217 \JFC{Perspectives pour SDD->Promela}
218 Among drawbacks of the method, one can argue that bounded delays is only
219 realistic in practice for close systems.
220 However, in real large scale distributed systems where bandwidth is weak,
221 this restriction is too strong. In that case, one should only consider that
222 matrix $s^{t}$ follows the iterations of the system, \textit{i.e.},
223 for all $i$, $j$, $1 \le i \le j \le n$, we have$
224 \lim\limits_{t \to \infty} s_{ij}^t = + \infty$.
225 One challenge of this work should consist in weakening this constraint.
226 We plan as future work to take into account other automatic approaches
227 to discharge proofs notably by deductive analysis~\cite{CGK05}.
230 % \chapter{Conclusion}
237 \chapter{Preuves sur les SDD}
239 \section{Convergence du mode mixe}\label{anx:mix}
240 \input{annexePreuveMixage}
243 \section{Correction et complétude de la
244 vérification de convergence par SPIN}\label{anx:promela}
245 \input{annexePromelaProof}
249 \chapter{Preuves sur les systèmes chaotiques}
252 \section{Continuité de $G_f$ dans $(\mathcal{X}_u,d)$}\label{anx:cont}
253 \input{annexecontinuite.tex}
256 \section{Caractérisation des fonctions $f$ rendant chaotique $G_{f_u}$ dans $(\mathcal{X}_u,d)$}\label{anx:chaos:unaire}
257 \input{caracunaire.tex}
260 \section{Preuve que $d$ est une distance sur $\mathcal{X}_g$}\label{anx:distance:generalise}
261 \input{preuveDistanceGeneralisee}
264 \section{Caractérisation des fonctions $f$ rendant chaotique $G_{f_g}$ dans $(\mathcal{X}_g,d)$}\label{anx:chaos:generalise}
265 \input{caracgeneralise.tex}
268 \section{Théorème~\ref{th:Adrien}}\label{anx:sccg}
276 \bibliographystyle{apalike}
277 \bibliography{abbrev,biblioand}