Go backward to ExamplesGo up to TopGo forward to Observation Congruence |

- 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.*

Author: Wolfgang Schreiner

Last Modification: June 8, 1998