有限概率pi演算的测试预检的特征

我们考虑了可能且必须测试有限pi演算的概率扩展的两个特征:一个基于概率弱模拟的概念,另一个基于Milner-Parrow-Walker模态逻辑的片段的概率扩展pi演算。 我们基于先前的概率CSP工作中使用的类似概念来建立模拟概念。 但是,与CSP(或其他不传递值的演算)不同,概率pi演算有几种可能的模拟定义,这是通过对名称量化进行范围划分的不同方式得出的。 我们表明,为了捕获测试先决条件,需要使用“最早的”仿真关系(类似于在非概率情况下的早期(bi)仿真的概念)。 两种表征中的关键思想是概率过程的“特征公式”的概念,以及公式的“特征检验”的概念。 正如Boreale和De Nicola在较早的π演算等效性测试工作中一样,我们使用不匹配算符扩展了pi演算语言,否则将无法进行特征检验。