Paper Details

%T A Denotational Study of Mobility
%A Joël-Alexis Bialkiewicz, Frederic Peschanski
%E Peter H. Welch, Herman Roebbers, Jan F. Broenink, Frederick R. M. Barnes, Carl G. Ritson, Adam T. Sampson, G. S. Stiles, Brian Vinter
%B Communicating Process Architectures 2009
%X 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.

If you have any comments on this database, including inaccuracies, requests to remove or add information, or suggestions for improvement, the WoTUG web team are happy to hear of them. We will do our best to resolve problems to everyone's satisfaction.

Copyright for the papers presented in this database normally resides with the authors; please contact them directly for more information. Addresses are normally presented in the full paper.