precong: are two agents related by the bisimulation precongruence?



This is NOT one half of a bisimulation congruence relation.

This is like pre (q.v.) except that we fiddle the =^a=> graph such that the roots P and Q don't have tau arrows to themselves but Q does have an eps arrow to itself, which is deemed to match a tau-arrow from P to a divergent state P' which is related to Q. (We copy the roots, in fact, so if P or Q occur as derivatives of themselves then in that context they will have tau loops like all other nodes. The effect is simply to treat the first transition specially, just as in equality vs w. bisim.)

See also

  • strongpre
  • pre
    Edinburgh Concurrency Workbench (v7.1). Page generated: Sun Jul 18 11:46:51 BST 1999