Communicating Automata and Pi Calculus

Lecturer: Prof. A.J.R.G. Milner (rm135@cl.cam.ac.uk)

No. of lectures: 16

Prerequisites: No formal prerequisites, but it is best to have attended either Semantics of Programming Languages or Foundations of Functional Programming in Part IB

Computing is a special case of communication.

What does this mean for computation theory? Communicating systems with fixed, fluid and mobile connectivity (e.g. Java applets are mobile).

Theory of interactive automata.

Example: a vending machine. Internal and external behaviour; black boxes.

Interactive sequential processes and their equivalence.

Labelled transitions; strong bisimulation. Examples of interactive behaviour.

A calculus of concurrent systems (CCS).

Communication is mutual observation. Reaction rules to define behaviour formally.

Transition rules and bisimulation for concurrent processes.

Hence strong process equivalence and its algebraic properties.

Observable and unobservable actions, weak bisimulation.

Hence weak equivalence based upon the notion of experiment.

Analysis of several examples.

Lottery, job shop, scheduler, buffer, counter.

Systems with mobile connectivity.

Example: mobile phones, illustrating the pi calculus.

The pi calculus, a calculus of mobile systems.

Reaction rules to define its behaviour; strong congruence.

Applications of pi calculus.

Systems which handle resources reliably; data structures regarded as interactive processes; mutable data.

Sorts: a type discipline for pi calculus.

Object-oriented programming and functional programming represented in pi calculus.

Commitment rules and strong bisimulation in pi calculus.

Hence strong equivalence. Important properties of self-replicating processes.

Experiments and weak bisimulation in pi calculus.

Hence weak equivalence. Examples: imperative programming, an elastic buffer. Theorem: the lambda calculus is faithfully represented in pi calculus.

Pict: a programming language based upon pi calculus.

Its control features and type discipline. Examples of Pict programming.

Recommended texts (optional):

Milner, R. (1993). The polyadic pi calculus: a tutorial. In Logic and Algebra of Specification (ed. Bauer, F.L., Brauer, W. & Schwichtenberg, H.). NATO ASI Series F, vol. 94, pp. 203-246. Springer-Verlag.

Milner, R. (1989). Communication and Concurrency. Prentice-Hall.

Hoare, C.A.R. (1985). Communicating Sequential Processes. Prentice-Hall.