Go backward to Properties of Bisimulation
Go up to Top
Go forward to Summary

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.

Id: ccs2.tex,v 1.1 1996/06/12 15:55:52 schreine Exp schreine