Bisimulazione forte

La prima proprietà che vogliamo mostrare è come la strong bisimulation sia preservata da alcune operazioni sulle relazioni (teniamo a mente quanto visto in precedenza su relazioni inverse e composte):

Proposizione 6..1   Si assuma che ogni $\mathcal{S}_i \: (i = 1,2,\dots)$ sia una bisimulazione forte, allora anche le seguenti relazioni sono bisimulazioni forti:

1. ${Id}_{\mathcal{P}}$

2. $\mathcal{S}_i^{-1}$

3. $\mathcal{S}_1\mathcal{S}_2$

4. $\cup_{i \in I}\mathcal{S}_i$

Dimostrazione. Proveremo solo la 3, le altre sono altrettanto facili. Supponiamo dunque che

$$(p,r) \: \in \: \mathcal{S}_1\mathcal{S}_2$$

Per qualche $q$, avremo che

$$(p,q) \: \in \: \mathcal{S}_1 \quad \wedge \quad (q,r) \: \in \: \mathcal{S}_2$$

Sia adesso $p \stackrel{\alpha}{\longrightarrow} p'$. Allora per qualche $q'$ avremo, dal momento che $(p,q) \: \in \: \mathcal{S}_1$

$$q \stackrel{\alpha}{\longrightarrow} q' \quad \wedge \quad (p',q') \: \in \: \mathcal{S}_1$$

Inoltre, poichè $(q,r) \: \in \: \mathcal{S}_2$ si ha, per qualche $r'$

$$r \stackrel{\alpha}{\longrightarrow} r' \quad \wedge \quad (q',r') \: \in \: \mathcal{S}_1$$

Da questo si ottiene $(p',r') \: \in \: \mathcal{S}_1\mathcal{S}_2$. In modo del tutto simile si trova che se $r \stackrel{\alpha}{\longrightarrow} r'$, allora possiamo trovare un $p'$ tale che $p \stackrel{\alpha}{\longrightarrow} p'$ e $(p',r') \: \in \: \mathcal{S}_1\mathcal{S}_2$. $\qedsymbol$

Dimostriamo due proprietà accennate in precedenza ma che non abbiamo provato:

Proposizione 6..2   $\:$

1. $\sim$ è la più larga bisimulazione forte;

2. $\sim$ è una relazione di equivalenza.

Dimostrazione. Dimostriamo i due asserti separatamente:

1. Dal punto 4. della proposizione 6.1 si vede come l'unione di bisimulazioni forti sia ancora una bisimulazione forte: dunque, anche $\sim$ lo è e comprende tutte le altre bisimulazioni.

2. Per provare che sia una relazione di equivalenza, cioè che sia riflessiva simmetrica e transitiva, mostriamo che valgono queste proprietà:
   

   Riflessività: $\forall p \quad p \: \sim \: p$ dal punto 1. della proposizione 6.1;
   

   Simmetria: se $p\:\sim\: q$ allora $(p,q) \in \mathcal{S}$ per qualche bisimulazione forte $\mathcal{S}$. Allora $(q,p) \in \mathcal{S}^{-1}$ e quindi $q \: \sim \: p$ per il punto 2. della proposizione 6.1;
   

   Transitività: se $p\:\sim\: q$ e se $q \: \sim \: r$ allora $(p,q) \in \mathcal{S}_1$ e $(q,r) \in \mathcal{S}_2$ per qualche bisimulazione forte $\mathcal{S}_1$ ed $\mathcal{S}_2$. Dunque $(p,r) \: \in \: \mathcal{S}_1\mathcal{S}_2$ e quindi $p \: \sim \: r$ per il punto 3. della proposizione 6.1.

$\qedsymbol$

Vogliamo dunque provare che $\sim$ soddisfa le proprietà che abbiamo chiamato ($*_{\sim}$). Sappiamo che metà dell'implicazione vale, in quanto 'sse' è stato rimpiazzato da 'implica', dal momento che $\sim$ è una bisimulazione forte; rimane dunque da provare l'altra metà. Per fare questo, definiamo dapprima una nuova relazione, $\sim'$ in termini di $\sim$ nel modo seguente:

Definizione 6..1   $p \: \sim ' \: q$ sse, $\forall \alpha \: \in \: Act_{\tau}$,

1. $\forall p': \: p \stackrel{\alpha}{\longrightarrow} p' \quad \exists q' : \: q \stackrel{\alpha}{\longrightarrow} q' \quad \wedge \quad p' \: \sim \: q'$

