main.aux

   1 \relax
   2 \providecommand\hyper@newdestlabel[2]{}
   3 \catcode `:\active
   4 \catcode `;\active
   5 \catcode `!\active
   6 \catcode `?\active
   7 \providecommand\HyperFirstAtBeginDocument{\AtBeginDocument}
   8 \HyperFirstAtBeginDocument{\ifx\hyper@anchor\@undefined
   9 \global\let\oldcontentsline\contentsline
  10 \gdef\contentsline#1#2#3#4{\oldcontentsline{#1}{#2}{#3}}
  11 \global\let\oldnewlabel\newlabel
  12 \gdef\newlabel#1#2{\newlabelxx{#1}#2}
  13 \gdef\newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}}
  14 \AtEndDocument{\ifx\hyper@anchor\@undefined
  15 \let\contentsline\oldcontentsline
  16 \let\newlabel\oldnewlabel
  17 \fi}
  18 \fi}
  19 \global\let\hyper@last\relax
  20 \gdef\HyperFirstAtBeginDocument#1{#1}
  21 \providecommand\HyField@AuxAddToFields[1]{}
  22 \providecommand\HyField@AuxAddToCoFields[2]{}
  23 \providecommand\@newglossary[4]{}
  24 \@newglossary{main}{glg}{gls}{glo}
  25 \select@language{french}
  26 \@writefile{toc}{\select@language{french}}
  27 \@writefile{lof}{\select@language{french}}
  28 \@writefile{lot}{\select@language{french}}
  29 \@writefile{toc}{\contentsline {part}{I\hspace  {1em}Syst\IeC {\`e}me Bool\IeC {\'e}ens}{1}{part.1}}
  30 \@writefile{toc}{\contentsline {chapter}{\numberline {1}Iterations discr\IeC {\`e}tes de Syst\IeC {\`e}mes Dynamiques bool\IeC {\'e}ens}{3}{chapter.1}}
  31 \@writefile{lof}{\addvspace {10\p@ }}
  32 \@writefile{lot}{\addvspace {10\p@ }}
  33 \@writefile{toc}{\contentsline {section}{\numberline {1.1}Syst\IeC {\`e}me dynamique bool\IeC {\'e}en}{3}{section.1.1}}
  34 \newlabel{sub:sdd}{{1.1}{3}{Système dynamique booléen}{section.1.1}{}}
  35 \newlabel{eq:asyn}{{1.1}{3}{Système dynamique booléen}{equation.1.1.1}{}}
  36 \@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}}
  37 \newlabel{fig:g:iter}{{1.1}{4}{$g(x_1,x_2)=(\overline {x_1},x_1\overline {x_2}) $}{figure.1.1}{}}
  38 \@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}}
  39 \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}{}}
  40 \@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}}
  41 \newlabel{fig:xplgraphIter}{{1.3}{4}{Graphes d'itérations de fonctions booléennes dans $\Bool ^2$}{figure.1.3}{}}
  42 \@writefile{toc}{\contentsline {section}{\numberline {1.2}Graphe d'it\IeC {\'e}rations}{4}{section.1.2}}
  43 \newlabel{sub:grIter}{{1.2}{4}{Graphe d'itérations}{section.1.2}{}}
  44 \@writefile{toc}{\contentsline {section}{\numberline {1.3}Graphe d'interactions}{4}{section.1.3}}
  45 \newlabel{sub:sdd:inter}{{1.3}{4}{Graphe d'interactions}{section.1.3}{}}
  46 \@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}}
  47 \newlabel{fig:g:inter}{{1.4}{5}{$g(x_1,x_2)=(\overline {x_1},x_1\overline {x_2}) $}{figure.1.4}{}}
  48 \@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}}
  49 \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}{}}
  50 \@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}}
  51 \newlabel{fig:xplgraphInter}{{1.6}{5}{Graphes d'interactions de fonctions booléennes dans $\Bool ^2$}{figure.1.6}{}}
  52 \@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}}
  53 \newlabel{sub:metric}{{1.4}{5}{Distance sur l'espace $\llbracket 1;n\rrbracket ^{\Nats }\times \Bool ^n$}{section.1.4}{}}
  54 \@writefile{toc}{\contentsline {chapter}{\numberline {2}Combinaisons Synchrones et Asynchrones de Syst\IeC {\`e}mes Bool\IeC {\'e}ens}{7}{chapter.2}}
  55 \@writefile{lof}{\addvspace {10\p@ }}
  56 \@writefile{lot}{\addvspace {10\p@ }}
  57 \@writefile{toc}{\contentsline {section}{\numberline {2.1}G\IeC {\'e}n\IeC {\'e}ralisation au cadre asynchrone}{7}{section.2.1}}
  58 \newlabel{eq:pseudo}{{2.1}{7}{Généralisation au cadre asynchrone}{equation.2.1.1}{}}
  59 \newlabel{eq:async}{{2.2}{7}{Généralisation au cadre asynchrone}{equation.2.1.2}{}}
  60 \newlabel{eq:conv}{{2.3}{7}{Généralisation au cadre asynchrone}{equation.2.1.3}{}}
  61 \citation{Bah00}
  62 \@writefile{toc}{\contentsline {section}{\numberline {2.2}Exemple jouet}{8}{section.2.2}}
  63 \@writefile{lof}{\contentsline {figure}{\numberline {2.1}{\ignorespaces Fonction $f$ de l'exemple jouet.}}{8}{figure.2.1}}
  64 \newlabel{fig:mix:map}{{2.1}{8}{Fonction $f$ de l'exemple jouet}{figure.2.1}{}}
  65 \@writefile{lof}{\contentsline {figure}{\numberline {2.2}{\ignorespaces Graphe d'interaction associ\IeC {\'e} \IeC {\`a} $f$.}}{8}{figure.2.2}}
  66 \newlabel{fig:mix:xplgraph}{{2.2}{8}{Graphe d'interaction associé à $f$}{figure.2.2}{}}
  67 \@writefile{lof}{\contentsline {figure}{\numberline {2.3}{\ignorespaces It\IeC {\'e}rations parall\IeC {\`e}lles de $f$.}}{9}{figure.2.3}}
  68 \newlabel{fig:mix:xplparaFig}{{2.3}{9}{Itérations parallèlles de $f$}{figure.2.3}{}}
  69 \@writefile{lof}{\contentsline {figure}{\numberline {2.4}{\ignorespaces Extrait d'it\IeC {\'e}rations chaotiques.}}{9}{figure.2.4}}
  70 \newlabel{fig:mix:xplchaoFig}{{2.4}{9}{Extrait d'itérations chaotiques}{figure.2.4}{}}
  71 \citation{Hol03}
  72 \citation{Wei97}
  73 \@writefile{toc}{\contentsline {chapter}{\numberline {3}Preuve de convergence de syst\IeC {\`e}mes bool\IeC {\'e}ens}{11}{chapter.3}}
  74 \@writefile{lof}{\addvspace {10\p@ }}
  75 \@writefile{lot}{\addvspace {10\p@ }}
  76 \newlabel{chap:promela}{{3}{11}{Preuve de convergence de systèmes booléens}{chapter.3}{}}
  77 \@writefile{toc}{\contentsline {section}{\numberline {3.1}Exemple jouet}{11}{section.3.1}}
  78 \@writefile{loe}{\addvspace {10\p@ }}
  79 \@writefile{loe}{\contentsline {xpl}{\numberline {\let \autodot \@empty }Exemple}{11}{thmt@dummyctr.dummy.1}}
  80 \@writefile{lof}{\contentsline {figure}{\numberline {3.1}{\ignorespaces Fonction \IeC {\`a} it\IeC {\'e}rer}}{11}{figure.3.1}}
  81 \newlabel{fig:map}{{3.1}{11}{Fonction à itérer}{figure.3.1}{}}
  82 \@writefile{lof}{\contentsline {figure}{\numberline {3.2}{\ignorespaces Graphe d'int\IeC {\'e}raction}}{11}{figure.3.2}}
  83 \newlabel{fig:xplgraph}{{3.2}{11}{Graphe d'intéraction}{figure.3.2}{}}
  84 \@writefile{lof}{\contentsline {figure}{\numberline {3.3}{\ignorespaces Exemple pour SDD $\approx $ SPIN.}}{11}{figure.3.3}}
  85 \@writefile{toc}{\contentsline {section}{\numberline {3.2}Rappels sur le langage PROMELA}{12}{section.3.2}}
  86 \newlabel{sec:spin:promela}{{3.2}{12}{Rappels sur le langage PROMELA}{section.3.2}{}}
  87 \@writefile{lof}{\contentsline {figure}{\numberline {3.4}{\ignorespaces Declaration des types de la traduction.}}{12}{figure.3.4}}
  88 \newlabel{fig:arrayofchannels}{{3.4}{12}{Declaration des types de la traduction}{figure.3.4}{}}
  89 \@writefile{loe}{\contentsline {xpl}{\numberline {\let \autodot \@empty }Exemple}{12}{thmt@dummyctr.dummy.2}}
  90 \@writefile{lof}{\contentsline {figure}{\numberline {3.5}{\ignorespaces Process init.}}{13}{figure.3.5}}
  91 \newlabel{fig:spin:init}{{3.5}{13}{Process init}{figure.3.5}{}}
  92 \@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}}
  93 \newlabel{fig:scheduler}{{3.6}{13}{Process scheduler pour la stratégie pseudo pérodique}{figure.3.6}{}}
  94 \@writefile{lof}{\contentsline {figure}{\numberline {3.7}{\ignorespaces Codage du graphe d'int\IeC {\'e}raction de $f$. }}{13}{figure.3.7}}
  95 \newlabel{fig:spin:hasnext}{{3.7}{13}{Codage du graphe d'intéraction de $f$}{figure.3.7}{}}
  96 \@writefile{lof}{\contentsline {figure}{\numberline {3.8}{\ignorespaces Sauvegarde de l'\IeC {\'e}tat courant}}{14}{figure.3.8}}
  97 \newlabel{fig:spin:sauve}{{3.8}{14}{Sauvegarde de l'état courant}{figure.3.8}{}}
  98 \@writefile{lof}{\contentsline {figure}{\numberline {3.9}{\ignorespaces Mise \IeC {\`a} jour des \IeC {\'e}l\IeC {\'e}ments.}}{14}{figure.3.9}}
  99 \newlabel{fig:proc}{{3.9}{14}{Mise à jour des éléments}{figure.3.9}{}}
 100 \@writefile{lof}{\contentsline {figure}{\numberline {3.10}{\ignorespaces Application de la fonction $f$.}}{14}{figure.3.10}}
 101 \newlabel{fig:p}{{3.10}{14}{Application de la fonction $f$}{figure.3.10}{}}
 102 \@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}}
 103 \newlabel{sec:spin:translation}{{3.3}{14}{Du système booléen au modèle PROMELA}{section.3.3}{}}
 104 \@writefile{toc}{\contentsline {subsection}{\numberline {3.3.1}La strat\IeC {\'e}gie}{14}{subsection.3.3.1}}
 105 \newlabel{sub:spin:strat}{{3.3.1}{14}{La stratégie}{subsection.3.3.1}{}}
 106 \@writefile{toc}{\contentsline {subsection}{\numberline {3.3.2}It\IeC {\'e}rer la fonction $f$}{14}{subsection.3.3.2}}
 107 \newlabel{sub:spin:update}{{3.3.2}{14}{Itérer la fonction $f$}{subsection.3.3.2}{}}
 108 \@writefile{lof}{\contentsline {figure}{\numberline {3.11}{\ignorespaces R\IeC {\'e}cup\IeC {\'e}rer les valeurs des elements}}{15}{figure.3.11}}
 109 \newlabel{fig:val}{{3.11}{15}{Récupérer les valeurs des elements}{figure.3.11}{}}
 110 \@writefile{lof}{\contentsline {figure}{\numberline {3.12}{\ignorespaces Diffuser les valeurs des elements}}{15}{figure.3.12}}
 111 \newlabel{fig:broadcast}{{3.12}{15}{Diffuser les valeurs des elements}{figure.3.12}{}}
 112 \@writefile{toc}{\contentsline {subsection}{\numberline {3.3.3}Gestion des d\IeC {\'e}lais}{15}{subsection.3.3.3}}
 113 \newlabel{sub:spin:vt}{{3.3.3}{15}{Gestion des délais}{subsection.3.3.3}{}}
 114 \@writefile{toc}{\contentsline {subsection}{\numberline {3.3.4}Propri\IeC {\'e}t\IeC {\'e} de convergence universelle}{16}{subsection.3.3.4}}
 115 \newlabel{eq:ltl:conv}{{3.1}{16}{Propriété de convergence universelle}{equation.3.3.1}{}}
 116 \@writefile{toc}{\contentsline {section}{\numberline {3.4}Correction et compl\IeC {\'e}tude de la d\IeC {\'e}marche}{16}{section.3.4}}
 117 \newlabel{sec:spin:proof}{{3.4}{16}{Correction et complétude de la démarche}{section.3.4}{}}
 118 \@writefile{loe}{\contentsline {theorem}{\numberline {1}Th\IeC {\'e}or\IeC {\`e}me\thmtformatoptarg {Correction}}{16}{theorem.1}}
 119 \newlabel{Theo:sound}{{1}{16}{Correction}{theorem.1}{}}
 120 \@writefile{loe}{\contentsline {theorem}{\numberline {2}Th\IeC {\'e}or\IeC {\`e}me\thmtformatoptarg {Compl\IeC {\'e}tude}}{16}{theorem.2}}
 121 \newlabel{Theo:completeness}{{2}{16}{Complétude}{theorem.2}{}}
 122 \citation{RC07}
 123 \citation{BM99}
 124 \citation{BM99}
 125 \citation{RC07}
 126 \citation{BM99}
 127 \@writefile{toc}{\contentsline {section}{\numberline {3.5}Donn\IeC {\'e}es pratiques}{17}{section.3.5}}
 128 \newlabel{sec:spin:practical}{{3.5}{17}{Données pratiques}{section.3.5}{}}
 129 \@writefile{loe}{\contentsline {theorem}{\numberline {3}Th\IeC {\'e}or\IeC {\`e}me\thmtformatoptarg {Nombre d'\IeC {\'e}tats }}{17}{theorem.3}}
 130 \@writefile{loe}{\contentsline {Proof}{\numberline {1}Preuve}{17}{Proof.1}}
 131 \citation{RC07}
 132 \citation{BM99}
 133 \citation{BCVC10:ir}
 134 \citation{BM99}
 135 \citation{BCV02}
 136 \citation{Cha06}
 137 \citation{CGK05}
 138 \@writefile{lof}{\contentsline {figure}{\numberline {3.13}{\ignorespaces Exp\IeC {\'e}rimentations avec des it\IeC {\'e}rations synchrones}}{18}{figure.3.13}}
 139 \newlabel{fig:sync:exp}{{3.13}{18}{Expérimentations avec des itérations synchrones}{figure.3.13}{}}
 140 \@writefile{lof}{\contentsline {figure}{\numberline {3.14}{\ignorespaces Exp\IeC {\'e}rimentations avec des it\IeC {\'e}rations asynchrones}}{18}{figure.3.14}}
 141 \newlabel{fig:async:exp}{{3.14}{18}{Expérimentations avec des itérations asynchrones}{figure.3.14}{}}
 142 \@writefile{toc}{\contentsline {section}{\numberline {3.6}Conclusion}{18}{section.3.6}}
 143 \newlabel{sec:spin:concl}{{3.6}{18}{Conclusion}{section.3.6}{}}
 144 \@writefile{lof}{\contentsline {figure}{\numberline {3.15}{\ignorespaces Contre exemple de convergence pour~\ref  {fig:RC07CE}}}{19}{figure.3.15}}
 145 \newlabel{fig:RC07CE}{{3.15}{19}{Contre exemple de convergence pour~\ref {fig:RC07CE}}{figure.3.15}{}}
 146 \@writefile{toc}{\contentsline {chapter}{\numberline {A}Preuves sur les SDD}{21}{appendix.A}}
 147 \@writefile{lof}{\addvspace {10\p@ }}
 148 \@writefile{lot}{\addvspace {10\p@ }}
 149 \@writefile{toc}{\contentsline {section}{\numberline {A.1}Preuve du th\IeC {\'e}or\IeC {\`e}me~\ref  {th:Adrien}}{21}{section.A.1}}
 150 \newlabel{anx:sccg}{{A.1}{21}{Preuve du théorème~\ref {th:Adrien}}{section.A.1}{}}
 151 \@writefile{loe}{\addvspace {10\p@ }}
 152 \@writefile{loe}{\contentsline {lemma}{\numberline {1}Lemme}{21}{lemma.1}}
 153 \newlabel{lemma:subgraph}{{1}{21}{}{lemma.1}{}}
 154 \@writefile{loe}{\contentsline {Proof}{\numberline {2}Preuve}{21}{Proof.2}}
 155 \@writefile{loe}{\contentsline {lemma}{\numberline {2}Lemme}{21}{lemma.2}}
 156 \newlabel{lemma:iso}{{2}{21}{}{lemma.2}{}}
 157 \@writefile{loe}{\contentsline {Proof}{\numberline {3}Preuve}{21}{Proof.3}}
 158 \@writefile{loe}{\contentsline {Proof}{\numberline {4}Preuve}{21}{Proof.4}}
 159 \@writefile{toc}{\contentsline {section}{\numberline {A.2}Preuve de continuit\IeC {\'e} de $G_f$ dans $(\mathcal  {X},d)$}{22}{section.A.2}}
 160 \newlabel{anx:cont}{{A.2}{22}{Preuve de continuité de $G_f$ dans $(\mathcal {X},d)$}{section.A.2}{}}
 161 \@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}}
 162 \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}{}}
 163 \@writefile{loe}{\contentsline {lemma}{\numberline {3}Lemme\thmtformatoptarg {Strategy Equivalence}}{23}{lemma.3}}
 164 \newlabel{lemma:strategy}{{3}{23}{Strategy Equivalence}{lemma.3}{}}
 165 \@writefile{loe}{\contentsline {Proof}{\numberline {5}Preuve}{23}{Proof.5}}
 166 \@writefile{loe}{\contentsline {lemma}{\numberline {4}Lemme\thmtformatoptarg {Existence of SPIN Execution}}{24}{lemma.4}}
 167 \newlabel{lemma:execution}{{4}{24}{Existence of SPIN Execution}{lemma.4}{}}
 168 \newlabel{eq:Mij0}{{A.1}{24}{Existence of SPIN Execution}{equation.A.3.1}{}}
 169 \newlabel{eq:correct_retrieve}{{A.2}{24}{Existence of SPIN Execution}{equation.A.3.2}{}}
 170 \@writefile{loe}{\contentsline {Proof}{\numberline {6}Preuve}{24}{Proof.6}}
 171 \@writefile{toc}{\contentsline {paragraph}{Initial case:}{24}{section*.3}}
 172 \@writefile{toc}{\contentsline {paragraph}{Inductive case:}{24}{section*.4}}
 173 \@writefile{loe}{\contentsline {lemma}{\numberline {5}Lemme}{25}{lemma.5}}
 174 \@writefile{loe}{\contentsline {Proof}{\numberline {7}Preuve}{25}{Proof.7}}
 175 \@writefile{loe}{\contentsline {theorem}{\numberline {4}Th\IeC {\'e}or\IeC {\`e}me\thmtformatoptarg {Soundness wrt universal convergence property}}{25}{theorem.4}}
 176 \newlabel{Theo:sound}{{4}{25}{Soundness wrt universal convergence property}{theorem.4}{}}
 177 \@writefile{loe}{\contentsline {Proof}{\numberline {8}Preuve}{25}{Proof.8}}
 178 \@writefile{loe}{\contentsline {theorem}{\numberline {5}Th\IeC {\'e}or\IeC {\`e}me\thmtformatoptarg {Completeness wrt universal convergence property}}{26}{theorem.5}}
 179 \newlabel{Theo:completeness}{{5}{26}{Completeness wrt universal convergence property}{theorem.5}{}}
 180 \@writefile{loe}{\contentsline {Proof}{\numberline {9}Preuve}{26}{Proof.9}}
 181 \bibstyle{apalike}
 182 \bibdata{abbrev,biblioand}
 183 \bibcite{Bah00}{Bahi, 2000}
 184 \bibcite{BCV02}{Bahi and Contassot-Vivier, 2002}
 185 \bibcite{BCVC10:ir}{Bahi et~al., 2010}
 186 \bibcite{BM99}{Bahi and Michel, 1999}
 187 \bibcite{Cha06}{Chandrasekaran, 2006}
 188 \bibcite{CGK05}{Couchot et~al., 2005}
 189 \bibcite{Hol03}{Holzmann, 2003}
 190 \bibcite{RC07}{Richard and Comet, 2007}
 191 \bibcite{Wei97}{Weise, 1997}