论文标题
二进制会议的概率分析
Probabilistic Analysis of Binary Sessions
论文作者
论文摘要
我们研究了与一类有限国家马尔可夫链有关的二进制会话类型的概率变体。会话类型中的概率注释可以使会话成功终止的概率的推理，以确定某些用户确定的成功终止概念。我们为一个简单的会话进行了一种类型的系统，该系统具有概率选择，并表明良好的过程的成功概率与他们使用的会话相符。为此，类型系统需要跟踪不同会话中概率选择的传播。
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.
