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$, $\mathrm{\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 $\mathrm{\Lambda }$:

per ogni $p^{\prime }$ in $S$,

$p\stackrel{\alpha }{\to }{p}^{\prime }$

implica che esiste un $q^{\prime }$ in $S$ tale che

$q\stackrel{\alpha }{\to }{q}^{\prime }$

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

$q\stackrel{\alpha }{\to }{q}^{\prime }$

implica che esiste un $p^{\prime }$ in $S$ tale che

$p\stackrel{\alpha }{\to }{p}^{\prime }$

e $(p^{\prime },q^{\prime })\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$.

Template:Controllo di autorità Template:Portale