Bocchi, Laura and Melgratti, Hernan and Tuosto, Emilio - On Resolving Non-determinism in Choreographies

lmcs:5389 - Logical Methods in Computer Science, September 24, 2020, Volume 16, Issue 3
On Resolving Non-determinism in Choreographies

Authors: Bocchi, Laura and Melgratti, Hernan and Tuosto, Emilio

Choreographies specify multiparty interactions via message passing. A realisation of a choreography is a composition of independent processes that behave as specified by the choreography. Existing relations of correctness/completeness between choreographies and realisations are based on models where choices are non-deterministic. Resolving non-deterministic choices into deterministic choices (e.g., conditional statements) is necessary to correctly characterise the relationship between choreographies and their implementations with concrete programming languages. We introduce a notion of realisability for choreographies - called whole-spectrum implementation - where choices are still non-deterministic in choreographies, but are deterministic in their implementations. Our notion of whole spectrum implementation 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 give a type discipline for checking whole-spectrum implementations. As a case study, we analyse the POP protocol under the lens of whole-spectrum implementation.


Volume: Volume 16, Issue 3
Published on: September 24, 2020
Submitted on: April 19, 2019
Keywords: Computer Science - Software Engineering,Computer Science - Logic in Computer Science


Share

Consultation statistics

This page has been seen 81 times.
This article's PDF has been downloaded 47 times.