Bisimulazione

Nel campo dell'informatica teorica la bisimulazione è una relazione binaria tra sistemi a transizione di stati, che associa due sistemi quando si comportano nello stesso modo, quando cioè un sistema simula l'altro e viceversa.

Intuitivamente due sistemi sono bisimilari se le transizioni di uno possono essere ordinatamente mimate dall'altro, ed è in questo senso che si dice che un osservatore non è in grado di distinguerli.

Dato un sistema a transizione di stati (${\displaystyle S}$, ${\displaystyle \Lambda }$, ${\displaystyle \to }$), una relazione di bisimulazione è una relazione binaria ${\displaystyle R}$ su ${\displaystyle S}$ (quindi ${\displaystyle R\in S\times S}$) tale che sia ${\displaystyle R}$^-1 and ${\displaystyle R}$ è una simulazione.

Equivalentemente ${\displaystyle R}$ è una bisimulazione se per ogni coppia di elementi ${\displaystyle p,q}$ in ${\displaystyle S}$ con ${\displaystyle (p,q)}$ in ${\displaystyle R}$, per ogni ${\displaystyle \alpha }$ in ${\displaystyle \Lambda }$:

per ogni ${\displaystyle p'}$ in ${\displaystyle S}$,

${\displaystyle p{\overset {\alpha }{\rightarrow }}p'}$

implica che esiste un ${\displaystyle q'}$ in ${\displaystyle S}$ tale che

${\displaystyle q{\overset {\alpha }{\rightarrow }}q'}$

con ${\displaystyle (p',q')\in R}$; e, simmetricamente, per ogni ${\displaystyle q'}$ in ${\displaystyle S}$

${\displaystyle q{\overset {\alpha }{\rightarrow }}q'}$

implica che esiste un ${\displaystyle p'}$ in ${\displaystyle S}$ tale che

${\displaystyle p{\overset {\alpha }{\rightarrow }}p'}$

e ${\displaystyle (p',q')\in R}$.

Dati due stati ${\displaystyle p}$ e ${\displaystyle q}$ in ${\displaystyle S}$, ${\displaystyle p}$ è bisimilare a ${\displaystyle q}$, scritto ${\displaystyle p\,\sim \,q}$, se esiste una bisimulazione ${\displaystyle R}$ tale che ${\displaystyle (p,q)\in R}$.