## pre: are two agents related by the (weak) bisimulation preorder?

`pre(A,B);`

### Notes

This is NOT one half of a weak bisimulation relation!
Returns true iff A and B are related by some weak bisimulation preorder.
R is a weak bisimulation preorder iff PRQ implies

Q is no more divergent than P and

P=^a=>P' implies Q=^a=>Q' and P' R Q' and

either P diverges globally or Q=^a=>Q' implies P=^a=>P' and P' R Q'
(except that we allow Q=^a=>Q' to go unmatched if P is locally
divergent at a)

We set divergence by maximal fixpoint: a thing gets to be marked not
globally divergent by not having @ as a summand or component (even
under restriction/relabelling), and not having any tau-successors, or
having every tau-successor satisfy that. Then P diverges at a iff
P=a=>P' globally divergent. (So, e.g., @ does not diverge at tau.)

### See also

strongpre
precong

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