db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"<br>
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"<br>

%T A Denotational Study of Mobility
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"<br>
%A  Joël\-Alexis Bialkiewicz,  Frederic Peschanski
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"<br>
%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.