Realisability of Global Types: Decidability and Verification

Behavioural Types define how information is exchanged in distributed systems. An example is Multiparty Session Types (MPST), which describe interactions between multiple participants using global protocols and their local counterparts. Ensuring correct implementation, including deadlock freedom and session conformance, is a central concern in MPST. While most research targets peer-to-peer communication, real-world systems often use different communication models such as mailbox-based or causally ordered messaging. A key challenge is that protocols valid in one model may fail in another. In this work, we develop a flexible MPST framework parameterized by different network semantics, including asynchronous, peer-to-peer, causal ordering, and synchronous. We study the realizability problem from a semantic perspective, aiming to understand its fundamental limits. My contributions include a proof of undecidability for weak realizability under synchronous semantics, and enhancements to the ReSCu tool for checking deadlock freedom in synchronous systems. This approach embeds communication models as a parameter and provides a basis for verifying distributed systems beyond classical settings.