A rewriting strategy to verify observational congruence

We are concerned with the verification of behavioural equivalences for CCS specifications. We consider their axiomatic presentations thus relying on a term rewriting approach to verify the equivalence. In this framework it happens that, while some behavioural equivalences do admit a finite canonical term rewriting system, the completion of observational congruence diverges. In the paper we present a complete rewriting strategy for observational congruence that permits to reduce a finite CCS specification to normal form without attempting any completion.