Go backward to Properties of BisimulationGo up to TopGo forward to Summary |

- Stability:
*P*is stable if*P*has no`tau`-derivative.

- Derivation of equality:
- If
*P*~~*Q*and both are stable, then*P*=*Q*. - If
*P*~~*Q*then`alpha`.*P*=`alpha`.*Q*

- If
*P*=*Q*(observation congruence)- If
*P*->^{alpha}*P'*, then*Q*=>^{alpha}*Q'*with*P'*~~*Q'*(and vice versa). - Preserved under all process operators.

- If

*Observation congruence is the equality of the process algebra.*

Author: Wolfgang Schreiner

Last Modification: June 8, 1998