概率扩展的非概率过程的测试公理化

理论计算机科学电子笔记172（2007）359-397www.elsevier.com/locate/entcs关于检验概率过程的邓宇昕B，1Rob vanGlabbeekA，BMatthew HennessyC，A，2Carroll MorganB，1 Chenyi ZhangA，BANational ICT Australia，Locked Bag 6016，Sydney，NSW 1466，Australia澳大利亚悉尼新南威尔士大学计算机科学与工程学院C信息学系，萨塞克斯大学，Falmer，Brighton，BN 1 9QN，英国摘要我们开发了一个一般的测试方案的概率过程，产生了两个理论：概率可能测试和概率必须测试。这些都适用于一个简单的概率版本的过程演算CSP。我们研究的代数理论的概率测试，并表明，许多公理的标准测试不再是有效的，在我们的概率设置，即使是非概率CSP过程中，概率测试的区分能力是远远大于标准测试。 我们开发了一种方法，推导出有效的概率可能测试的基础上的概率扩展的概念模拟不等式。利用这一点，我们得到一个完整的公理化的非概率过程的概率可能测试。关键词：概率过程，不确定性，CSP，变迁系统，测试等价，模拟，完全公理化，结构操作语义1介绍操作语义学在计算机科学中发挥了有益的作用，因为这个主题的诞生[32，15，38，6]。但是随着[47]的出版（重新出版为[48]），人们意识到，结构合理的操作语义为指定编程语言的语义提供了一种优雅的组合方法由于它的数学基础，结构操作语义学也可以用来推理程序的行为属性，甚至在某种程度上，它也会对指称语义的必要性提出质疑操作语义的力量在进程演算的发展中最为明显：CCS [39]的语义理论，互模拟等价，完全建立在操作语义的基础上。提供了有力1 我们感谢澳大利亚研究委员会（ARC）资助DP034557的支持。2这项研究是在皇家学会/Leverhulme Trust高级研究奖学金期间进行的。1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.02.013360Y. Deng等人理论计算机科学电子笔记172（2007）359用于建立过程等价的共归纳证明方法;它还支持组合和代数推理技术。对于CSP [22]，情况有些不同：故障模型[5]是定义性的，并用于证明代数定律的合理性，这些定律是CSP作为过程规范语言的后续发展的特征然而，后来很明显，就像CCS一样，这个模型及其代数理论可以使用基于过程测试概念的纯操作概念来完全证明[45，12]。因此，有了CSP，我们就拥有了所有可能的世界中最好• 一个指称模型，• 一种运作模式，• 代数理论，所有这些在某种意义上都是等价的。本文的主题是概率过程演算。标准过程演算的各种语义方法本质上是非确定性过程的理论，其中非确定性表示可以以完全不可预测的方式重新解决的可能选择。有了概率结构，解决方案在某种程度上是可以预测的，因为它是量化的;但是量化的和非量化的选择形式之间的相互作用需要密切关注。问题主要在于两种选择形式不同，而不是一种被量化，另一种没有：例如，当考虑恶魔和天使的选择时，会发生类似的结果因为它们的分布不同，所以有必要仔细考虑它们发生的顺序，以及它们如何相互分布。第一篇关于概率过程演算的论文[16，9，36]是用概率选择代替非确定性和概率选择的调和始于[21]，在文献[25，58，24，53，33，34，51，43，49，7，29，54]中受到了很多关注，甚至在序列世界[23，42]中，以及最近在一般语义领域[41，40，44，55，57]中;因此可以说这是该领域的中心问题之一。CSP使这个问题变得更加有趣，因为它已经有了两种选择形式（内部和外部），所以概率选择成为第三种。本文的重点是代数理论的发展以下[58]我们将测试[12]的原始思想应用于概率过程，得出过程之间的两个精化关系，概率可能预定和概率必须预定。例如，P±p可以Q意味着Q可能通过测试的概率至少与P可能通过然后，我们将这个概率测试的一般框架应用于简单的有限概率进程代数pCSP，pCSP是通过向CSP的简化版本添加概率选择运算符而获得的。为了做到这一点，我们首先需要将pCSP解释为概率标记转移系统[30，21，51]，这是众所周知的标记转移系统概念的推广，它描述了进程可能与其用户的交互。有了这些概括，事实证明，很少有吸引人的代数Y. Deng等人理论计算机科学电子笔记172（2007）359361芬芬CSP代数理论的基本定律，以及它的指称模型，在概率选择的情况下仍然有效;这可以通过一系列反例来证明，这些反例由区分过程表达式的测试组成。本文的主要结果是发展的方法证明积极的代数恒等式。我们发展了概率过程模拟的概念，写作P±SQ表示过程Q可以模拟P的行为。接下来我们将展示• 模拟关系±S由pCSP• 所述模拟关系被包括在所述概率性可预排序中：P±SQ意味着P±p可以Q。这使我们能够发展一个代数理论的概率可能测试，我们简要概述。模拟的概念也可以通过引入失败的概念来适应，以获得概率必须预排序的类似结果;但为了保持论文简洁，省略了细节。然而，我们确实表明，正如预期的那样，基于必须检验的理论比基于可能检验的理论更具区分性;具体地说，P±p必须Q蕴涵Q±p可能P。在最后一节中，我们使用概率测试重新检查标准（非概率）CSP的行为我们表明，这些是在一般情况下更歧视，比非概率测试，我们给出了一个完整的方程表征所产生的可能理论。虽然本文在pCSP方面发展了一个概率测试的代数理论，但我们可以使用CCS或ACP的概率版本获得类似的结果，因为这些演算中定义的过程可以同样解释。2测试过程很自然地认为进程的语义是由它们通过测试的能力决定的[12，20，5，58，52];进程P1和P2被认为是语义等价的，除非有一个测试可以区分它们。实际使用的测试通常代表用户或其他进程与Pi交互的方式。让我们首先建立一个通用的测试场景，在其中可以制定这个想法。它假定• 一组过程Proc• 一组测试T，可以应用于过程• 一组结果O，将测试应用于过程的可能结果• 一个函数Apply：T × Proc→P+（O），表示将特定检验应用于特定过程的可能结果。这里P+（O）表示O的有限个非空子集的集合;因此将测试T应用于过程P的结果Apply（T，P）通常是一组结果，表示过程的行为，实际上测试，可能是不确定的。一个更一般的理论将允许Apply（T，P）是任意的362Y. Deng等人理论计算机科学电子笔记172（2007）359芬O的非空子集，但对于我们在本文中考虑的有限过程类，结果的有限集合是足够的。此外，有些结果被认为比其他结果更好;例如，测试的应用可能只是成功，也可能失败，成功总比失败好。 所以我们可以假设O被赋予一个偏序，其中o1≤o2意味着o2是比o1更好的结果。当比较对进程应用测试的结果时，我们需要比较O.有两种标准的方法来进行这种比较，基于将这些集合视为O的Hoare或Smyth幂域的元素[19，3]。对于O1，O2∈P+（O），我们令(i)O1±HoO2，如果对每个o1∈O1，存在某个o2∈O2，使得o1≤o2(ii) O1±SmO2，如果对任意的o2∈O2，存在某个o1∈O1，使得o1≤o2.使用这两种比较方法，我们得到两个不同的语义前序过程：(i) 设P，Q∈P_（？）(ii) 类似地，设P±必Q，如果对每个检验T，Apply（T，P）±SmApply（T，Q）。我们用PmayQ和PmustQ来表示相关的等价。该术语可以并且必须指以下相同的重新表述主意.令Pass<$O是O的向上闭子集，即满足oJ≥o∈Pass<$oJ∈Pass，被认为是可以被视为通过测试的结果的集合。然后我们说，一个进程P可以通过一个测试T，其结果用Pass表示，“现在P±可能Q i <$$>T∈T <$Pass∈P↑（O）（PmayPassT Q可能通过T）P±mustQi <$T∈T <$Pass∈P↑（O）（PmustPassT<$QmustPassT）其中P↑（O）是O的向上闭子集的集合。原始的测试理论[12，20]是通过使用作为结果集而获得的O两点晶格不⊥其中T表示测试应用的成功，而T表示失败。然而，对于概率过程，我们考虑将测试应用于以给定概率成功的过程。因此，我们把单位区间[0， 1]作为结果的集合，并按照标准的数学排序;如果0≤p q≤ 1，那么以概率q成功被认为比以概率p成功更好。这就产生了概率过程的两个前序，为了方便起见，我们将它们分别命名为±pmay和±pmust，并分别对应pmay和pmust这些前序及其相关等价物首先被定义为Y. Deng等人理论计算机科学电子笔记172（2007）359363芬[58]王和拉森。目前的文件的目的是将它们应用到一个简单的概率进程代数。在这样做之前，让我们先指出一个有用的简化：[0，1]的有限子集（更一般地说，[0，1]的闭子集）上的Hoare和Smyth前序分别由它们的最大和最小元素确定。命题2.1对于O1，O2∈P+（Oprob），我们有(i) O1±HoO2当且仅当max（O1）≤max（O2）(ii) O1±SmO2当且仅当min（O1）≤min（O2）.证据简 单 的计算。Q与非概率情形一样，我们也可以定义一个组合了may-must-preorder的测试预序;我们在这里不研究这种组合3有限概率CSP我们首先定义语言及其操作语义。然后，我们展示了如何一般的概率测试理论刚刚概述可以应用到这个语言的过程。3.1语言设Act是一组动作，由a，b，c，. . ，哪些进程可以执行。然后，有限概率CSP过程由以下语法给出P：：= 0| a.P | P H P | P Q P |一个P|A P | P p⊕ P各种结构的直观含义很简单：(i) 0表示已停止的进程。(ii) a.P，其中a在Act中，是一个过程，它首先执行动作a，然后作为P继续进行。(iii) PHQ是进程P和Q之间的内部选择;它将像P或像Q一样工作，但用户无法确定是哪个。(iv) PQQ是P和Q之间的外部选择;同样，它的行为要么像P或者类似于Q，但是在这种情况下，根据用户的需求(v) P|AQ，其中A是Act的子集，表示进程P和Q正在运行 并联它们可以通过同时执行来自A的相同动作来同步;这样的同步导致内部动作τ/∈Act。此外，P和Q可以独立地进行来自（Act\A）{τ}的任何动作。(vi) Pp<$Q，其中p是一个任意概率，一个严格介于0和1之间的实数，是P和Q之间的概率选择。在概率为p时，它将像P一样行动，在概率为（1-p）时，它将像Q一样行动。364Y. Deng等人理论计算机科学电子笔记172（2007）359我们使用pCSP表示由该语法定义的术语集，CSP表示不使用概率选择的子集当然，CSP语言在其所有的荣耀[5，22，45]中有更多的运算符;我们只是选择了一个代表性的选择，添加概率选择以获得CSP的基本概率版本 我们的并行操作符不是CSP原语，但它可以很容易地用CSP连续性来表示，特别是P|AQ =（P <$AQ）\A，其中<$A和\A是[ 45 ]的并行复合和隐藏算子。它也可以用CCS的并行组合、重命名和限制操作来表示我们之所以选择这个（非结合）算子，是因为它便于定义检验在过程中的应用。像往常一样，我们倾向于忽略0的出现;操作前缀运算符a。绑定比任何二元运算符都强，二元运算符之间的优先级将通过括号或空格表示我们有时也会使用n元二进制运算符的版本，例如i∈Ipi Pi，Σi∈Ipi= 1，且i∈I Pi.3.2pCSP的操作语义上述对各种操作符的直观理解可以通过操作语义来形式化，该操作语义将每个过程项与表示其可以对用户请求作出反应的方式的图形状结构相关联。让我们简要回顾一下（非概率）CSP的这个过程。定义3.1标号跃迁系统（LTS）是一个三重S，Actτ，→ π，其中(i) S是一组状态(ii) Actτ是一组动作Act，增加了一个新的动作符号τ来表示同步，更一般地说，是内部不可观察的活动(iii) →S×Actτ×S表示执行动作的效果。它通常是使用更简单的方法，而不是在s−α→sj中保持f（s，α，SJ）∈→。CSP的操作语义通过赋予术语集LTS的结构来获得。具体而言，(i) 状态集合S被认为是来自语言CSP的所有项(ii) P−α→Q的关系式在这些方程的x中是独立定义的。在[45]中可以找到一个精确的定义为了在操作上解释完整的pCSP，我们需要概括LTS的概念，以考虑概率。首先，我们需要一些概率分布的符号。 在集合S上的（离散）概率分布是Σ一个映射Δ：S→[0，1]，其中s∈SΔ（s）= 1.Δ的支持度由下式给出：[Δ|：={s∈S| Δ（s）>0}。对于我们的简单设置，我们只需要分布-具有有限支集的分布;令D（S），在其上的范围为Δ， Θ， Φ，表示S上所有此类分布的集合。我们用s表示点分布，满足.1如果t=s，s（t）=0否则Y. Deng等人理论计算机科学电子笔记172（2007）359365Σ而如果pi≥0且Δi是每个i在某个有限指标集I中的分布，则i∈Ipi·Δi由下式给出：Σ（i∈Ipi·Δi）（s）=Σi∈Ipi·Δi（s）Σ如果i∈Ipi= 1，那么很容易看出这是D（S）中的分布，我们将有时写为p1·Δ 1 +. +p n·Δ n，当索引集合I为{1，.，n}。我们现在可以给出LTS的概率概括：定义3.2概率标记转移系统（pLTS）是一个三元组S，行为τ，→ τ，其中(i) S是一组状态(ii) Actτ是一组动作Act，被一个新动作τ增强，如上所述(iii) → ⊆ S×Actτ× D（S）。与hLTSs一起，我们所有的 y都是−→αΔ代替（s，α，Δ）∈ →。 LTS可以是被视为退化pLTS，其中仅使用点分布。现在，我们通过关联以下内容，将CSP的操作解释模拟为LTS：pCSP是一个特定的pLTS，p，Actτ，→ π。 然而，有两个主要的差异：(i) 只有pCSP中的项的子集将被用作pLTS中的状态集Sp(ii) pCSP中的项将被解释为Sp上的分布，而不是Sp的元素。首先，我们定义我们用途：使用的状态子集Sp：它是满足(i) 0 ∈Sp(ii) a.P∈Sp(iii) PH Q∈ Sp(iv) s1，s2∈Sp蕴涵s1Qs2∈Sp(v)s1，s2∈Sp蕴涵s1|As2∈Sp.因此，Sp是pCSP表达式的集合，其中概率选择算子p的每次出现都是弱保护的，即在a.P或PHQ形式的子表达式内。将pCSP中的项解释为D（Sp）中的分布如下：（一）0 =零（二）a.P = a.P（三）PHQ = PH Q（四）Pp<$Q =p· P +（1−p）· Q（v） PQQ =P Q Q(vi) P|AQ = P |阿 Q 。在最后两种情况下，我们利用了Q和|A可以看366Y. Deng等人理论计算机科学电子笔记172（2007）359（AcTION）a. P−→aP（整数）（一）PHQ−→τP（电话分机：I.（一）s1−→τΔ（整数）R）的PHQ−→τQ（电话分机：I. R）的s2−→τΔs1Qs2−→τ（电话分机：（一）ΔQs2s1Qs2−→τ（电话分机：R）的s1QΔs1−→aΔs2−→aΔs1Qs2−→aΔ（第二段）（一）s1−α→Δs1Qs2−→aΔ（第二段）R）的s2−α→ΔS1|As2−→αΔ|As2α/∈AS1|As2−α→s1|一α/∈AΔ（第二段）（一）s1−→aΔ1，s2−→aΔ2s1Qs2 −→τΔ 1|AΔ 2a∈AFig. 1. pCSP的操作语义。 这里a的范围超过Act，α的范围超过Actτ。作为Sp上的二元运算符，因此可以以标准方式提升到D（Sp）。即我们定义（Δ1 QΔ2）（s）=.Δ1（t1）·Δ2（t2）如果s=t1Qt2，0否则Δ 1|AΔ 2类似地给出;注意，作为结果，我们有 P = P，对所有P∈ Sp。在图1中给出了所有由s-α→确定的定义。该规则与用于将CSP解释为LTS的标准规则类似[45]，修改后考虑到动作的结果必须是分布。 例如，（INT. L）和（INT. R）说PHQ做出了一个内在的不可观察的选择，要么像P，要么像Q。 同样，四个 规则（EXT. 1）、（电话分机：R）、（EXT. I. L）和（EXT. I. R）可以可以理解为对外部选择操作符给出了标准解释：进程PQQ可以执行其组件P和Q的任何外部操作，这解决了选择;它也可以执行它们的任何内部操作，但是当这些组件选择没有解决。3.3概率选择的优先性我们的操作语义需要Q和|概率选择上的分布：PQ（Qp<$R） = （PQQ）p<$（P Q R）Y. Deng等人理论计算机科学电子笔记172（2007）359367P|A（Qp<$R） = （P|AQ）p（P|A/RES/2004/10/Add.1368Y. Deng等人理论计算机科学电子笔记172（2007）359∅∅在6.5节中，这些恒等式将作为may检验的公理返回。然而，这并不是我们测试方法的结果：它是我们将pCSP表达式解释为分布的硬连线。我们可以通过引入pCSP作为一种双排序语言来获得相同的结果，由语法P：：= S | Pp PS：：= 0| a.P | PHP | 公司简介 |AS|A S并引入了像PQ（Q p<$R）和P|A（Q p<$R）作为语法上正确的表达式的句法糖，|A超过P。在这种情况下，S-表达式将构成pCSP的pLTS中的状态集Sp，并且 对于任何s∈ Sp，s = s。我们的操作语义的一个结果是，在进程a中。（b 1至c）|D2动作D可以在A之前或在概率选择B之后被调度在B和C之间-但是它不能被调度在A之后和这个概率选择之前。我们证明了这一点，因为我们认为Pp≠Q不是一个以做出概率选择开始的过程，而是一个刚刚做出这样一个选择的过程，并且概率p不大于也不小于过程P。因此，a. （Pp<$Q）是一个过程，在进行a步骤时，在备选目标P和Q之间进行概率选择。该设计决策与以前的工作完全一致，具有非确定性，概率选择和并行组合[21，58，51]。此外，进程P和Q之间的概率选择不优先于并行调度的动作，可以简单地写为τ。（PpQ）。这里τ.P是PHP的缩写。使用图1中H的操作语义，τ.P是一个在某些情况下，存在解决方案。P−→τP，所以τ。（PpQ）是一个过程，从概率选择开始，模拟为一个内部行为，概率为p的过程为P。与τ并行安排的任何活动。（PpQ）现在可以在此内部操作之前或之后进行调度，因此可以在做出选择。 特别地，a. （b1至c）| d允许d在a2和概率选择。3.4pCSP工艺的图形表示我们通过将上面定义的pLTS的可从 P 到达的部分绘制为有限无环有向图来图形化地描述pCSP表达式P的操作语义。 考虑到在pLTS中从状态到分布的转换，我们需要引入额外的边来将分布连接回状态，从而获得二分图。状态由形式为·的节点表 示 ， 分 布 由 形 式 为 的 节 点 表 示 。 对 于 任 意 的 状 态 s 和 分 布 Δ ， 当s−α→Δwedranedefroms to Δ，labelledwit h α。接下来，离开节点的数据都标记有来自Actτ的动作。 对于任意分布Δ和[ Δ]中的状态s，|，Δ的支撑，我们画出从Δ到s的边，标记为Δ（s）。因此，离开一个节点的边被标记为和为1的正实数。 因为对于我们的简单语言，所得到的有向二部图是非循环的，所以我们省略了边上的箭头，并假设控制权是Y. Deng等人理论计算机科学电子笔记172（2007）3593691ττBττB2222紧张; 到1个dD1紧张; 到C1 1C1 1i) D. ii）b. 0Hc. 0一iii) （bHc）Q（d1a）iv）a1（（bHc）Q（d1a））2 3 2图二. 示例pLTS从上到下图2中描述了几个示例。 我们发现 D。0 作为点分布d。0，用一个从根到状态d的边的树表示，用概率1标记。0的情况。反过来，这个状态被表示为具有一个向外边缘的子树，由唯一可能的动作d标记为0 。最后，这也是一个点分布，表示为一个子树，其中一条边通向一个叶子，标记为概率1。这些标记为概率1的边出现得如此频繁，以至于忽略它们以及表示点分布的相关节点是有意义的。在这个D 。0 是一个简单的树，其中一条边由动作d标记。同样的约定大大简化了ii）中bHc的表示，导致LTS详细描述了两个动作之间的内部选择。通常，这个图的端点应该合并，因为它们都代表进程0。然而，为了清晰起见，在图形表示中，我们经常将底层图展开为树，从而多次表示相同的对（bHc）Q（d1a）的解释更有趣.这就需要上面的定义中的条款（v），从而得到分布（bHc）QΔ，其中Δ是由（d1a）的解释产生的分布，本身是两点分布映射两个状态d. 0和a。0的概率为1。结果再次是两点分布，这次将两个状态（bHc）Qd和（bHc）Qa映射到1。通过使用图1中的规则进一步解释这两个状态，可以获得iii）中的最终结果。最后，在iv）中，我们显示了图形1212τBDDτττCDB一一C一131313ττττBD ad c d b a c a370Y. Deng等人理论计算机科学电子笔记172（2007）359ττ（a.ω 1 <$（b Q c.ω））|Act（b Q c Q d）41434a.ω |Act（bQc Q d）（bQc.ω）|Act（bQcQ d）ττ0 |第0幕ω |第0幕ω0 |第0幕应用（（a.ω1<$（bQc.ω）），（bQcQd））=1·{0}+3·{0，1} ={0，3}44 4 4图三. 测试示例当该项与简单过程a概率性地组合时产生的表示。0的情况。总而言之，操作语义赋予pCSP pLTS的结构，函数将pCSP中的过程项解释为pLTS中的分布，这些分布可以用有限的无环有向图（通常画成树）表示，边用概率或动作标记，因此，用动作和概率标记的边交替（尽管在图片中我们可能会抑制1标记的边和点分布）。3.5测试pCSP工艺现在让我们把第2节的测试理论应用到pCSP。 与标准理论[12，20]一样，我们使用来自pCSP本身的任何过程作为测试，此外还可以使用特殊符号ω来报告成功。例如，a.ω1<$（bQc.ω）4是一个概率测试，25%的时间请求一个动作，75%的时间请求一个动作。C可以执行。如果它被用作必须测试，要求c动作的75%额外要求b是不可能的。 正如在[12，20]中，不是ω的执行构成成功，而是到达ω是可能的状态。ω-action的引入只是一种定义状态上的成功谓词的方法，而不必用这种谓词显式地丰富过程的语言。形式上，令ω/∈Actτ，并将Actω写成Actτ {ω}，将Actω写成Actτ {τ，ω}。在图1中，我们现在让a在Actω上，α在Actω上。测试可能有子项ω.P，但其他过程可能没有。 为了将测试T应用于流程P，我们并行地、紧密同步地运行它们;也就是说，我们运行组合的流程T|第P幕在这里，P只能与T同步，而测试T除了与被测试的过程同步之外，也只能执行成功动作ω;当然，测试者和被测试者都可以执行内部动作。中提供了一个示例图3，其中测试a.ω1<$（bQc.ω）应用于过程bQcQd。 我们4Y. Deng等人理论计算机科学电子笔记172（2007）359371芬可以看到，25%的时间测试是不成功的，因为它没有达到ω是可能的状态，75%的时间它可能是成功的，这取决于如何解决动作b和c之间的内部选择，但它不是必须成功的情况。不|动作P 可表示为有限图，该有限图编码了测试T与过程P的所有可能的交互。它只包含动作τ和ω。τ的每一次出现都代表了一个非确定性的选择，或者是T或P本身的选择，或者是P对T的请求的非确定性响应，而分布则代表了T和P中潜在概率的分辨率。 我们使用结构 T|行动P 定义Apply（T，P），[0，1]的非空有限子集，表示将T应用于P将成功的概率集合。首先，我们定义一个函数Results（），当它应用于Sp中的任何状态时，都会返回[0， 1]的有限子集。定义将要求它也适用于分布，为此，我们需要使用选择函数从[0， 1]的子集中收集元素。设R：Sp→P+（[0，1]），c：X→[0，1]，其中X是Sp的子集.然后我们写c∈XR，如果对于X中的每个s，c（s）∈R（s），结果收集函数可以定义如下：⎧ω⎪⎨{1}ifs−→,结果={Results（Δ）|s−→τ⎩⎪Δ}ifs−/−→ω，s−→τ，{0}否则哪里结果R（Δ）={Σs∈[Δ|Δ（s）·c（s）|c∈[Δ|结果}然而，我们倾向于使用更方便的符号，而不是显式地使用选择R结果（Δ） =Δ（s1）· R结果（s1）+... + Δ（sn）·R结果（sn）其中[Δ |={s1，. s n}。请注意，Results（）确实是一个定义良好的函数，因为pLTSSp，Actτ，→是无限分支的，并且是有根据的。例如，考虑图4中的转换系统，其中我们标记了节点作为参考。则Results（s1）={1，0}，而Results（s2）={1}，因此Results（Δ s）= 1·{1，0}+1·{1}，由于只有两个可能的2 2选择函数c ∈[Δ|结果，进一步评估为{1，1}。类似地，结果（t1）S2= Results（t2）={0，1}，并使用四个选择函数c∈[Δt|研究结果计算Results（Δt）=1·{ 0，1} +3·{ 0，1}得到{0，1，3， 1}。4 4 4 4定义3.3对于任意P ∈ pCSP和T ∈T，设Apply（T，P）= Results（ T |ActP ）。有了这个定义，我们现在有两个pCSP的测试前序，一个基于可能测试P±pmayQ，另一个测试必须P±pmustQ。372Y. Deng等人理论计算机科学电子笔记172（2007）359τ2ΔsΔt1434s1s2τt1t2τω ω ωResults（Δs）={1， 1} Results（Δt）={ 0，1，3， 1}2 4 44反例见图4。 收集结果我们将在本节中看到，许多标准测试公理在概率选择存在的情况下是无效的。我们还提供了一些涉及概率选择的分配律的反例，这些分配律乍一看似乎是合理的。在所有情况下，我们通过展示一个检验T来建立一个陈述P/p可以Q使得max（Apply（T，P））max（Apply（T，Q））和语句P /p必须Q通过展示测试T使得min（Apply（T，P））min（Apply（T，Q））。如果max（Apply（T，P））>max（Apply（T，Q）），我们特别发现P/±p可以Q，并且在min（Apply（T，P））>min（Apply（T，Q））的情况下，我们得到P/±p必须Q。例4.1公理a. （Pp<$Q）=a.Pp<$a.Q是不可靠的。考虑图5中的示例。在R1中，b和c之间的概率选择是在动作a之后做出的，而在R2中 ， 选 择 是 在 动 作 发 生 之 前 做 出 的 。 这 些 过 程 可 以 通 过 不 确 定 性 检 验T=a.b.ωHa.c.ω来区分。首先考虑在R1上运行这个测试.测试会立即做出选择，分别在R1上运行测试a.b.ω或测试a.c.ω;事实上，运行任何一个测试的结果都是完全相同的。考虑a.b.ω。当在R1上运行时，a操作立即发生，并且在b或c上运行b.ω之间存在概率选择，给出可能的结果{1}或{0};组合这些结果根据函数Results（）的定义，我们得到1·{0} +1·{ 1} ={1}。2 2 2由于运行测试a.c.ω具有相同的效果，因此Apply（T，R1）结果为相同的集合{1}。现在考虑在R2上运行测试T.因为R2和T|动作R2，从概率选择开始，由于函数Results（）的定义，测试必须首先分别应用于概率分量a.b和a. c，然后将结果概率组合。当在a.b上运行测试时，立即在测试中做出不确定性选择，运行a.b.ω或a.c.ω。对于前者，我们得到结果{1}，对于后者，我们得到结果{0}，所以总的来说，对于a.b运行T，我们得到可能的结果{0， 1}。当我们在a. c上运行，因此Apply（T，R2）=1· { 0， 1} +1· { 0， 1} ={ 0，1， 1}。2 2 2所以我们有R2/±pmayR1和R1/±pmustR2。1212ττττωY. Deng等人理论计算机科学电子笔记172（2007）359373ττB1212ττ ττττ22a aCω ωR1 = a. （b1<$c）R2=a.b1<$a. c T=a.b.ωHa.c.ω2 2τ ττ τω ω不|R 1T法案|第二幕Apply（T，R1）={1} Apply（T，R2）={ 0，1， 1}2 2图五、反例：行动前缀不分布在概率选择例4.2公理a. （PHQ）=a.PHa.Q是不可靠的。众所周知，这个公理在标准测试理论中对非概率过程是有效的。然而，考虑图6中的实例R1和R2，注意这些过程不包含任何概率选择。 但他们可以由概率检验T = a区分。（b.ω1<$c.ω）;详情见图6。2将T应用于R2只有一个可能的结果，即概率1，因为在概率选择之前进行非确定性选择。另一方面，当T应用于R1时，有三种可能的结果，0，1和1，因为相应地概率选择优先于非确定性选择。所以我们有R1/±pmayR2和R2/±pmustR1。例4.3公理a. （PQQ）=a.PQa.Q是不可靠的。这个公理在标准的may测试语义中是有效的。 然而，考虑两个过程R1 = a。（bQc），R2=a.bQa. c和概率检验T= a。（b.ω1<$c.ω）。现在Apply（T，R1）={ 1}并且Apply（T，R2）={1}。在那里-22因此R1/±p可以R2，R1/±p必须R2。一1212B C1212a一bCττττ121 12 212τ τωω374Y. Deng等人理论计算机科学电子笔记172（2007）359τ1212ττ ττ一ττ一ττ一一1212BCBCBCω ωR1 = a. （b H c）R2= a.b H a. cT = a. （b.ω1<$c.ω）2τ τω ω不|R 1T法案|第二幕Apply（T，R1）={ 0，1， 1} Apply（T，R2）={1}2 2见图6。 反例：动作前缀不分布在内部选择例4.4公理P=PQP是不可靠的。设R1，R2分别表示（a1<$b）和（a1<$b）Q（a1<$b）很容易21 2 2计算Apply（a.ω，R1）={2}，但是，由于我们解释exter的方式，作为pLTS中状态分布的算子的最终选择，事实证明，R2 = （（a Q a）1 <$（a Q b））1<$（（b Q a）1 <$（b Q b）） ，因此Apply（a.ω，R2）={3}。2 2 24因此，R2/±p可以是R1，R2/±p必须是R1.例4.5公理Pp<$（QHR）=（Pp<$Q）H（Pp<$R）是不可靠的。考虑过程R1=a1<$（bHc）和R2=（a1<$b）H（a1<$c），2 2 2试验T1=a.ωH（b.ω1<$c.ω）。 在最好的情况下，当我们应用T12对于R1，我们得到概率1，即max（Apply（T1，R1））= 1。 非正式地说，因为当它被应用于R1的子过程a时，乐观地说，子测试a.ω实际上是运行的。另一半时间，当它应用于子过程（bHc）时，乐观地说，子测试Tr=（b.ω1<$c.ω）实际上2采用 在这里，乐观地说，我们得到概率1：b.当使用ω时，它可以应用于子进程b，而当使用c.ω时，它可以应用于c。形式上我们有ττττ121 12 212τ τωωY. Deng等人理论计算机科学电子笔记172（2007）359375224Apply（T1，R1）=1·Apply（T1，a）+1·Apply（T1，bHc）2 2=1·（Apply（a.ω，a）<$Apply（Tr，a））+1·（Apply（T1，b）<$Apply（T1，c）<$Apply（a.ω，bHc）<$Apply（Tr，bHc））=1·（{1}<${ 0}）+1·（{0，1}<${ 0，1}<${ 0}<${ 0，1， 1}）2 2 2 2 2={ 0，1，1，3， 1}42 4然而，无论我们多么乐观地将T1应用于R2，我们都无法得到概率1;我们最多只能希望3，当T1应用于子过程（a1<$b）时可能会发生。 特别是当子进程a被测试时，2可以使用子测试a.ω，给出概率1，并且当子过程b被可以使用子检验（b.ω1<$c.ω），给出概率1。 我们离开22请读者正式Apply（T1，R2）={ 0，1，1，3}由此可得出R1/±pmayR2。42 4我们还可以证明，R2/±p必须R1，使用测试T2=（b.ω Q c.ω）H（a.ω 1 <$（b.ω 1 <$c.ω））.3 2从悲观的角度来推理，将T2应用于R1时可能发生的最坏情况是我们得到的概率为0.每次测试子过程a时，当使用子测试（b.ωQc.ω）时，将出现最坏的概率;这导致概率为0。类似地当测试子过程（bHc）时，子测试（a.ω1<$（b.ω1<$c.ω））将3 2概率为0。 换句话说，min（Apply（T2，R1））= 0。 当将T2应用于R2，事情不会这么糟的。当T2应用于子过程（a1<$b）时，将出现最坏的概率，即概率1。我们留给读者去检查，26形式上Apply（T2，R1）={ 0，1，1，1，2}和Apply（T2，R2）={1，1，1，2}。63 2 3 632 3例4.6公理PH（Qp<$R）=（PHQ）p<$（PHR）是不可靠的。设R1=aH（b1<$c），R2=（aHb）1<$（aHc），T=a. （ω1<$0）Qb.ω. 人能2 2 2检查Apply（T，R1）={1}和Apply（T，R2）=1{1， 1} +1{1， 0} ={1，1，3}。2 2 2 2 2因此，我们有R2/±p可以R1和R1/±p必须R2。42 4例4.7公理PQ（QHR）=（PQQ）H（PQR）是不可靠的。设R1=（a1<$b）Q（cHd），R2=（（a1<$b）Qc）H（（a1<$b）Qd），2 2 2T=（a.ω1<$c.ω）H（b.ω1<$d.ω）。 这一次我们得到Apply（T，R1）={ 0，1，1，3， 1}2 24 2 4且Ap ply（T，R2）={1，3}.所以R1/±p可以是R2，R2/±p一定是R1.4 4例4.8公理PH（QQR）=（PHQ）Q（PHR）是不可靠的。设R1=（a1<$b）H（（a1<$b）Q0），R2=（（a1<$b）H（a1<$b））Q（（a1<$b）H0）.2 2 2 2 2得到Apply（a.ω，R1）={1}和Apply（a.ω，R2）={1，3}。所以R2/±p可以是R1。2 2 4设R3和R4是用一个1阶b替换公理中的P、Q和R的2376Y. Deng等人理论计算机科学电子笔记172（2007）359以上现在Apply（a.ω，R3）={1，3}和Apply（a.ω，R4）={3}。所以R4/±p一定是R3。2 4 4Y. Deng等人理论计算机科学电子笔记172（2007）359377例4.9公理Pp<$（QQR）=（Pp<$Q）Q（Pp<$R）是不可靠的。设R1=a1<$（bQc），R2=（a1<$b）Q（a1<$c），R3=（aQb）1<$（aQc）.2 2 2 2R1是公理左手边的instance，R2是公理右手边的instance。手边。这里我们使用R3作为推理R2的工具，但是在第8节中我们需要R3在它自己的权利。注意R2 =1· R1 +1· R3 。设T=a.ω.很容易看出2 2Apply（T，R1）={1}且Apply（T，R3）={ 1}。因此，Apply（T，R2）={3}。2 4所以我们有R2/±pmayR1和R2/±pmustR1。在本节的所有例子中，这是唯一一个我们可以证明±pmay和±pmay都失败的例子，也就是说，可以与公理相关联的两个不等式对于may检验都是不可靠的 设T = a。（ω1<$0）H（b.ω1