Technical reports

Contexts and embeddings for closed shallow action graphs

Gian Luca Cattani, James J. Leifer, Robin Milner

July 2000, 56 pages

DOI: 10.48456/tr-496

Abstract

Action calculi, which have a graphical presentation, were introduced to develop a theory shared among different calculi for interactive systems. The π-calculus, the λ-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.

Full text

PS (0.2 MB)

BibTeX record

@TechReport{UCAM-CL-TR-496,
  author =	 {Cattani, Gian Luca and Leifer, James J. and Milner, Robin},
  title = 	 {{Contexts and embeddings for closed shallow action graphs}},
  year = 	 2000,
  month = 	 jul,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-496.ps.gz},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-496},
  number = 	 {UCAM-CL-TR-496}
}