Mobility Reading Group

Resolving Non-determinism in Choreographies

Laura BOCCHI, Hernán MELGRATTI, Emilio TUOSTO

23rd European Symposium on Programming (ESOP 2014). p. 512 - 493

Resolving non-deterministic choices of choreographies is a crucial task. We introduce a novel notion of realisability for choreographies –called whole-spectrum implementation– that rules out deterministic implementations of roles that, no matter which context they are placed in, will never follow one of the branches of a non-deterministic choice. We show that, under some conditions, it is decidable whether an implementation is whole-spectrum. As a case study, we analyse the POP protocol under the lens of whole-spectrum implementation.

Paper (ESOP14) Electronic version via DOI

BibTeX
Short
Long

@inproceedings{BMT2014,
  author = {Laura Bocchi and Hernán Melgratti and Emilio Tuosto},
  title = {{Resolving Non-determinism in Choreographies}},
  booktitle = {23rd European Symposium on Programming},
  series = {LNCS},
  volume = {8410},
  pages = {512--493},
  publisher = {Springer},
  year = 2014
}

@inproceedings{BMT2014,
  author = {Laura Bocchi and Hernán Melgratti and Emilio Tuosto},
  title = {{Resolving Non-determinism in Choreographies}},
  booktitle = {23rd European Symposium on Programming},
  series = {LNCS},
  volume = {8410},
  pages = {512--493},
  publisher = {Springer},
  doi = "10.1007/978-3-642-54833-8_26",
  year = 2014
}