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.