Skip to main content
Kent Academic Repository

On Resolving Non-determinism in Choreographies

Bocchi, Laura, Melgratti, Hernán, Tuosto, Emilio (2020) On Resolving Non-determinism in Choreographies. Logical Methods in Computer Science, 16 (3). 18:1-18:69. ISSN 1860-5974. (KAR id:83104)


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.

Item Type: Article
Uncontrolled keywords: Choreographies, realisation, implementation, determinism, completeness
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Laura Bocchi
Date Deposited: 24 Sep 2020 08:30 UTC
Last Modified: 10 Dec 2022 04:03 UTC
Resource URI: (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.