Synthesising Choreographies from Local Session Types (extended version)

TL;DR

This paper introduces a typing system that enables the synthesis of global choreographies from local session types, facilitating the design and analysis of multiparty distributed interactions.

Contribution

It presents a novel method for deriving global interaction protocols from local endpoint behaviors using a formal typing system.

Findings

Successful synthesis of choreographies from local types under certain conditions

Formal proof of correctness of the synthesis process

Potential applications in automated choreography generation

Abstract

Designing and analysing multiparty distributed interactions can be achieved either by means of a global view (e.g. in choreography-based approaches) or by composing available computational entities (e.g. in service orchestration). This paper proposes a typing systems which allows, under some conditions, to synthesise a choreography (i.e. a multiparty global type) from a set of local session types which describe end-point behaviours (i.e. local types).