Probabilities in Session Types

TL;DR

This paper extends multiparty session types to include probabilistic behaviors in distributed systems, providing a formal calculus and typing system to analyze such probabilistic processes.

Contribution

It introduces a novel probabilistic process calculus with an extended typing system based on session types, enabling formal reasoning about probabilistic distributed systems.

Findings

Defined a probabilistic process calculus with internal and external choices.

Extended session types to handle probabilistic behaviors.

Illustrated the calculus and typing system with a motivating example.

Abstract

This paper deals with the probabilistic behaviours of distributed systems described by a process calculus considering both probabilistic internal choices and nondeterministic external choices. For this calculus we define and study a typing system which extends the multiparty session types in order to deal also with probabilistic behaviours. The calculus and its typing system are motivated and illustrated by a running example.