基于CSP的SOC演算中的同步和异步通信

可在www.sciencedirect.com在线获取理论计算机科学电子笔记312（2015）69-88www.elsevier.com/locate/entcs在SOC的CSP中实现同步和异步A beerS. Al-Humaimeedy<$，2001MaribelFern'andez<$2英国伦敦国王学院信息学系沙特阿拉伯沙特国王大学信息技术系摘要面向服务的计算（SOC）是基于服务组合的，即松散耦合的自治异构服务，通过组合来实现特定的任务。 在CSP进程代数的框架下，提出了一种新的SOC演算，旨在改进SOC演算的验证技术，提高SOC演算的表达能力.本文介绍了微积分的一部分它用内置的缓冲器扩展了CSP，以促进直接异步通信。我们提供了演算的操作语义，并通过实现异步通信功能来扩展FDR（CSP模型检查器）。关键词：异步，CSP，异步演算，缓冲器，SOC演算。1介绍面向服务的计算（SOC）是一种基于服务组合的计算模式，服务组合是指松散耦合的、所有异构的服务的集合，这些服务被组合在一起以实现特定的任务。在SOC范例中，服务可以单独使用消息进行通信，其中消息可以同步或异步发送。在Web服务（WS）标准[18，25]中，消息根据预定义的交互模式[9]发送这些交互模式包括请求-响应 模式和请求-响应模式，表示同步通信。 以同步在通信中，消息的发起者暂停处理，直到它收到响应。另一方面，单向和通知模式代表1电子邮件：Abeer@ksu.edu.sa2电子邮件：Maribel. kcl.ac.ukhttp://dx.doi.org/10.1016/j.entcs.2015.04.0051571-0661/© 2015作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。70A.S. Al-Humaimeedy，M.Fernández/Electronic Notes in Theoretical Computer Science 312（2015）69异步通信，其中消息的发起者继续运行下一个编码语句，而不挂起处理。进程演算，如SCC [5]和CaSPiS [6]，提供了同步通信的交互模式的正式规范，允 许 设 计 人 员 推 理 SOC 系 统 的 正 确 性 。 其 他 正 式 的 系 统 ， 如 COWS [16] 和Conversation Calculus [24]，只考虑异步通信，因为互联网标准中的同步通信通常由TCP/IP [12]等网络协议实现据我们所知，没有一个为SOC开发的正式演算同时支持同步和异步通信。在本文中，我们提出了一个新的进程演算，称为CSPa，支持混合同步和异步通信。我们的演算可以被描述为Hoare的CSP [ 13 ]的简化版本CSP被选为我们演算的基础，因为它的通信模型支持混合同步/交织通信。在CSP中，参与并行组合的所有进程都在预定义的事件集上同步。 例如，设p、q、r是CSP进程，则在并行组合（p∈ {|甲乙丙|}q{|甲乙丙|}r）时，进程p、q和r仅在事件a、b上同步，其余事件被独立地评估。这种形式的平行合成称为广义平行合成。在CSP中，并行合成有另一个版本，称为字母并行合成[20]，写作pαp<$αqq，其中参与者同步所有共享事件。然而，通过将接口集设置为（αp<$αq），可以将字母化并行组合编码在广义并行组合中。这里，αp表示p在本文中，我们只考虑广义平行合成。因此，从现在开始，当我们写平行合成时，我们指的是广义的平行合成。CSPa的新颖之处在于引入了隐式缓冲器，通道语义以透明的方式促进异步通信。换句话说，CSPa包括异步通信原语，这些原语依赖于缓冲器，但是设计者不需要创建、维护或终止缓冲器。我们提供了一个操作语义来解释缓冲器是如何工作的。此外，我们研究了我们的演算和CSP之间的关系，我们编码我们的演算在原来的CSP。虽然CSPa中的新结构并没有增强CSP的表达能力，因为新结构可以在CSP中编码，但CSPa通过用一个转换替换编码转换来简化推理在以前的工作中，我们扩展了CSP与原语模型动态补偿[1]。在这里，我们只专注于通信原语：我们通过允许异步通信，除了其标准的混合同步/交错通信，增强CSP。更确切地说，我们扩展了并行组合运算符，以允许混合同步，交错和异步通信。在未来的工作中，我们计划还包括原语，以创建和维护会话和模型的流动性，以获得一个富有表现力的计算，A.S. Al-Humaimeedy，M.Fernández/Electronic Notes in Theoretical Computer Science 312（2015）6971（Ⅲ）i=1ǁlus用于SOC建模。我们观察到，虽然SOC演算配备了形式语义，这使得正式验证的属性，一个功能不提供的WS标准，这些标准仍然是占主导地位的建模语言。在我们看来，这主要是因为正式的方法往往被认为难以应用。为了方便我们的演算的实际使用，我们在CSP模型检查器（FDR [11]）中编码了CSPa。罗斯福实现了数学机器和霍尔为推理系统的外部行为而建立的精化理论。它提供了简单的证明技术来断言规范和实现之间的一致性，死锁自由和发散自由，以及确定性和互模拟（我们在第6节的示例中说明了其中的一些特性）。其他模型检查器，如SPIN [14]，它接受Promela或Maude [2]中的模型，如果这些检查被实现，则可以使用在模型检查器PAT [23]中实现了细化检查，但我们选择FDR是因为CSP#（PAT的输入语言）不支持我们在本文中扩展的广义并行组合运算符论文概述：第2节回顾了CSP的一些基本概念。 第三节介绍了CSPa。第4节讨论了CSP和CSPa之间的关系。第5节介绍了CSPa在FDR中的实现。第6节通过一个例子说明了这个扩展的可用性。第7节讨论相关工作。最后，第8节总结并讨论了未来的发展方向。2预赛我们假设读者熟悉CSP的核心理论。下面我们简要回顾一下它的语法和操作语义。关于更多的细节，我们请读者参考[20];我们的符号主要来自它。在本文的其余部分，使用以下符号：p，q，。. . 表示亲，cesses;cesses是包含系统中所有可观察事件的全集; a，b用于在此集合上范围。τ（ 相 应 地 ， 是 万 有 集 合 τ ， 此 外 还 有 无 声 事 件 τ （ 分 别 为 ， 终 止 事 件（Event）。τ帽-大写字母A，B表示可观察事件的集合;s表示列表，而x表示a列表中有x元素。CSP进程由以下语法定义。p，q：：= a → p |pQq |p H q |pAq |p; q |p\A |p R |μp.f（p）|p|||Q |SKIP|停止其中a可以是原子动作的名称，通过通道a输入（写为a？x），通过通道a输出（写为a！x）或它们的组合（例如a！x？y）。（2）交叉（|||）和并行复合（parallelcomposition，简称CABA）运算符有索引版本编写为|||Ni=1分别√操作语义在图1中给出，其中e−a→，−a→.x，−τ→，−→表示标记的转移关系。这里，a表示原子操作，a.x表示通过通道a输入或输出，其中x可以是变量或数据;72A.S. Al-Humaimeedy，M.Fernández/Electronic Notes in Theoretical Computer Science 312（2015）69（Ⅲ）和a.x被认为是事件。停止是什么都不做的过程。SKIP是立即成功终止的进程。前置（a→p）是准备参与事件a，然后表现为p的过程。外部选择（pQq）是由p或q的第一个动作的环境决定的。内部选择（pHq）是内部解决的;因此，在内部行动τ之后，任何一个选择都是可用的。递归函数（μp.f（p））使用显式固定点符号定义，其中f（p）是涉及过程p的CSP项，μp.f（p）定义与p=f（p）完全相同的过程。这里的递归法则是，递归定义的过程μp.f（p）满足定义它的方程，即，μp.f（p）=f[μp.f（p）/p]（CSP中不动点递归的细节可以在[20]中找到）。在Hiding（p\a）中，动作a隐藏在进程p中，即外部环境无法观察到它。如果R是一个将集合A中的事件映射到集合B中的事件的关系，则Renaming（p R）是将进程p中的事件从A映射到B。在顺序组合（p;q）中，如果p成功终止，则执行q。在并行组合（p<$Aq）中，p和q是并行执行的，并且只在A中的事件上同步;事件不在A中的是交错的。并行组合不要求进程在终端事件上同步。因此，如果p或q准备好成功终止，即评估事件，然后进程可以终止，然后平行组合将演化到称为Ω的中间状态，直到两个进程终止，则并行组合将成功终止;这称为分布式终止。 在交错（p|||q）来自过程p、q的事件可以以任何顺序执行。除了前缀运算符为a和a.x提供不同的规则外，图1中的a事件规则可以是a或a.x，其中x是变量或值。在规则（par3）中，由于整个a.x是一个事件，所以a.x只能在x和y的值相等或者它们中的一个或两个都是输入变量的情况下与a.y在本文中，我们假设列表上的标准函数和条件if-then-else是可用的，并作为τ转换执行。我们在下面回顾弱转移[21]、双相似性[21]和相似性[17]关系的定义定义2.1[弱跃迁](i)=是−τ→的自反传递闭包（即=是−τ→）。 因此，p=pJ表示p可以通过执行零个或多个内部动作而演化为pJ（二）=a是=−a→=，对于a∈。因此，p=apJ表示p可以通过在a之前和之后执行具有任何数量（可能为零）的内部动作的可见动作a来转换为pJ。（iii）=n表示使用=n或=an的0个或多个步骤的序列。定义2.2[双相似性]双相似性关系，记为p，是最大的对称关系，使得当p≠q时，则：(i) 如果p−a→pJ，则n q=a<$qJ且pJ<$qJ。A.S. Al-Humaimeedy，M.Fernández/Electronic Notes in Theoretical Computer Science 312（2015）6973√√∈τ√√（skip）（prefix）（a→p）−a→pa∈n跳过−→停止（prefix-out）（a！x→p）−a→.xpa.x∈n （prefix-in）（a？x→p）−a→.vp[v/x]a.v∈(exch 1，2）p−a→p′q−→bq′（a，b∈π）（exch3，4）p−τ→p′q−τ→q′（英寸1，2）pQq−a→p′τpQq−→bq′τ（rec）pQq−τ→p′QqτpQq−τ→pQq′pHq −→p p Hq −→qp−a→p′p−a→p′μp.f（p）−→f[μp.f（p）/p]p ST OP（hid1，2，3）p\A−a→p′\A（a∈/A）p\A−τ→p′\A（a∈A）−→√p\A−→ST OPp−a→p′p−τ→p′p−→停止（rem 1、2、3）bp<$R）−→（aRb）p′（R）p<$R）−τ→p′<$R）√p<$R）−→ST OP（seq1，2）p−a→p′p;q−a→p′;q（a <$τ）p−→p′p;q−→q（intv1，2）p−a→p′p|||q−a→p′|||Qq−a→q′p|||q−a→p|||q′ （a∈τ）（par1，2，3）p−a→p′p<$Aq−a→p′<$Aqq−a→q′p<$Aq−a→p<$Aq′p−a→p′q−a→q′p<$Aq−a→p′<$Aq′（a∈A）（第1、2、3部分）p−→停止p<$Aq−τ→Ω<$Aqq−→停止p<$Aq−τ→p<$AΩΩ<$√Ω−→STOP图1. CSP(ii) 如果p−τ→pJ，则q=<$qJ且pJ<$qJ。我们说两个过程p和q是双相似的，如果p<$q。定义2.3[相似性]相似关系，用≤表示，是最大的关系，使得当p≤q时，则：(i) 如果p−a→pJ，则n =qJ。 q=a<$qJ且pJ≤qJ。(ii) 若p−τ→pJ，则有<$qJ.q=<$qJ且pJ≤qJ。我们说，如果p≤q，则过程q模拟过程p。3CSPa中的混合同步/异步通信在CSP中，并行组合操作符不强制同步事件。相反，它是由一个接口集参数化的，该接口集管理参与者之间的同步。接口集内的事件应该同时求值，而接口集外的事件即使是共享的，也可以独立求值。独立地评估事件并不能将通道的数据从输入过程传递到输出过程.如果设计师想要精确性（即，要延迟传输的数据），它们需要定义和维护显式缓冲器。为了避免这种负担，我们在CSPa中包含了内置的缓冲器，与CSP中的事件相关联，并扩展了CSP的语义来建模异步通信。通过这种方式，并行性成为微积分中的一个原始概念，与同步性处于同一级别，设计人员不需要处理创建和维护缓冲器的实现细节为了实现这个解决方案，我们用两个事件扩展了CSP一个！x，表示a的我们还扩展的过渡关系如下：前缀a？进程中的>x表示该进程准备好接受A这个输入转换规则类似于CSPa←.x标签可以被读取为通道a的输入x（输入通道意味着从缓冲器输出（asy-in） a？>x→pa−←→.vp[v/x]如果事件a！和表示与Ba的通信，其中Ba表示通道a的内置缓冲器。head（s）→Ba（tail（s））Qa？x→pa−←→.xpA.S. Al-Humaimeedy，M.Fernández/Electronic Notes in Theoretical Computer Science 312（2015）6975在哪里数据是由评估a的过程消耗的？>x. 一个！x和a？>x将使用CSP的原始并行组合进行同步为了允许这些新事件被图1中的并行组合、规则（par 1-par 3）和图1中的其他CSP操作符评估，我们创建集合B以包含事件类型：a←.x和a→.x，如下所示：B ={a←，a→|a ∈channels（n）}其中，channels（channel）是从事件中提取通道名称的函数。之后，我们将更新为B。因此，CSP现在可以评估新类型的事件。根据定义3.1，无界缓冲器有三个选项：（i）无条件地输入数据;（ii）如果缓冲器不为空，则输出数据;（iii）如果系统终止，则终止。在设计Ba时，FIFO策略是通过将新数据附加到缓冲器列表的末尾来实现的，并且进程总是消耗列表中的第一个元素引入隐式缓冲器背后的直觉是在发送和接收消息之间引入延迟。这将允许进程继续执行，而无需等待接收者获取消息。在双向通信（两个进程之间）中，如果缓冲器在通信的中间引入，那么从第一个进程发送的消息将存储在缓冲器中，直到接收方进程准备好获取消息。然而，在CSP中的多路通信（多个进程通信）中，我们应该解释并行性意味着什么。在我们的模型中，我们希望保留多路通信的CSP模型，并添加了可扩展性。在多路通信中，阻塞信道可能会引入非确定性，如例3.2所示。示例3.2考虑系统是吗？>x→跳过a？>y→SKIPa！<3 →跳过其中进程不同步（即交错）;我们编写用于具有空同步集的并行合成的RISK根据我们的模型，通信可以以任何顺序发生。如果输出是第一个完成的，那么值3将存储在Ba中，然后由输入事件检索。但是，哪个输入事件将从缓冲器（a？>x或a？”““不，“他没有具体说明。或者是？>x得到值，a？>y将等待一个新的值，或者相反。在CSPa中，我们可以通过在输入事件或输出事件与缓冲器之间进行同步来避免这种非确定性，如下面的示例所示例3.3假设在一个系统中发生以下通信：是吗？>x → SKIP {a？什么？>y→SKIPa！3→跳过假设缓冲器是空的，那么根据我们的模型，值3将76A.S. Al-Humaimeedy，M.Fernández/Electronic Notes in Theoretical Computer Science 312（2015）69存储在Ba中，然后由输入事件检索。在这里，输入事件是同步的，因此？x和a？>y应该得到相同的值（即3）。因此，在CSPa中，有两种结晶度可用：(i) 同步通信，但在输入和输出值之间有延迟.这可以通过同步输入事件和输出事件来实现。因此，如果缓冲器为空，则所有输出事件同时发生并将数据上传到缓冲器，然后所有输入事件从缓冲器获得相同的值。请注意，CSPa遵守CSP同步规则，其中整个a.n事件被视为同步。例如，在CSP中，事件a。3只能与a同步。3或a.x，如果x是输入变量（在后一种情况下，x将被3取代不太严格的同步通信可以通过仅在输入事件（如例3.3）或输出事件上同步来实现。(ii) 交错通信，值不会丢失，而是存储在缓冲器中。然而，在这种情况下，buffer事件的执行顺序事件缓冲区可以看作是共享内存中所有进程都可以访问的区域。 我们在下面定义 一 个 过 程 ， 我 们 称 之 为 buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-buffered-定义3.4 [Bu-1-Bu]过程Bu-1-Bu是所有单个事件Bu-1的平行组合，即B = |||i∈B i. 交错运算符用于强调事件缓冲器在输入或输出时不同步。进程通过执行到新状态的转换（= Bjj）而演进：Bj，Bj， . .为了让buffered-xmls与整个系统一起工作，我们将它与系统并行安装，作为预处理步骤，从而允许系统以异步模式执行。缓冲器将与整个系统并行工作，并对所有具有→或←的事件进行同步。由于进程之间的通信仅在它们并行工作时才发生，因此使用并行组合操作符来安装buffered-browser。定义3.5[缓冲系统]如果p是CSPa过程，则缓冲过程与p相关的是p{a←，a→|a∈}B.我们使用无声动作τ来表示预处理步骤，其中系统与缓冲器并行放置。这是安全的，只要系统的外部可见行为通过添加具有τ作用量的额外起始状态而保持不变，其中该系统别无选择，只能采取这种不可见的作用量，并且表现得像一个受限制此外，这将隐藏向系统添加缓冲器的效果。最后，重要的是确保缓冲器不引入非终止，即，如果系统终止，则缓冲器也应当终止。为了实现这一点，我们引入了一种新的终止方法CSPa进程，即同步A.S. Al-Humaimeedy，M.Fernández/Electronic Notes in Theoretical Computer Science 312（2015）6977Σ{a ←，a→|a∈}ΣΣ{a ←，a→|a∈}Σ{a ←，a→|a∈}Σ −→终止，它取代了CSP中的分布式终止。在同步的术语中，CSPa过程在评估事件的时间上同步，即，终止因此，如果进程终止，那么缓冲器将被迫终止，好的，详见命题3.8（这个特征在我们微积分的其他部分也很重要，用于处理补偿和会话）。以下规则实现同步终止：√ √（parST）p−→STOPq−→ST OPpAq−→ST OP请注意，图1中的规则（parST）取代了规则（parT1，2，3）。我们将在本节的其余部分证明我们的缓冲系统是由原始系统模拟的。也就是说，我们的缓冲系统不会引入原始系统无法实现的新的定理3.6F或每个p∈CSP a，（p<${a←，a→|a∈B<$J）≤p，其中eB<$J过程B的状态：B=BJ。是任何证明为了证明根据定义2.3的模拟，我们需要依次考虑由缓冲系统执行的转换，并将它们与进程p执行的转换相匹配。根据定义3.1和3.4，缓冲系统可以进行以下转换：• 缓冲过程执行τ如下：（p）BJ）−τ→（pBJJ）按规则（rec，par1）过程p不变，因此：p=p• buffered进程执行←.x如下：（p{a←，a→|a∈} BJ）a−←→.x（pJ<${a←，a→|a∈} B. B.JJ）b.y规则（exch1，par3）a←.x然后，这个转换以如下方式与过程p匹配：p−→pJ• buffered进程执行→.x，如下所示：（p{a←，a→|a∈} BJ）a−→→.x（pJ<${a←，a→|a∈} B. B.JJ）b.y规则（exch1，par3）a→.x然后，这个转换以如下方式与过程p匹配：p−→pJ• buffered进程执行如下操作（p）BJ）按规则停止（exch1，parST）这是因为，根据定义3.1和3.4，如果环境发生此事件并终止，则缓冲器应在缓冲器上进行评估和同步然后，这个转换由过程p以如下方式匹配：√p−→停止Q3.1方向、死锁和终止在CSP中，数据单元可以被划分为若干分量（例如ItemID、ItemQ），并且这些分78A.S. Al-Humaimeedy，M.Fernández/Electronic Notes in Theoretical Computer Science 312（2015）69量在同步模式下可以在两个方向上同时传送（例如a？项目ID！ItemQ，其中ItemID是重新-A.S. Al-Humaimeedy，M.Fernández/Electronic Notes in Theoretical Computer Science 312（2015）6979的1−→an接收到，并且在信道a）上同时发送项目Q在CSPa中，类似于[13，20]，通道具有明确的方向，其中整个数据单元每次在一个方向上加载或消耗（例如，是吗？项目ID。项目Q，a！项目ID、项目Q）。在演算中添加缓冲器会显著影响系统的性能，并引入额外的设计错误。例如，如果由于通道缓冲器已满而无法评估输出，则系统可能会以死锁结束。为了避免引入死锁，Hoare建议这些缓冲器是无界的。我们都遵循了霍尔由于规则（parST），与系统并行安装的缓冲存储器将在系统终止时终止。这是由于环境在外部激活定义3.7[终止的过程]终止的过程是一个过程，它不能进化更多（即：不能进行任何转换）。在CSPa中，作为原始CSP，一个k如果存在p−a→0，则过程p终止p1−→. . .pn−→ST OP，其中而STOP是不能进行任何转换的原始进程如果an=0，则该过程成功终止，否则该过程没有进一步的过渡。注1在CSP中，如果一个进程不能进化更多，那么它等同于STOP;详见[20]。命题3.8缓冲器不引入死锁或非终止的转移序列，即：（i）如果缓冲器-缓冲器成功终止，则p成功终止。(ii)如果通道缓冲器在输入时不为空，则缓冲器仅在p个块时才块。(iii)如果bu-1有无限步的跃迁，那么p也有。证明我们证明命题的情况如下：(i) 如果缓冲区成功终止，则进程p也成功终止。这是因为如果进程p成功终止，则在环境中可观察到事件事件将解决外部如定义3.1所示，使用规则（parST），使用SKIP选项进行选择(ii) 如果通道缓冲器不为空，即系统不会阻塞，因为没有数据要检索，则作为定理3.6的结果，如果p∈ {a←，a→|a∈ n}Bn有块或无穷序列的跃迁，则p有这个块或无穷序列的跃迁。Q4CSPa与CSP在本节中，我们首先讨论CSPa到CSP的编码，然后通过证明编码过程与我们的微积分的原始过程弱双相似来推理我们编码的正确性（定理4.3）。这个结果表明，CSPa并没有严格地增强CSP的表达能力， CSPa中的新结构可以在CSP中编码，但是，CSPa简化了80A.S. Al-Humaimeedy，M.Fernández/Electronic Notes in Theoretical Computer Science 312（2015）69<$SKIP）=term→SKIP（Ⅲ）是啊！<→p）=a→.x→<$p）在CSP的上下文中，通过提供用于建模的显式原语来由于编码，我们可以使用CSP的指称模型来推理CSPa系统的正确性。非正式地说，CSPa和CSP之间的主要差异是与缓冲器的隐藏通信和同步终止。为了便于编码，我们定义了新的终止信号项，用于在进程终止时强制同步。此终止信号稍后将隐藏在系统中此外，我们将Ba（在定义3.1中定义）编码为以下CSP过程：Ba（s）=if null（s）则（（a←.x−→Ba（<$x<$））Q（term→SKIP））else（（a→.head（s）−→Ba（tail（s））Q（a<$.x−→Ba（s-<$x<$）Q（term→SKIP））其中null（s）、head（s）和tail（s）是列表上的标准函数，它们分别检查列表是否为空，检索列表中的第一个元素，并返回列表中除第一个元素之外的所有元素。我们还将B编码为以下CSP进程：|||i∈B i. 我们定义从CSPa到CSP的编码如下：第4.1节编码[编辑] ]：CSPa→CSP定义为：[。[1] =p\{term}，其中，除以下情况外，φp）是同态定义的一个？>→p）=a<$.v→<$p[v/x]）<$p<$Aq）=（<$p）<${term}<$A<$q））引理4.2如果q=p\A，则：(i) 如果σ∈/A，则p−σ→pJ惠q−σ→qJ，其中reqJ=pJ\A。(ii) 若σ∈A，则p−σ→pJ<$q−τ→qJ，其中reqJ=pJ\A。 Also，q−τ→qJ意味着对于σ∈ A，p−σ→pj或p−τ→pJ。对于Topr ove（i）的Pr o，我们首先证明了若σ∈/A则p−σ→pJ<$q−σ→qJ且qJ=pJ\A. 如果σ∈/A，则σ有两种情况：(i) Ifσ的形式为a，a←， a→或τ，则a根据规则（hid1），如果p−σ→pJ且σ∈/A则q−σ→qJ且qJ=pJ\A。(ii) 如果σ = σ，则根据规则（hid3），如果p√停止，然后q√停下来，J−→ −→这意味着q=STOP，但在CSP中，STOP\A=STOP（请参见[20]因此，qJ=STOP\A。A.S. Al-Humaimeedy，M.Fernández/Electronic Notes in Theoretical Computer Science 312（2015）6981−→其次，我们证明了如果σ∈/A，则q−σ→qJ<$p−σ→pJ，其中qJ=pJ\A。如果σ∈/A，则σ有两种情况：(i) Ifσ的形式为a，a←， a→或τ，则by规则（hid1）如果q=p\A−σ→pJ\A，这意味着p−σ→pJ。(ii) 如果σ = σ，则根据规则（hid3），如果p\A 停止，这意味着p停止。但是，在CSP中，STOP\−→A=STOP（参见[20]），因此，q−→=停止\A.因此，如果σ∈/A，则p−σ→pJ惠q−σ→qJ，其中qJ=pJ\A。为了证明（ii），我们首先证明如果σ∈A，则pqJ=PJ\A，这是规则（hid2）的直接结果−σ→pJ<$q-τ→qJ，其次，我们证明了对于σ∈A，q−τ→qJ<$p−σ→pJ，其中qJ=pJ\A，或p−τ→pJ。q−τ→qJ可以在两种情况下发生：(i) 如果按照规则（hid1），p−τ→pJ，那么我们就完成了。(ii) 如果p−σ→PJ且σ∈Aby规则（hid2）.Q定理4.3设[. ]：CSPa→CSP是定义4.1中的编码。 每p∈CSPa，p∈ [p].证明我们只对编码的四种非同态情况给出证明同态的平凡遵循。我们将证明上述四种情况下的编码是弱双相似的源过程。现将这四起案件说明如下：(i) SKIP√τ√我们证明：若SKIP−→ST O P ，则[SKIP]−→STOP.过渡SKIP跳过过渡。−→STOP遵循规则（跳过），并且是唯一的编码过程以如下方式匹配此转换：τ√[SKIP]−→−→STOP by rules（prefix，hid2，skip）.τ在另一个方向上，[ SKIP ]唯一可能的转换是[SKIP]−→按规则跳过（prefix，hid2）。此转换匹配为：SKIP=SKIP。因此，根据定义2.2跳过[跳过]。(ii) 是吗？>x→pa←.va←.v我们提出：如果一个？>x→p−→p[v/x]，则[a？>x→p]−→a[p[v/x]]。（a？）>x→p）is：（a？>x→p）−←→.vp[v/x]by规则（asy-in）。这种转换是由编码过程以以下方式匹配的：[a？>x→p]a−←→.v[p[v/x]]by规则（prefix-in，hid1）。J82A.S. Al-Humaimeedy，M.Fernández/Electronic Notes in Theoretical Computer Science 312（2015）69在另一个方向上，唯一可能的过渡[a？>x→p]是：[a？>x→p]a−←→.v[p[v/x]]by规则（prefix-in，hid1）。CSPa进程以下列方式配合这一过渡A.S. Al-Humaimeedy，M.Fernández/Electronic Notes in Theoretical Computer Science 312（2015）6983a→.xJ（Ⅲ）（par3，hid1）.−→W e knowthat，if[p]−σ→[pJ]then<$p）−σ→<$pJ）by引理4.2.W e knowthat，if[q]−σ→[qJ]then<$q）−σ→<$qJ）by引理4.2.−→√√√（a？>x→p）a−←→.vp[v/x]byrule（asy-in）.因此，根据定义2.2（a？>x→p）n[a？>x→p](iii) 一个！x→p）n[a？>x→p](iv) p<$Aq<$σ σ我们证明，如果σ，则p<$Aq−→r蕴涵[p<$Aq]−→[r]，否则，√τ√p<$Aq−→r意味着[p<$Aq]−→<$[r]。首先考虑（p<$Aq）的可能跃迁：• 若p−σ→pJ且σ∈/A，则（p<$Aq）−σ→（pJ<$Aq）byy规则（par 1）。编码过程以如下方式匹配此转换：σJ这意味着，如果<$p） −→<$p） 和σ∈/A然后σJ（p<$<$q））\{term} −→（<$p）<$<$q））\{term}按规则（1）{term}A{term}A(par1，hid1）。• 若q−σ→qJ且σ∈/A，则（p<$Aq）−σ→（p<$AqJ）byy规则（par 2）。编码过程以如下方式匹配此转换：σJ这意味着，如果<$q） −→<$q） 和σ∈/σJA然后（p<$<$q））\{term} −→（<$p）<$<$q））\{term}按规则（1）{term}A{term}A(par2，hid1）。• 若p−σ→pJ且q−σ→qJ，则（p<$Aq）−σ→（pJ<$AqJ）i f σ∈Aby规则（par3）。编码过程以如下方式匹配此转换：Weknowthat，if[p]−σ→[pJ]andnd[q]−σ→[qJ]then<$p）−σ→<$pJ）and<$q）−σ→由引理4.2推导出的q 。σJ这意味着，如果<$p） −→<$p）和<$q）−→<$q） ，则σ（p<${term}<$A<$q））\{term}−→（<$pJ）<${term}<$A <$qJ））\{term}如果σ∈Abyruleses• 如果p−→STOP且q−→STOP，则（p<$Aq）−→STOPby rule（parST）。编码过程以如下方式匹配此转换：我们知道，如果[p]τSTOP和[q]τSTOP，项τ∗√项τ−→−→−→84A.S. Al-Humaimeedy，M.Fernández/Electronic Notes in Theoretical Computer Science 312（2015）69p）第{term}项A<$<$p）−→STOP和<$q）−→−→这意味着，如果p- →由引理4.2停止。term τ停下来τ项τ∗√ST OPth<$en）−→−→−→（<$q））\{term} −→（q）−→−→ −→A.S. Al-Humaimeedy，M.Fernández/Electronic Notes in Theoretical Computer Science 312（2015）6985（2）∈（2）J{term}Aσ（）（）（）（Ⅲ）（（））{term}A（Ⅲ）−→（Ⅲ）（Ⅲ）和[q]−σ→[qJ]then<$p）−σ→<$pJ）和<$q）−σ→<$qJ）<$q））\{term}−σ→<$）（<$pJ）{term}A<$q））\{term}如果σ∈Abyrules[p]−τ→SKIP和[q]−τ→SKIP则<$p）t−er→mSKIP和<$q）t−er→mSKIP<$q））\{term}<$−τ→）Jστ τ√（SKIP{term}ASKIP）\{term}−→−→ →按规则停止(par3、hid2、partT1、hid1、partT2、hid1、partT3、hid3）。在另一个方向上，由于通过定义4.1，[p<$Aq] =（p<${term}<$Aq）\{term}，[p<$Aq]的可能转换为：如果σ/σ{term}和[p]−σ→[pJ]，则by引理4.2如果[p]−σ→[pJ]thenp −→ p.这意味着，如果p−σ→<$pJ）then（<$p）<$q））\{term}−→（pJ<${te rm}<$Aq）\{te rm}其中σ∈/Ay规则（par 1，hid 1）.这个转移可以通过CSPa过程以如下方式匹配：如果p−σ→pJ，则（p<$Aq）−σ→（pJ<$Aq）ifσ∈/Aby规则（par 1）。• 如果σ∈/{term}和[q]−σ→[qJ]thenbyLemma4.2如果[q]