Spahn
bisimulation

This entry is about

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

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

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

A path logic

Definition (p.35): A path bisimulation wrt. PP, between objects X 1,X 2X_1,X_2 of MM is defined to be a set RR of pairs of paths (p 1:PX 1,p 2:PX 2)(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 2p_1,p_2 are initial paths, then (p 1,p 2)R(p_1,p_2)\in R.

(2a) If (p 1,p 2)R(p_1,p_2)\in R and if p 1 =p 1mp^\prime_1=p_1 m, with mPm\in P, then there is a p 2 p^\prime_2 such that (p 1 ,p 2 )R(p^\prime_1,p^\prime_2)\in R and p 2 m=p 2p^\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)RIf (p_1,p_2)\in R with p 1:PX 1p_1:P\to X_1, p 2:PX 2p_2:P\to X_2 and m:P Pm:P^\prime\to P in PP, then (p 1m,p 2m)R(p_1m,p_2m)\in R.

Lemma (p.37): If X 1,X 2X_1,X_2 are PP-bisimilar, then X 1X_1, X 2X_2 are strong path bisimilar wrt. PP.

Created on February 18, 2013 at 05:36:37. See the history of this page for a list of all contributions to it.