In theoretical computer science, a bisimulation is a binary relation between state transition systems, associating systems that behave in the same way in that one system simulates the other and vice versa.

Intuitively two systems are bisimilar if they, assuming we view them as playing a game according to some rules, match each other's moves. In this sense, each of the systems cannot be distinguished from the other by an observer.

Given a labeled state transition system (S, Λ, →), where S is a set of states, ${\displaystyle \Lambda }$ is a set of labels and → is a set of labelled transitions (i.e., a subset of ${\displaystyle S\times \Lambda \times S}$), a bisimulation is a binary relation ${\displaystyle R\subseteq S\times S}$, such that both R and its converse ${\displaystyle R^{T}}$ are simulations. From this follows that the symmetric closure of a bisimulation is a bisimulation, and that each symmetric simulation is a bisimulation. Thus some authors define bisimulation as a symmetric simulation.

Equivalently, R is a bisimulation if and only if for every pair of states ${\displaystyle (p,q)}$ in R and all labels λ in ${\displaystyle \Lambda }$:

Given two states p and q in S, p is bisimilar to q, written ${\displaystyle p\,\sim \,q}$, if and only if there is a bisimulation R such that ${\displaystyle (p,q)\in R}$. This means that the bisimilarity relation ∼ is the union of all bisimulations: ${\displaystyle (p,q)\in \,\sim \,}$ precisely when ${\displaystyle (p,q)\in R}$ for some bisimulation R.

The set of bisimulations is closed under union; therefore, the bisimilarity relation is itself a bisimulation. Since it is the union of all bisimulations, it is the unique largest bisimulation. Bisimulations are also closed under reflexive, symmetric, and transitive closure; therefore, the largest bisimulation must be reflexive, symmetric, and transitive. From this follows that the largest bisimulation—bisimilarity—is an equivalence relation.

Bisimulation can be defined in terms of composition of relations as follows.

Given a labelled state transition system ${\displaystyle (S,\Lambda ,\rightarrow )}$, a bisimulation relation is a binary relation R over S (i.e., R ⊆ S × S) such that ${\displaystyle \forall \lambda \in \Lambda }$