Detail

Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types

Multiparty session types are a type system that can ensure the safety
and liveness of distributed peers via the global specification of
their interactions. To construct a global specification from a set of
distributed uncontrolled behaviours, this talk explores the problem of
fully characterising multiparty session types in terms of
communicating automata.

We equip global and local session types with labelled transition
systems (LTSs) that faithfully represent asynchronous communications
through unbounded buffered channels. Using the equivalence between the
two LTSs, we identify a class of communicating automata that exactly
correspond to the projected local types.

We exhibit an algorithm to synthesise a global type from a collection
of communicating automata. The key property of our findings is the
notion of multiparty compatibility which non-trivially extends the
duality condition for binary session types.