Probabilistic imperative process algebra

TL;DR

This paper extends an existing process algebra with probabilistic choice operators, enabling better modeling and verification of probabilistic algorithms in distributed computing.

Contribution

It introduces a probabilistic extension to an ACP-based process algebra, resolving probabilistic choices prior to other process decisions.

Findings

Supports modeling of probabilistic distributed algorithms

Facilitates verification of properties in probabilistic processes

Addresses canonical problems like leader election and consensus

Abstract

In a previous paper, a process algebra based on ACP (Algebra of Communicating Processes) was proposed in which processes involving data can be handled by means of features originating from imperative programming. In this paper, an extension of that process algebra with probabilistic choice operators is presented that rests on the principle that probabilistic choices are always resolved before choices involved in alternative composition and parallel composition are resolved. This extension can be useful, among other things, for specifying the patterns of behaviour expressed by algorithms that are important in the area of distributed computing and verifying properties about them. Many canonical problems in that area, such as the leader election problem and the consensus problem, call for a probabilistic algorithm.