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.
Dato un sistema a transizione di stati (
S
{\displaystyle S}
Λ
{\displaystyle \Lambda }
→
{\displaystyle \to }
relazione di bisimulazione è una relazione binaria
R
{\displaystyle R}
S
{\displaystyle S}
R
∈
S
×
S
{\displaystyle R\in S\times S}
R
{\displaystyle R}
-1 and
R
{\displaystyle R}
simulazione .
Equivalentemente
R
{\displaystyle R}
p
,
q
{\displaystyle p,q}
S
{\displaystyle S}
(
p
,
q
)
{\displaystyle (p,q)}
R
{\displaystyle R}
α
{\displaystyle \alpha }
Λ
{\displaystyle \Lambda }
per ogni
p
′
{\displaystyle p'}
S
{\displaystyle S}
p
→
α
p
′
{\displaystyle p{\overset {\alpha }{\rightarrow }}p'}
implica che esiste un
q
′
{\displaystyle q'}
S
{\displaystyle S}
q
→
α
q
′
{\displaystyle q{\overset {\alpha }{\rightarrow }}q'}
con
(
p
′
,
q
′
)
∈
R
{\displaystyle (p',q')\in R}
q
′
{\displaystyle q'}
S
{\displaystyle S}
q
→
α
q
′
{\displaystyle q{\overset {\alpha }{\rightarrow }}q'}
implica che esiste un
p
′
{\displaystyle p'}
S
{\displaystyle S}
p
→
α
p
′
{\displaystyle p{\overset {\alpha }{\rightarrow }}p'}
e
(
p
′
,
q
′
)
∈
R
{\displaystyle (p',q')\in R}
Dati due stati
p
{\displaystyle p}
q
{\displaystyle q}
S
{\displaystyle S}
p
{\displaystyle p}
bisimilare a
q
{\displaystyle q}
p
∼
q
{\displaystyle p\,\sim \,q}
R
{\displaystyle R}
(
p
,
q
)
∈
R
{\displaystyle (p,q)\in R}
