Cours et TD du 05/10/2023
Équivalence
Plusieurs méthodes :
- On regarde ce qui est observable de l’extérieur des systèmes et on compare si c’est la même (c’est ce qu’on a fait au Cours 1)
- On peut vérifier si les deux systèmes comparés sont capables de faire les mêmes actions, dans les deux sens. Il suffit d’un chemin permettant l’équivalence pour avoir une équivalence. (simulation, exemple : A puis B, puis A, puis B…)
- On peut vérifier en faisant comme le point précédent, mais on peut faire une simulation depuis n’importe quel graphe, c’est-à-dire, on peut faire avancer n’importe quel système en premier tant que l’autre répond (bisimulation, exemple : A, puis B, puis B, puis A)
Relation de simulation
Soit un système donné : S = (Q, \Delta, \Sigma)
On a : R \subseteq Q\times Q la simulation SSI \forall a \in \sigma, \forall q_{1}' \in Q_{1}, q_{1} \xrightarrow[\qquad\Sigma]{a} q_{1}' \RA \exists q_{2}' \in Q, q_{2} \xrightarrow[\qquad\Sigma]{a} q_{2}' et (q_{1}', q_{2}')\in R
Aussi, q \subseteq q' SSI \exists R une simulation (q, q') \in R
q \backsimeq_{sim} q' SSI q \subseteq q' et q' \subseteq q
Relation de bisimulation
Soit un système donné : S = (Q, \Delta, \Sigma)
On a : R \subseteq Q\times Q la simulation SSI \forall a \in \Sigma, \forall q_{1}' \in Q_{1}, q_{1} \xrightarrow[\qquad\Sigma]{a} q_{1}' \RA \exists q_{2}' \in Q, q_{2} \xrightarrow[\qquad\Sigma]{a} q_{2}' et (q_{1}', q_{2}')\in R et \forall q_{2}' \in Q_{2}, q_{2} \xrightarrow[\qquad\Sigma]{a} q_{2}' \RA \exists q_{1}' \in Q, q_{1} \xrightarrow[\qquad\Sigma]{a} q_{1}' et (q_{2}', q_{1}')\in R
Aussi, q \subseteq q' SSI \exists R une bisimulation (q, q') \in R
q \backsimeq_{bisim} q' SSI q \subseteq q' et q' \subseteq q
Réseau de Petri
Exemple
Soit 2 étudiants, ils travaillent dans une salle et à un instant t ils prennent une clé pour entrer dans une salle dortoir et se reposer, il n’y a qu’une place dans le dortoir. Ensuite l’étudiant revient dans la salle de travail.
Définition
Soit un réseau de Petri R : R(P, T, \Delta) avec ensemble de place P, de transition T et relation reliant les places et les transitions \Delta, donc \Delta \subseteq P\times T \cup T\times P.
Un marquage
Fonction qui associe à chaque place sa valeur : soit le marquage M : P \ra \N
Soit \triangleright une relation de transition entre marquages
\forall M_{1}, M_{2} des marquages de R
M_{1}\triangleright M_{2} SSI \exists t\in T : M_{1} \triangleright_{t} M_{2}
Notation
Soit t \in T (une transition)
^{\bullet}t = \{p\in P | (p, t) \in \Delta \}
t^{\bullet} = \{p\in P| (t, p) \in \Delta \}
Donc
M_{1} \triangleright_{t} M_{2} SSI
- \forall p \in \ ^{\bullet}t, M_{1}(p) > 0
- \forall p \in P \begin{cases} M_{1}'(p) = M_{1} (p) - 1 \text{ si } p \in \ ^{\bullet}t \\\\ M_{1}'^{(p)}= M_{1}(p) \text{ sinon} \end{cases}
alors :
\forall p \in P \begin{cases} M_{2}'(p) = M_{2} (p) + 1 \text{ si } p \in t^{\bullet} \\\\ M_{2}'^{(p)}= M_{2}(p) \text{ sinon} \end{cases}
Accessibilité
\triangleright = \underset{t \in T}{U} \triangleright_{t} \triangleright^{\*} = \underset{i\geqslant 0}{U}\triangleright^{i} \begin{cases}\triangleright^{0} = Id \\\\ \triangleright^{i+1} = \triangleright^{i}\circ\triangleright\end{cases}
Relation d’accessibilité par un chemin dans le graphe des marquages : \text{Acc}(M) = \{M' | M \triangleright^{*}M'\}
Boucle infinie : P_{1}, P_{2} \ra (1, 0) \ra (1, 1) \ra (1, 2) \ra \dots
- K \in \N
- Un réseau est K-borné pour un marquage initial M_{init} SSI \forall M \in \text{Acc}(M_{init}), \forall p \in P : M(p) \leqslant K
Lecture et écriture
Modélisation d’un lecteur et un écrivain :
Modélisation de deux lecteurs et un écrivain :
Modélisation d’un producteur/consommateur avec buffer :
