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 formaleModifica

Dato un sistema a transizione di stati ( ,  ,  ), una relazione di bisimulazione è una relazione binaria   su   (quindi  ) tale che sia  -1 and   è una simulazione.

Equivalentemente   è una bisimulazione se per ogni coppia di elementi   in   con   in  , per ogni   in  :

per ogni   in  ,

 

implica che esiste un   in   tale che

 

con  ; e, simmetricamente, per ogni   in  

 

implica che esiste un   in   tale che

 

e  .

Dati due stati   e   in  ,   è bisimilare a  , scritto  , se esiste una bisimulazione   tale che  .


Controllo di autoritàGND (DE4619739-4