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

lmcs:5389 - Logical Methods in Computer Science, September 24, 2020, Volume 16, Issue 3 - https://doi.org/10.23638/LMCS-16(3:18)2020
On Resolving Non-determinism in ChoreographiesArticle

Authors: Laura Bocchi ; Hernan Melgratti ; Emilio Tuosto

    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
    Accepted on: August 10, 2020
    Submitted on: April 19, 2019
    Keywords: Computer Science - Software Engineering,Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • Behavioural Application Program Interfaces; Funder: European Commission; Code: 778233

    1 Document citing this article

    Consultation statistics

    This page has been seen 1081 times.
    This article's PDF has been downloaded 212 times.