2. $\forall q': \: q \stackrel{\alpha}{\longrightarrow} q' \quad \exists p' : \: p \stackrel{\alpha}{\longrightarrow} p' \quad \wedge \quad p' \: \sim \: q'$.

Dalla proposizione 6.2, punto 1., sappiamo che $\sim$ è una bisimulazione forte, possiamo allora dedurre che

$$p \: \sim \: q$$   implica$$\quad p \: \sim ' \: q \qquad \qquad(\char93 )$$

Rimane da provare il viceversa, cioè che $p \: \sim ' \: q$ implica $p\:\sim\: q$. Il seguente risultato è sufficiente:

Lemma 6..1   La relazione $\sim'$ è una bisimulazione forte.

Dimostrazione. Sia $p \: \sim ' \: q$ e $p \stackrel{\alpha}{\longrightarrow} p'$. E' sufficiente trovare un $q'$ tale che $q \stackrel{\alpha}{\longrightarrow} q'$ e $p' \: \sim ' \: q'$. Ma per la definizione di $\sim'$ possiamo infatti trovare questo $q'$ tale che $q \stackrel{\alpha}{\longrightarrow} q'$ e $p' \: \sim \: q'$. Grazie a (#) sappiamo allora che $p' \: \sim ' \: q'$, e con questo si conclude la prova. $\qedsymbol$

Si è quindi dimostrato che $\sim$ soddisfa ($*_{\sim}$):

Proposizione 6..3   $p\:\sim\: q$ sse, $\forall \alpha \: \in \: Act_{\tau}$

• $p \stackrel{\alpha}{\longrightarrow} p'$   allora$\quad \exists q' : \: q \stackrel{\alpha}{\longrightarrow} q' \quad \wedge \quad p'\: \sim \: q'$

• $q \stackrel{\alpha}{\longrightarrow} q'$   allora$\quad \exists p' : \: p \stackrel{\alpha}{\longrightarrow} p' \quad \wedge \quad p'\: \sim \: q'$

Quello che vogliamo fare è provare che molte delle leggi di inferenza introdotte per CCS possono essere provare vere se si interpreta '=' come la bisimulazione forte; quanto proveremo adesso risulta valido anche per la nozione di bisimulazione debole (più generosa). In ogni caso, le $\tau$ laws non sono valide per la bisimulazione forte ma soltanto per la nozione debole.

Proposizione 6..4   Le monoid laws:

1. $p+q \: \sim \: q+p$

2. $p+(q+r) \: \sim \: (p+q)+r$

3. $p+p \: \sim \: p$

4. $p+nil \: \sim \: p$

Dimostrazione. Dimostreremo solo il punto 2.; gli altri seguono procedimenti simili. Supponiamo che

$$p+(q+r) \stackrel{\alpha}{\longrightarrow} p'$$

Allora dalla semantica della regola Somma sia ha che $p \stackrel{\alpha}{\longrightarrow} p'$ oppure $q \stackrel{\alpha}{\longrightarrow} p'$ oppure $r \stackrel{\alpha}{\longrightarrow} p'$. In ognuno dei casi possiamo facilmente inferire da Somma che $(p+q)+r \stackrel{\alpha}{\longrightarrow} p'$. Questo dimostra la proprietà (i) di ($*_{\sim}$), il punto (ii) si dimostra in modo simile. $\qedsymbol$

Proposizione 6..5   Le static laws:

1. $p\vert q \: \sim \: q\vert p$

2. $p\vert(q\vert r) \: \sim \: (p\vert q)\vert r$

3. $p\vert nil \: \sim \: p$

4. $p\setminus L \: \sim \: p$   se$\: \mathcal{L}(p) \cap(L\cup\overline{L})= \emptyset$

5. $p\setminus K\setminus L \: \sim \: p\setminus(K\cup L)$

6. $p [ f ] \setminus L \: \sim \: p\setminus f^{-1}(L)[f]$

7. $(p\vert q)\setminus L \: \sim \: p\setminus L \vert q\setminus L$   if$\: \mathcal{L}(p) \cap \overline{\mathcal{L}(q)}\cap(L\cup \overline{L})= \emptyset$

8. $p[Id] \: \sim \: p$

