Bisimulazione ed equivalenza forte

Ciò che si vuole ottenere è una relazione di equivalenza che soddisfi la seguente proprietà:

p e q sono equivalenti sse, per ogni azione $\alpha$, ogni derivazione di p con $\alpha$ è equivalente a qualche derivazione di q con $\alpha$, e viceversa.

con $p,q \in \mathcal{P}$, l'insieme dei processi.

Scrivendo in modo formale, utilizzando il simbolo $\sim$ per la nostra equivalenza, si ha:

p $\sim$ q sse, $\forall \alpha \: \in \: Act \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad$ ($*_{\sim}$)

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'$.

Purtroppo quanto appena scritto non è una definizione, in quanto esistono molte relazioni di equivalenza che soddisfano questa proprietà! Ci accontenteremmo di eguagliare più processi possibili, fintantoche la proprietà sopra è verificata: quello che allora stiamo cercando è la più grande (più debole o più generosa, in quanto identifica più processi) relazione $\sim$ che soddisfi questa proprietà. Per raggiungere questo obiettivo dovremo compiere alcuni passi intermedi, il primo dei quali è la definizione di bisimulazione forte:

Definizione 5..9 (Bisimulazione forte)   Una relazione binaria $\mathcal{S} \: \subseteq \: \mathcal{P}\times\mathcal{P}$ è una bisimulazione forte se $(p,q) \: \in \: \mathcal{S}$ implica, $\forall \alpha \in Act$:

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

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

Come si può notare, ogni relazione $\sim$ che soddisfa la proprietà ($*_{\sim}$), è anche una bisimulazione. La condizione della definizione, però, è più debole della condizione in ($*_{\sim}$), in quanto al posto di 'sse' abbiamo 'implica', e dunque si hanno molte bisimulazioni forti: anche $\mathcal{S} = \emptyset$ è una bisimulazione forte!

Definiamo allora l'equivalenza forte:

Definizione 5..10 (Equivalenza forte)   p e q sono fortemente equivalenti oppure fortemente bisimili, $p\:\sim\: q$, se esiste una bisimulazione forte $\mathcal{S}$ tale che $(p,q) \: \in \: \mathcal{S}$. In modo equivalente:

$$\sim \: = \: \bigcup \{ \mathcal{S} \:$$    tale che $$\: \mathcal{S} \:$$    sia una bisimulazione forte$$\}$$

La relazione di equivalenza forte è la più grande bisimulazione forte, ovvero quella che contiene tutte le bisimulazioni forti.

L'importanza della bisimulazione forte è che permette di associare sistemi che, all'interno di uno stesso ambiente, si comportano esattamente nello stesso modo; ma se da un lato questo è un vantaggio, da un'altro è un vincolo troppo stretto dal momento che risulta essere fin troppo sensibile alle azioni interne dei processi: spesso non è necessario considerarle al pari delle azioni visibili. Per questo motivo vengono usate delle altre equivalenze, dette deboli in quanto le azioni invisibili non vengono considerate, e che risultano comunque di grande importanza.

Alcuni importanti risultati sono che:

$$\sim \quad \Longrightarrow \quad {\sim}_t$$

$$\sim \quad \Longrightarrow \quad {\simeq}_{test} \Longrightarrow \quad {\approx}_t$$