Axioms for Concurrency

We study properties of equational characterisations of congruences defined over process algebras. The languages on which we concentrate are based on CCS, and our equivalences are generally restricted to observational congruences. We start by defining and investigating the notion of extensionality or w-completeness of an axiomatisation with respect to some semantic equivalence, as an extension of simple completeness, and show that, whereas in some cases the ability to wcompletely axiomatise a system is straightforward, there are sometimes difficulties in doing this when our algebra contains the symmetric full merge operator. We then consider the problem of decomposing a process into the parallel composition of simpler processes. Here we present several example systems where we can prove that any process term can be expressed uniquely as the parallel composition of prime process terms, those processes which cannot themselves be expressed as a parallel composition of at least two nontrivial processes. We next consider the possibility of the nonexistence of finite axiomatisations for certain systems. In particular, we show that strong observational congruence over a subset of the usual CCS algebra with the full merge operator cannot be completely characterised by any finite set of equational axioms, thus requiring the power of the Expansion Theorem to present an infinite set of axioms within a single axiom schema. We then go on to prove that no reasonable stronger notion of congruence can be finitely axiomatised, thus explaining the difficulty presented in searching for complete laws for noninterleaving semantic congruences where the Expansion Theorem fails. Finally we consider the same problems in an algebra containing . a sequencing operator rather than the usual CCS action prefixing operator.