概率符号Pi演算的有限公理化

摘要

随着计算机技术和网络通信技术的高速发展，以并发性、分布性、实时性、异构性和互操作性等主要特征的并发分布式系统已成为计算机技术的主流方向。并发现象以其固有的复杂性，对计算机科学家提出了挑战。与顺序计算不同，对并行与并发计算实质的认识尚处于初级阶段。 进程代数主要是用来描述并发计算的数学模型，它研究并发现象，即多个计算主体(进程)同时活动，通过交换信息(通讯)进行协作，以共同完成预期任务的特定计算现象。对于一个进程演算，通常需要研究其语法语义，而公理化系统便是理解其操作语义的一个很好的方法。 近年来，在解决并发系统问题的算法构造过程中，随机方法被证明是一种重要的工具。相对确定算法而言，随机算法可以更加有效，因为它们通常有着更加简单的结构，使用更少的内存，并且可以得到一些确定算法不能得到的好结果。 传统上，对并发系统进行建模的进程演算中，并不涉及定量分析，因此对于一个并发系统会以多大的概率发生某个动作这样的问题就无法提供有用的信息。但是从应用的角度来看，进行这样的定量分析非常必要，因为在本质上并发系统的许多方面是与随机相关的，或至少可以建模成随机行为。因此，在传统的模型中加入随机因素可以更加有效来分析并发系统。 在本文中，首先介绍一种概率进程演算，称为sp。sp是演算的一个概率扩展，在演算的基础上加入概率选择符，同时支持概率选择和不确定选择。接着，分别介绍强概率符号互模拟、弱概率符号互模拟以及概率符号同余的定义，并给出强概率符号互模拟和概率符号同余的公理化系统，最后证明公理化系统的正确性和完备性。公理化系统的正确性比较容易证明，故本文的大部分篇幅用于证明其完备性。对于强概率符号互模拟，首先证明其同余性，在此基础上给出包含推导规则、选择规则和约束规则的公理化系统。同样地，证明任意进程都可以分解为多个相对简单的子进程之和。对于弱概率符号互模拟，由于其不具有同余性，我们提出了符号观测同余，并在强概率符号互模拟的基础上加入规则，组成了其公理化系统，其完备性证明同强互模拟一样。为了处理并发算子，使用了扩展规则，使任意并发算子都能够转化为等价的不含并发算子的进程。 本文的创新点在于首次在概率选择和不确定选择同时存在的情况下，给出了概率符号互模拟的公理化系统。