preuve promela traduite

[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{tikz}
\usepackage{pgfplots}
\usepgfplotslibrary{groupplots}

%\usepackage[font=footnotesize]{subfig}
\usepackage[utf8]{inputenc}
\usepackage{thmtools, thm-restate}
\usepackage{multirow}
\usepackage{algorithm2e}
\usepackage{mathtools}

%\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[couchot@femto-st.fr]{Jean-François}{Couchot}

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


\newcommand {\tv}[1] {\lVert #1 \rVert_{\rm TV}}
\def \top {1.8}
\def \topt {2.3}
\def \P {\mathbb{P}}
\def \ov {\overline}
\def \ts {\tau_{\rm stop}}
\def\rl{{^{.}}}

\DeclarePairedDelimiter\abs{\lvert}{\rvert}%
\DeclarePairedDelimiter\norm{\lVert}{\rVert}%

% Swap the definition of \abs* and \norm*, so that \abs
% and \norm resizes the size of the brackets, and the 
% starred version does not.
\makeatletter
\let\oldabs\abs
\def\abs{\@ifstar{\oldabs}{\oldabs*}}
%
\let\oldnorm\norm
\def\norm{\@ifstar{\oldnorm}{\oldnorm*}}
\makeatother

\newtheorem{theorem}{Théorème}
\newtheorem{lemma}{Lemme}
\newtheorem{corollary}{Corollaire}
\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}

Ce chapitre formalise tout d'abord ce qu'est 
un réseau booléen (section~\ref{sec:sdd:formalisation}. On y revoit 
les différents modes opératoires, leur représentation à l'aide de 
graphes et les résultats connus de convergence).
Ce chapitre montre ensuite à la section~\ref{sec:sdd:mixage}
comment combiner ces modes pour converger aussi 
souvent, mais plus rapidement vers un point fixe. Les deux 
dernières sections ont fait l'objet du rapport~\cite{BCVC10:ir}.

\section{Formalisation}\label{sec:sdd:formalisation}
\input{sdd}

\section{Combinaisons synchrones et asynchrones}\label{sec:sdd:mixage}
\input{mixage}

\section{Conclusion}

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, après avoir introduit les bases sur les réseaux bouléens,
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}






\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}\label{chap:carachaos}

La suite de ce document se focalise sur des systèmes dynamiques discrets qui ne 
convergent pas. Parmi ceux-ci se trouvent ceux qui sont \og chaotiques\fg{}.
La première section  de ce chapitre rappelle ce que sont les systèmes 
dynamiques chaotiques et leur caractéristiques. Celles-ci dépendent 
tout d'abord de la stratégie itérée. La section~\ref{sec:TIPE12} 
se focalise sur le schéma unaire tandis que la section~\ref{sec:chaos:TSI}
considère le mode généralisé. Pour chacun de ces modes, 
une distance est définie. Finalement, la section~\ref{sec:11FCT}
exhibe des conditions suffisantes premettant d'engendrer 
des fonctions chaotiques seon le mode unaire.
Les sections~\ref{sec:TIPE12} et~\ref{sec:11FCT} ont été publiées 
dans~\cite{bcgr11:ip}.

\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é}\label{sec:chaos:TSI}
\input{15TSI}


\section{Générer des fonctions chaotiques}\label{sec:11FCT}
\input{11FCT} 

\section{Conclusion}
Ce chapitre a montré que les itérations unaires sont chaotiques si
et seulement si le graphe $\textsc{giu}(f)$ est fortement connexe et 
que les itérations généralisées sont chaotiques si
et seulement si le graphe $\textsc{gig}(f)$ est aussi fortement connexe.
On dispose ainsi à priori d'une collection infinie de fonctions chaotiques.
Le chapitre suivant s'intéresse à essayer de prédire le comportement 
de telles fonctions. 


\chapter{Prédiction des systèmes chaotiques}
\input{chaosANN}




\part{Applications à la génération de nombres pseudo aléatoires}

\chapter{Caractérisation des générateurs chaotiques}
\input{15RairoGen}

\chapter{Les générateurs issus des codes de Gray}
\input{14Secrypt}



\part{Application au marquage de média}


\chapter{Des embarquement préservant le chaos}\label{chap:watermarking} 
\input{oxford}

\chapter{Une démarche de  marquage de PDF}
\input{ahmad}


\chapter{Une démarches plus classique de dissimulation: STABYLO}
 \input{stabylo}

\chapter{Schéma de stéganographie: les dérivées du second ordre}
 \input{stegoyousra}



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

\JFC{Perspective ANN}

In  future  work we  intend  to  enlarge  the comparison  between  the
learning   of  truly   chaotic  and   non-chaotic   behaviors.   Other
computational intelligence tools such  as support vector machines will
be investigated  too, to  discover which tools  are the  most relevant
when facing a truly chaotic phenomenon.  A comparison between learning
rate  success  and  prediction  quality will  be  realized.   Concrete
consequences in biology, physics, and computer science security fields
will then be stated.
Ajouter lefait que le codede gray n'est pas optimal.
On pourrait aussi travailler à établir un classement qui préserverait 
le fait que deux configurations voisines seraient représentées 
par deux entiers voisins. Par optimisation? 
 
\JFC{Perspectives pour les générateurs} : marcher ou sauter... comment on 
pourrait étendre, ce que l'on a déjà, ce qu'il reste à faire.


\JFC{prespectives watermarking : réécrire l'algo nicolas dans le formalisme
du chapitre 8}

% TSI 2015 



% \chapter{Conclusion}

% Blabla blabla.


\appendix

\chapter{Preuves sur les réseaux discrets}

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


\chapter{Preuves sur les générateurs de nombres pseudo-aléatoires}\label{anx:generateur}
\input{annexePreuveDistribution}
\input{annexePreuveGrayEquilibre}
\input{annexePreuveStopping}

\chapter{Preuves sur le marquage de média}\label{anx:marquage}
\section{Le marquage est $\epsilon$-sego-secure}
\input{annexePreuveMarquagedhci}

\section{Le mode $f_l$ est doublement stochastique}\label{anx:marquage:dblesto}
\input{annexePreuveMarquagefldblement}

\section{Le marquage est correct et complet}\label{anx:preuve:marquage:correctioncompletue}
\input{annexePreuveMarquageCorrectioncompletude}
\backmatter

\section{Complexité d'Algorithmes de stéganographie}
\label{anx:preuve:cplxt}
\input{annexePreuvesComplexiteStego}



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