Paper Details

Communicating Process Architectures (CPA)
 Title: A Denotational Study of Mobility
 Conference: Communicating Process Architectures 2009
 Authors: Joél-Alexis Bialkiewicz, Frederic Peschanski
UPMC Paris Universitas
 Abstract: This paper introduces a denotational model and refinement theory for a process algebra with mobile channels. Similarly to CSP, process behaviours are recorded as trace sets. To account for branching-time semantics, the traces are decorated by structured locations that are also used to encode the dynamics of channel mobility in a denotational way. We present an original notion of split-equivalence based on elementary trace transformations. It is first characterised coinductively using the notion of split-relation. Building on the principle of trace normalisation, a more denotational characterisation is also proposed. We then exhibit a preorder underlying this equivalence and motivate its use as a proper refinement operator. At the language level, we show refinement to be tightly related to a construct of delayed sums, a generalisation of non-deterministic choices. 

BibTeX Entry

Full paper