Bisimulazione di branching

Questa equivalenza si pone tra la weak e la strong bisimulation, in quanto da una parte tratta le azioni invisibili in modo diverso dalle azioni visibili, ma cambia il modo di considerare gli stati intermedi.L'idea di questa relazione è quella di rilassare le richieste della strong bisimulation in modo da non differenziare processi come $p = \alpha.\beta.nil$ e $q = \alpha.\tau.\tau.\beta.nil$: chiaramente si ha che $p \: \not\sim \: q$, ma possiamo notare che dopo che entrambi hanno eseguito l'azione $\alpha$, i processi risultanti sono debolmente bisimili e le azioni $\tau$ nel mezzo non fanno cambiare classe di equivalenza agli stati intermedi. Possiamo vedere la bisimulazione di branching come il modo di uguagliare un processo che fa un azione ed un altro processo che fa tante azioni $\tau$ per poter giungere a poter fare la stessa azione passando per stati equivalenti.

Definizione 5..14 (Bisimulazione di branching)   Sia T un LTS e sia $\mathcal{R}$ una relazione sugli stati di T; $\mathcal{R}$ è una bisimulazione di branching su $T$ se è simmetrica e soddisfa la seguente condizione: se $(r,s) \in \mathcal{R}$ e $r \stackrel{\alpha}{\longrightarrow} r'$ allora implica

• $\alpha = \tau \quad \wedge \quad (r',s) \in \mathcal{R}$ oppure,

• $\exists s',s'': \: s \: \stackrel{\varepsilon}{\Longrightarrow} \: s' \: \st... ...edge \quad (r,s') \in \mathcal{R} \quad \wedge \quad (r',s'') \in \mathcal{R}$

La bisimulazione di branching considera due sistemi equivalenti soltanto se ci sono le stesse traccie visibili ed in esse gli stati intermedi, anche quelli raggiunti attraverso azioni $\tau$, hanno comportamento equivalente.

Definizione 5..15 (Equivalenza di branching)   Sia T un LTS e $p,q$ appartengano agli stati di T, allora $p \: {\approx}_b \: q$ (p bisimile di branching a q, oppure p branching equivalent a q) se e solo se esiste una bisimulazione di branching $\mathcal{R}$ tale che $p\mathcal{R}q$ ( $(p,q)\in\mathcal{R}$).