[moca] paper on termination

[Davide Sangiorgi <Davide.Sangiorgi@xxxxxxxxxxxxxxx>]

I have put in 

ftp://ftp-sop.inria.fr/mimosa/personnel/davides/ter.ps

a paper on the termination of mobile processes. The title and
the abstract are below. Comments are very welcome!

Best wishes to everybody for the new year,
Davide


---------------

Title: Termination of processes
 
Abstract:
A process terminates if it cannot produce an infinite sequence of
reductions M -> M_1 -> M_2 ...  Termination is a useful property in
concurrency.  For instance, a terminating applet, when loaded on a
machine, will not run for ever, possibly absorbing all computing
resources (a `denial of service' attack).  Similarly, termination
guarantees that queries to a given service originate only finite
computations.

We ensure termination of a non-trivial subset of the pi-calculus by a
combination of conditions on types and on the syntax.  The proof of
termination is in two parts.  The first uses the technique of logical
relations -- a well-know technique of lambda-calculi -- on a small set
of non-deterministic `functional' processes.  The second part of the
proof uses techniques of process calculi, in particular techniques of
behavioural preorders.

 
  
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
 http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html