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.
翻译:在先前的一篇论文中,提出了一种基于ACP(通信进程代数)的进程代数,它借助源自命令式编程的特性来处理涉及数据的进程。本文提出对该进程代数进行扩展,引入概率性选择算子,其原则是概率性选择总是在涉及选择组合与并行组合的选择之前先被解析。这一扩展可用于(尤其包括)描述分布式计算领域中重要算法所表现的行为模式,并验证它们的相关性质。该领域的许多经典问题,例如领导者选举问题和共识问题,都需要使用概率性算法。