理论计算机科学电子笔记175（2007）51-61www.elsevier.com/locate/entcsMonic火柴Filippo Bonchi，Tobias HeindelDipartimentodiInformatica，Universita`diPisa，Italy摘要本文提出了一个一般的理论，将允许系统地从一个给定的减少系统的行为一致性，尊重并发性不可或缺的技术成果。这一理论是建立在一个基于文本和语境的文本分类的基础上的，后者是Leifer和Milner提出的相对推出的一个例子。为了将DPO重写的并发性理论提升到借用的上下文，我们将研究粘附范畴中具有monic匹配的DPO重写的特殊情况：更具体地，我们提供了一个广义的Butter Rumey引理以及Local Church Rosser和Maxelism定理。关键词：粘着范畴，行为一致性，借用语境，DPO1介绍和动机进程演算是描述交互式系统的一个成熟工具。一个过程的进程，如果被解释为一个封闭系统，则由一个归约系统（RS）来描述;此外，每个过程都是一个有标签的转移系统（LTS）的一个状态，它描述了过程如何与其环境相互作用：在这种情况下，过程被认为是一个开放系统。双重推出方法（DPO）也可以用来模拟封闭和开放系统：一个还原步骤对应于一个DPO重写，而与环境的交互被描述为一个由借来的上下文标记的转换，这是环境的一部分DPO方法的优点之一现在这篇文章的主要动机是将这个优点提升到开放系统的环境中，即为LTS提供描述与环境的并发交互的标签第一种从给定的RS中导出LTS的方法之一在[13]中提出。生成的LTS的转换由允许还原的“最小”上下文标记1这项工作得到了S EGRAVIS研究培训网络、IST 2004-16004 SE n-SO RIA和MIUR PRIN 2005015824 ART的部分支持。1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.04.01652F. Bonchi，T.Heindel/Electronic Notes in Theoretical Computer Science 175（2007）51到具有“空”环境作为标签的转换）。例如，在CCS中，其中具有REDUCTONRUL E XR。P|X. Q→P|Q，这是一个过程。0c annotperform任何还原本身，但只能在形式[−]的上下文中还原。|a.P：他必须把他的经验告诉我们。0−[−]|a−。→PP.的主要属性导出的LTS是其相关联的互模拟关系是同余，即，它涉及表现出相同行为的两个过程。每一个环境。然而，要检查双相似性，不需要检查所有上下文，但考虑作为标签给出的Leifer和Milner的工作[ 13 ]已经被扩展到一个丰富的范畴，该范畴由S A SS ONE和S O B O C INSKI [ 1 4 ]构成，而E H R I G和K O N I G在[ 6 ]中为DPO重写（关于图）设计了一个类似的框架，称为借用上下文重写（DPOBC）。最后[15]介绍了一个包含理论（遵循[7，8]的DPO最后一项最普遍的工作的结果适用于每一种粘合剂。 这意味着，给定一个粘附重写系统[12]的系统规范，可以生成一个具有相关互模拟同余的LTS而RSs和LTSs是系统状态之间的关系（族），DPO重写的并发理论关注的是转换之间的关系，即重写（参见例如[10，1]）。例如，连续两次应用规则←→W可能会导致图表 .这两次重写是连续的独立的，即人们可以交换它们而没有任何进一步的并发症;此外，人们甚至可以“同时”应用它们应用程序对应于并行规则的单个应用程序W→。与此相反，考虑一个咖啡自动售货机：它可以卖咖啡，然后拿铁咖啡macchiato或者以相反的顺序执行，但不是同时执行（除非你操作的机器有故障，会因为并发执行而产生一滩卡布奇诺咖啡）。 后一个示例解释了tw o CCSprocess esc$>|m<$andc′。m<$+m<$。c¯，其中每个元素都是均衡的到CCS的标准互模拟。 此外，前面讨论的生成的LTS不考虑这些细微差别的行为。本文的目的是对互模拟同余，尊重并发的生成。在这里，我们报告了在这个方向上研究的第一步。其主要思想是饱和一组给定的生产与所有并行的生产，然后应用借来的上下文方法来生成一个互模拟同余，尊重并发。更具体地说，给定一组初始规则，P，我们将创建一个卫星，P不会被用来协调我们在他那里的大小[15]的结果;P_j的成员可以并发地应用于相应的并行生产的P_J_p和D_v_w_y_一个核心问题是平行规则的适当概念。并行规则通常在DPO中被定义为余积;但这种构造不能在DPOBC中使用，因为在那里，匹配的态射必须是monic的。 在[10]中给出了所需的并行规则的概念，其研究了图的情况下使用monic匹配（DPOa/i）的DPO重写。然而，这项工作不能直接适应F. Bonchi，T.Heindel/Electronic Notes in Theoretical Computer Science 175（2007）5153SK1L1L2f1f2CK2E1E2w2SJK1R1L2K2FJ2E1D1E3w3我RL⎟因为其结果的证明取决于副产品，而粘合剂类别通常不具有副产品。2地方教会Rosser和DPOa/i的我们首先回顾[12]中提出的粘合剂类别中DPO 剩余时间在本节中，我们确定了一个粘合剂类别C，所有提到的物体和箭头都属于该类别。定义2.1（制作和重写）p的一个p是满足p=L<$−lK−→R的p，莫尼克湖 给定一个箭头f：L→C，我们说p重写（f，p）CtoDatmatchf，并且如果存在一个图中包含两个推出，如右图所示Ll Kr RfghCv Ew D在粘着范畴的借用语境理论中，我们只遇到匹配态射f是monic的特殊情况，因此从现在开始我们将假设所有的匹配都是monic的。图范畴中DPO重写的这一片段在[10]中被称为DPOa/i。他们的结果涉及强版本的顺序和平行的独立性。定义2.2（（强）并行和顺序独立性）设被给予生产pi=Li←−liK−r→i对于i∈{1， 2}，设（f1，p1）（f2，p2）（f1，p1）（fJ，p2）改写为D1=C=D2（C =D1==2==D）。 如果存在态射s和t（sJ和tJ），使得它们在下面的重写的合成图中可交换，则y是独立的。R1R2⎛⎜⎜1⎜F1⎜⎞R2β⎟⎟⎟D1w1不D2Cv1D不它们是强平行（顺序）独立的，如果w1≠t和w2≠s（v1≠t，J和w3J）是monic。在[10]中，对于图的情况，DPOa/i的证明定理已经被证明。然而，证据不能直接提升到粘合剂类别，因为它取决于副产品的存在。此外，文[12]给出的关于具有余积的粘着范畴的Chelelism定理并不转移到DPOa/i上。技术贡献其主要思想是用推顶替换图中这将使我们能够使[10]的DPOa/i理论可用于粘合剂类别。下一个定义将解释上积如何被推出所取代54F. Bonchi，T.Heindel/Electronic Notes in Theoretical Computer Science 175（2007）5121定义2.3设下列正方形为推出：Qx2x1A2A1我2我1一y2QY1B2B1。j2j1B然后我们用A1+ QA2表示A，用B1+ QB2表示B.设f1和f2是满足y1= f1<$x1和y2= f2<$x2的两个态射，f：A → B是满足f1<$i1=j1<$f1和f2 <$i2= j2<$f2的唯一态射，则f记为f1+ Qf2.对于初始对象0，表达式A1+0A2等价于A1+A2，对于f1+0f2和f1+f2也是如此。这种即同时进行。更具体地说，这两个规则需要在它们的只读部分的交叉点粘合在一起。定义2.4（并行生产）设p1=L1L1←−K1R1−→R1anddp2=l2r2x1x2L2<$−K2−→R2是一个子，K1<$−Q−→K2是一个子。如果所有对（l1<$x1，l2<$x2），（x1，x2）和（r1<$x1，r2<$x2）的推出都存在，则p1和p2在Q上的平行合成l1+Ql2r1+Qr2p1+ Qp2= L1+ QL2<$− K1+ QK2−→ R1+ QR2。如果涉及的三个推出图的态射都是幺一的，则称产生式p1 + Qp2是真的. 2现在我们准备好用公式表示主要定理，当我们在粘着范畴中使用DPOa/i这个证明依赖于[11]中的Butter Schmidt引理的一个修改版本，用于定理2.5（DPOa/i中的非线性和地方教会Rosser）l1r1l2r24Letp1=L1<$−K1−→R1anddp2=L2<$−K2−→R2是质子，并让L>f→−1CandL>f→−2C是态射。则以下是等价的。（f1，p1）（f2，p2）(i) 存在强并行独立重写D 1 <$=C =<$D 2。（f1，p1）（fJ，p2）(ii) 这是一个非常简单的等价条件，即C ==（f2，p2）（fJ，p1）(iii) 这是一个非常简单的等价条件，即C =D2==1==D。（f1+Qf2，p1+Qp2）(iv) 有一个重写C=[2]这个构造等价于[10]的定义9.5中给出的构造[3]由于[11]是一个相当难以接近的来源，我们选择给出整个证明。[4]不需要像[12]中所假设的那样，它们是线性的。F. Bonchi，T.Heindel/Electronic Notes in Theoretical Computer Science 175（2007）5155p当Q为p（b（k）K1→C时，即 Q= KK。2Q→K2）123结论和进行为了将现有的DPO重写的并发性理论扩展到DPO与借用上下文的交互式设置（DPOBC），我们定义了所需的并行产生式类型，并证明了DPOa/i在粘着范畴中的Local Church Rosser和Parallelism定理。除了填补文献中的这一空白，这些定理可能被证明是有用的，为未来的研究有关DPOa/i重写粘合剂类别。这不是不可能的，因为DPOa/i方法比DPO更直观，更有表现力，如[10]所示。事实上，DPOBC并不是唯一一个自然产生monic匹配需求的应用：例如，考虑粘合重写系统[2]和名义演算[9]的encondig过程的工作。我们将使用所提出的结果从一组给定的规则的并发尊重互模拟同余更具体地说，并行规则的构造将用于生成所有给定产生式的闭包，如下所示：给出一个预处理PweconnstructheclosurePiathe wrulesp∈Pp∈P<$p，pJ∈P<$K&<$−iQ>−→jp+QpJ∈P<$KPJ其中Kp表示规则p的接口，即给定规则p=X←Y→Z，我们将Y写成Kp。通常在借用的上下文重写和反应系统理论的更一般的设置中，LTS是使用规则集P导出的，而在这里我们使用P <$p p ppos e to us e P<$。在执行以下操作时，请将CCS文件从数据库中删除在这两个过程中，|mmndc。m<$+m<$。c。这种新的模式允许从[15]的borrow-dcont ext技术中的用户生成的信息同时与环境进行通信[−] |C.P |m.Qathechannesm andc（此相关内容适用于此位置）|m<$−−→P|Q）while the he lattercannnot（insignnsc. m<$+m<$。c<$−[−]|c−。P−z|-m-。→QP|Q）。还有其他几个互模拟的建议，尊重并发[4，3，5]，但他们是基于因果关系的概念我们的建议在概念上与这些不同，因为它不允许环境观察因果关系，而只是系统与环境同时相互作用的可能方式换句话说，我们认为系统是黑箱，而直觉上，现有的等价似乎通过观察因果依赖性打开了黑箱。重新设计我们的CCS示例，我们将提供类似的数据集|mmndc。m<$+m<$。这些过程与前一个过程具有相似性，但与后一个过程却不具有相似性，而所引用的文献的双相似性则区分了这两个过程，因为前一个过程可以独立地完成其转换，而后一个过程则不能。因果性和并发性之间的微妙相互作用，特别是在借用的语境重写的情况下，是正在进行的研究的主要兴趣56F. Bonchi，T.Heindel/Electronic Notes in Theoretical Computer Science 175（2007）51确认我们要感谢法比奥·加杜奇、乌戈·蒙塔纳里和匿名裁判对这篇论文的评论。引用[1] Baldan，P.， A. Coradini，H. Ehrig，M. L？we，U. 我是安娜和F。 Rossi，代数图变换的一致性，在 ： H 。 Ehrig ， H.-J. Kreowski ， U.Montanari 和 G.Rozenberg ， editors ， Handbook of GraphGrammars and Computing by Graph Transformation（1999），pp.107-188[2] Baldan，P.， A. Coradini，T.他说，B. KüonigandP.Sobocinski， Process s s e ses o radhesiverrritingsssstems.，n：L.AcetoanddA.Ing'olfsdo'ttir，editors，FoSSaCS，LectureNotesinComputerScience3921（2006），pp. 202-216[3] Baldan，P.，A. Corradini和U. Montanari，上下文网络的历史保持互模拟。，在：D. 伯特角Choppy和P.D. Mosses，editors，WADT，Lecture Notes in Computer Science 1827（1999），pp.291-310.[4] 贝德纳奇克湾一、遗传的历史保存互模拟或什么是未来的力量完美的程序逻辑，技术报告，波兰科学院，格但斯克（1991年）。[5] 贝斯特，E.，R. R. Devillers，A. Kiehn和L. Pomello，Petri网中的并发互模拟。，Acta Inf.28（1991），pp. 231-264。[6] H.和B。 K？oni g，D P O 应 用 程 序 中 的 Derivingbimu ation c o nconce esin c o n c e e DPoachgriting，in：Proc. of FoSSaCS '04（2004），pp. 151[7] Gadducci，F.和R. Heckel，An Inductive View of Graph Transformation。，在：F. Parisi-Presicce，编辑，WADT，Lecture Notes in Computer Science 1376（1997），pp.223-237.[8] Gadducc i， F.， R.他 叫 M. 事 实 上 ， 一 个 双 中 心 的 几 何 体 是 一 个 无 约 束 的 过 程 图 。 ， Electronic NotesTheoretical Computer Science 29（1999）.[9] Gadducci，F.和联合Montanari，通过过程的图形编码观察名义结石的减少，在：A。米德尔多普河谷vanOostrom，F.van Raamsdonk和R.C. de Vrijer，editors，Processes，Terms and Cycles，Lecture Notesin Computer Science 3838（2005），pp.106比126[10] 哈 伯 ， A. ， J.MüllerandD.PLUMP 、 DOUBLE-P 为 重 新 设 计 的 材 料 提 供 了 大 量 的 材 料 。 ，MathematicalStructures in Computer Science 11（2001），pp. 637-688.[11] Kreowski ， H. -J. ， “M an i pul at i one n v o n G r aph m an i pul at i onen ， “P h. D.sis ，TechnischeUniversitéatBerlin（1977）.[12] Lack，S.和P.Sobocin'ski，Adhesiveandquuasiadhesivecategories，TheoreticalInformaticsandApplications 39（2005），pp. 511-546[13] Leifer ， J.J. 和 R.Milner ， Deriving bisimulation congruences for reactive systems 。 ， 在 ：C.Palamidessi，编辑，CONCUR，计算机科学讲义1877（2000），pp。243-258[14] 是一个，维。 和P. 因此，Bocin'ski，使用2-C语言导出双镜像。，N ord. J. 开玩笑吧。第10（2003）号决议，第10页。163-。[15] 是一个，维。 和P. 因此，博奇因的基，反应系统是在COSPANS，N：PROC。 LICS'05（2005），pp. 311-320F. Bonchi，T.Heindel/Electronic Notes in Theoretical Computer Science 175（2007）5157B1A1f1X2一FBI1I2的1一一一个2J1J2e1Bee2的11（§）CCEA推广的Butter Cheryl引理引理A.1（一般黄油引理）Qy1x1y2一个2i1i2j1j2B2A1Qx1x2一个2Q一年二年B1B2C E（A.1）设上面是交换图，其中所有内部正方形和左正方形的边界都是推出，并且f：A→B，a：A→C和e：B→E是唯一的中介态射，使得j1<$f1=f<$i1j2<$f2=f<$i2（A.2）a1=ai1a2=ai2（A.3）e1=ej1e2=ej2（A.4）FinallyletC具有DiagramsB<$f−1的所有值的1A1−→F2C和B2←−一个2A2−→C。则对于任何态射c：C → E，下列是等价的。(i) 存在一个交换图（ii）该图A1A2AfBB1（乙）C（†）B2a e是一个推。其中，正方形（）、（†）和（）是推出。证据首先，我们证明蕴涵（i）成立。为此，将给定的图组合成一个图（见图F2f1一个2F2B1C1c（c）C2B2e1D1D1D2D2e2E58F. Bonchi，T.Heindel/Electronic Notes in Theoretical Computer Science 175（2007）51（A.5））。F. Bonchi，T.Heindel/Electronic Notes in Theoretical Computer Science 175（2007）5159接下来，我们需要检查ef=ca;为此，我们将使用i1和i2共同为epic，也 就 是 说 ， 它 足 以 表 明efi1=cai1和efi2=cai2都成立;这两个方程是可导出的使 用 第 （ i ） 项 、 公 式（A.4）、图表（A.5）、平方和公式（A.3）。换句话说，第（二）项的平方（§）是可交换的;它仍然表明它位于-这是推出的普遍性质。因此，假设有一个通勤图，（A.5）FA Ba（§）eC.（A.6）XH现 在 我 们 用 式 （ A.3 ） 、 图 （ A.6 ） 和 图 （ A.1 ） 推 导 出 ha1=kj1<$f1 和ha2=kj2<$f2。因为平方（ψ）和（†）是推出的，所以存在唯一确定的态射z1：D1→X和z2：D2→X，满足z1=hz2=h（A.7）z1<$b1=k<$j1z2<$b2= k <$j2.（A.8）使用等式（A.7）和Square（X）是推出的事实，我们导出恰好有一个态射z：E→X，使得zd1=z1和zd2=z2（A.9）稍等这个z是我们正在寻找的中介态射的候选者（见图（A.6））。进一步，我们用式（A.4）、图（A.1）、式（A.9）和式（A.8）推导出zej1=kj1和zej2=kj2然而，j1和j2是共同的epic，这产生ze=k。此外，还可以使用Square（square）表示zc=h等式（A.9）和等式（A.7），即我们有等式z∈ e = k和z ∈ c = h。（A.10）还需要证明z是唯 一的中介态射，即每一QX1X2y1i1i2A1A2y2f1f2的1一C一个2B1（）（†）B2FB1C1c（c）C2B2e1D1D1D2D2e2EJ1eJ2BCEK60F. Bonchi，T.Heindel/Electronic Notes in Theoretical Computer Science 175（2007）51的1一个2e1e2一个B1B21其他态射：E→X满足e=k和等于z。因此，假设给出了满足方程（A.11我们把现在我们推导出1：=（A.12）1使用公式（A.12）、项目（i）、公式（A.4）、公式（A.11）、公式（A.10）、项目（i）、公式（A.12）和公式（A.9）。进一步根据公式（A.12）、平方（A）、公式（A.11）、公式（A.10）、平方（A）和公式（A.9），可得出公式1c1=z1c1和公式2c2=z2c2利用方程（A.13）和方程（A.14），我们可以得出结论，因为对（b1，c1）和（b2，c2）是共同的epic，并且因为平方（f）和（f）是推出的。然而，使用方程（A.12）和方程（A.9），我们我还可以推导出，由于d1=z<$d1和d2=z<$d2，和D2是共同的Epic。其次，我们证明了蕴涵（ii）<$（i）。通过假设，我们有以下的交换图。的1I1一i2A2一C（A.15a）BJ1Bj2BeE（A.15b）进一步，我们构造了（f1，a1）和（f2，a2）对的推出，并将它们组合成下图QX1X2A1i1B1（乙）Ai2一C一个2F2（†）B2c1c2D1D2上面的三角形根据假设交换。现在我们用图（A.15 a）、正方形（§）、图（A.1）和图（A.15 b）推导出ca1=e1f1;方程ca2=e2f2也类似。 因此，存在唯一态射d1：D1→E和d2：D2→E，使得以下成立。d1<$b1=e1和d1<$c1=c（A.16 a）d2<$b2=e2和d2<$c2=c（A.16 b）f1的12F. Bonchi，T.Heindel/Electronic Notes in Theoretical Computer Science 175（2007）5161y1X1f1A1i1的1y2X2i2A2一个2F2C1B1D1c（c）D1K1H1EX1X2B1A1f1A2B2F2I1I2J1一J2FK1BKK2这还表明，平方Cc11E是一个pushout。为此，设有两个态射h1：D1→X和h2：D2→X，使得h1 c1= h2c2。（A.17）因此，在定义了k1：=h1<$b1和k2：=h2<$b2之后，由于图（A. 1）是可交换的，我们得到下面的可交换图（A. 18）。Q一一B1（乙）C（†）B2（A.18）X利用它的交换性和方程（A.17），我们导出k1<$y1=k2<$y2;因此存在唯一态射k：B→X，使得k1= k <$j1和k2= k <$j2。（A.19）此外，k1y1= k2 y2通过y 1的“展开”，意味着k1f1 x1= k2 f2 x2，y2，它为我们提供了一个唯一确定的态射u：A→X，使得k1<$f1= u<$i1和k2<$f2= u<$i2。（A.20）现在检查Q一年二年X我们看到k1<$f1=k<$f<$i1和k2<$f2=k<$f <$i2;因此d2d2C2B2D2d2h2K2D1C2D62F. Bonchi，T.Heindel/Electronic Notes in Theoretical Computer Science 175（2007）51kf=u（A.21）F. Bonchi，T.Heindel/Electronic Notes in Theoretical Computer Science 175（2007）5163从（A.20）中u的特征可以得出。然而，我们也可以导出k1<$f1=h1<$c1<$a<$i 1和k2<$f2=h2<$c2<$a<$i 2，其中nc e h1<$c1<$a=u（A=. 21）kf其中我们使用中介态射u的唯一性来导出第一个等式(see公式（A.20））。由于h1<$c1=h2<$c2，我们也得到h2<$c2<$a=k<$f。现在，由于Square（§）是一个推出，我们知道存在唯一的态射z：E→X，使得zc = hz = k， 其 中 h = h1<$c1= h2<$c2 。（A.22）这个态射z是我们正在寻找的中介态射的候选。为了证明它是唯一的，我们将使用b1和c1共同为epic来导出zd1=h1。现在利 用 Square （ § ） 和 （ A.22 ） 我 们 导出 z<$d1<$c1=h1<$c1; 进 一步 利 用（ A.16 a ） 、 （ A.15 b ） 、 （ A.19 ） 和 （ A.18 ） 我 们 导 出z<$d1<$b1=h1<$b1。这表明z<$d1=h1，加上必要的修改，z<$d2=h2;因此z是从E→X的中介态射。它仍然表明它是唯一的一个。设E→X是一个态射，使得d1= h1和d2= h2成立;我们必须证明d = z。利用平方（square）、假设和方程（A.22），我们推导出：如果k=k，则z=k也成立，因为e和c是共同的epic;因此，它仍然需要证明k=k。由于j1和j2是共同的epic，这足以表明，ej1=kj1和ej2=kj2。然而，我们可以推导出（见图（A.18），假设和图（A.1）），k1y1=ej1y1，并且作必要的修改后，k2y2=ej2y2。这就产生了一个唯一的箭头，使得ej1=k1，ej2=k2。扩展k1和k2的定义，我们得到了k1=k1，k2=k2，证明完成了。
