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

strongpre(A,B);

Notes

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