9. $p[f] \: \sim \: p[f']$

10. $p[f][f'] \: \sim \: p[f\circ f']$

11. $(p\vert q)[f] \: \sim \: p[f]\vert q[f]$

Dimostrazione. Tutte queste leggi possono essere dimostrate esibendo un'appropriata bisimulazione forte. La più difficile è la 2. e per questo la analizziamo subito.

Per questo punto, abbiamo bisogno di mostrare che $\mathcal{S}$ è una bisimulazione forte, dove

$$\mathcal{S} = \{( \: p_1\vert(p_2\vert p_3), (p_1\vert p_2)\vert p_3 \: ) \: : p_1,p_2,p_3 \: \in \: \mathcal{P} \}$$

Supponiamo ora che $p_1\vert(p_2\vert p_3) \stackrel{\alpha}{\longrightarrow} q$. Ci sono tre casi, con relativi sottocasi, che possono verificarsi:

Caso 1

$p_1 \stackrel{\alpha}{\longrightarrow} p_1'$, e $q \equiv p_1'\vert(p_2\vert p_3)$ .
E' facile allora mostrare che $(p_1\vert p_2)\vert p_3 \stackrel{\alpha}{\longrightarrow} r \equiv (p_1'\vert p_2)\vert p_3$, e chiaramente $(q,r) \: \in \: \mathcal{S}$.

Caso 2

$p_2\vert p_3 \stackrel{\alpha}{\longrightarrow} p_{23}'$ e $q \equiv p_1\vert p_{23}'$

Caso 2.1

$p_2 \stackrel{\alpha}{\longrightarrow} p_2'$ e $p_{23}' \equiv p_2'\vert p_3$
Allora $q \equiv p_1\vert(p_2'\vert p_3)$, ed è facile vedere che $(p_1\vert p_2)\vert p_3 \stackrel{\alpha}{\longrightarrow} r \equiv (p_1\vert p_2')\vert p_3$, e chiaramente $(q,r) \: \in \: \mathcal{S}$.

Caso 2.2

$p_3 \stackrel{\alpha}{\longrightarrow} p_3'$ e $p_{23}' \equiv p_2\vert p_3'$
In modo simile al Caso 2.1.

Caso 2.3

$\alpha = \tau, p_2 \stackrel{l}{\longrightarrow} p_2' \: \wedge \: p_3 \stackrel{\overline{l}}{\longrightarrow} p_3'$ e $p_{23}' \equiv p_2'\vert p_3'$
Allora $q \equiv p_1\vert(p_2'\vert p_3')$, ed è facile vedere che $(p_1\vert p_2)\vert p_3 \stackrel{\tau}{\longrightarrow} r \equiv (p_1\vert p_2')\vert p_3'$, e chiaramente $(q,r) \: \in \: \mathcal{S}$

Caso 3

$\alpha = \tau, p_1 \stackrel{l}{\longrightarrow} p_1' \: \wedge \: p_2\vert p_3 \stackrel{\overline{l}}{\longrightarrow} p_{23}'$ e $q \equiv p_1'\vert p_{23}'$

Caso 3.1

$p_2 \stackrel{\overline{l}}{\longrightarrow} p_2'$ e $p_{23}' \equiv p_2'\vert p_3$
Allora $q \equiv p_1'\vert(p_2'\vert p_3)$, ed è facile vedere che $(p_1\vert p_2)\vert p_3 \stackrel{\tau}{\longrightarrow} r \equiv (p_1'\vert p_2')\vert p_3$, e chiaramente $(q,r) \: \in \: \mathcal{S}$

Caso 3.2

$p_3 \stackrel{\overline{l}}{\longrightarrow} p_3'$ e $p_{23}' \equiv p_2\vert p_3'$
In modo simile al Caso 3.1

Questo prova la condizione 1. della definizione 5.9; la condizione 2. segue da un'argomentazione simmetrica, ed abbiamo così mostrato che $\mathcal{S}$ è una strong bisimulation.

Le altre parti della proposizione sono trattate in maniera simile. Per 4. si deve provare che, per un fissato $L$, la relazione

$$\mathcal{S} = \{ (P\setminus L, P) \: : \: p \: \in \: \mathcal{P}, \mathcal{L}(p) \cap (L \cup \overline{L}) = \emptyset \}$$

