Bisimulazione ed equivalenza debole (osservazionale)

Abbiamo appena visto la nozione di bisimulazione forte, nella quale ogni azione $\alpha$ di un processo deve corrispondere ad un'azione $\alpha$ dell'altro, anche per le azioni $\tau$. Quanto faremo adesso sarà rilassare questa richiesta ed ottenendo dunque una relazione più debole (in quanto identifica più processi): ciò che si richiede ora è che ogni azione $\tau$ venga corrisposta con zero o più azioni $\tau$. Questo ci porterà alla definizione di bisimulazione debole e quindi alla definizione di una equivalenza debole o, come viene più spesso chiamata, dell'equivalenza osservazionale.

Procederemo in modo analogo a quanto fatto per l'equivalenza forte, rimandando al capitolo relativo alla bisimulazione la visione di una serie di importanti risultati.

Cerchiamo dunque una nozione di equivalenza, che chiameremo equivalenza osservazionale, che rispetti la seguente proprietà:

p e q sono osservazionalmente equivalenti sse, per ogni azione $\alpha$, ogni derivazione da p tramite $\alpha$ è osservazionalmente equivalente a qualche discendenza da q tramite l'azione $\alpha$, e similmente per il viceversa.

Chiameremo questa equivalenza $\approx$ e formalmente scriviamo:

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

1. $\forall p': \: p \stackrel{\alpha}{\longrightarrow} p' \quad \exists q' : \: ... ...ckrel{\hat{\alpha}}{\Longrightarrow} q' \quad \wedge \quad p' \: \approx \: q'$;

2. $\forall q': \: q \stackrel{\alpha}{\longrightarrow} q' \quad \exists p' : \: ... ...ckrel{\hat{\alpha}}{\Longrightarrow} p' \quad \wedge \quad p' \: \approx \: q'$.

dove

$$\stackrel{\hat{\alpha}}{\Rightarrow} \: = \: \left\{ \begin{... ...el{\varepsilon}{\Rightarrow} & a = \tau \end{array} \right.$$

Operando in modo analogo a quanto fatto per la strong bisimulation, cerchiamo ora la più grande relazione che soddisfi ( $*_{\approx}$); procediamo dunque come già visto:

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

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

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

Possiamo ora definire l'equivalenza osservazionale, o bisimilarità:

Definizione 5..12 (Equivalenza osservazionale)   p e q sono osservazionalmente equivalenti oppure bisimili (debolmente), $p\:\approx\: q$, se esiste una bisimulazione debole $\mathcal{S}$ tale che $(p,q) \: \in \: \mathcal{S}$. In modo equivalente:

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