Available electronically as gzipped postscript (214k) and in hard copy by emailing tech-reports@cl.cam.ac.uk
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
reactive system, 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 relative pushouts exist in the
reactive system. In the present paper we treat closed, shallow
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.
@techreport{cattani/leifer/milner:conecag,
author = {Cattani, Gian Luca and Leifer, James J and Milner, Robin},
title = {Contexts and Embeddings for a Class of Action Graphs},
institution = {Computer Laboratory, University of Cambridge}
number = {496}
year = {2000},
month = {jul},
note = {Submitted}
}