Skip to main content

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)

PDF Publisher pdf
Language: English


Download (1MB) Preview
[thumbnail of 1904.08337.pdf]
Preview
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL
https://lmcs.episciences.org/

Abstract

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: 16 Feb 2021 14:15 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/83104 (The current URI for this page, for reference purposes)
Bocchi, Laura: https://orcid.org/0000-0002-7177-9395
  • Depositors only (login required):

Downloads

Downloads per month over past year