Go backward to Examples Go up to Top Go forward to Observation Congruence

Properties of Bisimulation

• Propositions:
  • ~~ is the largest bisimulation.
  • ~~ is an equivalence relation.
  • P ~~ tau.P
• ~~ is not yet equality:
  • ~~ not preserved by summation.
  • a.0 + b.0 ~~ a.0+tau.b.0 does not hold!
  • Proof: if (P,Q) were in a bisimulation S, then, since Q ->^tau b.0, we need (P', b.0) in S with P =>^epsilon Q'. But the only P' is P itself but (P,b.0) can be not in S, since P ->a 0, while b.0 has no a-descendant.
• Relations:
  • P~Q implies P=Q implies P~~Q

Equality not yet fully captured.