ICALP 2013. Joint work with Nobuko Yoshida.
Multiparty session types is a type discipline that can ensure the safety and liveness of distributed peers via the global specifica- tion of the interaction. To construct a global specification from a set of distributed uncontrolled behaviours, this paper 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 rep- resent asynchronous communications through unbounded buffered channels. Using the equivalence between the two LTSs, we iden- tify three classes of communicating automata that exactly corre- spond to the projected local types of three different multiparty ses- sion type theories. We exhibit decidable algorithms 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 that was valid for binary session types.
This short version is quite similar to the one that appeared in the proceedings [pdf].