From d8d9d52ff5feb79ffff00a8e487581e3958ce326 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= Date: Sun, 4 Dec 2011 21:45:25 +0100 Subject: [PATCH] Initial commit. --- .gitignore | 3 + cours.tex | 218 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 221 insertions(+) create mode 100644 .gitignore create mode 100644 cours.tex diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..3eec47d --- /dev/null +++ b/.gitignore @@ -0,0 +1,3 @@ +*.aux +*.log +*.pdf diff --git a/cours.tex b/cours.tex new file mode 100644 index 0000000..fe1ae96 --- /dev/null +++ b/cours.tex @@ -0,0 +1,218 @@ +\documentclass[a4paper,french,9pt]{article} +\usepackage[reset]{geometry} +\geometry{a4paper, top=2cm, bottom=2.0cm, left=4.4cm, right=4.47cm} +\usepackage[frenchb]{babel} +\usepackage[utf8]{inputenc} +\usepackage[T1]{fontenc} +\usepackage{amsmath} +\usepackage{amssymb} +\usepackage{multirow} +\usepackage{tikz} +\usetikzlibrary{positioning,calc,chains,intersections} +\def\P{\mathcal{P}} +\def\GUi{G \cup \{i\}} +\def\transition#1{\stackrel{#1}{\longrightarrow}} +\def\Transition#1{\stackrel{#1}{\Longrightarrow}} +\def\forte{\sim} +\def\observationnelle{\approx} +\def\conf{\ \text{conf}\ } +\DeclareMathOperator{\Tr}{Tr} +\def\si{\quad\text{si}\quad} +\let\simule\gtrsim +\let\estsimulepar\gtrsim +\begin{document} + +\section{Définitions} + +\begin{description} +\item[LTS] (Labeled Transition System = Système de transitions étiquetées) : $$P = \langle\P,A,\rightarrow,P\rangle$$ + \begin{description} + \item[$\P$]: États. $\P = \{P, Q, R, \dots\}$. + \item[$A$]: Actions (étiquettes que l'on mettra sur les transitions). $A \subseteq \GUi$. $G$ est l'ensemble des actions observables. $i$ + est l'action interne que le système peut faire de lui-même. + \item[$\rightarrow$]: Transitions. $\rightarrow \in \P\times A\times\P$. $P\transition{a}Q$~: le système se tranforme, passe de $P$ à $Q$ + en exécutant $a$. + \item[$P$]: Nom du LTS, et aussi son premier état (donc $P \in \P$). + \end{description} +\item[Trace]: Ensemble des listes d'actions que l'on peut exécuter. La trace vide est notée $\varepsilon$. + \begin{center} + \begin{tikzpicture}[node distance=5mm] + \node (p) {P}; + \node[above right= of p] (q) {Q}; + \node[below right= of p] (r) {R}; + \node[right= of q] (stop1) {Stop}; + \node[right= of r] (stop2) {Stop}; + \draw[->] (p) -- node[above,near start] {a} (q); + \draw[->] (p) -- node[below,near start] {a} (r); + \draw[->] (q) -- node[above] {b} (stop1); + \draw[->] (r) -- node[above] {c} (stop2); + \end{tikzpicture} + \end{center} + $$\Tr(P) = \{\varepsilon, a, ab, ac\}$$ +\item[Chemin]: Si $P\transition{a_1}P_1\transition{a_2}\cdots\transition{a_n}P_n$ où $a_i \in \GUi$, on note $P\transition{t}P_n$ avec $t = + a_1; a_2; \dots; a_n$. $(a_3,a_4)$ est un sous-chemin de $P$. +\item[Exécution] Une exécution partielle de $P$ est un chemin de $P$ partant de l'état initial $P$. Une exécution complète de $P$ est une q + exécution partielle de $P$ que l'on ne peut pas compléter (j'ai pas compris là…). +\item[Chemin observable] On note $P_1\Transition{a}P_2$ avec $a \neq i$ si $P_1\transition{i^*}Q\transition{a}R\transition{i^*}P_2$. $i^*$ q + signifie 0 ou plusieurs exécutions de l'action interne. + + Si $P\Transition{a_1}P_1\Transition{a_2}\cdots\Transition{a_n}P_n$ où $a_i \neq i$, on note $P\Transition{t}P_n$ avec $t = a_1; a_2; + \dots; a_n$. + + $\hat{t}$ est le chemin obtenu en enlevant toutes les actions internes de $t$. Si $P\transition{t}Q$ alors $P\Transition{\hat{t}}Q$. +\item[Trace observable] Une trace observable de $P$ est une exécution partielle observable. +\end{description} + +\section{LOTOS} + +\def\fakerowspace{&&&&\\} +\hspace{-2.75cm} +\begin{tabular}{|lllcl|} + \hline + % + \fakerowspace + \multirow{1}{2cm}{Action prefix} & \multirow{1}{*}{$;:A\times P \rightarrow P$} + & $\text{ACT}$ & $\frac{\vphantom{P\transition{a}P'}}{a;P\transition{a}P}$ & $a \in \GUi$ \\ + \fakerowspace + \hline + % + \fakerowspace + \multirow{3}{2cm}{Choice} & \multirow{3}{*}{$[]:P\times P \rightarrow P$} + & $\text{CHOICE}_1$ & $\frac{P\transition{a}P'}{P[]Q\transition{a}P'}$ & $a \in \GUi$ \\ + \fakerowspace + & & $\text{CHOICE}_2$ & $\frac{Q\transition{a}Q'}{P[]Q\transition{a}Q'}$ & $a \in \GUi$ \\ + \fakerowspace + \hline + % + \fakerowspace + \multirow{3}{2cm}{Composition parallèle indépendante} & \multirow{3}{*}{$|||:P\times P \rightarrow P$} + & $\text{COM}_1$ & $\frac{P\transition{a}P'}{P|||Q\transition{a}P'|||Q}$ & $a \in \GUi$ \\ + \fakerowspace + & & $\text{COM}_2$ & $\frac{Q\transition{a}Q'}{P|||Q\transition{a}P|||Q'}$ & $a \in \GUi$ \\ + \fakerowspace + \hline + % + \fakerowspace + \multirow{5}{2cm}[-2mm]{Synchro totale} & \multirow{5}{*}[-2mm]{$||:P\times P \rightarrow P$} + & $\text{COMP}_1$ & $\frac{P\transition{a}P'\;\wedge\; Q\transition{a}Q'}{P||Q\transition{a}P'||Q'}$ & $a \in \GUi$ \\ + \fakerowspace + & & $\text{COMP}_{i1}$ & $\frac{P\transition{i}P'}{P||Q\transition{i}P'||Q}$ & \\ + \fakerowspace + & & $\text{COMP}_{i2}$ & $\frac{Q\transition{i}Q'}{P||Q\transition{i}P||Q'}$ & \\ + \fakerowspace + \hline + % + \fakerowspace + \multirow{5}{2cm}[-2mm]{Synchro sur un ensemble $S \subseteq$ de portes visibles} & \multirow{5}{*}[-2mm]{$|[S]|:P\times\mathcal{P}(G)\times P \rightarrow P$} + & $\text{SYNC}_1$ & $\frac{P\transition{a}P'}{P|[S]|Q\transition{a}P'|[S]|Q}$ & $a \in G, a \not\in S, a \neq i$ \\ + \fakerowspace + & & $\text{SYNC}_2$ & $\frac{P\transition{a}P'}{P|[S]|Q\transition{a}P'|[S]|Q}$ & $a \in G, a \not\in S, a \neq i$ \\ + \fakerowspace + & & $\text{SYNC}_3$ & $\frac{P\transition{a}P'\;\wedge\; Q\transition{a}Q'}{P|[S]|Q\transition{a}P'|[S]|Q'}$ & $a \in S, a \neq i$ \\ + \fakerowspace + \hline + % + \fakerowspace + \multirow{3}{2cm}{Rendre une action invisible} & \multirow{3}{*}{$\text{\small hide}\dots\text{\small{}in}:\mathcal{P}(G)\times P \rightarrow P$} + & $\text{HIDE}_1$ & $\frac{P\transition{a}P'}{(\text{\small hide }a\text{\small{} in }P)\transition{i}(\text{\small hide }a\text{\small{} in }P')}$ & $a \in G, a \neq i$ \\ + \fakerowspace + & & $\text{HIDE}_2$ & $\frac{P\transition{i}P'}{(\text{\small hide }a\text{\small{} in }P)\transition{i}(\text{\small hide }a\text{\small{} in }P')}$ & $a \in G, a \neq i$ \\ + \fakerowspace + \hline + % + \fakerowspace + \multirow{1}{2cm}{Renommage} & \multirow{1}{*}{$P[\dots]:P\times G \times G \rightarrow P$} + & $\text{REN}$ & $\frac{P[a]\transition{a}P'[a]}{P[p]\transition{b}P'[b]}$ & $\begin{array}{ll}a \in G,& a \neq i\\b \in G,& b \neq i\end{array}$ \\ + \fakerowspace + \hline + % +\end{tabular} + +\clearpage +\section{Comparaison de LTS} + +\subsection{Équivalence forte $\forte$} + +Def. $P \forte Q\si \forall a \in \GUi,\quad \left(P \transition{a} P'\right) \Rightarrow \left(\exists\, Q \transition{a} Q' \;\wedge\; P' \forte Q'\right)$, et vice versa de $Q$ vers $P$~: $\left(Q \transition{a} Q'\right) \Rightarrow \left(\exists\, P \transition{a} P' \;\wedge\; P' \forte Q'\right)$ + +En français ça donne~: quand $P$ fait une action, $Q$ sait la faire aussi, et vice versa, donc $Q$ est capable de simuler $P$, et $P$ est +capable de simuler $Q$. On appelle ça la bisimulation. + +Si $P$ évolue en interne, $Q$ \emph{doit} évoluer en interne. + +L'équivalence forte permet de tester si deux processus ont le même degré d'indéterminisme externe. + +\subsection{Équivalence observationnelle $\observationnelle$} + +Def. $P \observationnelle Q\si \forall a \in \GUi,\quad \left(P\transition{a}P'\right) \Rightarrow \left(\exists\, + Q\Transition{\hat{a}}Q' \;\wedge\; P' \observationnelle Q'\right)$ et vice vesa de $Q$ vers $P$~: $\left(Q\transition{a}Q'\right) +\Rightarrow \left(\exists\, P\Transition{\hat{a}}P' \;\wedge\; P' \observationnelle Q'\right)$. + +Si $P$ évolue en interne, $Q$ \emph{peut ne pas} évoluer en interne. + +Si $P$ fait une action, $Q$ peut faire beaucoup de $\transition{i}$, mais doit faire l'action. + +L'équivalence observationnelle ne détecte pas tous les livelock. $P$ et $Q$ sont observationnellement équivalents alors que Q peut refuser +$b$ indéfiniment et toujours faire i. + +$$P\transition{a}\transition{b} \quad\observationnelle\quad Q\transition{a}\tikz[remember picture]{\node[coordinate] (ab) {};}\transition{b}$$ +\begin{tikzpicture}[remember picture, overlay] + \node[coordinate,yshift=1mm] (abs) at (ab) {}; + \draw (abs) edge[->,out=45,in=135,looseness=1,loop,distance=0.8cm,shorten <=1mm, shorten >=1mm] node[fill=white,inner sep=1.5pt] {\scriptsize $i$} (abs); +\end{tikzpicture} + +\subsection{Congruence opérationnelle $=$} + +Def. $P=Q \si \forall a \in \GUi,\quad \left(P\transition{a}P'\right) \Rightarrow \left(\exists\, Q\Transition{a}Q' + \;\wedge\; P' \observationnelle Q'\right)$ et vice versa de $Q$ vers $P$~: $\left(Q\transition{a}Q'\right) \Rightarrow \left(\exists\, + P\Transition{a}P' \;\wedge\; P' \observationnelle Q'\right)$. + +La différence avec l'équivalence opérationnelle est le $Q\Transition{a}Q'$ au lieu de $Q\Transition{\hat{a}}Q'$. Il est à noter qu'une fois +qu'on a vérifié que la première transition n'était pas l'action invisible, on utilise l'équivalence observationnelle. + +Cela a pour but d'avoir $\transition{a}\transition{b}\neq\transition{i}\transition{a}\transition{b}$, mais +$\transition{a}\transition{b}=\transition{a}\transition{i}\transition{b}$. + +Cependant, comme pour l'équivalence observationnelle, on ne détecte pas tous les livelock (même exemple que ci-dessus). + + +\subsection{Simulation} + +Def. $P \simule Q \si \forall a \in \GUi,\quad \left(Q\transition{a}Q'\right) \Rightarrow \left(\exists\, P\Transition{a}P' \;\wedge\; P' + \simule Q'\right)$. On dit \og $P$ simule $Q$\fg. + +Attention, la bisimulation $P \forte Q$ n'est pas $\left(P \simule Q \;\wedge\; P \estsimulepar Q\right)$, car dans simul, à la fin on a $P' +\simule Q'$, alors que dans la bisimulation on a $P' \forte Q'$. La bisimulation $P \forte Q$ est donc une condition plus forte que la +simulation mutuelle de P et Q $\left(P \simule Q \;\wedge\; P \estsimulepar Q\right)$. + +\subsection{Force des comparaisons} + +$$ P \forte Q \Rightarrow P = Q \Rightarrow P \observationnelle Q $$ + +\clearpage +\subsection{Conformité $\conf$} + +Les comparaisons des sections précédentes ne détectent pas tous les livelock, et nécessitent une description complète de la spécification, +car ces relations sont symmétriques. On cherche donc une relation assymétrique de conformité, $P\conf S$ qui nous permettra de dire que $P$ +est une implantation correcte de $S$. + +On écrit $S\text{ must }A\text{ after }t$ pour dire que $S$ doit accepter les actions de l'ensemble $A$ après le chemin $t$. + +Def. $Q\text{ must }A\text{ after }t \si \forall Q \Transition{t} Q',\quad \forall a \in A, \quad Q'\transition{a}Q"$. + +On écrit $P\text{ may refuse }A\text{ after }t$ pour dire que $P$ peut refuser une des actions de $A$ (ou toutes les actions de $A$, selon +les définitions) après le chemin $t$. + +\def\myfnote{\footnote{Je ne sais pas trop si c'est $\forall A \subseteq G$ ou $\forall A \subseteq \GUi$.}} + +$$ +P \conf S\si\forall A \subseteq G\myfnote,\quad S\text{ must }A\text{ after }t \Rightarrow P\text{ must }A\text{ after }t +$$ + +En prennant la contraposée, on obtient un test de conformité (équivalent à la définition ci-dessus)~: + +$$ +\forall t \in \Tr(S),\quad P\text{ may refuse }A\text{ after }t \Rightarrow S\text{ may refuse }A\text{ after }t +$$ + +\end{document}