Bisimulazione debole

Come fatto per la bisimulazione forte, intendiamo ora dimostrare proprietà analoghe anche per la bisimulazione debole.

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

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. La dimostrazione si svolge in modo simile a quanto fatto in precedenza (proposizione 6.1); nel punto 3. abbiamo però bisogno del risultato che se $(q,r) \: \in \: \mathcal{S}_i$ e $q \stackrel{\hat{\alpha}}{\Longrightarrow} q'$ allora, per qualche $r', \: r \stackrel{\hat{\alpha}}{\Longrightarrow} r'$ e $(q',r') \: \in \: \mathcal{S}_i$. $\qedsymbol$

Proposizione 6..9   $\:$

1. $\approx$ è la più larga bisimulazione;

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

Dimostrazione. Anche in questo caso, la dimostrazione segue la linea della proposizione 6.2, solo che ci si deve basare sul risultato ottenuto sopra. $\qedsymbol$

Continuando con l'analogia, vogliamo dunque provare che $\approx$ soddisfa ( $*_{\approx}$): definiamo dunque una nuova relazione, $\approx'$ in termini di $\approx$ nel modo seguente:

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

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

Dalla proposizione 6.2, punto 1., sappiamo che $\approx$ è una bisimulazione debole, e possiamo dedurre similmente che $p\:\approx\: q$ implica $p \: \approx ' \: q$, rimane da provare che $p \: \approx ' \: q$ implica $p\:\approx\: q$ :

Lemma 6..2   La relazione $\approx'$ è una bisimulazione debole.

Dimostrazione. Analogo al lemma 6.1. $\qedsymbol$

Abbiamo dunque dimostrato che $\approx$ soddisfa ( $*_{\approx}$), cioè che:

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

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

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

Presentiamo ancora ulteriori proprietà della bisimulazione, e guardiamo proprio al caso emblematico che la distingue da $\sim$:

Proposizione 6..11   $p \: \approx \: \tau.p$

Dimostrazione. Dal momento che abbiamo mostrato l'uguaglianza di $\approx$ e $\approx'$, proveremo $p \: \approx' \: \tau.p$. Da prima consideriamo ogni azione $p \stackrel{\alpha}{\longrightarrow} p'$ di $p$: chiaramente $\tau.p \stackrel{\tau}{\longrightarrow}p \stackrel{\alpha}{\longrightarrow} p'$, quindi $\tau.p \stackrel{\hat{\alpha}}{\Longrightarrow} p'$, e sappiamo che $p' \approx p'$. D'altra parte, consideriamo la sola azione $\tau.p \stackrel{\tau}{\longrightarrow}p$ di $\tau.p$: questa è chiaramente corrisposta dall'azione nulla $p \stackrel{\varepsilon}{\Longrightarrow} p$ di $p$, poichè $\hat{\tau}=\varepsilon$. Abbiamo dunque che $p \: \approx' \: \tau.p$ e di conseguenza $p \: \approx \: \tau.p$. $\qedsymbol$

Quello che abbiamo dimostrato è proprio la potenza della bisimulazione: consente di ignorare le azioni $\tau$ durante l'investigazione sulla bisimilarità! Purtroppo però, proprio a causa della prelazione dell'azione $\tau$, la bisimulazione non è preservata dalla Somma, come si vede da questo esempio:

$$b.nil \approx \tau.b.nil$$

$$a.nil+b.nil \not\approx a.nil+\tau.b.nil$$

Per questo, la nozione di '$\approx$' non è quella di uguaglianza '=', ma le due nozioni sono molto vicine: vedremo in seguito come un modifica minima nella definizione di $\approx$ li renda concetti equivalenti.

Definizione 6..3   $p$ è stabile se non ha derivazioni $\tau$.

Proposizione 6..12   Se $p\:\approx\: q$ e sono entrambi stabili, allora $p =q$.

Da questo risultato, sembra che la differenza tra bisimulazione ed uguaglianza stia esclusivamente nella presenza di azioni $\tau$ iniziali. Il seguente risultato lo evidenzia ancora maggiormente:

Proposizione 6..13   Se $p\:\approx\: q$ allora $\alpha.p = \alpha.q$.

Questo implica che la bisimulazione viene preservata dalla Sequenzalizzazione (in questo caso è addirittura rafforzata!) e da tutti gli altri operatori ad eccezione della Somma.