Operational and Algebraic Semantics of Concurrent Processes

R. Milner

Abstract: A calculus is presented for expressing and analysing concurrent processes which may communicate with one another. The view taken is that processes are not mathematical objects whose nature is universally agreed. Therefore we cannot start from a well-understood domain of entities known as processes. Rather we adopt the approach by which the lambda calculus was first introduced; we begin by defining a small language whose constructions reflect simple operational ideas, and then give the language meaning as a transition system by means of inference rules for evaluation. Thereafter we define a congruence relation over the language, called observation-congruence, based upon the idea of bisimulation from David Park. A process is then taken to be a congruence class of terms.

This congruence relation is therefore interpreted as equality of processes. Much of the paper is taken up with developing the algebra of this equality, in particular with the existence and uniqueness of solutions of equations which define processes recursively. It is then demonstrated that observation equivalence is characterised by a simple modal logic. The paper concludes with a brief study of confluence and determinacy.

The paper brings up to date the theory of CCS, a Calculus for Communicating Systems.

LFCS report ECS-LFCS-88-46

Previous | Index | Next