A simulation between two systems (incl. PLs, calculi, transition systems, etc.) is a relation between their terms with the property that if then every behaviour of is a behaviour of .
A bisimulation is a simulation whose inverse is also a simulation. Thus iff every behaviour of is a behaviour of and vice versa.
Let be labelled transition systems.
A relation is a simulation from to just if whenever and then there exists a with and . Thus, two states are in a simulation if every behaviour of (in this case emitting a label) can be 'matched' by a behaviour of (emitting the same label), in a way that preserves the property of being in a simulation.
A bisimulation is a simulation whose inverse is also a simulation.
See Andy Gordon's 1999 article.
Sangiorgi, Davide. 2011. Introduction to Bisimulation and Coinduction. Cambridge: Cambridge University Press. https://doi.org/10.1017/CBO9780511777110.
@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}
}
Sangiorgi, Davide, and Jan Rutten, eds. 2011. Advanced Topics in Bisimulation and Coinduction. Cambridge: Cambridge University Press. https://doi.org/10.1017/CBO9780511792588.
@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}
}
Gordon, Andrew D. 1999. ‘Bisimilarity as a Theory of Functional Programming’. Theoretical Computer Science 228 (1–2): 5–47. https://doi.org/10.1016/S0304-3975(98)00353-3.
@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}
}