@INPROCEEDINGS{BM:OBCCP,
  title = {{Open bisimulation for the concurrent constraint pi-calculus}},
  author = {{Maria Grazia} {Buscemi} and {Ugo} {Montanari}},
  booktitle = {Proceedings of ESOP 2008, 17th European Symposium on Programming},
  pages = {254--268},
  abstract = { The concurrent constraint pi-calculus (cc-pi-calculus) has been introduced as a model for concluding Service Level Agreements. The cc-pi calculus combines the synchronous communication paradigm of process calculi with the constraint handling mechanism of concurrent constraint programming. While in the original presentation of the calculus a reduction semantics has been proposed, in this work we investigate the abstract semantics of cc-pi processes. First, we define a labelled transition system of the calculus and a notion of open bisimilarity a'la pi-calculus that is proved to be a congruence. Next, we give a symbolic characterisation of bisimulation and we prove that the two semantics coincide. Essentially, two processes are open bisimilar if they have the same stores of constraints - this can be statically checked - and if their moves can be mutually simulated. A key idea of the symbolic transition system is to have `contextual' labels, i.e. labels specifying that a process can evolve only in presence of certain constraints. Finally, we show that the polyadic Explicit Fusions calculus introduced by Gardner and Wischik can be translated into monadic cc-pi and that such a transition preserves open bisimilarity. The mapping exploits fusions and tuple unifications as constraints. },
  publisher = {Springer},
  series = {LNCS},
  volume = {4960},
  year = {2008},
  url = {http://rap.dsi.unifi.it/sensoriasite/CCpiSem.pdf},
  main = {Y},
  partner = {UNIPI},
  school = {Pisa},
  task = {T5.1},
}