Spahn bisimulation

This entry is about

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

Definition (p.13): 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$.

Theorem (p.14): Two transition systems (and so synchronisation trees), over the same labelling set $L$, are $Bran_L$-bisimilar iff they are strongly bisimilar.

A path logic

Definition (p.35): A path bisimulation wrt. $P$, between objects $X_1,X_2$ of $M$ is defined to be a set $R$ of pairs of paths $(p_1:P\to X_1,p_2:P\to X_2)$ with common domain such that

(1) Initial paths are related: If $p_1,p_2$ are initial paths, then $(p_1,p_2)\in R$.

(2a) If $(p_1,p_2)\in R$ and if $p^\prime_1=p_1 m$, with $m\in P$, then there is a $p^\prime_2$ such that $(p^\prime_1,p^\prime_2)\in R$ and $p^\prime_2 m=p_2$.

(2b) The symmetric condition to (2a).

A path bisimulation is called to be strong if additionally (3) is satisfied.

(3) $If (p_1,p_2)\in R$ with $p_1:P\to X_1$, $p_2:P\to X_2$ and $m:P^\prime\to P$ in $P$, then $(p_1m,p_2m)\in R$.

Lemma (p.37): If $X_1,X_2$ are $P$-bisimilar, then $X_1$, $X_2$ are strong path bisimilar wrt. $P$.