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.

Probabilistic Analysis of Binary Sessions

Luca Padovani;
2020-01-01

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.
2020
Inglese
contributo
1 - Conferenza
31st International Conference on Concurrency Theory, CONCUR 2020
Vienna, Austria
2020
Internazionale
Leibniz International Proceedings in Informatics, LIPIcs
Esperti anonimi
Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Dagstuhl, Germany
GERMANIA
171
1
21
21
Deadlock freedom; Probabilistic choices; Session types; Static analysis
ARGENTINA
1 – prodotto con file in versione Open Access (allegherò il file al passo 6 - Carica)
5
info:eu-repo/semantics/conferenceObject
04-CONTRIBUTO IN ATTI DI CONVEGNO::04A-Conference paper in volume
Omar Inverso; Hernán Melgratti; Luca Padovani; Catia Trubiani; Emilio Tuosto
273
open
File in questo prodotto:
File Dimensione Formato  
LIPIcs-CONCUR-2020-14-2.pdf

Accesso aperto

Tipo di file: PDF EDITORIALE
Dimensione 582.5 kB
Formato Adobe PDF
582.5 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/1763393
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? ND
social impact