Axiomatising Finite Concurrent Processes

We re-examine the well-known observational equivalence between processes with a view to modifying it so as to distinguish between concurrent and purely nondeterministic processes. Observational equivalence is based on atomic actions or observations. In the first part of this paper we generalise these atomic observations so that arbitrary processes may act as observers. We show, for a particular language based on finite (CCS) terms, that the generalised equivalence coincides with observational equivalence; the more powerful observers do not lead to a finer equivalence. In the second part of the paper we consider observers which can distinguish the beginning and ending of atomic actions. The resulting equivalence distinguishes a concurrent process from the purely nondeterministic process obtained by interleaving its possible actions. We give a complete axiomatisation for the congruence generated by the new equivalence.