概率进程演算的测试语义

进程演算是描述和分析并发计算的重要模型。由De Nicola和Hennessy提出的基于may前序和must前序的测试语义为研究进程演算提供了有力的工具。概率进程演算在传统进程演算中加入概率选择操作子，以描述和分析随机分布式系统的概率行为。如何给出概率进程演算的测试语义是一个众人关心但还没有很好解决的问题。在本项目中我们将对这一问题进行全面的探索: 1.我们将建立一个一般化的测试框架并应用到具体的概率进程演算（如概率CSP）；2.我们将定义一个模态逻辑，给出may前序和must前序的模态刻画；3.我们将定义模拟和failure模拟关系，证明它们与上述两种前序关系模态刻画的一致性，以建立测试语义和模拟语义的密切关系；4.我们将试图在概率CSP中为may前序和must前序建立完备可靠的公理化系统。 5.我们还打算建立一套对应于测试语义的指称语义。