\relax 
\providecommand\hyper@newdestlabel[2]{}
\catcode `:\active 
\catcode `;\active 
\catcode `!\active 
\catcode `?\active 
\providecommand\HyperFirstAtBeginDocument{\AtBeginDocument}
\HyperFirstAtBeginDocument{\ifx\hyper@anchor\@undefined
\global\let\oldcontentsline\contentsline
\gdef\contentsline#1#2#3#4{\oldcontentsline{#1}{#2}{#3}}
\global\let\oldnewlabel\newlabel
\gdef\newlabel#1#2{\newlabelxx{#1}#2}
\gdef\newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}}
\AtEndDocument{\ifx\hyper@anchor\@undefined
\let\contentsline\oldcontentsline
\let\newlabel\oldnewlabel
\fi}
\fi}
\global\let\hyper@last\relax 
\gdef\HyperFirstAtBeginDocument#1{#1}
\providecommand\HyField@AuxAddToFields[1]{}
\providecommand\HyField@AuxAddToCoFields[2]{}
\providecommand\@newglossary[4]{}
\@newglossary{main}{glg}{gls}{glo}
\select@language{french}
\@writefile{toc}{\select@language{french}}
\@writefile{lof}{\select@language{french}}
\@writefile{lot}{\select@language{french}}
\@writefile{toc}{\contentsline {part}{I\hspace  {1em}Syst\IeC {\`e}me Bool\IeC {\'e}ens}{1}{part.1}}
\@writefile{toc}{\contentsline {chapter}{\numberline {1}Iterations discr\IeC {\`e}tes de Syst\IeC {\`e}mes Dynamiques bool\IeC {\'e}ens}{3}{chapter.1}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\@writefile{toc}{\contentsline {section}{\numberline {1.1}Syst\IeC {\`e}me dynamique bool\IeC {\'e}en}{3}{section.1.1}}
\newlabel{sub:sdd}{{1.1}{3}{Système dynamique booléen}{section.1.1}{}}
\newlabel{eq:asyn}{{1.1}{3}{Système dynamique booléen}{equation.1.1.1}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {1.1}{\ignorespaces $g(x_1,x_2)=(\overline  {x_1},x_1\overline  {x_2}) $}}{4}{figure.1.1}}
\newlabel{fig:g:iter}{{1.1}{4}{$g(x_1,x_2)=(\overline {x_1},x_1\overline {x_2}) $}{figure.1.1}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {1.2}{\ignorespaces $h(x_1,x_2)=(\overline  {x_1},x_1\overline  {x_2}+\overline  {x_1}x_2)$}}{4}{figure.1.2}}
\newlabel{fig:h:iter}{{1.2}{4}{$h(x_1,x_2)=(\overline {x_1},x_1\overline {x_2}+\overline {x_1}x_2)$}{figure.1.2}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {1.3}{\ignorespaces Graphes d'it\IeC {\'e}rations de fonctions bool\IeC {\'e}ennes dans $\ensuremath  {\mathds  {B}}^2$}}{4}{figure.1.3}}
\newlabel{fig:xplgraphIter}{{1.3}{4}{Graphes d'itérations de fonctions booléennes dans $\Bool ^2$}{figure.1.3}{}}
\@writefile{toc}{\contentsline {section}{\numberline {1.2}Graphe d'it\IeC {\'e}rations}{4}{section.1.2}}
\newlabel{sub:grIter}{{1.2}{4}{Graphe d'itérations}{section.1.2}{}}
\@writefile{toc}{\contentsline {section}{\numberline {1.3}Graphe d'interactions}{4}{section.1.3}}
\newlabel{sub:sdd:inter}{{1.3}{4}{Graphe d'interactions}{section.1.3}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {1.4}{\ignorespaces $g(x_1,x_2)=(\overline  {x_1},x_1\overline  {x_2}) $}}{5}{figure.1.4}}
\newlabel{fig:g:inter}{{1.4}{5}{$g(x_1,x_2)=(\overline {x_1},x_1\overline {x_2}) $}{figure.1.4}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {1.5}{\ignorespaces $h(x_1,x_2)=(\overline  {x_1},x_1\overline  {x_2}+\overline  {x_1}x_2)$}}{5}{figure.1.5}}
\newlabel{fig:h:inter}{{1.5}{5}{$h(x_1,x_2)=(\overline {x_1},x_1\overline {x_2}+\overline {x_1}x_2)$}{figure.1.5}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {1.6}{\ignorespaces Graphes d'interactions de fonctions bool\IeC {\'e}ennes dans $\ensuremath  {\mathds  {B}}^2$}}{5}{figure.1.6}}
\newlabel{fig:xplgraphInter}{{1.6}{5}{Graphes d'interactions de fonctions booléennes dans $\Bool ^2$}{figure.1.6}{}}
\@writefile{toc}{\contentsline {section}{\numberline {1.4}Distance sur l'espace $\delimiter "487E912 1;n\delimiter "587F913 ^{\ensuremath  {\mathbb  {N}}}\times \ensuremath  {\mathds  {B}}^n$}{5}{section.1.4}}
\newlabel{sub:metric}{{1.4}{5}{Distance sur l'espace $\llbracket 1;n\rrbracket ^{\Nats }\times \Bool ^n$}{section.1.4}{}}
\@writefile{toc}{\contentsline {chapter}{\numberline {2}Combinaisons Synchrones et Asynchrones de Syst\IeC {\`e}mes Bool\IeC {\'e}ens}{7}{chapter.2}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\@writefile{toc}{\contentsline {section}{\numberline {2.1}G\IeC {\'e}n\IeC {\'e}ralisation au cadre asynchrone}{7}{section.2.1}}
\newlabel{eq:pseudo}{{2.1}{7}{Généralisation au cadre asynchrone}{equation.2.1.1}{}}
\newlabel{eq:async}{{2.2}{7}{Généralisation au cadre asynchrone}{equation.2.1.2}{}}
\newlabel{eq:conv}{{2.3}{7}{Généralisation au cadre asynchrone}{equation.2.1.3}{}}
\citation{Bah00}
\@writefile{toc}{\contentsline {section}{\numberline {2.2}Exemple jouet}{8}{section.2.2}}
\@writefile{lof}{\contentsline {figure}{\numberline {2.1}{\ignorespaces Fonction $f$ de l'exemple jouet.}}{8}{figure.2.1}}
\newlabel{fig:mix:map}{{2.1}{8}{Fonction $f$ de l'exemple jouet}{figure.2.1}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {2.2}{\ignorespaces Graphe d'interaction associ\IeC {\'e} \IeC {\`a} $f$.}}{8}{figure.2.2}}
\newlabel{fig:mix:xplgraph}{{2.2}{8}{Graphe d'interaction associé à $f$}{figure.2.2}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {2.3}{\ignorespaces It\IeC {\'e}rations parall\IeC {\`e}lles de $f$.}}{9}{figure.2.3}}
\newlabel{fig:mix:xplparaFig}{{2.3}{9}{Itérations parallèlles de $f$}{figure.2.3}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {2.4}{\ignorespaces Extrait d'it\IeC {\'e}rations chaotiques.}}{9}{figure.2.4}}
\newlabel{fig:mix:xplchaoFig}{{2.4}{9}{Extrait d'itérations chaotiques}{figure.2.4}{}}
\citation{Hol03}
\citation{Wei97}
\@writefile{toc}{\contentsline {chapter}{\numberline {3}Preuve de convergence de syst\IeC {\`e}mes bool\IeC {\'e}ens}{11}{chapter.3}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\newlabel{chap:promela}{{3}{11}{Preuve de convergence de systèmes booléens}{chapter.3}{}}
\@writefile{toc}{\contentsline {section}{\numberline {3.1}Exemple jouet}{11}{section.3.1}}
\@writefile{loe}{\addvspace {10\p@ }}
\@writefile{loe}{\contentsline {xpl}{\numberline {\let \autodot \@empty }Exemple}{11}{thmt@dummyctr.dummy.1}}
\@writefile{lof}{\contentsline {figure}{\numberline {3.1}{\ignorespaces Fonction \IeC {\`a} it\IeC {\'e}rer}}{11}{figure.3.1}}
\newlabel{fig:map}{{3.1}{11}{Fonction à itérer}{figure.3.1}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {3.2}{\ignorespaces Graphe d'int\IeC {\'e}raction}}{11}{figure.3.2}}
\newlabel{fig:xplgraph}{{3.2}{11}{Graphe d'intéraction}{figure.3.2}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {3.3}{\ignorespaces Exemple pour SDD $\approx $ SPIN.}}{11}{figure.3.3}}
\@writefile{toc}{\contentsline {section}{\numberline {3.2}Rappels sur le langage PROMELA}{12}{section.3.2}}
\newlabel{sec:spin:promela}{{3.2}{12}{Rappels sur le langage PROMELA}{section.3.2}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {3.4}{\ignorespaces Declaration des types de la traduction.}}{12}{figure.3.4}}
\newlabel{fig:arrayofchannels}{{3.4}{12}{Declaration des types de la traduction}{figure.3.4}{}}
\@writefile{loe}{\contentsline {xpl}{\numberline {\let \autodot \@empty }Exemple}{12}{thmt@dummyctr.dummy.2}}
\@writefile{lof}{\contentsline {figure}{\numberline {3.5}{\ignorespaces Process init.}}{13}{figure.3.5}}
\newlabel{fig:spin:init}{{3.5}{13}{Process init}{figure.3.5}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {3.6}{\ignorespaces Process scheduler pour la strat\IeC {\'e}gie pseudo p\IeC {\'e}rodique. }}{13}{figure.3.6}}
\newlabel{fig:scheduler}{{3.6}{13}{Process scheduler pour la stratégie pseudo pérodique}{figure.3.6}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {3.7}{\ignorespaces Codage du graphe d'int\IeC {\'e}raction de $f$. }}{13}{figure.3.7}}
\newlabel{fig:spin:hasnext}{{3.7}{13}{Codage du graphe d'intéraction de $f$}{figure.3.7}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {3.8}{\ignorespaces Sauvegarde de l'\IeC {\'e}tat courant}}{14}{figure.3.8}}
\newlabel{fig:spin:sauve}{{3.8}{14}{Sauvegarde de l'état courant}{figure.3.8}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {3.9}{\ignorespaces Mise \IeC {\`a} jour des \IeC {\'e}l\IeC {\'e}ments.}}{14}{figure.3.9}}
\newlabel{fig:proc}{{3.9}{14}{Mise à jour des éléments}{figure.3.9}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {3.10}{\ignorespaces Application de la fonction $f$.}}{14}{figure.3.10}}
\newlabel{fig:p}{{3.10}{14}{Application de la fonction $f$}{figure.3.10}{}}
\@writefile{toc}{\contentsline {section}{\numberline {3.3}Du syst\IeC {\`e}me bool\IeC {\'e}en au mod\IeC {\`e}le PROMELA}{14}{section.3.3}}
\newlabel{sec:spin:translation}{{3.3}{14}{Du système booléen au modèle PROMELA}{section.3.3}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3.1}La strat\IeC {\'e}gie}{14}{subsection.3.3.1}}
\newlabel{sub:spin:strat}{{3.3.1}{14}{La stratégie}{subsection.3.3.1}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3.2}It\IeC {\'e}rer la fonction $f$}{14}{subsection.3.3.2}}
\newlabel{sub:spin:update}{{3.3.2}{14}{Itérer la fonction $f$}{subsection.3.3.2}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {3.11}{\ignorespaces R\IeC {\'e}cup\IeC {\'e}rer les valeurs des elements}}{15}{figure.3.11}}
\newlabel{fig:val}{{3.11}{15}{Récupérer les valeurs des elements}{figure.3.11}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {3.12}{\ignorespaces Diffuser les valeurs des elements}}{15}{figure.3.12}}
\newlabel{fig:broadcast}{{3.12}{15}{Diffuser les valeurs des elements}{figure.3.12}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3.3}Gestion des d\IeC {\'e}lais}{15}{subsection.3.3.3}}
\newlabel{sub:spin:vt}{{3.3.3}{15}{Gestion des délais}{subsection.3.3.3}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3.4}Propri\IeC {\'e}t\IeC {\'e} de convergence universelle}{16}{subsection.3.3.4}}
\newlabel{eq:ltl:conv}{{3.1}{16}{Propriété de convergence universelle}{equation.3.3.1}{}}
\@writefile{toc}{\contentsline {section}{\numberline {3.4}Correction et compl\IeC {\'e}tude de la d\IeC {\'e}marche}{16}{section.3.4}}
\newlabel{sec:spin:proof}{{3.4}{16}{Correction et complétude de la démarche}{section.3.4}{}}
\@writefile{loe}{\contentsline {theorem}{\numberline {1}Th\IeC {\'e}or\IeC {\`e}me\thmtformatoptarg {Correction}}{16}{theorem.1}}
\newlabel{Theo:sound}{{1}{16}{Correction}{theorem.1}{}}
\@writefile{loe}{\contentsline {theorem}{\numberline {2}Th\IeC {\'e}or\IeC {\`e}me\thmtformatoptarg {Compl\IeC {\'e}tude}}{16}{theorem.2}}
\newlabel{Theo:completeness}{{2}{16}{Complétude}{theorem.2}{}}
\citation{RC07}
\citation{BM99}
\citation{BM99}
\citation{RC07}
\citation{BM99}
\@writefile{toc}{\contentsline {section}{\numberline {3.5}Donn\IeC {\'e}es pratiques}{17}{section.3.5}}
\newlabel{sec:spin:practical}{{3.5}{17}{Données pratiques}{section.3.5}{}}
\@writefile{loe}{\contentsline {theorem}{\numberline {3}Th\IeC {\'e}or\IeC {\`e}me\thmtformatoptarg {Nombre d'\IeC {\'e}tats }}{17}{theorem.3}}
\@writefile{loe}{\contentsline {Proof}{\numberline {1}Preuve}{17}{Proof.1}}
\citation{RC07}
\citation{BM99}
\citation{BCVC10:ir}
\citation{BM99}
\citation{BCV02}
\citation{Cha06}
\citation{CGK05}
\@writefile{lof}{\contentsline {figure}{\numberline {3.13}{\ignorespaces Exp\IeC {\'e}rimentations avec des it\IeC {\'e}rations synchrones}}{18}{figure.3.13}}
\newlabel{fig:sync:exp}{{3.13}{18}{Expérimentations avec des itérations synchrones}{figure.3.13}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {3.14}{\ignorespaces Exp\IeC {\'e}rimentations avec des it\IeC {\'e}rations asynchrones}}{18}{figure.3.14}}
\newlabel{fig:async:exp}{{3.14}{18}{Expérimentations avec des itérations asynchrones}{figure.3.14}{}}
\@writefile{toc}{\contentsline {section}{\numberline {3.6}Conclusion}{18}{section.3.6}}
\newlabel{sec:spin:concl}{{3.6}{18}{Conclusion}{section.3.6}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {3.15}{\ignorespaces Contre exemple de convergence pour~\ref  {fig:RC07CE}}}{19}{figure.3.15}}
\newlabel{fig:RC07CE}{{3.15}{19}{Contre exemple de convergence pour~\ref {fig:RC07CE}}{figure.3.15}{}}
\@writefile{toc}{\contentsline {chapter}{\numberline {A}Preuves sur les SDD}{21}{appendix.A}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
\@writefile{toc}{\contentsline {section}{\numberline {A.1}Preuve du th\IeC {\'e}or\IeC {\`e}me~\ref  {th:Adrien}}{21}{section.A.1}}
\newlabel{anx:sccg}{{A.1}{21}{Preuve du théorème~\ref {th:Adrien}}{section.A.1}{}}
\@writefile{loe}{\addvspace {10\p@ }}
\@writefile{loe}{\contentsline {lemma}{\numberline {1}Lemme}{21}{lemma.1}}
\newlabel{lemma:subgraph}{{1}{21}{}{lemma.1}{}}
\@writefile{loe}{\contentsline {Proof}{\numberline {2}Preuve}{21}{Proof.2}}
\@writefile{loe}{\contentsline {lemma}{\numberline {2}Lemme}{21}{lemma.2}}
\newlabel{lemma:iso}{{2}{21}{}{lemma.2}{}}
\@writefile{loe}{\contentsline {Proof}{\numberline {3}Preuve}{21}{Proof.3}}
\@writefile{loe}{\contentsline {Proof}{\numberline {4}Preuve}{21}{Proof.4}}
\@writefile{toc}{\contentsline {section}{\numberline {A.2}Preuve de continuit\IeC {\'e} de $G_f$ dans $(\mathcal  {X},d)$}{22}{section.A.2}}
\newlabel{anx:cont}{{A.2}{22}{Preuve de continuité de $G_f$ dans $(\mathcal {X},d)$}{section.A.2}{}}
\@writefile{toc}{\contentsline {section}{\numberline {A.3}Preuve de Correction et de compl\IeC {\'e}tude de l'approche de v\IeC {\'e}rification de convergence \IeC {\`a} l'aide de SPIN}{23}{section.A.3}}
\newlabel{anx:promela}{{A.3}{23}{Preuve de Correction et de complétude de l'approche de vérification de convergence à l'aide de SPIN}{section.A.3}{}}
\@writefile{loe}{\contentsline {lemma}{\numberline {3}Lemme\thmtformatoptarg {Strategy Equivalence}}{23}{lemma.3}}
\newlabel{lemma:strategy}{{3}{23}{Strategy Equivalence}{lemma.3}{}}
\@writefile{loe}{\contentsline {Proof}{\numberline {5}Preuve}{23}{Proof.5}}
\@writefile{loe}{\contentsline {lemma}{\numberline {4}Lemme\thmtformatoptarg {Existence of SPIN Execution}}{24}{lemma.4}}
\newlabel{lemma:execution}{{4}{24}{Existence of SPIN Execution}{lemma.4}{}}
\newlabel{eq:Mij0}{{A.1}{24}{Existence of SPIN Execution}{equation.A.3.1}{}}
\newlabel{eq:correct_retrieve}{{A.2}{24}{Existence of SPIN Execution}{equation.A.3.2}{}}
\@writefile{loe}{\contentsline {Proof}{\numberline {6}Preuve}{24}{Proof.6}}
\@writefile{toc}{\contentsline {paragraph}{Initial case:}{24}{section*.3}}
\@writefile{toc}{\contentsline {paragraph}{Inductive case:}{24}{section*.4}}
\@writefile{loe}{\contentsline {lemma}{\numberline {5}Lemme}{25}{lemma.5}}
\@writefile{loe}{\contentsline {Proof}{\numberline {7}Preuve}{25}{Proof.7}}
\@writefile{loe}{\contentsline {theorem}{\numberline {4}Th\IeC {\'e}or\IeC {\`e}me\thmtformatoptarg {Soundness wrt universal convergence property}}{25}{theorem.4}}
\newlabel{Theo:sound}{{4}{25}{Soundness wrt universal convergence property}{theorem.4}{}}
\@writefile{loe}{\contentsline {Proof}{\numberline {8}Preuve}{25}{Proof.8}}
\@writefile{loe}{\contentsline {theorem}{\numberline {5}Th\IeC {\'e}or\IeC {\`e}me\thmtformatoptarg {Completeness wrt universal convergence property}}{26}{theorem.5}}
\newlabel{Theo:completeness}{{5}{26}{Completeness wrt universal convergence property}{theorem.5}{}}
\@writefile{loe}{\contentsline {Proof}{\numberline {9}Preuve}{26}{Proof.9}}
\bibstyle{apalike}
\bibdata{abbrev,biblioand}
\bibcite{Bah00}{Bahi, 2000}
\bibcite{BCV02}{Bahi and Contassot-Vivier, 2002}
\bibcite{BCVC10:ir}{Bahi et~al., 2010}
\bibcite{BM99}{Bahi and Michel, 1999}
\bibcite{Cha06}{Chandrasekaran, 2006}
\bibcite{CGK05}{Couchot et~al., 2005}
\bibcite{Hol03}{Holzmann, 2003}
\bibcite{RC07}{Richard and Comet, 2007}
\bibcite{Wei97}{Weise, 1997}