## Axioms for Concurrency

**Faron Moller**
*Abstract:* 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 *w*-completely 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 onto 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.

**Ph.D Thesis - Price £7.50**

*ECS-LFCS-89-84 (also published as CST-59-89)*

Previous |

Index |

Next