Ph.D.: ``Operational congruences for reactive systems''

[James Leifer <James.Leifer@xxxxxxxx>]

I'm pleased to announce that the following Ph.D. dissertation is now
being distributed as a technical report and is available for download.

-James Leifer
 INRIA Rocquencourt

=================================================================

Author:        James J. Leifer

Title:         ``Operational congruences for reactive systems''

Distribution:  Ph.D. Dissertation and Technical Report 521, Computer
               Laboratory, University of Cambridge

Supervisor:    Robin Milner

URL:           http://pauillac.inria.fr/~leifer/

Abstract: 

The dynamics of process calculi, e.g. CCS, have often been defined
using a labelled transition system (LTS). More recently it has become
common when defining dynamics to use reaction rules ---i.e. unlabelled
transition rules--- together with a structural congruence. This form,
which I call a reactive system, is highly expressive but is limited in
an important way: LTSs lead more naturally to operational equivalences
and preorders.

So one would like to derive from reaction rules a suitable LTS. This
dissertation shows how to derive an LTS for a wide range of reactive
systems. A label for an agent (process) a is defined to be any context
F which intuitively is just large enough so that the agent Fa (``a in
context F'') is able to perform a reaction. The key contribution of my
work is the precise definition of ``just large enough'', in terms of
the categorical notion of relative pushout (RPO), which ensures that
several operational equivalences and preorders (strong bisimulation,
weak bisimulation, the traces preorder, and the failurespreorder) are
congruences when sufficient RPOs exist.

I present a substantial example of a family of reactive systems based
on closed, shallow action calculi (those with no free names and no
nesting). I prove that sufficient RPOs exist for a category of such
contexts. The proof is carried out indirectly in terms of a category
of graphs and embeddings and gives precise (necessary and sufficient)
conditions for the existence of RPOs. I conclude by arguing that these
conditions are satisfied for a wide class of reaction rules. The
thrust of this dissertation is, therefore, towards easing the burden
of exploring new models of computation by providing a general method
for achieving useful operational congruences.

=================================================================

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