概率并发理论

与经典并发理论相比，概率并发进程的语义理论还不成熟，在形式化语义方面还有许多公开问题未被解决。其中一个基本问题是如何在特定概率模型上比较各种常见的语义如互模拟语义、测试语义和trace 语义。在本项目中我们将对这一问题进行全面探索，力图澄清一般无限状态无限分支、无限状态有限分支、有限状态无限分支、有限状态有限分支模型、以及一般完全概率模型上互模拟语义、模拟语义、测试语义、trace 语义等之间的相互关系，建立关于概率并发进程比较完整的语义理论。另外，目前在有限状态有限分支模型上对概率行为等价和前序关系的判定仅限于划分求精算法，这要求预先生成被考虑系统的整个状态空间，且只适用于等价关系的判定，在实际应用中往往表现不佳。因此，在本项目中我们考虑设计局部算法以判定行为等价和前序关系。这类算法可动态生成所需的状态空间，对等价关系和前序关系的判定均适用，且在验证否定结论时通等常效率较高而具应用前景。

随着计算机网络和通信技术的发展，对并发分布式系统的研究变得越来越重要。概率并发理论探讨如何用形式化的方法严格描述并发计算系统以期指导实际系统的规范、设计和定量的分析与验证。经过多年的努力，我们对概率并发进程语义的认识逐渐加深,已经取得阶段性的成果，具体反映在如下几个方面：（1）厘清了有限状态概率标号迁移系统上测试语义与模拟语义的联系与区别；并把有关结论扩展到其它高级的模型如概率Pi演算、加权的马尔可夫决策进程、马尔可夫自动机等；（2）引入其它形式的语义如实数值回报测试和利益测试语义，并与经典的测试语义综合比较；（3）出版英文专著《Semantics of Probabilistic Processes：An Operational Approach》,对互模拟语义从度量、逻辑、以及算法等角度进行刻画,对测试语义从模态逻辑和余归纳的角度来刻画。后者很重要因为我们得到一种语义对正面和负面结论都容易证明：为说明两个进程是行为关联的，我们用余归纳的方法；为说明两个进程不是关联的，我们只需给出一个测试进程见证这两个进程的差别；（4）我们发现利用概率互模拟的思想可以帮助理解量子进程的行为，定义量子并发程序行为等价关系，并开发算法验证程序等价；（5）对于量子高阶函数式语言，可以为线性上下文等价关系找到合适的余归纳证明方法。因此，我们从程序等价的角度初步建立了概率并发理论的基本思想、原理和证明方法，而且指出其对于研究量子程序语义的作用，这为我们将来深入研究量子程序的语义理论奠定了坚实的基础。