Department of Computer Science and Technology

Technical reports

Operational congruences for reactive systems

James Leifer

September 2001, 144 pages

This technical report is based on a dissertation submitted March 2001 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Trinity College.

DOI: 10.48456/tr-521

Abstract

The dynamics of process calculi, eg. CCS, have often been defined using a labelled transaction system (LTS). More recently it has become common when defining dynamics to use reaction rules –ie. 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 notation of relative pushout (RPO), which ensures that several operational equivalences and preorders (strong bisimulation, weak bisimulation, the traces preorder, and the failures preorder) 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 RPOs exist for a category of such contexts. The proof is carried out indirectly in terms of a category of action graphs and embeddings and gives precise (necessary and sufficient) conditions for the existance 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.

Full text

PS (0.9 MB)

BibTeX record

@TechReport{UCAM-CL-TR-521,
  author =	 {Leifer, James},
  title = 	 {{Operational congruences for reactive systems}},
  year = 	 2001,
  month = 	 sep,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-521.ps.gz},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-521},
  number = 	 {UCAM-CL-TR-521}
}