进程代数中的几何方法及其应用

理论计算机科学电子笔记162（2006）183-190www.elsevier.com/locate/entcs关于过程Clemens Grabmayera，1，2 Jan Willem Klopa，b，c，3 BasLuttikd，c，4计算机科学荷兰阿姆斯特丹自由大学b荷兰奈梅亨大学计算机科学系cCWI，阿姆斯特丹，荷兰d荷兰埃因霍温理工大学数学与计算机科学系摘要本文讨论了进程代数的几何方法。我们主要提出问题，尚未能提供重要答案。保留字： 进程代数，进程图，几何，周期，堆栈，包，队列。1周期过程我们的出发点是表1中的公理系统BPA和保护递归。我们对非线性递归特别感兴趣，其中允许递归变量的乘积，与线性递归相反，X| X = aY + b，Y = cX + dY，只产生正则（有限状态）过程。非线性递归还允许有限状态进程，例如计数器|C = uDC，D = uDD + d（动作u，d表示“向上”和“向下”）或过程堆栈，它可以由BPA上的线性递归方程的无限集合定义（参见图10）。表2的左手边），更值得注意的是，通过非线性递归方程的有限集合（参见。表2的右侧）。这个简单的框架已经具有丰富的结构。在[1]中，这个框架与上下文无关语法（CFG）联系在一起1这篇文章是在作者受雇于NWO项目GeoProc时写的（“过程的几何学”，第113号）。612.000.313）。2 电子邮件地址：clemens@cs.vu.nl3 电子邮件地址：jwk@cs.vu.nl4 电子邮件：s. p. tue.nl1571-0661© 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.111184C. Grabmayer等人/理论计算机科学电子笔记162（2006）183x+y=y+xx+（y+z）=（x+y）+zx+x=x（x+y）·z =x·z+y·z（x·y）·z =x·（y·z）Sλ= 0·S0+1统计S1Sdσ = 0· S0dσ +1· S1dσ +d· Sσ(ford= 0或d= 1，且任意字符串σ）S =T·ST = 0·T0 +1统计1T0 =0+T·T0T1 =1+T·T1表1BPA（Basic Process Algebra）表2堆栈，无限线性和有限非线性BPA规范Greibach范式在那里，事实是成立的，而语言平等问题的CFG的先验地说，这并不令人难以置信，因为一个过程比一种语言（它的有限终止痕迹的集合）有更多的内部Baeten，Bergstra和Klop在[ 1 ]中证明了可判定性，作为关于相应过程图的周期几何或拓扑的结果的推论。在图1中，展示了两个例子的周期性：左侧的堆栈和过程的周期性。|X = bY + dZ，Y = d+ dX + bYY，Z = b + bX + dZZ在右侧（该图重复了三个有限图片段α，β和γ，如下图2所示）。Fig. 1.树状周期过程[1]中的几何证明是复杂的。对于可判定性的推论，随后通过使用表格方法 和 规 则 项 发 现 了 更 多 的 流 线 型 方 法 （ 参 见 。 Cauca l in[7] ， Huétte landdStirlingin[11]，anddGroote in [10]）.此外，几何方面的研究，例如由Caucal在[8]和Burkart，Caucal和Ste Eschen在[5]。事实上，相关C. Grabmayer等人/理论计算机科学电子笔记162（2006）183185Muller和Schupp [12]早在1985年就提出了上下文无关图的概念。我们认为，仍然有很多需要解释的几何方面的过程图。我们提出了一个问题，关于BPA中的周期图分为两种：图2问题1.1一个方程组E（在格雷巴赫规范形式中）是否产生一个线性（I型）或分支（II型）图是可判定0123456图二. ‘Linear’ periodic graphs (type I, left), ‘branching’ periodic graphs (type II,另一个类型II的图是图3中的递归BPA -specification.xml中的“butterfly”过程图。|X = a + bY + fXY，Y = cX + dZ，Z = gX + eXZ。I型和II型图之间的区别的相关性是明确的图三. 一个下面，为了表明某些图不是类型I或类型II。在BPA可定义图的研究中，一个重要的性质是“赋范”。一个图是赋范的，如果从它的每个节点都有一条路到一个终止节点。(In术语重写术语这被称为弱归一化属性WN。一个节点的范数则是到终点的最小步数最初，上下文无关过程（BPA-可定义过程）的可判定性一C一D一CBDC一CBDBBC一DB186C. Grabmayer等人/理论计算机科学电子笔记162（2006）183[1]只有一种情况，即在正常情况下。随后，Christ ens en、Huéttel和Stirlin gin[9]将其推广到所有BPA-定义一个bl e process es。注意，进程图中的节点的范数在互模拟下保持不变：如果通过用水平“水平”线绘制过程图，将具有相同范数的点布置在相同水平上（参见图2中的左图和图3中的图）来形象地表示范数，则互模拟仅与水平线上的点相关。将一个赋范图折叠到它的标准形是一个水平方向的压缩。一个重要的问题是BPA定义的过程是否在最小化下是封闭的（即，在压缩图使得它在互模拟下是最小的情况下;所得到的图也被称为这种说法是否真的成立的问题在[1]中没有解决。使一个图规范化可以大大改变它的几何形状。例如，考虑上面提到的计数器C。C的进程图g是节点C、DC、DDC、...的线性序列。由向右的U 形台阶和向左的D 形台阶连接。进程代数PA 中的mergeCC有一个类似于图6中左边的进程Bag的网格图。但是，如果我们通过识别对角线上的双相似节点来将C∈ C的图g折叠到它的标准型，我们再次得到C的图g所以一个网格可以折叠成一个线性图。当图被压缩到它们的标准形式时，规范性起着一定的作用。在[5]中，Burkart，Caucal和Ste Escheren给出了以下BPA-图的例子，该图在压缩到标准形式之后不再是BPA-图：对于具有递归定义的过程，|Z = aAZ+cD，A =aAA+cD+b，D = dD在BPA中，图4中左边的图是其相关联的BPA-过程图，而右边的图是相应的最小化，其不具有BPA -图的周期性结构。请注意，这两个图都不是赋范的。见图4。 最小化条件下BPA问题1.2如何刻画那些标准图又是BPA-图的BPA -图？我们注意到，问题1.2已经在Caucal的工作中得到了相当多的关注与上面给出的非赋范情况的反例相比，[7]他证明了下面的定理。定理1.3（Caucal，1990）赋范BPA-图类在极小化下是闭的.在[ 1 ]中首次提到了CFG和BPA可定义过程之间的（明显）联系图1和图2中右侧的图就是一个示例C. Grabmayer等人/理论计算机科学电子笔记162（2006）183187上面：它确定为上下文无关语言（CFL）的语言的单词具有相等数量的字母b和d。下面是一个耐人寻味的问题问题1.4CFL的经典泵浦引理与BPA可定义过程中的周期性有何图五. 语言L。另一个有趣的观察，由于H.P. Barendregt，如下。众所周知，语言L ={a nb n c n|n≥ 0}不是CFL。这种语言可以作为图5中的三角形无限极小图的有限迹的集合来获得。直觉上很明显，这个图不是树状周期的。这就引出了下一个问题。问题1.5图5中的图不是BPA-图（当严格建立时）的事实是否可以用来得出L不是CFL的结论，应用CFL和BPA中的可定义性之间2BPA中袋由BPA公理定义的运算的表达能力是有限的;基本上只能定义顺序过程公理系统PA是BPA的一个扩展，包含了合并运算符（交织）和辅助运算符（左合并）的公理在PA中，我们对进程Bag（over data）有一个简洁的递归定义{0， 1}）如下：B= 0（0 B）+1（1 B）。Bergstra和Klop在[3]中证明了Bag过程不能用BPA上的有限递归规范来定义。考虑到图6中的最小流程图，这并不奇怪：不是树状的，而是“网格状”的。下面我们给出这个事实的另一种证明。定理2.1（Bergstra，Klop，1984）Bag不是BPA可定义的。证明（草图）假设过程Bag是BPA可定义的。那么在BPA中存在一个递归规范E，使得Bag是双相似的，具有树型周期188C. Grabmayer等人/理论计算机科学电子笔记162（2006）183见图6。过程Bag的最小过程图（在左侧）和Bag的终止变量Bag t的最小过程图（在右侧）。图g（E）是Baeten，Bergstra和Klop在[1]中定义的图。则g（E）是根据[ 5 ]中使用的术语的5在[5]中，Burkart，Caucal和Ste Becaen证明了，对于每个BPA-图G，G的标准图是“模式图”，这意味着它可以根据确定性（超图）语法通过长度为ω的约简序列从有限（超图）[6]由于Bag本身是一个标准图，因此Bag是BPA-图g（E）的标准图，因此Bag是一个模式图。Caucal在[8]中的一个定理指出，根据Muller和Schupp在[ 12 ]中的定义，所有有限度的（有根）模式图都是7由此可见，Bag是上下文无关的。然而，根据[12]中的定义，验证Bag实际上不是上下文无关图这样，我们就得出了一个与我们的假设相矛盾的结论，即Bag可以用BPA来定义。Q通过使用Caucal例如，对于Bag的终止版本Bagt（其中Bagt被赋范），其过程图在图6中的右侧，可以如下推理这个图是规范的，所以如果它是BPA可定义的，那么它将是I型或II型图。然而，对于I型图，它认为球面B（s，ρ）中的节点数线性依赖于ρ，其中s是中心，ρ是半径;对于II型图，这种依赖性是指数形式的。但对于所考虑的图，球B（s，ρ）中的节点数仅二次依赖于ρ。因此，该图不是BPA可定义的。[5]在Caucal的早期论文（例如[6]和[8]）中，BPA-图被称为“字母图”。[6]根据Caucal和Montfort在[ 6 ]中使用的这个定义的因为“regular”属性的使用因为流程图可能导致错误的关联，所以我们在这里避免使用（超）图重写中的术语。[7]请注意，Muller和Schupp定义中的“上下文无关”图类C. Grabmayer等人/理论计算机科学电子笔记162（2006）183189ΣQ = Qλ =d∈ Dr1（d）·QdΣQσd =s2（d）·Qσ +e∈ Dr1（e）·Qeσd(ford∈D，且σ∈D<$）ΣQ =d∈ Dr1（d）（ρc3→s2<$H）（ρs2→s3（Q）<$s2（d）·Z）ΣZ =d∈D r3（d）·Z在最小化的情况下，我们在哪里需要保持BPA的可定义性袋t的过程图显然不是通过BPA定义获得的过程图，因为它不是I型或II型但是这里考虑的是过程的等价性模互模拟--所以不难想象存在Bagt的BPA定义E，使得在压缩到规范形式之后g（E）可以（g（E））就是图6中右边Bagt的过程图（Bagt）。所以可以（g（E））= graph（Bagt）保持。但由于保持性质，定理1.3，我们有can（g（E））=g（EJ），对于某些BPA-规范EJ，因此g（EJ），因此图（Bagt），是I型或II型的，quodnon。3队列的奇怪几何在范式过程Stack和Bag之后，我们现在转向第三个范式过程Queue（具有无限容量的先进先出版本）。表3给出了无限BPA规格。表3队列，无限BPA-规范和以前一样，我们的努力是以有限的方式指定队列。Bergstra和Tiuryn [4]证明了系统BPA不足以做到这一点;事实上，他们证明了队列甚至不能在具有握手通信的ACP中定义（参见[2]对公理系统ACP的完整处理）。 但队列有一个在ACP中使用重命名操作符的有限递归规范（参见表4，该规范最初是由于Hoare使用表4队列，有限ACP-指定重命名下面是一个雄心勃勃的问题问题3.1是否存在可由握手通信定义的过程的几何（拓扑）性质？最后，我们转向进程队列的几何性质。令人惊讶的是，以一种“整洁”的方式绘制队列的过程图是出乎意料的问题（参见。也见图7），类似于堆叠和袋。我们想揭示这种困难的问题3.2在二叉树空间中是否可以拟合g190C. Grabmayer等人/理论计算机科学电子笔记162（2006）183引用见图7。 尝试在“树空间”中绘制队列[1] 贝滕，J. C. M.，J. A. Bergstra和J. W. Klop，Decidability of bisimulation equivalence for processgenerating context-free languages，Journal of the ACM40（1993），pp. 653-682.[2] Baeten，J.C. M. 和W.P. Weijland，[3] 伯格斯特拉，J. A.和J. W. Klop，递归定义过程的代数和正则过程的代数，在：J. Paredaens，编辑，ICALP82比95[4] 伯格斯特拉，J. A.和J.Tiuryn，队列的进程代数语义，Fundamenta InformaticaeX（1987），pp. 213-224。[5] Burkart，O.，D. Caucal和B. Ste Escheren，互模拟崩溃和过程分类学，在：U。Montanari and V.Sassone，editors，Proceedings of CONCUR247-262.[6] Caucal，D.和R. Montfort，On the transition graphs of automata and grammars，in：Proceedings ofWG 90，LNCS484（1990），pp. 61-86号。[7] Caucal，D.， Graphecanoniquesdegraph e salg'ebriques，Theoret. 为了我。 和Appl. 24（1990），pp. 339[8] Caucal，D.，关于前缀重写的规则结构，理论计算机科学106（1992），pp。61-86号。[9] Chris te nse n，S.，H. Hütte landC. Stirling，Bisimulationeuivalenceisdecid ablefo r alcontext-freeprocesses，Information and Computation 121（1995），pp. 143比148[10] Groote，J.F.、A short proof of the decidability of bisimulation for normed BPA-processes，Information Processing Letters42（1992），pp.167-171。[11]Hüttel，H. 和DC。 Stirling，ACtionspekloude r thanwords：Provingbisimilarityforcontexfreeprocesses，in：Proceedings of LICS'91，1991，pp. 376-386.[12] Muller，D. P. Schupp，The theory of ends，pushdown automata，and second order logic，TheoreticalComputer Science37（1985），pp. 51比75