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.

Definizione formale

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

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

per ogni $p'$ in $S$,

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

implica che esiste un $q'$ in $S$ tale che

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

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

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

implica che esiste un $p'$ in $S$ tale che

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

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

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

Controllo di autorità	GND (DE) 4619739-4