Technical reports

An evaluation based approach to process calculi

Joshua Robert Xavier Ross

January 1999, 206 pages

This technical report is based on a dissertation submitted July 1998 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Clare College.

Abstract

Process calculi have, starting with Milner’s CCS, traditionally been expressed by specifying the operational semantics in terms of action-labelled transition relations between process expressions. Normally this has been done using transitions that are inductively defined by rules following the structure of the process expressions. This approach has been very successful but has suffered from certain problems. One of these is that the construction of weak, branching-time congruences has not been as simple as one might wish. In particular the natural weak bisimulations are not congruences, typically shown up by the introduction of summation. Secondly this method has not lent itself to the development of congruences for calculi that combine features of concurrency and higher-order functional languages. Another problem is more aesthetic. It is that in order to write these transition relations we need to use silent (τ) actions which are supposed to be unobservable. However, we need to represent them explicitly and make explicit reference to them in defining the congruence relations.

In this thesis, an approach to process calculi based on evaluation to committed forms is presented. In particular two process calculi are given. The first is a first-order CCS-like calculus, NCCS. This demonstrates the possibility of giving natural weak branching-time congruences, with such features as summation, without the use of explicit silent silent actions. Various bisumulations are defined on NCCS, and these are related to existing equivalences for CCS. The second is a higher order calculus, based on CML; a higher-order functional language extended with concurrent features. Again it is shown that a natural weak branching-time congruence exists. In both cases a transition relation is also given and the relationship between evaluation and transition is shown.

Full text

PDF (13.5 MB)

BibTeX record

@TechReport{UCAM-CL-TR-456,
  author =	 {Ross, Joshua Robert Xavier},
  title = 	 {{An evaluation based approach to process calculi}},
  year = 	 1999,
  month = 	 jan,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-456.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-456},
  number = 	 {UCAM-CL-TR-456}
}