Bisimulazione

Da Wikipedia, l'enciclopedia libera.

Nel campo dell'informatica teorica la bisimulazione è una relazione binaria tra sistemi a transizione di stati, che associa sistemi i quali si comportano nello stesso modo nel senso che un sistema simula l'altro e viceversa.

Intuitivamente due sistemi sono bisimilari se le mosse di uno corrispondono a quelle dell'altro. In questo senso ognuno dei sistemi non può essere distinto dall'altro da un osservatore.

Definizione formale[modifica | modifica sorgente]

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.