Department of Computer Science and Technology

Technical reports

Name-passing process calculi: operational models and structural operational semantics

Sam Staton

June 2007, 245 pages

This technical report is based on a dissertation submitted December 2006 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Girton College.

This version of the report incorporates minor changes to the June 2007 original, which were released March 2008.

DOI: 10.48456/tr-688

Abstract

This thesis is about the formal semantics of name-passing process calculi. We study operational models by relating various different notions of model, and we analyse structural operational semantics by extracting a congruence rule format from a model theory. All aspects of structural operational semantics are addressed: behaviour, syntax, and rule-based inductive definitions.

A variety of models for name-passing behaviour are considered and developed. We relate classes of indexed labelled transition systems, proposed by Cattani and Sewell, with coalgebraic models proposed by Fiore and Turi. A general notion of structured coalgebra is introduced and developed, and a natural notion of structured bisimulation is related to Sangiorgi’s open bisimulation for the π-calculus. At first the state spaces are organised as presheaves, but it is reasonable to constrain the models to sheaves in a category known as the Schanuel topos. This sheaf topos is exhibited as equivalent to a category of named-sets proposed by Montanari and Pistore for efficient verification of name-passing systems.

Syntax for name-passing calculi involves variable binding and substitution. Gabbay and Pitts proposed nominal sets as an elegant model for syntax with binding, and we develop a framework for substitution in this context. The category of nominal sets is equivalent to the Schanuel topos, and so syntax and behaviour can be studied within one universe.

An abstract account of structural operational semantics was developed by Turi and Plotkin. They explained the inductive specification of a system by rules in the GSOS format of Bloom et al., in terms of initial algebra recursion for lifting a monad of syntax to a category of behaviour. The congruence properties of bisimilarity can be observed at this level of generality. We study this theory in the general setting of structured coalgebras, and then for the specific case of name-passing systems, based on categories of nominal sets.

At the abstract level of category theory, classes of rules are understood as natural transformations. In the concrete domain, though, rules for name-passing systems are formulae in a suitable logical framework. By imposing a format on rules in Pitts’s nominal logic, we characterise a subclass of rules in the abstract domain. Translating the abstract results, we conclude that, for a name-passing process calculus defined by rules in this format, a variant of open bisimilarity is a congruence.

Full text

PDF (2.1 MB)

BibTeX record

@TechReport{UCAM-CL-TR-688,
  author =	 {Staton, Sam},
  title = 	 {{Name-passing process calculi: operational models and
         	   structural operational semantics}},
  year = 	 2007,
  month = 	 jun,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-688.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-688},
  number = 	 {UCAM-CL-TR-688}
}