This HTML5 document contains 30 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dctermshttp://purl.org/dc/terms/
n8https://kar.kent.ac.uk/id/eprint/83104#
n2https://kar.kent.ac.uk/id/eprint/
n16https://kar.kent.ac.uk/83104/
wdrshttp://www.w3.org/2007/05/powder-s#
n14http://purl.org/ontology/bibo/status/
dchttp://purl.org/dc/elements/1.1/
rdfshttp://www.w3.org/2000/01/rdf-schema#
n4https://kar.kent.ac.uk/id/subject/
n6https://demo.openlinksw.com/about/id/entity/https/raw.githubusercontent.com/annajordanous/CO644Files/main/
n9http://eprints.org/ontology/
bibohttp://purl.org/ontology/bibo/
n18https://kar.kent.ac.uk/id/publication/
n17https://kar.kent.ac.uk/id/org/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n10https://kar.kent.ac.uk/id/document/
n13https://kar.kent.ac.uk/id/
xsdhhttp://www.w3.org/2001/XMLSchema#
n19https://demo.openlinksw.com/about/id/entity/https/www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/
n11https://kar.kent.ac.uk/id/person/

Statements

Subject Item
n2:83104
rdf:type
bibo:Article n9:EPrint n9:ArticleEPrint bibo:AcademicArticle
rdfs:seeAlso
n16:
n9:hasDocument
n10:3217201 n10:3217202 n10:3217199 n10:3217200 n10:3217129 n10:3217130
n9:hasPublished
n10:3217129
dc:hasVersion
n10:3217129
dcterms:title
On Resolving Non-determinism in Choreographies
wdrs:describedby
n6:export_kar_RDFN3.n3 n19:export_kar_RDFN3.n3
dcterms:date
2020-09-24
dcterms:creator
n11:ext-6399070bafbe877e6eaefccf8b80d2dc n11:ext-l.bocchi@kent.ac.uk n11:ext-6fe5e43e9a450873be25058ff5e1cd82
bibo:status
n14:peerReviewed n14:published
dcterms:publisher
n17:ext-1e471e62b7bed4d2a1282cb19165a99f
bibo: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.
dcterms:isPartOf
n13:repository n18:ext-18605974
dcterms:subject
n4:QA76
bibo:authorList
n8:authors
bibo:issue
3
bibo:volume
16