Observation Congruence
- 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
- P = Q (observation congruence)
- If P ->alpha P', then Q =>alpha Q'
with P' ~~ Q' (and vice versa).
- Preserved under all process operators.
Observation congruence is the equality of the process algebra.
Author: Wolfgang Schreiner
Last Modification: June 8, 1998