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



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