Asynchronous Multiparty Session Type Implementability is Decidable -- Lessons Learned from Message Sequence Charts

TL;DR

This paper proves the decidability of the implementability problem for a specific class of multiparty session types with sender-driven choice, using techniques adapted from high-level message sequence charts, and explores related variants.

Contribution

It establishes the first positive decidability result for implementability of global types with sender-driven choice, extending HMSC techniques to MSTs.

Findings

Decidability of implementability for sender-driven choice global types.

Adaptation of HMSC techniques to MST setting.

Introduction of an undecidable variant of the problem.

Abstract

Multiparty session types (MSTs) provide efficient means to specify and verify asynchronous message-passing systems. For a global type, which specifies all interactions between roles in a system, the implementability problem asks whether there are local specifications for all roles such that their composition is deadlock-free and generates precisely the specified executions. Decidability of the implementability problem is an open question. We answer it positively for global types with sender-driven choice, which allow a sender to send to different receivers upon branching and a receiver to receive from different senders. To achieve this, we generalise results from the domain of high-level message sequence charts (HMSCs). This connection also allows us to comprehensively investigate how HMSC techniques can be adapted to the MST setting. This comprises techniques to make the problem algorithmically more tractable as well as a variant of implementability that may open new design space for MSTs. Inspired by potential performance benefits, we introduce a generalisation of the implementability problem that we, unfortunately, prove to be undecidable.