STDM~\cite{CW01} est une instance de ces schémas de marquage.
Ce chapitre présente une application de STDM au marquage de documents PDFs.
-\JFC{annonce du plan}
+La première section fournit quelques rappels sur la STDM. Le schéma basé sur
+cette approche est présenté à la section~\ref{sec:stdm:schema}.
+Finalement, la démarche expérimentale permettant de trouver un compromis entre
+robustesse et qualité visuelle est présentée à la section~\ref{sec:stdm:exp}
+Ce travail a été publié dans~\cite{BDCC16}.
+
+
\section{Rappels sur la Spread Transform Dither Modulation}
\label{sec:STDM}
Tous les éléments sont en place pour embarquer une marque
dans un fichier PDF selon le schéma STDM.
-\section{Application au marquage de documents PDF}
+\section{Application au marquage de documents PDF}\label{sec:stdm:schema}
On détaille successivement comment insérer une marque dans un document PDF,
puis comment l'extraire.
en remplaçant $x'$ par $\dot{x'}$ .
\end{enumerate}
-\section{Expérimentations }
+\section{Expérimentations}\label{sec:stdm:exp}
Le schéma de marquage est paramétré par $\Delta$, $d_0$ et la manière de construire le vecteur $p$ pour une taille $L$.
Les travaux réalisés se sont focalisés sur l'influence du paramètre
$D_S = \frac{\Delta^2}{12L}$ dans l'algorithme en satisfaisant
Formellement, \class{p}
$\preceq$ \class{q}
s'il existe un chemin de longueur $\alpha$
-($0<\alpha<|\mathcal{K}|$) entre un élément le la classe
+($0\le\alpha<|\mathcal{K}|$) entre un élément le la classe
\class{p} vers un élément de
-\class{q}.
-On remarque que si la \class{p}$\preceq$\class{q},
-il n'est alors pas possible que \class{q}$\preceq$\class{p}.
+\class{q}.
\begin{lemma}
Il existe un processus de renommage qui effecte un nouvel identifiant aux
\begin{Proof}
Tout d'abord, soit \class{p_1}, \ldots, \class{p_l} des classes
- contenant respectivement $n_1$,\ldots, $n_l$ éléments respectively
+ contenant respectivement les éléments $n_1$,\ldots, $n_l$
qui ne dépendent d'aucune autre classe.
Les éléments de \class{p_1} sont renommés par $1$, \ldots, $n_1$,
les elements de \class{p_i}, $2 \le i \le l$ sont renommés par
% Processes numbers are already compliant with the order $\preceq$.
% \end{xpl}
-\begin{Proof}[of Theorem~\ref{th:cvg}]
+\begin{Proof}[du théorème~\ref{th:cvg}]
Le reste de la preuve est fait par induction sur le numéro de classe.
Considérons la première classe \class{b_1} de $n_1$ éléments
pour chaque
$p_{k+1} \in$ \class{b_{k+1}} et $p_j \in$ \class{b_j}, $1 \le j \le k$.
- Il nous reste donc des itérations synchronous entre les
+ Il ne reste donc que des itérations synchrones entre les
elements of \class{b_{k+1}} en démarant dans des configurations
où tous les éléments de \class{b_j}, $1 \le j
- \le k$, on des valeurs constantes.
+ \le k$, ont des valeurs constantes.
D'après les hypothèses du théorème, cela converge.
\end{Proof}
-\JFC{Voir section~\ref{sec:spin:proof}}
+%\JFC{Voir section~\ref{sec:spin:proof}}
Cette section donne les preuves des deux théorèmes de correction et complétude
du chapitre~\ref{chap:promela}.
-\begin{lemma}[Strategy Equivalence]\label{lemma:strategy}
+\begin{lemma}[Stratégie équivalente]\label{lemma:strategy}
Soit $\phi$ un système dynamique discret de stratégie $(S^t)^{t \in \Nats}$
et $\psi$ sa traduction en promela.
Il existe une exécution de $\psi$ sous hypothèse d'équité faible telle
\end{Proof}
Dans ce qui suit, soit $Xd^t_{ji}$ la valeur de
-\verb+Xd[+$j$\verb+].v[+$i$\verb+]+ après le $t^{\text{th}}$ appel
+\verb+Xd[+$j$\verb+].v[+$i$\verb+]+ après le $t^{\text{ème}}$ appel
à la fonction
\verb+fetch_values+.
De plus, soit $Y^k_{ij}$ l'élément à l'indice $k$
La function $M_{ij}^{t+1}$ est obtenue à l'aide de mises à jour successives
de $M_{ij}^{t}$ au travers des deux functions \verb+fetch_values+ and
\verb+diffuse_values+. Par abus, soit $M_{ij}^{t+1/2}$
-la valeur de $M_{ij}^{t}$ après la première fonctions pendant l'itération
+la valeur de $M_{ij}^{t}$ après la première fonction pendant l'itération
$t$.
Dans ce qui suit, on considère les éléments $i$ et $j$
-dans $\llbracket n \rrbracket$.
+dans $[ \mathsf{N} ]$.
A l'itération $t$, $t \geq 1$, soit
$(Y^0_{ij},a^0_{ij},c^0_{ij})$ la valeur de $M_{ij}^t(0)$ en entrant
dans la fonction
Pour chaque sequence $(S^t)^{t \in \Nats}$,\linebreak $(D^t)^{t \in \Nats}$,
pour chaque fonction $F$,
il existe une exécution SPIN telle que pour toute itération $t$, $t
- \ge 1$, et pour chaque $i$ et $j$ in $\llbracket n \rrbracket$
+ \ge 1$, et pour chaque $i$ et $j$ dans $[ \mathsf{N} ]$
on a la propriété suivante:
\noindent Si le domaine de $M_{ij}^t$ n'est pas vide, alors
\left\{
\begin{array}{rcl}
M_{ij}^1(0) & = & \left(X_i^{D_{ji}^{0}}, 0,0 \right) \\
- \textrm{sit $t \geq 2$ alors }M_{ij}^t(0) & = &
+ \textrm{si $t \geq 2$ alors }M_{ij}^t(0) & = &
\left(X_i^{D_{ji}^{c}},D_{ji}^{c},c \right) \textrm{, }
c = \min\{l | D_{ji}^l > D_{ji}^{t-2} \}
\end{array}
\forall t'\, .\, 1 \le t' \le t \Rightarrow Xd^{t'}_{ji} = X^{D^{t'-1}_{ji}}_i
\label{eq:correct_retrieve}
\end{equation}
-\noindent Enfin, pour chaque $k\in S^t$, la valeurde
+\noindent Enfin, pour chaque $k\in S^t$, la valeur de
la variable \verb+Xp[k]+ en sortant du processus
\verb+update_elems+ est égale à
$X_k^{t}$ \textit{i.e.}, $F_{k}\left( X_1^{D_{k\,1}^{t-1}},\ldots,
- X_{n}^{D_{k\,{n}}^{t-1}}\right)$ à la fin de la $t^{\text{th}}$ itération.
+ X_{\mathsf{N}}^{D_{k\,{\mathsf{N}}}^{t-1}}\right)$ à la fin de la $t^{\text{th}}$ itération.
\end{lemma}
\begin{Proof}
La preuve est faite par induction sur le nombre d'itérations.
Pour le premier item, par definition de $M_{ij}^t$, on a $M_{ij}^1(0) = \left(
\verb+Xp[i]+, 0,0 \right)$ qui est égal à $\left(X_i^{D_{ji}^{0}},
0,0 \right)$.
-Ensuite, lepremier appel à la fonction \verb+fetch_value+
+Ensuite, le premier appel à la fonction \verb+fetch_value+
soit affecte à la tête de \verb+channels[i].sent[j]+ à \verb+Xd[j].v[i]+ soit ne modifie par
\verb+Xd[j].v[i]+.
Grâce au processus \verb+init+ process,
les deux cas sont égaux à
\verb+Xp[i]+, \textit{i.e.}, $X_i^0$. L'equation (\ref{eq:correct_retrieve}) est ainsi établie.
-Pour le dernier item, soit $k$, $0 \le k \le n-1$.
+Pour le dernier item, soit $k$, $0 \le k \le \mathsf{N}-1$.
A la fin de la première exécution du processus \verb+update_elems+,
-la valur de
+la valeur de
\verb+Xp[k]+ est $F(\verb+Xd[+k\verb+].v[0]+, \ldots,
-\verb+Xd[+k\verb+].v[+n-1\verb+]+)$.
+\verb+Xd[+k\verb+].v[+\mathsf{N}-1\verb+]+)$.
Ainsi par définition de $Xd$, ceci est égal à
-$F(Xd^1_{k\,0}, \ldots,Xd^1_{k\,n-1})$. Grâce à l'équation \Equ{eq:correct_retrieve},
+$F(Xd^1_{k\,0}, \ldots,Xd^1_{k\,\mathsf{N}-1})$. Grâce à l'équation \Equ{eq:correct_retrieve},
on peut conclure la preuve.
$\left(X_i^{D_{ji}^{c}}, D_{ji}^{c},c
\right)$ où $c$ est $\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$.
-A l'itération $l$, si $l < c + 1$ alors \verb+skip+ statement is executed in
-the \verb+fetch_values+ function. Thus, $M_{ij}^{l+1}(0)$ is equal to
-$M_{ij}^{l}(0)$. Since $c > l-1$ then $D_{ji}^c > D_{ji}^{l-1}$ and hence, $c$
-is $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$. Obviously, this implies also that
-$D_{ji}^c > D_{ji}^{l-2}$ and $c=\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$.
-
-We now consider that at iteration $l$, $l$ is $c + 1$. In other words, $M_{ij}$
-is modified depending on the domain $\dom(M^l_{ij})$ of $M^l_{ij}$:
+A l'itération $l$, si $l < c + 1$ alors l'instruction
+ \verb+skip+ est exécutée dans la fonction \verb+fetch_values+.
+ Ainsi, $M_{ij}^{l+1}(0)$ est égal à
+$M_{ij}^{l}(0)$. Puisque $c > l-1$, alors $D_{ji}^c > D_{ji}^{l-1}$ et donc, $c$
+est $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$.
+Cela implique que
+$D_{ji}^c > D_{ji}^{l-2}$ et $c=\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$.
+
+On considère maintenant qu'à l'itération $l$, celui-ci vaut $c + 1$.
+Dit autrement, $M_{ij}$ est modifié en fonction du domaine $\dom(M^l_{ij})$ de
+ $M^l_{ij}$:
\begin{itemize}
-\item if $\dom(M_{ij}^{l})=\{0\}$ and $\forall k\, . \, k\ge l \Rightarrow
- D^{k}_{ji} \neq l$ is established then $\dom(M_{ij}^{l+1})$ is empty and the
- first item of the lemma is established;
-\item if $\dom(M_{ij}^{l})=\{0\}$ and $\exists k\, . \, k\ge l \land D^{k}_{ji}
- = l$ is established then $M_{ij}^{l+1}(0)$ is $(\verb+Xp[i]+,l,c_{ij})$ that
- is added in the \verb+diffuse_values+ function s.t.\linebreak $c_{ij} =
- \min\{k \mid D^{k}_{ji} = l \} $. Let us prove that we can express
- $M_{ij}^{l+1}(0)$ as $\left(X_i^{D_{ji}^{c'}},D_{ji}^{c'},c' \right)$ where
- $c'$ is $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$. First, it is not hard to
- establish that $D_{ji}^{c_{ij}}= l \geq D_{ji}^{l} > D_{ji}^{l-1}$ and thus
- $c_{ij} \geq c'$. Next, since $\dom(M_{ij}^{l})=\{0\}$, then between
- iterations $D_{ji}^{c}+1$ and $l-1$, the \texttt{diffuse\_values} function has
- not updated $M_{ij}$. Formally we have
+\item si $\dom(M_{ij}^{l})=\{0\}$ et $\forall k\, . \, k\ge l \Rightarrow
+ D^{k}_{ji} \neq l$ sont vraies, alors $\dom(M_{ij}^{l+1})$ est vide et le premier
+ item du lemme est vérifié;
+\item si $\dom(M_{ij}^{l})=\{0\}$ et $\exists k\, . \, k\ge l \land D^{k}_{ji}
+ = l$ sont vraies, alors $M_{ij}^{l+1}(0)$ vaut $(\verb+Xp[i]+,l,c_{ij})$ qui est ajouté
+ dans la fonction \verb+diffuse_values+ de sorte que $c_{ij} =
+ \min\{k \mid D^{k}_{ji} = l \} $.
+ Prouvons qu'on peut exprimer
+ $M_{ij}^{l+1}(0)$ comme $\left(X_i^{D_{ji}^{c'}},D_{ji}^{c'},c' \right)$ où
+ $c'$ vaut $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$.
+ Tout d'abord, il n'est pas difficile de prouver que
+ $D_{ji}^{c_{ij}}= l \geq D_{ji}^{l} > D_{ji}^{l-1}$ et que
+ $c_{ij} \geq c'$.
+ Ensuite, comme $\dom(M_{ij}^{l})=\{0\}$, alors, entre les
+ itérations $D_{ji}^{c}+1$ et $l-1$, la fonction \texttt{diffuse\_values} n'a pas mis à jour
+ $M_{ij}$. On a ainsi la propriété
$$
\forall t,k \, .\, D_{ji}^c < t < l \land k \geq t \Rightarrow D_{ji}^k \neq
t.$$
-Particularly, $D_{ji}^{c'} \not \in \{D_{ji}^{c}+1,\ldots,l-1\}$. We can apply
-the third item of the induction hypothesis to deduce
-$\verb+Xp[i]+=X_i^{D_{ji}^{c'}}$ and we can conclude.
-
-\item if $\{0,1\} \subseteq \dom(M_{ij}^{l})$ then $M_{ij}^{l+1}(0)$ is
- $M_{ij}^{l}(1)$. Let $M_{ij}^{l}(1)= \left(\verb+Xp[i]+, a_{ij} , c_{ij}
- \right)$. By construction $a_{ij}$ is $\min\{t' | t' > D_{ji}^c \land
- (\exists k \, .\, k \geq t' \land D_{ji}^k = t')\}$ and $c_{ij}$ is $\min\{k |
- D_{ji}^k = a_{ij}\}$. Let us show $c_{ij}$ is equal to $\min\{k | D_{ji}^k >
- D_{ji}^{l-1} \}$ further referred as $c'$. First we have $D_{ji}^{c_{ij}} =
- a_{ij} > D_{ji}^c$. Since $c$ by definition is greater or equal to $l-1$ ,
- then $D_{ji}^{c_{ij}}> D_{ji}^{l-1}$ and then $c_{ij} \geq c'$. Next, since
- $c$ is $l-1$, $c'$ is $\min\{k | D_{ji}^k > D_{ji}^{c} \}$ and then $a_{ij}
- \leq D_{ji}^{c'}$. Thus, $c_{ij} \leq c'$ and we can conclude as in the
- previous part.
+En particulier, on a $D_{ji}^{c'} \not \in \{D_{ji}^{c}+1,\ldots,l-1\}$.
+On peut donc appliquer le troisième item de l'hypothèse d'induction pour déduire
+$\verb+Xp[i]+=X_i^{D_{ji}^{c'}}$ et on peut conclure.
+
+\item Si $\{0,1\} \subseteq \dom(M_{ij}^{l})$, alors $M_{ij}^{l+1}(0)$ vaut
+ $M_{ij}^{l}(1)$. Soit $M_{ij}^{l}(1)= \left(\verb+Xp[i]+, a_{ij} , c_{ij}
+ \right)$. Par construction, $a_{ij}$ vaut $\min\{t' | t' > D_{ji}^c \land
+ (\exists k \, .\, k \geq t' \land D_{ji}^k = t')\}$ et $c_{ij}$ est $\min\{k |
+ D_{ji}^k = a_{ij}\}$. Montrons que $c_{ij}$ est égal à $\min\{k | D_{ji}^k >
+ D_{ji}^{l-1} \}$, noté plus tard $c'$. On a tout d'abord $D_{ji}^{c_{ij}} =
+ a_{ij} > D_{ji}^c$. Puisque $c$ par définition est supérieur ou égal à $l-1$,
+ alors $D_{ji}^{c_{ij}}> D_{ji}^{l-1}$ et donc $c_{ij} \geq c'$. Ensuite, puisque
+ $c=l-1$, $c'$ vaut $\min\{k | D_{ji}^k > D_{ji}^{c} \}$ et donc $a_{ij}
+ \leq D_{ji}^{c'}$. Ainsi, $c_{ij} \leq c'$ et on peut conclure comme dans la partie précédente.
\end{itemize}
-The case where the domain $\dom(M^l_{ij})$ is empty but the formula $\exists k
-\, .\, k \geq l \land D_{ji}^k = l$ is established is equivalent to the second
-case given above and then is omitted.
+Le cas où le domaine $\dom(M^l_{ij})$ est vide mais où la formule $\exists k
+\, .\, k \geq l \land D_{ji}^k = l$ est vraie est équivalent au second
+cas ci-dessus et n'est pas présenté.
-Secondly, let us focus on the formula~(\ref{eq:correct_retrieve}). At iteration
-$l+1$, let $c'$ be defined as $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$. Two cases
-have to be considered depending on whether $D_{ji}^{l}$ and $D_{ji}^{l-1}$ are
-equal or not.
+Concentrons nous sur la formule~(\ref{eq:correct_retrieve}). A l'itération
+$l+1$, soit $c'$ défini par $c'=\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$. Deux cas peuvent
+apparaître selon que $D_{ji}^{l}$ et $D_{ji}^{l-1}$ sont égaux ou non.
\begin{itemize}
-\item If $D_{ji}^{l} = D_{ji}^{l-1}$, since $D_{ji}^{c'} > D_{ji}^{l-1}$, then
- $D_{ji}^{c'} > D_{ji}^{l}$ and then $c'$ is distinct from $l$. Thus, the SPIN
- execution detailed above does not modify $Xd_{ji}^{l+1}$. It is obvious to
- establish that $Xd_{ji}^{l+1} = Xd_{ji}^{l} = X_i^{D_{ji}^{l-1}} =
+\item Si $D_{ji}^{l} = D_{ji}^{l-1}$, puisque $D_{ji}^{c'} > D_{ji}^{l-1}$, alors
+ $D_{ji}^{c'} > D_{ji}^{l}$ et donc $c'$ est différent de $l$. L'exécution de SPIN
+ ne modifie pas $Xd_{ji}^{l+1}$. On a ainsi $Xd_{ji}^{l+1} = Xd_{ji}^{l} = X_i^{D_{ji}^{l-1}} =
X_i^{D_{ji}^{l}}$.
-\item Otherwise $D_{ji}^{l}$ is greater than $D_{ji}^{l-1}$ and $c$ is thus $l$.
- According to \Equ{eq:Mij0} we have proved, we have
- $M_{ij}^{l+1}(0)=(X_i^{D_{ji}^{l}},D_{ji}^{l},l)$. Then the SPIN execution
- detailed above assigns $X_i^{D_{ji}^{l}}$ to $Xd_{ji}^{l+1}$, which ends the
- proof of (\ref{eq:correct_retrieve}).
+\item Sinon, $D_{ji}^{l}$ et plus grand que $D_{ji}^{l-1}$ et $c$ est donc égal à $l$.
+ Selon l'équation \Equ{eq:Mij0}, on a
+ $M_{ij}^{l+1}(0)=(X_i^{D_{ji}^{l}},D_{ji}^{l},l)$. Ainsi l'exécution SPIN
+ affecte $X_i^{D_{ji}^{l}}$ à $Xd_{ji}^{l+1}$, ce qui termine la preuve
+(\ref{eq:correct_retrieve}).
\end{itemize}
-We are left to prove the induction of the third part of the lemma. Let $k$, $k
+Il reste à prouver la partie inductive de la troisième partie du lemme.
+Soit $k$, $k
\in S^{l+1}$. % and $\verb+k'+ = k-1$.
-At the end of the first execution of the \verb+update_elems+ process, we have
+A l'issue de la première exécutions
+du processus \verb+update_elems+, on a
$\verb+Xp[+k\verb+]+= F(\verb+Xd[+k\verb+][0]+,
-\ldots,\verb+Xd[+k\verb+][+n\verb+-1]+)+$. By definition of $Xd$, it is equal
-to $F(Xd^{l+1}_{k\,0}, \ldots,Xd^{l+1}_{k\,n-1})$. Thanks to
-\Equ{eq:correct_retrieve} we have proved, we can conclude the proof.
+\ldots,\verb+Xd[+k\verb+][+n\verb+-1]+)+$.
+Par définition $Xd=F(Xd^{l+1}_{k\,0}, \ldots,Xd^{l+1}_{k\,n-1})$.
+Grace à~\Equ{eq:correct_retrieve} déjà prouvée, on peut conclure la preuve.
\end{Proof}
% performed under weak fairness property; we then detail what are continuously
% enabled:
% \begin{itemize}
-% \item if the strategy is not defined as periodic, elements $0$, \ldots, $n$ are
+% \item if the strategy is not defined as periodic, elements $0$, \ldots, $\mathsf{N}$ are
% infinitely often updated leading to pseudo-periodic strategy;
% \item instructions that write or read into \verb+channels[j].sent[i]+ are
% continuously enabled leading to convenient available dates $D_{ji}$.
Lisboa, Portugal, July 2016.
\bibitem{kcm16:ip}
-Nesrine Khernane, J.-F. Couchot, A. Mostefaoui.
+N. Khernane, J.-F. Couchot, A. Mostefaoui.
\newblock Maximizing Network Lifetime in Wireless Video Sensor Networks Under Quality Constraints.
-\newblock In {\em The 19th ACM International Conference on Modeling, Analysis
-and Simulation of Wireless and Mobile Systems, MSWiM'16} Malta, to appear, November, 2016.
+\newblock In {\em MOBIWAC 2016: The 14th ACM* International Symposium on Mobility Management and Wireless Access} Malta, to appear, November, 2016.
\bibitem{BCDG07}
Fabrice Bouquet, Jean-Fran\c{c}ois Couchot, Fr\'ed\'eric Dadeau, and Alain
\mainmatter
-\part{Réseaux Discrets}
+\part{Réseaux discrets}
\chapter{Iterations discrètes de réseaux booléens}
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 sans, mais plus rapidement. Cette dernière section
-a fait l'objet du rapport~\cite{BCVC10:ir}.
+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}
\appendix
-\chapter{Preuves sur les SDD}
+\chapter{Preuves sur les réseaux discrets}
\section{Convergence du mode mixe}\label{anx:mix}
\input{annexePreuveMixage}
\end{equation}
\noindent active successivement les deux premiers éléments (24 est 11000)
et les quatre derniers éléments (15 est 01111).
-On dit que la stratégie est
-\emph{pseudo-periodique} si tous les éléments sont activés infiniment
-souvent.
% , it is sufficient to establish that the set $\{t \mid t \in \mathbb{N}
% \land \textit{bin}(s^t)[i] = 1\}$ is infinite for any $i$, $1 \le i \le n$,
% where
Dans le mode asynchrone, a chaque itération $t$, chaque composant peut
mettre à jour son état en
fonction des dernières valeurs qu'il connaît des autre composants.
-Obtenir ou non les valeurs les plus à jours dépend du temps de calcul et
+Obtenir ou non les valeurs les plus à jour dépend du temps de calcul et
du temps d'acheminement de celles-ci. On parle de latence, de délai.
Formalisons le mode les itérations asynchrone.
La \emph{relation de synchronisation} $\eqNode$ est
définie sur l'ensemble des n{\oe}uds par:
$i \eqNode j$ si $i$ et $j$ appartiennent à la même composante fortement
- connexe (CFC) dans $\Gamma(F)$.
+ connexe (CFC) dans $\Gamma(f)$.
\end{Def}
On peut facilement démontrer que la relation de synchronisation est une
classe.
Pour gommer cette distinction, on définit le mode suivant:
\begin{Def}[Itérations mixes avec delais uniformes]
- Le mode mixe a des \emph{délais uniformes}si pour chaque
+ Le mode mixe a des \emph{délais uniformes} si pour chaque
$t=0,1,\ldots$ et pour chaque paire de classes $(\class{p}, \class{q})$,
il existe une constante $d^t_{pq}$ telle que la propriété suivante est
établie:
mode synchrone.
\end{xpl}
-\subsection{Le mode généralisé asynchrone}
+\subsection{Le mode unaire asynchrone}
\label{sec:evalasync}
En terme de durée de convergence, ce mode peut être vu comme un
cas particulier du mode mixe où toutes les classes sont des singletons.
ne recouvrent nullement les communications.
\begin{xpl}
- La \Fig{fig:evalasync} présente un exemple d'exécution du mode généralisé
+ La \Fig{fig:evalasync} présente un exemple d'exécution du mode unaire
asynchrone.
Certaines communications issues de l'élément $4$ n'ont pas été représentées
pour des raisons de clarté.
Un outil qui construirait automatiquement toutes
les transitons serait le bienvenu.
Pour peu qu'on établisse la preuve de correction et de complétude de la
-démarche, la convergence du réseau discret ne repose alors que sur le verdict
+démarche, la convergence du réseau discret ne reposerait
+ alors que sur le verdict
donné par l'outil.
Cependant, même pour des réseaux discrets à peu d'éléments,
le nombre de configurations induites explose rapidement.
Les \emph{Model-Checkers}~\cite{Hol03,nusmv02,Blast07,MCErlang07,Bogor03}
-sont des classes d'outils qui adressent le problème de vérifier automatiquement
-qu'un modèle vérifie une propriété donnée. Pour traiter le problème d'explosion
+sont des classes d'outils qui adressent le problème de détecter automatiquement
+si un modèle vérifie une propriété donnée. Pour traiter le problème d'explosion
combinatoire, ces outils appliquent des méthodes d'ordre partiel, d'abstraction,
de quotientage selon une relation d'équivalence.
Ce chapitre montre comment nous simulons
-des réseaux discrets selon toutes les sortes d'itérations pour établir
+des réseaux discrets selon pour établir
formellement leur convergence (ou pas).
Nous débutons par un exemple et faisons quelques rappels sur
le langage PROMELA qui est le langage du model-checker
Nous présentons ensuite la démarche de traduction
de réseaux discrets dans PROMELA (\Sec{sec:spin:translation}).
Les théorèmes de correction et de complétude de la démarche
-sont ensuite donnés à la (\Sec{sec:spin:proof}).
-Des données pratiques comme la complexité et des synthèses d'expérimentation
+sont ensuite donnés à la \Sec{sec:spin:proof}.
+Des données pratiques comme la complexité et des synthèses d'expérimentations
sont ensuite fournies (\Sec{sec:spin:practical}).
Ce chapitre a fait l'objet du rapport~\cite{Cou10:ir}.
-On peut facilement vérifier que toutes les itérations synchrones initialisées
+On peut facilement vérifier que toutes les itérations parallèles
+synchrones initialisées
avec $x^0 \neq 7$ soit $(111)$
convergent vers $2$ soit $(010)$; celles initialisées avec
$x^0=7$ restent en 7.
-Pour les mode unaires ou généralisés avec une
+Pour les modes unaires ou généralisés avec une
stratégie pseudo périodique, on a des comportements qui dépendent
de la configuration initiale:
\begin{itemize}
Il définit:
\begin{itemize}
\item les constantes \verb+N+ et \verb+d_0+ qui précisent respectivement le nombre
- $n$ d'éléments et le délais maximum $\delta_0$;
+ ${\mathsf{N}}$ d'éléments et le délais maximum $\delta_0$;
\item les deux tableaux (\verb+X+ et \verb+Xp+) de \verb+N+ variables booléennes;
les cellules \verb+X[i]+ et \verb+Xp[i]+ sont associées à la variables $x_{i+1}$
d'un système dynamique discret;
L'instruction de réception consomme la valeur en tête du canal \verb+ch+
et l'affecte à la variable \verb+m+ (pour peu que \verb+ch+ soit initialisé et non vide).
De manière similaire, l'instruction d'envoi ajoute la valeur de \verb+m+ à la queue du canal
-\verb+ch+ (pour peu que celui-ci soit initialisé et non rempli).
-Dans les cas problématiques, canal non initialisé et vide pour une réception ou bien rempli pour un envoi,
+\verb+ch+ (pour peu que celui-ci soit initialisé et pas plein).
+Dans les cas problématiques, canal non initialisé et vide pour une réception ou plein pour un envoi,
le processus est bloqué jusqu'à ce que les conditions soient remplies.
La structures de contrôle \verb+if+ (resp. \verb+do+) définit un choix non déterministe
sera choisi aléatoirement puis exécuté.
Dans le process \verb+init+ détaillé à la {\sc Figure}~\ref{fig:spin:init},
-une boucle de taille $N$ initialise aléatoirement la variable globale de type tableau \verb+Xp+.
+une boucle de taille ${\mathsf{N}}$ initialise aléatoirement la variable globale de type tableau \verb+Xp+.
Ceci permet par la suite de vérifier si les itérations sont convergentes pour n'importe
-quelle configuration initiale $x^{(0)}$.
+quelle configuration initiale $x^{0}$.
Basiquement, le process est une boucle qui est débloquée lorsque la valeur du sémaphore
\verb+sync_mutex+ est 1. Dans ce cas, les éléments à modifier sont choisis
-aléatoirement (grâce à $n$ choix successifs) et sont mémorisés dans le tableau
+aléatoirement (grâce à ${\mathsf{N}}$ choix successifs) et sont mémorisés dans le tableau
\verb+mods+, dont la taille est \verb+ar_len+.
Dans la séquence d'exécution, le choix d'un élément mis à jour est directement
suivi par des mises à jour: ceci est réalisé grâce à la modification de la valeur du sémaphore
\subsection{Propriété de convergence universelle}
Il reste à formaliser dans le model checker SPIN le fait que les
itérations d'un système
-dynamique à $n$ éléments est universellement convergent.
+dynamique à ${\mathsf{N}}$ éléments est universellement convergent.
Rappelons tout d'abord que les variables \verb+X+ et \verb+Xp+
contiennent respectivement la valeur de $x$ avant et après la mise à jour.
puis présente ensuite les expérimentations issues de ce travail.
\begin{theorem}[Nombre d'états ]
- Soit $\phi$ un modèle de système dynamique discret à $n$ éléments, $m$
+ Soit $\phi$ un modèle de système dynamique discret à ${\mathsf{N}}$ éléments, $m$
arcs dans le graphe d'incidence
et $\psi$ sa traduction en PROMELA. Le nombre de configurations
de l'exécution en SPIN de $\psi$ est bornée par $2^{m(\delta_0+1)+n(n+2)}$.
Puisque le nombre d'arêtes du graphe d'incidence est $m$,
il y a $m$ canaux non constants, ce qui génère approximativement $2^{m(\delta_0+1)}$ états.
Le nombre de configurations est donc borné par $2^{m(\delta_0+1)+n(n+2)}$.
- On remarque que cette borne est traitable par SPIN pour des valeurs raisonnables de $n$,
+ On remarque que cette borne est traitable par SPIN pour des valeurs raisonnables de ${\mathsf{N}}$,
$m$ et $\delta_0$.
%\JFC{Donner un ordre de grandeur de cet ordre de grandeur}
L'exemple \textit{RE} est l'exemple de ce chapitre,
\cite{RC07} concerne un réseau composé de deux gènes
-à valeur dans $\{0,1,2\}$,
-AC2D est un automate cellulaire avec 9 elements prenant des
-valeurs booléennes en fonction de
-de 4 voisins et
+à valeur dans $\{0,1,2\}$ et
\cite{BM99} consiste en 10 process
qui modifient leurs valeurs booléennes dans un graphe d'adjacence proche
du graphe complet.
Comme la convergence n'est déjà pas établie pour les itérations synchrones
de~\cite{RC07}, il en est donc
de même pour les itérations asynchrones.
-La {\sc Figure}~\ref{fig:RC07CE} donne une trace de la sortie de SPIN de menant à la violation
+La {\sc Figure}~\ref{fig:RC07CE} donne une trace de la sortie de SPIN menant à la violation
de la convergence. Celle-ci correspond à une stratégie périodique qui répète
$\{1,2\};\{1,2\};\{1\};\{1,2\};\{1,2\}$ et débute avec $x=(0,0)$.
En raison de la dépendance forte entre les éléments
Pour tout $x$ et $y$ dans $\Bool^{\mathsf{N}}$, l'ensemble
$\Delta(x, y)$, contient les $i \in [{\mathsf{N}}]$
tels que $x_i \neq y_i$.
-Soit enfin $f : \Bool^n \rightarrow \Bool^{\mathsf{N}}$. Son $i^{\textrm{ème}}$ composant
+Soit enfin $f : \Bool^{\mathsf{N}} \rightarrow \Bool^{\mathsf{N}}$. Son $i^{\textrm{ème}}$ composant
est nommé $f_i$ qui est une fonction de $\Bool^{\mathsf{N}}$ dans $\Bool$.
Pour chaque
$x$ dans $\Bool^{\mathsf{N}}$, l'ensemble
\end{xpl}
\subsection{Réseau booléen}
-Soit $n$ un entier naturel représentant le nombre
-d'éléments étudiés (gènes, protéines,\ldots).
+Soit ${\mathsf{N}}$ un entier naturel représentant le nombre
+d'éléments étudiés.
Un réseau booléen est
défini à partir d'une fonction booléenne:
\[
défini par une suite
$S = \left(s^t\right)^{t \in \mathds{N}}$ qui est une séquence
d'indices dans $[{\mathsf{N}}]$. Cette suite est appelée \emph{stratégie unaire}.
- Il est basé sur la relation définie pour tout $i \in [{\mathsf{N}}]$ par
+ Ce mode est défini pour tout $i \in [{\mathsf{N}}]$ par
\begin{equation}
x^{t+1}_i=
\begin{theorem}\label{Prop:attracteur}
-Le point $x$ est un point fixe si et seulement si
+La configuration $x$ est un point fixe si et seulement si
$\{x\}$ est un attracteur du graphe d'itération (synchrone, unaire, généralisé).
En d'autres termes, les attracteurs non cycliques de celui-ci
sont les points fixes de $f$.
En outre, les interactions peuvent se représenter à l'aide d'un
graphe $\Gamma(f)$ orienté et signé défini ainsi:
-l'ensemble des sommet %s est
+l'ensemble des sommets est
$[{\mathsf{N}}]$ et il existe un arc de $j$ à $i$ de signe
$s\in\{-1,1\}$, noté $(j,s,i)$, si $f_{ij}(x)=s$ pour au moins
un $x\in\Bool^{\mathsf{N}}$.
$[{\mathsf{N}}]^{\Nats}$, on qualifie de:
\begin{itemize}
\item \emph{périodiques} celles
-qui sont constituées par une répétition indéfinie
+qui sont constituées par une répétition infinie
d'une même séquence $S$ complète relativement à $[{\mathsf{N}}]$.
En particulier toute séquence périodique est complète.
\item \emph{pseudo-périodiques} celles
-qui sont constituées par une succession indéfinie de séquences
+qui sont constituées par une succession infinie de séquences
(de longueur éventuellement variable non supposée bornée) complètes.
Autrement dit dans chaque stratégie pseudo-périodique, chaque indice de
-$1$ à ${\mathsf{N}}$ revient indéfiniment.
+$1$ à ${\mathsf{N}}$ revient infiniment.
\end{itemize}
-François Robert~\cite{Rob95}
-a énoncé en 1995 le théorème suivant de convergence
+On a le théorème suivant de convergence
dans le mode des itérations unaires.
-\begin{theorem}\label{Th:conv:GIU}
+\begin{theorem}[~\cite{Rob95}]\label{Th:conv:GIU}
Si le graphe $\Gamma(f)$ n'a pas de cycle et si la stratégie unaire est
pseudo-périodique, alors tout chemin de $\textsc{giu}(f)$ atteint
l'unique point fixe $\zeta$ en au plus ${\mathsf{N}}$ pseudo-périodes.
Le qualificatif \emph{pseudo-périodique} peut aisément
s'étendre aux stratégies généralisées comme suit.
Lorsqu'une stratégie généralisée est constituée d'une
-succession indéfinie de séquences de parties de $[{\mathsf{N}}]$
+succession infinie de séquences de parties de $[{\mathsf{N}}]$
dont l'union est $[{\mathsf{N}}]$, cette stratégie est {pseudo-périodique}.
-J. Bahi~\cite{Bah00} a démontré le théorème suivant:
+On a le théorème suivant.
-\begin{theorem}\label{Th:Bahi}
+\begin{theorem}[~\cite{Bah00}]\label{Th:Bahi}
Si le graphe $\Gamma(f)$ n'a pas de cycle et si la stratégie généralisée
est pseudo-périodique alors
tout chemin de $\textsc{gig}(f)$ (et donc de $\textsc{giu}(f)$)
les pixels dont les modifications induisent la distortion la plus faible
possible. Ceci revient à définir une fonction de signification $u$.
La complexité du schéma de stéganographie est peu ou prou celle du calcul
-de cette carte, et elle est élevée (cf partie~\ref{XXXXXXXX}) dans le cas
+de cette carte, et elle est élevée dans le cas
de ces algorithmes.
Nous avons proposé un algorithme~\cite{ccg15:ij}
de complexité beaucoup plus faible
Une adaptation d'une fonction de distorsion existante est étudiée
en Section~\ref{sec:distortion} et des expériences sont présentées
en Section~\ref{sec:experiments}.
+Ce chapitre a été publié dans~\cite{ccfg16:ip}.
%\end{figure}
-% \section{Conclusion}
-
-% The first contribution of this paper is to propose of a distortion
-% function which is based on second order derivatives. These
-% partial derivatives allow to accurately compute
-% the level curves and thus to look favorably on pixels
-% without clean level curves.
-% Two approaches to build these derivatives have been proposed.
-% The first one is based on revisiting kernels usually embedded
-% in edge detection algorithms.
-% The second one is based on the polynomial approximation
-% of the bitmap image.
-% These two methods have been completely implemented.
-% The first experiments have shown that the security level
-% is slightly inferior the one of the most stringent approaches. These first promising results encourage us to deeply investigate this research direction.
-
-% Future works aiming at improving the security of this proposal are planned as follows. The authors want first to focus on other approaches to provide second order derivatives with larger discrimination power.
-% Then, the objective will be to deeply investigate whether the H\"older norm is optimal when the objective is to avoid null second order derivatives, and to give priority to the largest second order values.
-
-
+\section{Conclusion}
+La principale contribution de ce chapitre est de proposer des
+fonctions de distorsion basées sur des approximations de dérivées
+secondes, l'idée sous-jacente étant qu'une zone où les lignes de niveau
+ne sont pas clairement définies est peu prédictible.
+Deux approches d'approximation ont été présentées.
+La première basée
+sur un produit de convolution, exploite des noyaux déjà intégrés dans des
+algorithmes de détection de bords.
+La seconde s'appuie sur une interpolation polynomiale de l'image.
+Ces deux méthodes onté été complètement implantées et leur sécurité
+face à des stéganalyseurs a été étudiée. Les résultats encouragent
+à poursuivre dans cette direction.
\ No newline at end of file
