Probabilistic Analysis of Binary Sessions
Logic in Computer Science
2020-07-24 v1
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.
Cite
@article{arxiv.2007.11832,
title = {Probabilistic Analysis of Binary Sessions},
author = {Omar Inverso and Hernán Melgratti and Luca Padovani and Catia Trubiani and Emilio Tuosto},
journal= {arXiv preprint arXiv:2007.11832},
year = {2020}
}