Safety of Uncertain Session Types with Interval Probability

In this article, we introduce and study a new kind of multiparty session type for a probabilistic process calculus that incorporates two forms of choice: probabilistic and nondeterministic. The main novelty of our approach is the use of interval probabilities in a type system in order to deal with uncertainty in a probabilistic process calculus. We present a decidable proof system that ensures deadlock freedom, type preservation and type safety, even when several types can be assigned to a process. The new typing system represents a conservative extension of the standard typing system based on multiparty session types (removing the probabilities from processes does not affect their well-typedness). We also define a probabilistic bisimulation between processes that are typed by using the same sorting and typing.