On deciding observational congruence of finite state CCS expressions by rewriting

In this paper we propose a term rewriting approach to verify the behavioural equivalence between recursive (finite-state) CCS specifications. Verifications are performed by executing the axiomatic presentation of behavioural equivalences by means of an associated term rewriting system. Till now, we have applied our approach to the axiomatic presentation of the observational congruence for finite CCS. In that case, when trying to execute the axiomatization by means of an equivalent term rewriting system, it results that the completion process diverges, i.e. the equivalent term rewriting system has an infinite number of rules. We have recovered this divergence by defining a particular rewriting strategy that is able to compute the normal form of a finite CCS term and verify the observational congruence of two terms without performing any completion of its axiomatization. In doing that, we have been supported by a precise notion of normal form of a finite CCS term with respect to the observational congruence.