eq: are two agents observationally equivalent (weakly bisimilar)?

eq(A,B);

Notes

Returns true iff the agents are related by some weak bisimulation. R is a weak bisimulation iff PRQ implies

whenever P -a-> P' there exists Q' st Q =^a=> Q' and P' R Q' and

whenever Q -a-> Q' there exists P' st P =^a=> P' and P' R Q'.

See also

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