论文部分内容阅读
在过去的十几年里,大多数研究主要集中在用进程代数对系统进行功能分析,很少涉及性能评价。一般的进程代数没有考虑概率,只能描述系统的功能特性,不能对系统进行性能评价,因此有必要在进程代数的基础上增加性能评价的参数(例如概率),这就发展成了后来的概率进程代数。事件结构是一种十分重要的真并发模型,非常适合于为进程代数提供一种具有可组合性的真并发语义。然而,在利用事件结构进行概率进程代数的指称语义研究领域,相关工作还不充分。本文中,我们采用概率事件结构作为语义模型,研究了概率进程代数的度量指称语义。 概率进程代数允许每一个动作被赋予一个固定的概率,消除了进程代数中的选择操作的非确定性。为了给出概率进程代数的语义,我们采用了具有概率指标的事件结构作为语义模型,这类事件结构通过赋予内部事件一个固定的概率,便可以刻画系统的概率行为。由于直接采用概率事件结构难以刻画递归进程,因此,本文在概率事件结构上采用了一种度量的方法。度量的距离函数是基于概率事件结构达到一致的最长因果集束链的长度。然而,在概率事件结构上定义的距离函数是一个伪度量,而不是度量,伪度量难以区分某些特殊事件,为了得到度量,我们构造了概率事件结构的等价类,从而得到有限近似的概率事件结构,并证明了由有限近似的概率事件结构及度量建立的度量空间是一个完备的超度量空间。根据Banach的不动点定理,我们定义了不扩张的进程表达式在这个完备度量空间上的度量指称语义,这项研究工作对形式验证和系统优化都具有重要的理论意义和现实意义。