Implementability of Asynchronous Communication Protocols - The Power of Choice

The work in this dissertation is the first to formally build a bridge between the world of MSTs and HMSCs. It presents a generalised MST projection operator for sender-driven choice. This allows a sender to send to different receivers when branching, which is crucial to handle common communication patterns from distributed computing. Nevertheless, the classical MST projection approach is inherently incomplete. Using our formal encoding from global types to HMSCs, we prove decidability of the implementability problem for global types with sender-driven choice. Furthermore, we develop the first direct and complete projection operator for global types with sender-driven choice, using automata-theoretic techniques, and show its effectiveness with a prototype implementation. Last, we introduce protocol state machines (PSMs) - an automata-based protocol specification formalism - that subsume both global types from MSTs and HMSCs with regard to expressivity. We use transformations on PSMs to show that many of the syntactic restrictions of global types are not restrictive in terms of protocol expressivity. We prove that the implementability problem for PSMs with mixed choice, which requires no dedicated sender for a branch but solely all labels to be distinct, is undecidable in general. With our results on expressivity, this shows undecidability of the implementability problem for mixed-choice global types.