suzanne.soy/2011-m2s3-systemes-reactifs
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

autocommit

Browse Source
This commit is contained in:
Georges Dupéron 2011-12-16 15:15:39 +01:00
parent d1be176e56
commit a6ad34b913
3 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

0
.gitignore vendored Normal file → Executable file
View File

0
cours-2011-11-04.tex Normal file → Executable file
View File

4
cours.tex Normal file → Executable file
View File

@ -107,7 +107,7 @@
\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$}
\multirow{5}{2cm}[-2mm]{Synchro sur un ensemble $S \subseteq G$ 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$ \\
@ -182,7 +182,7 @@ Cependant, comme pour l'équivalence observationnelle, on ne détecte pas tous l
\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'
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'