merge main

[hdrcouchot.git] / main.tex

%% Use the standard UP-methodology class
%% with French language.
%%
%% You may specify the option 'twoside' or 'oneside' for
%% the document.
%%
%% See the documentation tex-upmethodology on
%% http://www.arakhne.org/tex-upmethodology/
%% for details about the macros that are provided by the class and
%% to obtain the list of the packages that are already included. 

\documentclass[french]{spimufchdr}
\usepackage{dsfont}
\usepackage{graphicx}
\usepackage{listings}
%\usepackage[font=footnotesize]{subfig}
\usepackage[utf8]{inputenc}
\usepackage{thmtools, thm-restate}
%\declaretheorem{theorem}

%%--------------------
%% Search path for pictures
\graphicspath{{images/},{path2/}}

%%--------------------
%% Definition of the bibliography entries
\declarebiblio{J}{Journaux internationaux avec comités de lecture}{mabiblio}

%%--------------------
%% Title of the document
\declarehdr{Title}{XX Mois XXXX}
 
%%--------------------
%% Set the author of the HDR
\addauthor[first.name@utbm.fr]{First}{Name}
 
%%--------------------
%% Add a member of the jury
%% \addjury{Firstname}{Lastname}{Role in the jury}{Position}
\addjury{First}{Name}{Rapporteur}{Professeur à l'Université de XXX}
\addjury{First}{Name}{Examinateur}{Professeur à l'Université de XXX}
 
%%--------------------
%% Change the style of the text in the list of the members of the jury.
%% \Set{jurystyle}{ style of the text}
%\Set{jurystyle}{\small}

%%--------------------
%% Set the University where HDR was made
\hdrpreparedin{Université de Technologie de Belfort-Montbéliard}
 
%%--------------------
%% Set the English abstract
%\hdrabstract[english]{This is the abstract in English}
 
%%--------------------
%% Set the English keywords. They only appear if
%% there is an English abstract
%\hdrkeywords[english]{Keyword 1, Keyword 2}
 
%%--------------------
%% Set the French abstract
\hdrabstract[french]{Blabla blabla.}
 
%%--------------------
%% Set the French keywords. They only appear if
%% there is an French abstract
%\hdrkeywords[french]{Mot-cl\'e 1, Mot-cl\'e 2}

%%--------------------
%% Change the layout and the style of the text of the "primary" abstract.
%% If your document is written in French, the primary abstract is in French,
%% otherwise it is in English.
\Set{primaryabstractstyle}{\small}

%%--------------------
%% Change the layout and the style of the text of the "secondary" abstract.
%% If your document is written in French, the secondary abstract is in English,
%% otherwise it is in French.
%\Set{secondaryabstractstyle}{\tiny}

%%--------------------
%% Change the layout and the style of the text of the "primary" keywords.
%% If your document is written in French, the primary keywords are in French,
%% otherwise they are in English.
%\Set{primarykeywordstyle}{\tiny}

%%--------------------
%% Change the layout and the style of the text of the "secondary" keywords.
%% If your document is written in French, the secondary keywords are in English,
%% otherwise they are in French.
%\Set{secondarykeywordstyle}{\tiny}

%%--------------------
%% Change the speciality of the PhD thesis
%\Set{speciality}{Informatique}
 
%%--------------------
%% Change the institution
%\Set{universityname}{Universit\'e de Technologie de Belfort-Montb\'eliard}

%%--------------------
%% Add the logo of a partner or a sponsor
%\addpartner{partner_logo}
\newcommand{\JFC}[1]{\begin{color}{green}\textit{#1}\end{color}}
\newcommand{\vectornorm}[1]{\ensuremath{\left|\left|#1\right|\right|_2}}
\newcommand{\ie}{\textit{i.e.}}
\newcommand{\Nats}[0]{\ensuremath{\mathbb{N}}}
\newcommand{\Reels}[0]{\ensuremath{\mathbb{R}}}
\newcommand{\Zed}[0]{\ensuremath{\mathbb{Z}}}
\newcommand{\Bool}[0]{\ensuremath{\mathds{B}}}
\newcommand{\rel}[0]{\ensuremath{{\mathcal{R}}}}
\newcommand{\Gall}[0]{\ensuremath{\mathcal{G}}}
\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{Def}{Définition}

\begin{document}

 



\chapter*{Introduction}

Blabla blabla.

\mainmatter

\part{Réseaux Discrets}



\chapter{Iterations discrètes de réseaux booléens}
\JFC{chapeau à refaire}
\section{Formalisation}
\input{sdd}


\section{Combinaisons synchrones et asynchrones}
\input{mixage}


\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 de convergence de systèmes booléens]{Preuve automatique de  convergence}\label{chap:promela}
\input{modelchecking}



\JFC{Mixage}







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

% Blabla blabla.


\appendix

\chapter{Preuves sur les SDD}

\section{Convergence du mode mixe}\label{anx:mix}
\input{annexePreuveMixage}


\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},d)$}\label{anx:cont}
\input{annexecontinuite.tex}



\section{Théorème~\ref{th:Adrien}}\label{anx:sccg}
\input{annexesccg}




\backmatter

\bibliographystyle{apalike}
\bibliography{abbrev,biblioand}
\listoffigures
\listoftables
\listofdefinitions
 
\end{document}