Resolving non-determinism in choreographies
journal contribution
posted on 2015-03-16, 11:59 authored by L. Bocchi, H. Melgratti, Emilio TuostoResolving 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. © 2014 Springer-Verlag.
Funding
This work has been partially sponsored by Projects: EU 7FP Grant 295261 (MEALS), ANPCyT BID-PICT-2008-00319, Ocean Observatories Initiative and EPSRC EP/K034413/1.
History
Citation
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2014, 8410 LNCS, pp. 493-512Author affiliation
/Organisation/COLLEGE OF SCIENCE AND ENGINEERING/Department of Computer ScienceSource
23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014Version
- AM (Accepted Manuscript)
Published in
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)Publisher
Springer Verlag (Germany)issn
0302-9743eissn
1611-3349Copyright date
1007Available date
2015-12-31Publisher DOI
Publisher version
http://link.springer.com/chapter/10.1007/978-3-642-54833-8_26Temporal coverage: start date
2014-04-05Temporal coverage: end date
2014-04-13Language
enAdministrator link
Usage metrics
Categories
No categories selectedKeywords
Licence
Exports
RefWorks
BibTeX
Ref. manager
Endnote
DataCite
NLM
DC