title: Bisimulazione
text: # Bisimulazione
  
  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.
  
  ## Definizione formale
  
  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$.
  
  