Probabilistic Analysis of Binary Sessions

TL;DR

This paper introduces a probabilistic extension to binary session types, allowing reasoning about the likelihood of successful session termination using a type system that tracks probabilistic choices.

Contribution

It presents a novel probabilistic session type system that models success probabilities and ensures their correctness in process interactions.

Findings

Type system accurately predicts success probabilities

Probabilistic choices are effectively propagated across sessions

Ensures well-typed processes align with session success probabilities

Abstract

We study a probabilistic variant of binary session types that relate to a class of Finite-State Markov Chains. The probability annotations in session types enable the reasoning on the probability that a session terminates successfully, for some user-definable notion of successful termination. We develop a type system for a simple session calculus featuring probabilistic choices and show that the success probability of well-typed processes agrees with that of the sessions they use. To this aim, the type system needs to track the propagation of probabilistic choices across different sessions.