De la Wikipedia, enciclopedia liberă.
În domeniul informaticii teoretice , bisimularea este o relație binară între sistemele de tranziție de stare, care asociază două sisteme atunci când se comportă în același mod, adică atunci când un sistem îl simulează pe celălalt și invers.
Intuitiv, două sisteme sunt bisimilare dacă tranzițiile unuia pot fi imitate cu grijă de cealaltă și, în acest sens, se spune că un observator nu poate să le distingă.
Definiție formală
Având în vedere un sistem de tranziție de stat ( {\ displaystyle S} 
, {\ displaystyle \ Lambda} 
, {\ displaystyle \ to} 
), O relație de bisimulare este o relație binară {\ displaystyle R} 
pe {\ displaystyle S} (asa de {\ displaystyle R \ în S \ times S} 
) astfel încât este {\ displaystyle R} -1 și {\ displaystyle R} este o simulare .
Echivalent {\ displaystyle R} este o bisimulare dacă pentru fiecare pereche de elemente {\ displaystyle p, q} 
în {\ displaystyle S} cu {\ displaystyle (p, q)} 
în {\ displaystyle R} , pentru fiecare {\ displaystyle \ alpha} 
în {\ displaystyle \ Lambda} :
pentru fiecare {\ displaystyle p '} 
în {\ displaystyle S} ,
- {\ displaystyle p {\ overset {\ alpha} {\ rightarrow}} p '}
implică faptul că există un {\ displaystyle q '} 
în {\ displaystyle S} astfel încât
- {\ displaystyle q {\ overset {\ alpha} {\ rightarrow}} q '}
cu {\ displaystyle (p ', q') \ în R} 
; și, simetric, pentru fiecare {\ displaystyle q '} în {\ displaystyle S}
- {\ displaystyle q {\ overset {\ alpha} {\ rightarrow}} q '}
implică faptul că există un {\ displaystyle p '} în {\ displaystyle S} astfel încât
- {\ displaystyle p {\ overset {\ alpha} {\ rightarrow}} p '}
Și {\ displaystyle (p ', q') \ în R} .
Având în vedere două stări {\ displaystyle p} 
Și {\ displaystyle q} 
în {\ displaystyle S} , {\ displaystyle p} este asemănător cu {\ displaystyle q} , scris {\ displaystyle p \, \ sim \, q} 
, dacă există o bisimulare {\ displaystyle R} astfel încât {\ displaystyle (p, q) \ în R} 
.
