Probabilistic asynchronous pi-calculus

TL;DR

This paper introduces a probabilistic extension to the asynchronous pi-calculus, enabling reasoning about probabilistic correctness and solving previously impossible problems like electoral consensus.

Contribution

It defines a new probabilistic asynchronous pi-calculus with a clear operational semantics distinguishing internal probabilistic choices from external nondeterministic choices.

Findings

Able to solve the electoral problem in the probabilistic setting

Provides an implementation in a Java-like language

Distinguishes probabilistic and nondeterministic choices in semantics

Abstract

We propose an extension of the asynchronous pi-calculus with a notion of random choice. We define an operational semantics which distinguishes between probabilistic choice, made internally by the process, and nondeterministic choice, made externally by an adversary scheduler. This distinction will allow us to reason about the probabilistic correctness of algorithms under certain schedulers. We show that in this language we can solve the electoral problem, which was proved not possible in the asynchronous $\pi$-calculus. Finally, we show an implementation of the probabilistic asynchronous pi-calculus in a Java-like language.