• People
• Events
• Research

The Nonexistence of Finite Axiomatisations for CCS congruences

Abstract: In this paper, we examine equational axiomatisations for congruences over a simple sublanguage of Milner's process algebra CCS. We show that no finite set of equational axioms can completely characterise any reasonably-defined congruence which is at least as strong as Milner's strong congruence. In the case of strong congruence, this means that the Expansion Theorem of CCS cannot be replaced by any finite collection of equational axioms. Moreover, we thus also isolate a source of difficulty in axiomatising any reasonable non-interleaving semantic congruence, where the Expansion Theorem fails to hold.

ECS-LFCS-89-97