@InProceedings{BialkiewiczPeschanski09,
  title =        "{A} {D}enotational {S}tudy of {M}obility",
  author=        "Bialkiewicz,  Joël-Alexis and Peschanski,  Frederic",
  editor=        "Welch, Peter H. and Roebbers,  Herman and Broenink,  Jan F. and Barnes,  Frederick R. M. and Ritson,  Carl G. and Sampson,  Adam T. and Stiles,  G. S. and Vinter,  Brian",
  pages =        "239--261",
  booktitle=     "{C}ommunicating {P}rocess {A}rchitectures 2009",
  isbn=          "978-1-60750-065-0",
  year=          "2009",
  month=         "nov",
  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."
}