Bisimulation

In theoretical computer science a bisimulation is a binary relation between state transition systems, associating systems that behave in the same way in the sense that one system simulates the other and vice versa. In theoretical computer science a bisimulation is a binary relation between state transition systems, associating systems that behave in the same way in the sense that one system simulates the other and vice versa. Intuitively two systems are bisimilar if they match each other's moves. In this sense, each of the systems cannot be distinguished from the other by an observer. Given a labelled state transition system ( S {displaystyle S} , Λ, →), a bisimulation relation is a binary relation R {displaystyle R} over S {displaystyle S} (i.e., R {displaystyle R} ⊆ S {displaystyle S} × S {displaystyle S} ) such that both R {displaystyle R} and its converse R T {displaystyle R^{T}} are simulations. Equivalently R {displaystyle R} is a bisimulation if for every pair of elements p , q {displaystyle p,q} in S {displaystyle S} with ( p , q ) {displaystyle (p,q)} in R {displaystyle R} , for all α in Λ: for all p ′ {displaystyle p'} in S {displaystyle S} , and, symmetrically, for all q ′ {displaystyle q'} in S {displaystyle S} Given two states p {displaystyle p} and q {displaystyle q} in S {displaystyle S} , p {displaystyle p} is bisimilar to q {displaystyle q} , written p ∼ q {displaystyle p,sim ,q} , if there is a bisimulation R {displaystyle R} such that ( p , q ) {displaystyle (p,q)} is in R {displaystyle R} . The bisimilarity relation ∼ {displaystyle ,sim ,} is an equivalence relation. Furthermore, it is the largest bisimulation relation over a given transition system. Note that it is not always the case that if p {displaystyle p} simulates q {displaystyle q} and q {displaystyle q} simulates p {displaystyle p} then they are bisimilar. For p {displaystyle p} and q {displaystyle q} to be bisimilar, the simulation between p {displaystyle p} and q {displaystyle q} must be the converse of the simulation between q {displaystyle q} and p {displaystyle p} . Counter-example (in CCS, describing a coffee machine) : M = p . c ¯ . M + p . t ¯ . M + p . ( c ¯ . M + t ¯ . M ) {displaystyle M=p.{overline {c}}.M+p.{overline {t}}.M+p.({overline {c}}.M+{overline {t}}.M)} and M ′ = p . ( c ¯ . M ′ + t ¯ . M ′ ) {displaystyle M'=p.({overline {c}}.M'+{overline {t}}.M')} simulate each other but are not bisimilar.