## 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