Subject: categories: Preprint: Technical Report by Cattani, Leifer, and Milner

From: James Leifer <[email-masked]>
Date: Tue, 25 Jul 2000 19:08:10 +0100

The following paper: 

   TITLE:    Contexts and Embeddings for a Class of Action Graphs

   AUTHORS:  Gian Luca Cattani, James J. Leifer, and Robin Milner

is available as Technical Report 496, University of Cambridge Computer
Laboratory.  Copies may be obtained by sending email to:

   [email-masked]

or by downloading directly from these web addresses:

   http://www.cl.cam.ac.uk/users/glc25
   http://www.cl.cam.ac.uk/users/jjl21

An abstract is attached below.

   -- G.L. Cattani, J.J. Leifer, and R. Milner.

ABSTRACT:

Action calculi, which have a graphical presentation, were introduced
to develop a theory shared among different calculi for interactive
systems.  The pi-calculus, the lambda-calculus, Petri nets, the
Ambient calculus and others may all be represented as action calculi.
This paper develops a part of the shared theory.

A recent paper by two of the authors was concerned with the notion of
<i>reactive system</i>, essentially a category of process contexts
whose behaviour is presented as a reduction relation. It was shown
that one can, for any reactive system, uniformly derive a labelled
transition system whose associated behavioural equivalence relations
(e.g., trace equivalence or bisimilarity) will be congruential, under
the condition that certain <i>relative pushouts</i> exist in the
reactive system.  In the present paper we treat <i>closed, shallow</i>
action calculi (those with no free names and no nested actions) as a
generic application of these results.  We define a category of action
graphs and embeddings, closely linked to a category of contexts which
forms a reactive system.  This connection is of independent interest;
it also serves our present purpose, as it enables us to demonstrate
that appropriate relative pushouts exist.

Complemented by work to be reported elsewhere, this demonstration
yields labelled transition systems with behavioural congruences for a
substantial class of action calculi.  We regard this work as a step
towards comparable results for the full class.