文件标题：概率倒钩同余及其在概率CCS中的应用

理论计算机科学电子笔记190（2007）185-203www.elsevier.com/locate/entcs概率倒钩同余邓宇欣a，杜文杰ba中国上海交通大学yuxindeng@sjtu.edu.cn中国上海师范大学wenjiedu@shnu.edu.cn摘要本文定义了一个概率倒钩同余，它与CCS的概率扩展中的观测等价性相一致。基于这一重合结果，我们提供了一个健全的和完整的公理化的倒钩同余在有限片段的概率CCS。保留字：概率过程演算，Barbed同余，观测等价，公理化。1介绍目前进程代数已成为并行计算推理的重要模型.为了描述进程的操作行为，通常可以定义两种类型的语义：转换语义通过基于标记的转换系统，而归约语义是通过定义适当的等价（例如倒钩互模拟）基于未标记的转换系统。归约语义更简单，但在某些情况下比转换语义更有启发性，特别是当人们想要比较两个在语法上可能相距甚远的演算时。倒钩互模拟[14]是由Milner和Sangiorgi提出的，作为一种工具来描述基于一致互模拟的等价性，可以用于许多不同的演算。 其思想是为全局观察者提供最低限度的观察操作和过程状态的能力。然而，倒钩双模拟是一个非常弱的关系，它往往不能成为一个同余。 从倒钩互模拟中导出全等的一个简单方法是要求两个进程在所有上下文中都是倒钩互相似的。这样得到的同余称为倒钩同余，它的缺点是难以使用，因为在所有上下文中都是量化的。1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.07.011186Y. 邓，W。Du/Electronic Notes in Theoretical Computer Science 190（2007）185Sangiorgi在[15，定理3.3.2]中证明了弱互模拟与CCS [13]的一个变体中的带倒钩同余一致，该变体具有保护和。这个特征化结果是重要的，因为它允许我们使用弱互模拟所提供的共归纳证明技术来建立两个过程在倒刺同余下的等价性，并且我们不再需要考虑所有上下文。本文将Sangiorgi的结果推广到概率情形。更精确地说，我们在Milner的CCS的概率扩展中定义了观测等价和倒钩同余，然后证明了这两个等价在这个概率CCS中是一致的此外，我们提供了一个健全的和完整的公理化观测等价的概率CCS的有限片段。由于上述的重合结果，倒钩同余的公理化也是合理和完备的。观测等价性已经在各种概率过程代数中进行了研究[6，7，8]。然而，[6，7，8]中观测等价的定义需要组合弱跃迁的概念[17]，它由我们熟悉的基本弱跃迁的线性组合形成在本文中，我们采用了[9]中定义的弱跃迁的概念，它是通过将状态与状态分布之间的关系提升为分布与分布之间的关系而获得的。由于[9]的弱跃迁具有内置的线性组合，因此与[17]中的弱跃迁等价。然而，前者比后者更干净，更优雅，因为它只是通过插入一些不可见的转换来从强转换构造弱转换，就像在nonprob-probable设置中一样[13]。我们不再需要像[6，7，8]那样定义复杂的弱转移虽然很容易证明观察等价包含在倒刺同余中，但相反的包含是非平凡的。我们需要建立一类足够强大的证明模式类似于[15]，但我们的上下文构造稍微简单一些，尽管我们是在概率环境中。我们的公理化的完备性证明使用了与[7]中相关证明相同的思想：我们利用一个推广引理（引理5.6）作为我们的垫脚石来证明公理化是完备的。观察等价性（定理5.7）。虽然本文比文献[6，7]考虑了更多的算子，如平行复合算子，但它们在公理化中并不困难。 例如，我们使用概率版本的扩展法律，以消除所有出现的并行组成。关于概率等价的公理化还有许多其他的相关工作[10，4，2，18，1，3]。然而，它们中的大多数都是关于公理化概率强双相似性的，所以关于弱转换的有趣而微妙的问题并没有出现。就我们所知，在关于弱等价（例如分支双模拟）的工作中，没有一个涉及倒刺同余。本文其余部分的结构如下。在第2节中，我们提出了CCS的概率版本的语法和操作语义接下来，我们定义Y. 邓，W。Du/Electronic Notes in Theoretical Computer Science 190（2007）185187iii∈Ii i1 1n ni∈1..ni in ni ii∈1.. （n−1）11n−1n−1ii∈IΣΣ˜ ˜˜Σ˜Σi∈Ii∈I观察等效性，并表明它是第3节中的一致性。我们在第4节中定义了倒钩同余，并证明了它与观测等价的一致性。我们在第5节中提供了一个健全而完整的公理化，仅限于我们的微积分的有限片段。最后，我们在第6节中结束。2概率CCS在本节中，我们给出了CCS [13]的概率扩展，允许非确定性和概率选择。它类似于[5，11]中研究的结石。我们假设一个可数的原子动作集合，A={a，b，. }。给定一个不在A中的特殊作用量τ，我们令u，v，. 在动作集上的范围，Act=A<$A <${τ}，其中A={a<$|a∈A}。P的性能等级由以下系统定义：P：：=u。 Pi|伊斯坦堡岛|P1|P2|P\A|P[f]|Cx其中A→ A和f：Act→Act是重命名函数。这里i∈IpiPi代表a概率选择算子，其中p表示正概率，即，他们满足p∈（0，1]且p=1。有时我们对概率选择的某些分支感兴趣; 在这种情况下，我们把p P写成pP.. pP或（p P）埃普山口第二个结构 P代表不确定性 选择，偶尔我们可以写i∈1. mPi作为P1+. +Pm.当m= 0时，我们将不确定性选择视为0;当m= 1时，我们将其作为P1。我们也会感谢你。0如你我们使用|以表示通常的平行组合。限制和重命名操作符与CCS中的一样：P\A的行为类似于P，只要P不执行动作a∈A;P[f]的行为类似于P，其中每个动作a∈Act都被f（a）替换。常数C有一个定义defC=（x∈）P，其中P∈P，且P的一个参数是x的集合，其中可能发生在P.直觉是Cy的行为与P一样，y代替了x。为了简单起见，有时我们应该只在参数x中放入那些应该被实例化的P在给出进程的操作语义之前，我们需要介绍一些关于概率分布的符号。集合S上的（离散）概率分布是映射Δ：S→[0，1]，其中s∈SΔ（s）= 1.给出了Δ的支集以[|： ={s ∈ S| Δ（s）> 0}。令D（S），由Δ， Θ， Φ表示所有这些分布的集合。 我们用s来表示点分布，将概率1分配给状态s，将概率0分配给所有其他状态，因此[s|={s}。如果pi≥0且Δi是某个有限指标集I中每个i的分布，则i∈Ipi·Δi是由下式给出的分布：(1)（pi·Δi）（s） =pi·Δi（s）i∈I i ∈I其中i∈I pi= 1。 我们有时会把它写成p1·Δ 1+... + pn·Δ n，当索引集合I为{1，.，n}。188Y. 邓，W。Du/Electronic Notes in Theoretical Computer Science 190（2007）185i∈I11221 2 121 2 1211⎧=联合piPi−u→Δw her e Δ（P）={pi|i∈I，Pi=P}Pi−u→Δi∈IPi−u→ΔP−u→Δ对于某些i∈IP−u→ΔP|P−u→Δ|PP|P−u→P|ΔP1−a→Δ1P2−a<$→Δ2P1−a→<$Δ1P2−a→Δ2P1|P2−τ→ Δ 1|Δ 2P−u→Δ1u/∈A<$AP\A−u→Δ\AP1|P2−τ→ Δ 1|Δ 2P−v→Δ1f（v）=uP[f]−u→Δ[f]定义用户C=（x<$）P P{y<$/x<$}−→ΔCy−u→Δ表1操作语义对进程的某些操作可以直接扩展到进程的分布。设Δ1， Δ2是过程上的两个分布。我们定义Δ 1|Δ 2、Δ 1\A和Δ 1 [f]作为以下分布。（Δ1|Δ2）（P）d=ef⎩（Δ1\A）（P）d=ef⎩Δ 1（P1）·Δ 2（P2），如果P = P1|P20否则Δ1（PJ），如果P=PJ\A0否则（Δ1[f]）（P）defΔ1（PJ），如果P=PJ[f]0.00否则进程P的操作语义被定义为一个简单的概率自动机[16]，其状态是从P可到达的进程和转移关系由Tab1中的规则定义，其中P−u→Δdecrib是一个条件，Y. 邓，W。Du/Electronic Notes in Theoretical Computer Science 190（2007）185189通过执行动作u，离开P并导致分布Δ∈ D（P）。 规则的含义应该是不言自明的。概率和非确定性的选择在概率CCS的存在，使我们能够指定系统，具有概率和非确定性的行为。190Y. 邓，W。Du/Electronic Notes in Theoretical Computer Science 190（2007）185ΣΣΣ3观测等价性在概率环境中，由于从过程到分布的转换，类似互模拟的等价的定义有些复杂（参见例如，[12]）。因此，我们需要将过程之间的关系推广到分布之间的受[9]的启发，我们开发了下面的数学机制来做到这一点。设R P × P是过程与过程之间的关系我们把它提升到一个关系R <$D（P）× D（P），只要(i) Δ=i∈Ipi·Pi，其中I是有限的i和e x set，并且i∈Ipi=1(ii) 对于每个i∈I，存在一个过程Qi，使得PiRQi(iii) Θ=θi∈Ipi·Qi。这里重要的一点是，在Δ到i∈Ipi·Pi的分解（i）中，过程Pi不一定是不同的：也就是说，分解不是一般的独特.提升结构满足以下有用特性。引理3.1（i）如果R1<$R2，则R1<$R2（ii）如果R是传递关系，则R也是传递关系。Q证据 见附录aQ下面的命题继承自[9]的命题6.1支持3. 2Suppos e RP×Pand di∈Ipi=1. 现在我们有了(i) ΘiRΔiimplies（θi∈Ipi·Θi）R（θi∈Ipi·Δi）.(ii) 如果（i∈Ipi·Θi）RΔ，则对于某个分布集Δi，Δ =i∈Ipi·Δi，使得ΘiR Δi。QWewri eP−τ→τΔifei thrP−τ→Δo r Δ=P。We writ eP−u→ΔforP−u→Δifuτ。 为了定义弱转移，我们需要考虑转移序列，所以我们以这样一种方式概括过渡，即它们从分布到分布。LetΔ−u→εΘ无论何时(i) Δ=i∈Ipi·Pi，其中I是有限的i和e x set，并且i∈Ipi=1(ii) 对于achi∈I，heeisadist tributionΘisuchatPi−u→u Θi(iii) Θ=θi∈Ipi·Θ i。弱转换是以标准的方式定义的，除了它们现在适用于to dis tributions，andd−τ→isusedinsteadoff−τ→. 这意味着它的使用虽然分布可以在执行可见动作之前或之后执行一系列不可见移动，但是分布的不同部分可以执行不同数量的内部动作。•τˆτˆ∗设Δ1 = Δ2，只要Δ1（−→）Δ2。Y. 邓，W。Du/Electronic Notes in Theoretical Computer Science 190（2007）185191⇒⇒=•乌托乌托令Δ1 = Δ2表示Δ1 =Δ −→= Δ2。如果uuuΔ。=τ我们也写Δ1 = Δ2，因为Δ1 =2定义3.3等价关系R P × P是（弱）互模拟，如果PRQ和P−u→ΔimpliesQ=0使得Δ R Θ。两个过程P和Q是双相似的，记为PwQ，如果存在一个双相似过程，LationR s.t. PRQ。为了证明互模拟是最大的互模拟，我们需要建立互模拟的一些性质。引理3.4假设i∈Ipi =1andΔi=1对于每个i∈I，Φi，其中I是有限的我的意思是， （Relthati∈Ipi·Δi是对I的简单定义。）Thenpi·ΔiuΦii∈IQ证据 我们首先证明了u = τ的情况。对于每个i∈I，有一个数ki使得Δi= Δi0−τ→τΔi1−τ→τΔi2−τ→τ·· ·−τ→ˆΔ iki= Φ i。设k= max {ki|i∈I}，使用我知道了。Sincew ehav eΦ−τ→τ对于任何Φ∈ D（P），我们可以添加伪转换到这些序列，直到所有ki等于k。在准备之后，引理接着是k个提升转换的应用。现在，情况ui=τ之后是提升转换的另一个应用，−u→，通过一个假设u=τ的过程，可以得到并满足以下条件。Q引理3.5设R是互模拟。假设ΔR Φ和Δ−u→ΔJ。ThenuΦ=Φ 对于一些ΦJ使得ΔJRΦ J。证据第一个Δ R Φ意味着，(2)Δ =Δpi·Pi，PiRRi，Φ =Δpi·Ri;alsoΔ−u→ΔJmeansi∈Ii∈I(3)Δ=qj·Qj，Qj−u→Θj，ΔJ=qj·Θj，j∈J j ∈J我们可以像现在这样。L. O. G. 这意味着所有的代码都是空的，q是零。Nowdefn eIj={i∈I|Pi= Qj}和Ji={j∈J|Qj= Pi}，因此，(4)并注意到（5）uuJ192Y. 邓，W。Du/Electronic Notes in Theoretical Computer Science 190（2007）185{（i，j）|i∈I，j ∈ Ji}={（i，j）|j∈J，i ∈Ij}Δ（Pi）=qjanddΔ（Qj）=pij∈Jii ∈IjY. 邓，W。Du/Electronic Notes in Theoretical Computer Science 190（2007）185193jΔ（Qj） ·Θ⇒⇒一期+1Φ = Φ=j∈JiΔ（Pi）·ΦijΔ，则Φ =Δ，则Φ =因为（5）我们有Φ=i∈Ipi·Ri=i∈Ipi·j∈JqjiΔ（Pi）pi·qj·R现在对于Ji中的每个j，我们知道实际上Qj=Pi，因此从中间部分我的 天(2) （3）得到Ri=<$ Φij，使得ΘjR Φij.引理3.4得出乌鲁杰罗i∈Ipi·qjJ其中，在求和Pi=Qj内，因此，使用（4），ΦJ也可以写为（六）ΣΣpi·qj·ΦJj∈Ji∈Ij Δ（Qj）ij下面我们展示了ΔJR ΦJ，我们通过操纵ΔJ来实现，使得它具有与（6）中类似的形式：ΔJ=j∈Jqj·Θj=j∈Jqj·i∈Ipi ·Θj再次使用（5）=j∈Jpi·qji∈IjΔ（Qj） j将其与上面的（6）进行比较，我们可以看到所需的结果ΔJR ΦJ如下：根据命题3.2（i）的应用。Q引理3.6设R是互模拟。 假设ΔRΦndΔ=φΔJ。然后uΦ=Φ 对于一些ΦJ使得ΔJRΦ J。证据首先，我们考虑两个主张(i) IfΔRΦanddΔ−τ→πJτ⇒ˆ对于某个ΦJ，使得ΔR ΦJ(ii) 如果ΔRτ⇒ˆJτ⇒ˆ使得ΔJR ΦJ。权利要求（i）的证明与引理3.5的证明类似。（二）主张主张τˆ(i)通过归纳得出=的导数的长度。通过合并权利要求（二），利用引理3.5，我们得到了所需的结果。Q引理3.7设R =i{ Ri|Ri是互模拟}。那么R的等价闭包，记为R，是互模拟。证据如果PRQ，则存在一些互模拟R0，...，Rn−1和一些过程P0，...，Pn使得P = P0，Q = Pn，并且对于所有i，0 ≤ i0ifu∈A<$Ai∈I我我你好p（P\A），否则R2（ni∈IPi）\A=ni∈IPi\Ai∈I 我我N1（u.i∈IpiPi）[f] = f（u）. i∈IpiPi[f]N2（i∈IPi）[f]=i∈IPi[f]Ci∈1.. nu。 jpijPij=i∈1.. nu。 jpijPij+u. i∈1.. njripijw i thi∈1.. nri=1。E假设Pi ui.jpijPij和Qkvk。 lqklQkl.然后推断：P|Q = Qiui。jpij（Pij|Q）+Kvk。lqkl（P|Qkl）+ uiopp vkτ. j，l（pijqkl）（Pij|Qkl）其中uiopp vk表示ui和vk是互补动作，即，u′i=vk。表2公理系统AY. 邓，W。Du/Electronic Notes in Theoretical Computer Science 190（2007）185203uI I I I I II III III IIII I III我我引理5.5（饱和）如果P是正规形式，且P{Pi}i∈i且Δ（Pi）= pi则A ∈P = P + u.I piPi.= Δ与[Δ|为证据通过跃迁诱导。 我们严重依赖概率τ定律T1-3和公理C.详情见附录B。Q完备性的证明是通过对规范型P的深度d（P）的归纳建立的。其深度定义为：d（0）= 0d（u. ipiPi）= 1 +max{Pi}id（Pi）=max{d（Pi）}与[7]一样，我们证明了一个推广引理，并将其作为建立A的完备性的垫脚石。引理5.6（推广）如果P ≠wQ，则A ≠ τ.P = τ.Q。证据根据引理5.4，我们假设P和Q是正规形式。证明是通过归纳d=d（P）+d（Q）。我们考虑d>0的非平凡情形。让你。j∈J 是P的任何被加数。然后我们有P−u→Δ，其中hΔ=j∈Jrj·Rj。自P-2000年以来，uQ，存在θ使得Q=Θ和Δθw Θ。因此，我们认为，(10)Δ= φpi·Pi，Pi≠wQi，Θ = φpi·Qi.i∈I i ∈I从归纳假设出发， 可得出：A τ.Pi= τ. 所以我们可以用T3来推导出A u。p P=u。p τ.P= u.p τ.Q= u.p Q。以来Rj=Δ=∑i∈Ipi·Pi，i从S5开始向下流动，其中A为零。j∈JrjRj=联合我我我我们从Lemma5知道。5thatAτ。Q=pP. 现在观察到τ.Q=τ.Q + u。 i∈IpiQi= τ.Q + u. j∈JrjRj.综上所述，A τ.Q=τ.Q+P。对称地A <$τ.P=τ.P+Q。因此，我们建议，A τ.P=τ.Q乘T4。Q定理5.7（完备性）如果PwQ，则A <$P = Q。证据 这个证明与引理5.6类似。让你。j∈J 是P的任何被加数。然后我们有Pu−u→Δ，其中hΔ=j∈Jrj·Rj。由于Pw存在Θ使得Q = θ和Δ θwΘ。因此，我们认为，(11)Δ= φpi·Pi，Pi≠wQi，Θ = φpi·Qi.i∈I i ∈I由推广引理可得：A_τ.Pi=τ.所以我们可以用T3来推导出A u。p P=u。p τ.P= u.p τ.Q= u.p Q。以来Rj=Δ=∑i∈Ipi·Pi，i从S5开始向下流动，其中A为零。j∈JrjRj=⇒204Y. 邓，W。Du/Electronic Notes in Theoretical Computer Science 190（2007）185联合我我我我们从Lemma5知道。5thatAQ=pP.现在观察Q=Q + u。i∈IpiQi= Q + u. j∈JrjRj.简而言之，AQ=Q+P。 对称的AP=P+Q。 因此，我们建议，AP = Q。Q推论5.8 PbQiAP = Q。证据 定理4.4，5.2和5.7的直接结果。Q6总结发言本文提出了一个概率倒钩同余，并证明了它与CCS的概率扩张中的观测等价性是一致的对于有限过程，我们给出了一个完备的公理系统w.r.t. 倒钩同余在将来，在其他概率过程演算中建立类似的结果将是有趣的。在[15]中证明了在π-演算中倒钩同余与早期的互模拟同余一致。我们认为有可能将这个结果推广到概率π演算。引用[1] L. Aceto，Z. 是的，还有A。 我会把她赶走的。 E quuati onalaxi omsforpr obbilis ticbisimil a ri ty（prelimin ary报告）。技术报告RS-02-6，金砖国家，2002年。[2] S. 安多瓦概率进程代数博士论文，埃因霍温理工大学，2002年。[3] S. Andova，J. C. M. Baeten和T. A. C.威姆斯概率系统分支互模拟的完全公理化及其在协议验证中的应用 。 在 Proceedings of the 17th International Conference on Concurrency Theory ， Volume 4137ofLecture Notes in Computer Science，pages 327施普林格，2006年。[4] J. C. M. Baeten，J. A. Bergstra和S. A.斯莫尔卡公理化概率过程：具有生成概率的ACP。信息与计算，121（2）：234[5] C. Baier和M. Z.夸特科瓦斯卡概率过程的域方程。Mathematical Structures in Computer Science，10（6）：665[6] E. Bandini和R.塞加拉概率互模拟的公理化。第28届自动机、语言和编程国际学术讨论会论文集，讲义第2076卷计算机科学，第370-381页。Springer，2001年。[7] Y. Deng和C. Palamidessi。概率 有限状态行为的公理 化。Theoretical Computer Science，373（1-2）：92[8] Y. 登角，澳-地Palamidessi和J.庞概率有限状态行为的组合推理在过程中，术语和周期：迈向无限之路的步骤，献给Jan Willem Klop的文章，计算机科学讲义卷3838，第309-337页施普林格，2005年。[9] Y.登河，巴西-地van Glabbeek，M.亨尼西角Morgan和C.张某关于检验概率过程的注记。电子笔记理论计算机科学，172：359[10] A. Giacalone ， C.-C. Jou 和 S.A. 斯 莫 尔 卡 概 率 并 发 系 统 的 代 数 推 理 IFIP WG 2.2/2.3 WorkingConference on Programming Concepts and Methods，第453-459页，