On Resolving Non-determinism in Choreographies
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...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2020-09-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/5389/pdf |
| _version_ | 1797268543378554880 |
|---|---|
| author | Laura Bocchi Hernan Melgratti Emilio Tuosto |
| author_facet | Laura Bocchi Hernan Melgratti Emilio Tuosto |
| author_sort | Laura Bocchi |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:34:09Z |
| format | Article |
| id | doaj.art-157a6267981e418eb47dd04b40ae3130 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:34:09Z |
| publishDate | 2020-09-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-157a6267981e418eb47dd04b40ae31302024-03-08T10:31:24ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742020-09-01Volume 16, Issue 310.23638/LMCS-16(3:18)20205389On Resolving Non-determinism in ChoreographiesLaura BocchiHernan MelgrattiEmilio TuostoChoreographies 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.https://lmcs.episciences.org/5389/pdfcomputer science - software engineeringcomputer science - logic in computer science |
| spellingShingle | Laura Bocchi Hernan Melgratti Emilio Tuosto On Resolving Non-determinism in Choreographies Logical Methods in Computer Science computer science - software engineering computer science - logic in computer science |
| title | On Resolving Non-determinism in Choreographies |
| title_full | On Resolving Non-determinism in Choreographies |
| title_fullStr | On Resolving Non-determinism in Choreographies |
| title_full_unstemmed | On Resolving Non-determinism in Choreographies |
| title_short | On Resolving Non-determinism in Choreographies |
| title_sort | on resolving non determinism in choreographies |
| topic | computer science - software engineering computer science - logic in computer science |
| url | https://lmcs.episciences.org/5389/pdf |
| work_keys_str_mv | AT laurabocchi onresolvingnondeterminisminchoreographies AT hernanmelgratti onresolvingnondeterminisminchoreographies AT emiliotuosto onresolvingnondeterminisminchoreographies |