nLab bisimulation




In set theory

Let SS be a set equipped with a binary relation \prec. Then a bisimulation is a binary relation \sim such that for all xSx \in S and ySy \in S such that xyx \sim y, the following conditions hold:

  • for all aSa \in S such that axa \prec x, there exists a bSb \in S such that byb \prec y and aba \sim b
  • for all bSb \in S such that byb \prec y, there exists a aSa \in S such that axa \prec x and aba \sim b

In category theory

In Joyal-Nielsen-Winskel (p.13) is given the following definition. For what a “path category in a category of models” is, see there.


Let PP be a path category in a category of models MM. Two objects X 1,X 2X_1,X_2 are called to be PP-bisimilar if there is a span of PP-open maps X 1XX 2X_1\leftarrow X\to X_2.

The relation of PP-open maps and open maps is given by Proposition 11, p.32:


If PP is a dense full subcategory of MM, then ff-is PP-open iff M(,f)M(-,f) is an open map.

See also


Last revised on October 20, 2022 at 21:30:46. See the history of this page for a list of all contributions to it.