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 so dice che un osservatore non è in gradi di distringuerli.

Definizione formale[modifica | modifica wikitesto]

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.