可逆性和并发

理论计算机科学电子笔记192（2007）93-108www.elsevier.com/locate/entcs可逆性和并发伊恩·菲利普斯1伦敦帝国理工学院计算机系180 QueenIrek Ulidowski2莱斯特大学计算机科学系University Road，莱斯特，LE1 7RH，英国摘要在生物系统和量子计算等令人兴奋的应用领域，人们对可逆计算模型的兴趣越来越大。可逆过程代数RCCS [2]和CCSK [8]被发展，并提出了一般的技术，以扭转其他的过程操作。本文表明，可逆性的概念可以弥合一些交错模型和非交错并发模型之间的差距我们证明了与可逆过程代数相关的转移系统等价于标号素事件结构的模型。此外，我们表明，正向-反向互模拟对应于遗传的历史保持互模拟的设置没有自动并发和没有自动因果关系。关键词：可逆计算，标记转移系统，素事件结构，遗传历史保持互模拟1引言CCS with Communication Keys（CCSK）[8]是CCS的可逆版本，可用于建模和分析系统的双向行为，例如生物化学反应中分子的结合和解结合。CCSK的定义是以结构运算语义（SOS）的形式给出的，并利用SOS方法给出了将其它过程代数的算子转换为可逆算子的过程[8]。其主要思想是，动态运营商（可以在过渡过程中被破坏）转换的过程中，到静态运营商（这是保留），使用新的辅助运营商。为1电子邮件地址：iccp@doc.ic.ac.uk2电子邮件地址：iu3@mcs.le.ac.uk1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.08.01894I. 菲利普斯岛Ulidowski/Electronic Notes in Theoretical Computer Science 192（2007）93例如，选择P+Q的两边都被保留。因此，新可逆语言中的过程项在计算期间不会改变其整体结构。该过程的一个关键组成部分是通信密钥的概念。这些是唯一的标识符，被分配给过去的动作，并记录在过去动作的语法中，对于通信机制在正向和反向方向上正确工作至关重要。相反，在RCCS [2]中，过去的行为，包括通信，存储在外部设备上，如存储器。由[8]的过程产生的可逆算子的过程代数产生一个正向标号转移关系（ltr）→和一个反向ltr~，它是→的逆。这些ltr具有许多直观的性质，这些性质直接出现在可逆性的存在一些属性，例如逆钻石性质（见定义2.3）可以被认为是可逆跃迁系统的内在性质。其他属性，例如非重复属性（见2.1节），更具体，是使用通信密钥机制的结果。在本文中，我们研究了这类性质，并通过确定必须满足的几个性质，提出了可逆过渡系统的抽象定义。我们发现可逆转换系统足够丰富，可以表达事件、并发、因果和冲突等真正的并发（非交错）概念。因此，我们表明，可逆的过渡系统是等价的，作为模型的素事件结构。因此，我们可以在可逆转换系统的纯交错设置中研究和使用真正的并发语义。这一结果自然导致了关于可逆转移系统上定义的标准交织等价的区分能力的问题例如：正向-反向（FR）双向模拟关系[8]“最接近”的真正并发双向模拟是什么？FR互模拟是可逆转换系统上互模拟的一个自然概念，它显然比标准互模拟更精细，它区分了|b和ab + ba。它也比[ 5 ]中给出的两个版本的历史保持互模拟更精细，因为它不满足双折射定律：（a|（b + c））+（a |b）+（（a + c）|b）=（a）|（b+ c））+（（a + c）|（b）。我们发现FR互模拟与遗传历史保留（HHP）互模拟一致。这被认为是典型的真正的并发等价[1，5，7，3]。这个结果适用于没有自动并发和没有自动因果关系的可逆转移系统，并且由于CCSK产生了这样的转移系统，所以这个结果适用于CCSK。2素ltrs与素图我们提出了一类等价于标号素事件结构的转换系统以前，Sassone，Nielsen和Winskel [9]引入了具有独立关系的发生（oTSI）。独立关系通过给出它满足的条件来定义转换;它指出哪些转换是并发的。它的内容非常丰富，可以表达事件结构的因果关系和冲突关系。Sassone等人的研究表明，具有二元连续性的素事件结构，I. 菲利普斯岛Ulidowski/Electronic Notes in Theoretical Computer Science 192（2007）9395[ 9 ]这是一个很好的例子，因为它是一个特殊的性质（E）。独立地，van Glabbeek通过设置与必须满足的进程的并发历史相关的许多属性来定义历史保留进程图[4]。这些图和事件结构一样具有表现力。在这项工作中，我们遵循范Glabbeek在文献中，一个标记的过渡系统，或简称lts，可能有也可能没有初始状态。让我们认为ltr是一个结构，它指定了一个没有初始状态的转移关系，而lts是一个有初始状态的ltr。 因此，lts可以看作是有根ltr。2.1带标签的转移关系是一个结构（Proc，Lab，→），其中Proc是过程的集合，Lab是动作标签的集合，→ Proc×Lab×Proc是一个转移关系。 给定→，反向转移关系~是的逆→。 标号迁移系统是一个结构（Proc，Lab，→，I），其中I∈ Proc是初始状态。我们让P，Q，S，T，. 是典型的过程，a、b、c、d是典型的动作标签。我们将在整篇论文中保持实验室定义2.2[6]设（Proc，Lab，→）为ltr。 设λ为最小等价满足fyingg：ifP→a的关系Q→bSandP→bR→aS和Q/=R则（P，a，Q）（R，a，S）。写为[P，a，Q]的等价类是事件。定义标签通过设置l（[P，a，Q]）=a，从→/到Lab的函数l定义2.3素数ltr是满足以下条件的ltr（Proc，Lab，→）• WF（well-founded）没有无限的反向计算;• UT（uniquetransition）ifP→aQandP→bQ则a=b;• 如果P→a，则ED（event-determinism[9，4]）则Q=R;QandP→aR，和（P，a，Q）<$（P，a，R），• 如果Q→a，则RD（reverediamond）P，R→b P和Q/=R，则存在S使得S→aR，S→bQ;• FD（forwarddiamond）ifP→aQ→T，P→bR→T，QR，则有Ssuc hthatQ→bS，R→aS和S→ T。可以检查所有五个属性是相互独立的最有趣的例子表明ED和FD不能从其他的推导出来：分别见图1和图2请注意，当箭头不显示时，所有五个中的转换都应该从左到右读取在图1中，我们当P→aQ，P→aR和两个随机变量之间存在一个非线性关系时，活动注意，反向ED可以从RD和（正向）ED导出我们现在证明，我们在引言中简要概述的[8]的ltr是素数LTR的一个例子。不幸的是，篇幅不允许我们在这里给出ltr的相当长的定义命题2.4 [ 8 ]的ltr是一个素数ltr。96I. 菲利普斯岛Ulidowski/Electronic Notes in Theoretical Computer Science 192（2007）93一一BCBB一BB QaBaP a Q一b、 c、我a、c、bbRIPaa图1.一、CcacBC图二、证据 这在[8]中显示为RD和FD。WF很清楚。对于UT：很明显，ifP→aQandP→bQ，则转换具有相同的键。对于ED，注意项在计算期间不改变结构，除了一些静态运算符f变成辅助运算符fr。因此，任何fr[m]都必须是由菱形相对两侧的两个过渡在完全相同的位置创建的这一点也适用于。结果就是Q接下来，我们给出几个定义和结果，它们对证明我们的主要结果至关重要。定义2.5设（Proc，Lab，→）为ltr。从P到Q的路径是从P到Q的有限向前计算。定义2.6[4，定义3.1]假设ltr中的两条路径相邻，如果一条路径可以通过重新编程的示例P→a来从其他对象中恢复R→bQbyP→bS→aQ。说两条路是同伦的，如果它们通过自同构和传递相关，关闭邻接。请注意，我们可以假设R S在处理邻接的定义时，用UT的主要ltrs同伦路径有相同的事件。设（Proc，Lab，→）是一个素数ltr。 则不可逆过程为Irr={P∈Proc：P/~};设der（P）={Q∈Proc：P→<$Q}.引理2.7假设（Proc，Lab，→）是素数ltr。 假设P ∈Proc，Q，R ∈ Irr，s，t是从Q，R到P的路. 则Q = R，s，t是同伦的。证据 由RD和UT。QI. 菲利普斯岛Ulidowski/Electronic Notes in Theoretical Computer Science 192（2007）9397一一一U一不一UBP a Q不P a Qc bbRa图3.第三章。SP a Qa c aVW T UCBCRaS图四、R a S命题2.8素数ltr中具有相同端点的任何两条路都是同伦的.证据从引理2.7向后延伸到一个不可逆的过程，使用WF。Q命题2.8告诉我们，任何两条具有相同端点的路径都有相同的多事件集。我们想证明任何道路都不会重复事件如果是这种情况，则任何P∈Proc都与一个定义明确的事件集相关联，即从某个Q∈Irr到P的任何路径上的事件集。引理2.9设（Proc，Lab，→）是素数ltr。如果（P，a，Q）<$（R，a，S），则存在如图3所示的T，U，使得每个菱形的相对侧上的过程是不相等的，并且从T到P，R和从U到Q，S的路径中的事件都与[P，a，Q]不同。证据证明的实质是表明，如果有图4中第一个图中的P、Q、R、S、T、U，从P、R到T和从Q、S到U的跃迁，则存在V、W和适当的点跃迁（例如从V到P、R）。 我们使用反向ED和RD。Q命题2.10设（Proc，Lab，→）是素数ltr。在任何道路上都没有重复的事件。证据假设我们有一条从P到S经过Q，R的路径，如图4中的第二个图所示，其中（P，a，Q）<$（R，a，S）。然后通过引理2.9，我们有图3中的T，U。但是现在有两条不同的从T到R的路径，一条包含[P，a，Q ]，另一条包含[ P，a，Q]。98I. 菲利普斯岛Ulidowski/Electronic Notes in Theoretical Computer Science 192（2007）93没有 这与命题2.8相矛盾。Q有根路径是向前计算Pa1Pa2一个P其中P∈Irr.0→1 →··· →n0定义e eJ当且仅当ei=eJ，且所有包含eJ的代表的根路径也包含e的代表。(Note我们将[6]的定义推广到ltrs，而不是具有单个初始状态的过程图假设a2.11（侧边为菱形）在p边缘中，如果P→aQ→bR和[P，a，Q]/<[Q，b，R]中的n是S，则P→bS→aR。证据（草图，滥用事件之间的符号和事件的标签）由于[P，a，Q]/[Q，b，R]存在一条包含b但在b之前没有a的根路径。<使用引理2.9，我们将b的两个实例连接回它们共同的最早的b。在从R通过最早的b返回的路径上，必须有a的出现（延伸回coomon根并使用命题2.8）。因此，有一条路径π，beforea. 现在我们把一个pplyRD带到P→aQ→bR和顶部段π从a跃迁开始然后我们使用FD来沿着π提升aR，最终得到结果。Q定义2.12过程图（process graph）或图（graph）是一个lts，其中每个过程都可以通过初始状态的转移关系到达。命题2.13假设（Proc，Lab，→）是素数ltr。 如果P∈Irr，则der（P）在~下是闭的。证据 根据引理2.7。Q最后，我们准备好定义本文的中心结构定义2.14一个素（过程）图是一个图G=（G，Lab，→，I），使得（G，Lab，→）是一个素ltr。一个素图G的分支记为GG，→G，和IG。当上下文清楚时，我们将省略下标G，并且我们将使用这种命名约定与作为元组给出的其他结构。性质WF保证素图是无圈的。命题2.15设（G，Lab，→）是一个素数ltr，令I ∈ Irr。然后（der（I），Lab，（→der（I）2），I）是素图。证据我们使用命题2.13。很容易检验素数ltr的性质对der（I）成立。Q2.1CCSK工艺图我们在命题2.4中证明了CCSK的过程图是素图。此外，CCSK过程图满足附加性质：NR（非重复）在前向计算中没有重复的标签。I. 菲利普斯岛Ulidowski/Electronic Notes in Theoretical Computer Science 192（2007）9399B一B一B S一B一一BNR和WF意味着[4]中所谓的非重复性。CCSK图满足NR，这是使用引言中提到的密钥机制的结果：命题2.16 [ 8 ]的ltr满足NR。满足NR的素图称为非重复素图。我们将在第4节中证明，对应于非重复素图的素事件结构具有无自并发性[1]和无自因果性的性质2.2素图素图的几个性质，特别是ED和FD，在字符上是全局的：为了验证它们，可能需要检查图的任意大部分。然而，全局性质使它们在证明素图的其他性质和结果时非常有用。Sassone等人提出了一个悬而未决的问题，al. 在[9]中：人们能否找到一组仅涉及局部信息的属性，一种等价于素事件结构（具有二元结构）的转移系统形式？我们通过提出ED和FD性质的局部版本来回答具有一般（不一定是二元）约束的素事件结构的这个问题：• ED2（事件确定性2）如果 PQ则P=Q• FD2（正菱形2）Cc如果C请注意，ED 2可以被视为一种正向菱形属性的形式：如果S→a→bPandS→b→aP是一个向前的菱形，还有一个ab菱形，S到Q，则P=Q。 换句话说，如果有一个从S到P的正向菱形，那么这样的P是唯一的。定义2.17素2图被定义为素图，除了它的ltr分量分别满足ED 2和FD 2而不是ED和B一CCBP一一B100I. 菲利普斯岛Ulidowski/Electronic Notes in Theoretical Computer Science 192（2007）93请注意，ED 2定义中的图与图1中的第一个图同构。回头看RD，状态S是素数2图的唯一S。这可以使用RD三次，然后使用ED 2来证明。我们将用RD2表示具有唯一S的RD。我们还知道FD2中的P是唯一的，这可以用FD2和ED 2证明。我们可以通过反转ED 2中的箭头来定义反向事件决定论（反向ED 2）属性。然后从RD2容易地反向ED 2跟随。命题2.18素图是素2图，反之亦然。证据 省略Q3素事件结构我们想把素图映射成素事件结构，反之亦然，这样我们就可以比较FR互模拟和HHP互模拟。下面的基本事件结构的定义取自[6]，与Winskel [10]的原始定义一致。它推广了具有二元联系的素事件结构。定义3.1一个带标号的素事件结构是一个元组E =（E<，l），其中E是事件的集合，

下载后可阅读完整内容，剩余1页未读，立即下载