Termination of processes

A process terminates if it does not have an infinite sequence of reductions.

Termination is a useful property in concurrency. For instance, termination may be useful to show that when a given service is interrogated, it will eventually produce an answer. Similarly, a terminating applet, when loaded on a machine, will not run for ever on the machine, possibly absorbing all computing resources (a `denial of service' attack).

We ensure termination of a non-trivial subset of the pi-calculus by a combination of conditions based on types and on the syntax.

The proof of termination is in two parts. The first uses the technique of logical relation -- a well-know technique of lambda-calculi -- on a small set of `functional' processes. The second part of the proof uses techniques of process calculi, in particular techniques of behavioural preorders.