Properties of Bisimulation
- ~~ 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.
- P~Q implies P=Q implies P~~Q
Equality not yet fully captured.
Author: Wolfgang Schreiner
Last Modification: June 8, 1998