nLab bisimulation

Contents

Contents

Definition

In set theory

Let SS be a set equipped with a binary relation \prec. Then a bisimulation is a binary relation \sim on SS such that for all x,ySx, y \in S with 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

For labelled transition systems, Walker 1994 gives a definition equivalent to the following:

Definition

On a system with points P,Q,P,Q,\ldots and transition relations {α:αL}\{\overset{\alpha}{\rightarrow} \colon \alpha\in L\}, a bisimulation is a symmetric relation \sim such that whenever PQP\sim Q, αL\alpha\in L and PαPP\overset{\alpha}{\rightarrow}P', then QαQQ\overset{\alpha}{\rightarrow}Q' with PQP'\sim Q'.

Definition

The union of all bisimulation relations, as subsets of S×SS \times S, is a relation called bisimilarity.

Let traces(s)\mathrm{traces}(s) be the set of all possible (finite or infinite) transition sequences starting as ss. Trace equivalence, defined as sts\sim t if and only if traces(s)=traces(t)\mathrm{traces}(s)=\mathrm{traces}(t), is a bisimulation.

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.

Definition

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:

Proposition

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

References

Last revised on February 15, 2024 at 10:07:37. See the history of this page for a list of all contributions to it.