Dato un insieme di processi P, una relazione R ⊆ P × P (scritto p R q con (p,q) ∈ R) è detta bisimulazione forte se:
∀p, q.(p, q) ∈ R ⇒ {(∀μ,p'.p μ→ p'⇒ ∃q'.q → q' ∧ p' R q') ∧ (∀μ,q'.q μ→ q' ⇒ ∃p'.p → p' ∧ p' R q')
In termini intuitivi, la bisimulazione è una relazione di corrispondenza tra le mosse effettuabili dai due processi: "perchè vi sia una bisimulazione, se p effettua una transizione μ per andare in p', allora anche q deve poter fare una transizione μ in q', e i punti di arrivo devono anch'essi godere di questa proprietà"
La bisimulazione può essere vista come un "gioco" in cui un attaccante e un difensore si sfidano per dimostrare che i due programmi sono rispettivamente diversi e uguali.
La bisimilarità è la relazione di equivalenza formata dall'unione di tutte le bisimulazioni.
Notare che la definizione di bisimulazione è ricorsiva, questo significa che la bisimilarità è un concetto esprimibile come punto fisso, applicando il Teorema di Kleene.
Definiamo il funzionale Φ:
Φ(R) := {(p, q) | (∀μ, p′.p μ→ p′ ⇒ ∃q′.q μ→ q′ ∧ p′ R q′) ∧ (∀μ, q′.q μ→ q′ ⇒ ∃p′.p μ→ p′ ∧ p′ R q′)}
≃ := ⊔_n∈N Φ^n (P_f × P_f)
La CPO usata per il sistema è molto particolare; di solito si tende a cercare di trovare la relazione più stretta, qui cerchiamo l'approssimazione più grossolana e inclusiva possibile.
D = (p(P × P),⊑)
R ⊑ R' <=> R' ⊆ R
Quindi l'elemento ⊥ è il prodotto cartesiano P × P !
Cosa significa tutto questo? Significa che partiamo da tutte le coppie di processi del nostro insieme, e man mano eseguendo tante volte Φ, otteniamo un restringimento sempre maggiore (R1 indica i processi distinguibili in un passaggio, R2 in due, e così via..) fino al raggiungimento di un insieme di processi equivalenti (non distinguibili, neanche con un numero infinito di applicazioni di Φ), appunto la bisimilarità forte.
Cosa si intende con "forte" (termine che abbiamo usato fino ad ora)?
Con forte si intende l'inclusione di tutti i passaggi τ, silenziosi (senza comunicazione). La bisimulazione forte implica dunque che tutti i passaggi effettuati dal giocatore in attacco (colloquialmente le mosse di Alice) abbiano un corrispondente in difesa (mosse di Bob), anche se si tratta di operazioni silenti.
La bisimulazione debole rilassa questa condizione, pertanto una mossa τ può essere corrisposta ad un'inazione, una o più azioni τ. E' importante però notare che la bisimulazione debole (il cui insieme unione prende il nome di Bisimilarità debole) è una relazione di equivalenza, ma non di congruenza. Infatti due programmi a + b, a + τ.b sono di fatto equivalenti, ma la presenza di τ nel branch destro può "silenziosamente" precludere la scelta di questo, non a caso facendo vincere immediatamente il gioco di Alice.