è una bisimulazione forte. Ora, se $(P\setminus L, P) \: \in \: \mathcal{S}$, allora (per la condizione sopra) $p \stackrel{\alpha}{\longrightarrow} p'$ implica che $\alpha, \overline{\alpha} \: \not\in \: L$; rimane da mostrare che $(p' \setminus L, p') \: \in \: \mathcal{S}$. Ma $\mathcal{L}(p') \subseteq \mathcal{L}(p)$ per ogni $p'$ derivazione di $p$, così $\mathcal{L}(p') \cap (L \cup \overline{L}) = \emptyset$, e di conseguenza $(p' \setminus L, p') \: \in \: \mathcal{S}$ come richiesto.

Le restanti parti non introducono altre problematiche.

$\qedsymbol$

Proposizione 6..6 (Expansion law)   Sia $p \equiv (p_1[f_1]\vert\dots \vert p_n[f_n])\setminus L$, con $n \geq 1$. Allora

$$\begin{array}{rcl} p & \sim & \sum \left\{f_i(\alpha).(p_1... ...i(l_1)= \overline{ f_j(l_2)}, \: i < j \right\} \end{array}$$

Dimostrazione. Consideriamo dapprima il caso semplice nel quale non sono presenti Restrizioni e Relabelling. In fatti, possiamo provare quanto segue per induzione su n:

Se $p \equiv p_1 \vert \dots \vert p_n, \: n \geq 1$, allora $\qquad \qquad \qquad \qquad \qquad \qquad \qquad \quad$ ($*_{+}$)

$$\begin{array}{rcl} p & \sim & \sum \left\{\alpha.(p_1\vert... ...krel{\overline{l}}{\longrightarrow}p_j' \right\} \end{array}$$

Per $n = 1$ ci si riduce a provare che $p_1 \sim \sum \{\alpha.p_1' \: : \: p_1 \stackrel{\alpha}{\longrightarrow} p_1' \}$, il che è immediato. Assumiamo vero il risultato per $n$ e consideriamo $r \equiv p\vert p_{n+1}$. E' immediato, dall'applicazione delle regole di Composizione parallela che

$$\begin{array}{rcl} r & \sim & \sum \{\alpha.(p'\vert p_{n+... ...ckrel{\overline{l}}{\longrightarrow} p_{n+1}' \} \end{array}$$

Usiamo ora l'assunzione iniziale per $p \equiv p_1 \vert \dots \vert p_n, \: n \geq 1$, allora la parte destra può essere riformulata ne modo seguente (si noti che la prima sommatoria può essere divisa in due parti, a seconda che $p \stackrel{\alpha}{\longrightarrow} p'$ sia dovuto ad un singolo $p_i$ oppure all'interazione tra $p_i$ e $p_j$):

$$\begin{array}{rcl} & & \sum \left\{ \alpha.(p_1\vert \dot... ...rline{l}}{\longrightarrow} p_{n+1}' \right\} \\ \end{array}$$

Possiamo allora ricombinare la prima con la terza sommatoria e la seconda con la quarta per ottenere quanto si cercava:

$$\begin{array}{rcl} r & \sim & \sum \left\{\alpha.(p_1\vert... ...krel{\overline{l}}{\longrightarrow}p_j' \right\} \end{array}$$

Possiamo dunque estendere ($*_{+}$) per provare il teorema nella forma in cui è stato enunciato. Possiamo introdurre per prima il Relabelling, considerando $p_i \equiv q_i[f_i]$ in ($*_{+}$), ed osservando che $p_i$ ha una transizione $p_i \stackrel{\alpha}{\longrightarrow}p_i'$ sse $q_i$ ha una transizione $q_i \stackrel{\beta}{\longrightarrow}q_i'$ tale che $\alpha = f_i(\beta)$ e $p_i'=q_i'[f_i]$. Possiamo infine introdurre la Restrizione, usando l'equivalenza forte

$$q \setminus L \: \sim \: \sum \{ \beta.(q' \setminus L) \: : \: ... ...el{\beta}{\longrightarrow}q_i', \: \beta \: \not\in \: L \cup \overline{L} \}$$

dove $q \equiv q_1[f_1] \vert \dots \vert q_n[f_n]$.

$\qedsymbol$

Abbiamo quindi dimostrato tutte le leggi viste sostitudendo al simbolo '=' quello di bisimulazione forte '$\sim$'. Ciò che adesso vogliamo fare è provare che $\sim$ è una relazione di congruenza, cioè che se due processi sono bisimili fortemente, allora dove ce n'è uno si può sostituire l'altro.