cong: are two agents observationally congruent (equal)?

cong(A,B);

Notes

whenever A -a-> A' there exists B' st B =a=> B' and A' ~~ B' and

whenever B -a-> B' there exists A' st A =a=> A' and A' ~~ B'

(where A' ~~ B' means that A' and B' are weakly bisimilar)

See also