Go backward to Bisimulation and Observation EquivalenceGo up to TopGo forward to Examples |

- (Weak) bisimulation
- Binary relation
*S*such that*(P,Q)*in*S*implies - if
*P*->^{alpha}*P'*, then*Q*=>^{alpha^}*Q'*with*(P',Q')*in*S*(and vice versa).

- Binary relation
- Observation equivalence
*P*~~*Q**P*~~*Q*if*(P,Q)*in*S*for some weak bisimulation*S*.- ~~ =
`union`{*S*:*S*is a weak bisimulation}

Author: Wolfgang Schreiner

Last Modification: June 8, 1998