Bisimulazione

Da Wikipedia, l'enciclopedia libera.

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 distringuerli.

Definizione formale[modifica | modifica wikitesto]

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