This entry is about * [[André Joyal]], [[Mogens Nielsen]], [[Glynn Winskel]], Bisimulation from [[open map|open maps]], [pdf](http://www.brics.dk/RS/94/7/BRICS-RS-94-7.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$-[[nLab:open map]]s $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$.