nLab bisimulation

Definition

In set theory

Let $S$ be a set equipped with a binary relation $\prec$. Then a bisimulation is a binary relation $\sim$ on $S$ such that for all $x, y \in S$ with $x \sim y$, the following conditions hold:

• for all $a \in S$ such that $a \prec x$, there exists a $b \in S$ such that $b \prec y$ and $a \sim b$

• for all $b \in S$ such that $b \prec y$, there exists a $a \in S$ such that $a \prec x$ and $a \sim b$

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

Definition

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

Definition

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

Let $\mathrm{traces}(s)$ be the set of all possible (finite or infinite) transition sequences starting as $s$. Trace equivalence, defined as $s\sim t$ if and only if $\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 $P$ be a path category in a category of models $M$. Two objects $X_1,X_2$ are called to be $P$-bisimilar if there is a span of $P$-open maps $X_1\leftarrow X\to X_2$.

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

Proposition

If $P$ is a dense full subcategory of $M$, then $f$-is $P$-open iff $M(-,f)$ is an open map.

See also

• simulation

• extensional relation

• transition system

• cotopos

• coinduction

References

• Wikipedia (English), Bisimulation

• Peter Aczel, Non-Well-Founded Sets, especially Chapter 4.

• Sam Staton, Relating coalgebraic notions of bisimulation

• Davide Sangiorgi, On the Origins of Bisimulation and Coinduction

• André Joyal, Mogens Nielsen, Glynn Winskel, Bisimulation from open maps, pdf

• Bard Bloom, Sorin Istrail, Albert Meyer, Bisimulation can’t be traced, pdf

• Yde Venema, Algebras and Coalgebras, §6 (p.332-426).11(p.398-403) in Blackburn, van Benthem, Wolter, Handbook of modal logic, Elsevier, 2007.

• Pedro Resende, Quantales, finite observations and strong bisimulation, Theor. Comp. Sci. 254:1–2 (2001) 95–149, doi

• David Walker, On Bisimulation in the $\pi$-calculus, CONCUR ‘94: Concurrency Theory (1994).