Go backward to Strong BisimulationGo up to TopGo forward to Properties of Strong Equivalence |

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

- Corollaries:
- ~ is the largest strong bisimulation.
- ~ is an equivalence relation.

- Proposition:
*P*~*Q*iff, for all`alpha`,- If
*P*->^{alpha}*P'*, then*Q*->^{alpha}*Q'*with*(P',Q')*in*S*and vice versa.

Author: Wolfgang Schreiner

Last Modification: June 8, 1998