Simulations and bisimulations

A simulation between two systems (incl. PLs, calculi, transition systems, etc.) is a relation \mathcal{R} between their terms with the property that if s \mathcal{R} t then every behaviour of s is a behaviour of t.

A bisimulation is a simulation \mathcal{R} whose inverse is also a simulation. Thus s \mathcal{R} t iff every behaviour of s is a behaviour of t and vice versa.

In transition systems

Let (S, \rightarrow_S) (T, \rightarrow_T) be labelled transition systems.

A relation \mathcal{R} \subseteq S \times T is a simulation from S to T just if whenever s \mathcal{R} t and s \xrightarrow{\ell} s' then there exists a t' with t \xrightarrow{\ell} t' and s' \mathcal{R} t'. Thus, two states s \mathcal{R} t are in a simulation if every behaviour of s (in this case emitting a label) can be 'matched' by a behaviour of t (emitting the same label), in a way that preserves the property of being in a simulation.

A bisimulation is a simulation \mathcal{R} whose inverse \mathcal{R}^{-1} is also a simulation.

In functional programming

See Andy Gordon's 1999 article.

References

• There is a book-length introduction to the topic in

@book{sangiorgi_2011,
	address = {Cambridge},
	title = {Introduction to {Bisimulation} and {Coinduction}},
	isbn = {978-0-511-77711-0},
	publisher = {Cambridge University Press},
	author = {Sangiorgi, Davide},
	year = {2011},
	doi = {10.1017/CBO9780511777110}
}

• More advanced topics are covered in the volume

@book{sangiorgi_advanced_2011,
	address = {Cambridge},
	title = {Advanced {Topics} in {Bisimulation} and {Coinduction}},
	publisher = {Cambridge University Press},
	editor = {Sangiorgi, Davide and Rutten, Jan},
	year = {2011},
	doi = {10.1017/CBO9780511792588}
}

• The use of bisimilarity as a notion of program equivalence in functional programming languages is surveyed by

@article{gordon_bisimilarity_1999,
	title = {Bisimilarity as a theory of functional programming},
	volume = {228},
	doi = {10.1016/S0304-3975(98)00353-3},
	number = {1-2},
	journal = {Theoretical Computer Science},
	author = {Gordon, Andrew D.},
	month = oct,
	year = {1999},
	pages = {5--47}
}