## strongpre: are two agents related by the strong bisimulation preorder?

`strongpre(A,B);`

### Notes

This is NOT one half of a strong bisimulation relation!
Returns true iff A and B are related by some strong bisimulation preorder.
R is a strong 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 -a-> some globally
divergent state.)

Here "P diverges globally" means P has @ as a summand or component,
(possibly after variable lookup, possible under restriction/relabelling)
"P diverges locally at a" means P -a-> P' which diverges globally.
"Q is no more divergent than P" means if Q diverges (globally, at a) so does
P.

So if there are no @s in sight, this is the same as strongeq.

### See also

pre
precong

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