%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.
Pages © WoTUG, or the indicated author. All Rights Reserved.
Comments on these web pages should be addressed to: www at wotug.org