Message-passing protocols are an important tool to describe interacting processes in modern concurrent and distributed computing. It is important that such processes run without error, otherwise there could be interruptions in essential services. Multiparty Session Types (MPST) are a formal specification and framework for the verification of message-passing protocols with an arbitrary number of participants.

In top-down MPST, global types are used to describe the protocol from a high level. Each participant is typed with a session type. If the collection of the session types matches a global type, it is guaranteed that no errors occur.

Many real-world message-passing protocols use randomness, for example, Markov chains. In this dissertation, we develop and study a probabilistic variant of multiparty session types by extending the theory with probability intervals. This leads to challenges with subtyping, which we overcome by developing a top-down theory which does not need transitivity of subtyping. We prove subject reduction for this probabilistic extension.