并行合成方程公理化的探索

理论计算机科学电子笔记162（2006）43-48www.elsevier.com/locate/entcs平行合成方程公理化的探索：现状与问题卢卡·阿塞托Reykjav'ık大学计算机科学系103Reykjav'ık，Iceland奥尔堡大学9220奥尔堡，丹麦万·福金克阿姆斯特丹自由大学计算机科学系1081 HV Amsterdam，荷兰摘要本文叙述了在过程描述语言中对并行复合算子的等式公理化的探索，以及在形式语言理论的经典领域中的类似结果。 并指出了一些尚待解决的问题关键词：并发，进程代数，CCS，互模拟，等式逻辑，Hennessy1到目前为止的故事由于它们被设计为允许描述和分析交互过程的系统，所有过程描述语言都包含某种形式的并行组合运算符（也称为合并），允许一个人将两个过程术语彼此并行。这些操作符通常交错其参数的行为，并允许它们之间的某种形式的同步。为1 电子邮件地址：luca@ru.is2 电子邮件地址：wanf@cs.vu.nl1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.07644L. Aceto，W.Fokkink/Electronic Notes in Theoretical Computer Science 162（2006）43例如，米尔纳的CCS对二元运算符进行了运算，|，其预期语义由以下Plotkin风格的经典规则描述[20]：μJμJαJα<$Jx→ xy→yx→x，y→yμJμJ（一）τJ JX|y → x | yX|y→x|yX|y→x | y尽管上述规则以非常直观的方式描述了并行合成运算符的行为，但该运算符的等式特征并不简单。在他们的开创性论文[14]中，Hennessy和Milner在大量其他经典结果中，在CCS的递归自由片段上给出了双模拟等价的完整等式公理化[19]。亨尼西和米尔纳提出的公理化使用所谓的扩展定律来处理平行合成--直观地说，这个定律允许人们获得一个描述两个项的平行合成的初始跃迁的项，这些项的初始跃迁是已知的。该定律可以表示为以下方程模式. ΣΣμ i x i |. ΣΣγj yj =ΣΣμ i（x i|y）+Σγ j（x|y j）+τ（x i|y j）i∈Ij∈Ji∈Ij∈Ji∈I，j∈J，μi=γj（其中I和J是两个有限索引集，μi和γj是动作），它只不过是描述并行组合的操作语义的上述规则的方程式。尽管它的自然和简单的公式，膨胀定律，然而，是一个方程模式与可数无限数量的实例。这就提出了一个问题，即并行复合算子是否可以通过有限的方程集合在双模拟语义中公理化。Bergstra和Klop肯定地回答了这个问题，他们在[3]中用辅助左归并算子和通信归并算子给出了归并算子的有限等式公理化Moller在[17，18]中表明，在没有左合并算子的情况下，强互模拟(The进程代数PA [3]包含一个基于纯交织而无通信的并行组合运算符-即由（1）中的前两个规则描述的运算符-和左合并运算符。因此，辅助算子确实是获得平行合成的有限公理化所必需的。在可能不太知名的论文[13]中，Hennessy提出了一种基于CCS类递归自由过程语言的观察一致性公理化[14]该公理化使用了一个辅助算子，表示为|/由Hennessy，它本质上是左和通信合并运算符的组合，因为它的行为由（1）中的第一个和最后一个规则描述。所提出的观测同馀公理化在前引书中已被提出。这是一个无限的，因为它使用了[14]中的扩展定理的变体。这导致Bergstra和Klop在[3，第118页]中写道：“It seems thatL. Aceto，W.Fokkink/Electronic Notes in Theoretical Computer Science 162（2006）4345(Inop. Cit. Bergstra和Klop用γ来表示Hennessy的合并。Bergstra和Klop的猜想已经被Ingolfsdottir，Luttik和我们在[ 2 ]中证实，通过证明，在存在两个不同的互补动作的情况下，不可能使用Hennessy的合并算子提供CCS模互模拟的递归自由片段的有限公理化|/的。我们相信，这一结果进一步加强了左合并和通信合并算子作为辅助算子在互模拟语义中并行组合的有限等式表征中的地位。2未来一个可能的，尽管很有偏见，试图预测未来发展的方式沿着上述调查的研究路线是陈述我们目前正在试图解决的一些问题。开放问题1我们相信在这一点上要问的一个自然问题是是否存在一个保持互模拟等价的二元运算符，并且其除了CCS的递归自由片段，允许并行组合的有限等式公理化-参见[1，问题8]。我们推测，没有这样的操作符存在，因此，使用两个辅助操作符是必要的，以实现一个有限的公理化的并行组合互模拟语义。这一结果将使我们为Bergstra和Klop提出的算子的规范地位所寻求的定义目前，对这一猜想的某种形式的确认工作正在进行中，我们希望在不久的将来在其他地方报告这一情况。此时此刻，我们甚至还不清楚这个猜想的一般形式是如何建立起来的。如何证明在互模拟语义中，没有一个单一的二元很可能有强大的结果从通用代数和equa- tional逻辑是未知的，我们可以承担这一行的工作，但一些文献综述和查询通用代数邮件列表还没有发现任何答案前一节中提到的肯定结果都是关于公理系统的，当这些公理系统被限制为不包含变量出现的项时，这些公理系统是完备的关于具有ω-完备的并行复合算子的过程语言的行为等价的等式公理化知之甚少[12，16]中给出了早期的ω-完全公理化。最近，Fokkink和Luttik在[10]中证明了进程代数PA [3] a服从一个ω-完全公理化，如果底层的动作集是有限的，那么它是有限的。公开问题2在包含同步并行合成的进程代数上寻找双相似性的ω-完全公理化，例如，关于ACP第1节中提到的否定结果都是在强互模拟语义的背景下建立的。也许令人惊讶的是，更少的是已知的设置的一致性，抽象的内部步骤的过程行为。例如，在无递归的情况下，观察全等是否是可无限公理化的？46L. Aceto，W.Fokkink/Electronic Notes in Theoretical Computer Science 162（2006）43CCS的碎片答案当然是否定的，但我们仍然缺少对这一事实的证明！这使我们指出：公开题3证明了在递归、重标号和无限制的CCS上，观测同余没有有限的等式公理化。事实上，正如van Glabbeek最近在Concurrency上发表的一篇文章中所指出的那样，邮件列表，这可能会举行在一个更强大的形式。也就是说，人们可能试图证明这个否定的结果对于该语言的所有扩展都是正确的，并且具有GSOS操作的任何有限集合。(Note在观测一致性的设置中，左和通信合并运算符的操作语义使用前视。因此，这两个运营商不是全球SOS业务。许多开放的问题仍然存在，特别是在寻找丰富的过程描述语言的ω-完全公理化，但本文的空白太小，无法列出所有问题。3形式语言理论的传承在形式语言的历史悠久的理论中，并行组合作为shu_e运算符出现。毫不奇怪，舒氏的等式理论在文献中受到了相当大的关注在这里，我们仅限于提及一些与过程论有特殊关系的结果。在[22]中，Tschantz给出了连接和shu-e上的语言理论的一个有限方程公理化，解决了Pratt提出的一个公开问题。在证明这一结果时，他基本上重新发现了pomset的概念[21]--一种基于偏序的并发模型，其代数方面已经由Gischer在[11]中进行了研究--并证明了串并行pomset的方程理论与连接和shu_e语言的方程理论相一致Tschantz所采用的TschantzGischer和Tschantz的公理化后来在[9]中被推广到一种具有级联和并行复合算子的ω幂的二排序语言。然而，由于这些迭代算子的增加而产生的pomset代数的公理化必然是有限的，因为，如上文所示。 前引书没有一个有限的等式集合能够捕捉到所有涉及它们的合理Moller关于CCS和PA的无递归片段上无左归并的互模拟等价性的非有限公理化的结果文[17，18]中给出的算子被文[4，6，8]中给出的算子定义在形式语言理论中。首先，Bloom和E′sik提供了这些信息，有效的不等式在代数的语言配备了连接和shu ehavenof iteb as is。在[8]中，我们知道，所有的问题都是这样的L. Aceto，W.Fokkink/Electronic Notes in Theoretical Computer Science 162（2006）4347关于语言上的并、连接和变换的所有有效不等式的集合，相对于对连接和变换成立的所有有效不等式的集合没有有限的一阶公理化因此，某种形式的平行组合、排序和选择的组合很难在语言理论中用等式来描述而且我也有很多的工作要做。更重要的是，Bloom和E's在[6]中已经显示了这一点，一个有限字母表上的所有语言的多样性通过包含连接和shu_e的操作符而排序，并且表示仅包含空词的单例语言的常数不能通过在连接，联合和shu_e上的语言的等式理论中有效的一阶句子来无限地公理化在并行理论的背景下建立类似的优雅和力量的结果将是一个挑战，我们希望我们的研究社区的一些成员会遇到。引用[1] L. A CETO，Some of my favorite results in classic process algebra，BRICS Report NS-03-2，BRICS，Department of Computer Science，Aalborg University，2003年9月。[2] L. ACETO，W. FOKKINK，A. INGOLFSDOTTIR和 B. LUTTIK，CCS与Hennessy的合并没有有限的等式公理化，理论计算。科学，330（2005），pp. 377-405[3] J.B ERGSTRA和J. W. KLOP，同步通信的进程代数，信息与控制，60（1984），pp. 109-137[4] S. L.B型织机和Z.E'SIK，Nonfiniteeaxiomatizabilityofshueinqualities，inProceedingofTAPSOFT'95：软件开发的理论与实践，第六届国际联合会议CAAP/FASE，奥胡斯，丹麦，1995年5月22-26 日 ， P. D 。 Mosses ， M. Nielsen 和 M. I. Schwartzbach ， eds. ， 卷 915 计 算 机 科 学 讲 义 ， Springer-Verlag，1995，pp.318-333[5]文，语言簇中的自由shu_e代数，定理，计算。科学，163（1996），pp. 55-98.[6]，公理化语言中的“数”与“连接”，Inform.和计算，139（1997），pp. 62[7]，用偏序集运算生成的语言变种，数学。科学，7（1997），pp. 701-713[8] Z. E的 IK和M。 BERTOL， Nonfiniteaxiomatizailityoftheequationaltheeor y ofshue， ActaInform.， 35（1998），pp. 505-539[9] Z. 是的。 OKAWA ， Ser iesand d paraleloperationsonpomsets，inProceedingsoFoundationsofSoftwareTechnology and Theoretical Computer Science （ Chennai ， 1999 ） ， vol. 1738 of Lecture Notes inComput. 科学，Springer-Verlag，Berlin，1999，pp.316-328[10] W. FOKKINK和B. 刘文，交错式的一种ω-完全方程规范，第27届自动机、语言和程序设计学术讨论会论文集，日内瓦，美国。蒙塔纳里，J. Rolinn和E. Welzl编，第1853卷，《计算机科学讲义》，Springer-Verlag，2000年7月，729-743[11] J.L. GISCHER，pomsets方程理论，理论计算。科学，61（1988），pp. 199-224。[12] J. F. GROOTE，证明ω-完备性的新策略第458卷，Springer-Verlag，1990年，314-331[13] M.吴文，有限并发过程的公理化，北京：计算机科学出版社，17（1988），pp. 997-1017[14] M. HENNESSY和 R.李文，非确定性和并发性的代数学定律，计算机科学与工程学报。马赫数，32（1985），pp. 137-161。[15] R. 李文，通讯与并发，北京：计算机科学出版社，1999。48L. Aceto，W.Fokkink/Electronic Notes in Theoretical Computer Science 162（2006）43[16] F. M OLLER，并发公理，博士论文，爱丁堡大学计算机科学系，1989年7月。CST-59-89号报告。也作为ECS-LFCS-89-84出版。[17]左归并算子在进程代数中的重要性，第17届 ICALP会议论文集，Warwick，M。Paterson，编，卷443计算机科学讲义，Springer-Verlag，1990年7752-764。[18]，CCS同余的有限公理化的不存在性，第五届计算机科学逻辑年会论文集，费城，美国，IEEE计算机协会出版社，1990年，页。142-153。[19] D. Park，Concurrency and automata on in finite sequences，in：P. Deussen（Ed.），第五GI会议，卡尔斯鲁厄，德国，计算机科学讲义第104卷，Springer-Verlag，1981年，第104页。167- 183。[20] G. 李文彬，操作语义学的结构化方法，国立台湾科技大学，1998。[21] V.PRATT ， Modeling concurrency with partial orders ， InternationalJournalofParallelProgramming，15（1986），pp. 33比71[22] S. T. T SCHANTZ，连接下的语言和shu schanting，计算机科学中的数学结构，4（1994），pp. 505-511