ACP型进程代数：理论发展和设计原理

理论计算机科学电子笔记162（2006）79-85www.elsevier.com/locate/entcsACP型进程代数简·A Bergstraa，b，1一 荷兰阿姆斯特丹大学理学院程序设计研究组b荷兰乌得勒支大学哲学系应用逻辑小组摘要回顾了ACP风格进程代数的设计原理。在给定的范式的未来发展方向的大纲。保留字：进程代数，ACP，等式表示1过程代数这不是一个历史性的文件在任何意义上，并故意不试图追溯事实，发展或评论回到文献。事实上，这些联系和参考对于任何试图这样做的人来说都很容易找到ACP（1984）作为进程代数的等式表示的设计来自几个来源，并且在技术上代表了抽象数据类型的代数规范的传统，因为它从60年代后期开始被各种研究小组研究。从非加太国家方案的发展一开始，下列理论发展的备选方案和目标就发挥了核心作用：• 该理论在本质上类似于形式语言理论（Kleene代数），但更一般的是去掉了它的一个定律：交替复合优于顺序复合的右分配性。顺序组合和交替组合已经从形式语言理论中作为行为的基本组合子。这一决定对所有进一步设计阶段的结果具有决定性的影响。同时也是工艺代数设计的参数1电子邮件：janb@science.uva.nl1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.10580J.A. Bergstra/Electronic Notes in Theoretical Computer Science 162（2006）79在这个阶段做出的不同决定导致了其他并发理论，与ACP线相当，但在技术上不在ACP线之内。• 公理系统是以这样一种方式设计的，即模型的概念总是可以在预先存在的逻辑理论中找到。事实上，它总是表面上考虑公理系统作为理论在一些经典已知的逻辑，并在大多数情况下，这是一些片段的一阶逻辑与塔斯基语义作为其概念的模型。• 方程理论的丰富链（或者更确切地说树）的设计，提供了一个增量的特征，如BPA，PA，ACP，ACP与状态算子，或者相同的规范，每个扩展有一个死锁的步骤（delta），一个沉默的步骤（tau）或一个空的步骤（tau）或两者兼而有之。通过考虑在数学上共存而没有困难的特征集合，可以避免特征交互例如，将优先算子与弱互模拟相结合被证明是困难的，这导致了1998年左右的正交双模拟。这些方程理论链的灵感来自于量和数的数学理论：群、环、场、斜场等等。对于每个特征族（总是包括顺序和交替组合的BPA特征），首先要突出三个设计目标：· 首先，将设计一个捕获（强）互模拟语义的进程代数。· 方程必须是这样的，除了顺序组成和替代组成之外，所有的组成都可以在有限项上消除。(The整个主题在目标中找到它的根，以使用该目标的最弱公理找到并行合成的消除结果。· 如果可能的话，避免变量绑定机制，有时会付出很大的代价，因为这些机制偏离了构成抽象数据类型的等式规范的基石的通用代数背景。• 每个特定的特征集（操作符）通过方程或必要时通过条件方程给出初始代数规范。优选地，这些方程以这样的方式组织，使得也可用作项重写系统。只要有可能，就可以精心设计和使用有限的方程组，如果需要，还可以设计辅助函数（如抽象数据类型规范理论中所知）。证明这种辅助操作员确实是必要的，已经在许多情况下证明是可能的。显然，导出这样的负信息要比为其特定目的设计辅助算子困难得多。对有限指定的搜索导致了诸如左合并（有时是右合并）和通信合并之类的运算符，用于指定优先级运算符的unless运算符以及用于ACP定时版本的丰富辅助运算符集合。• 明确使用初始代数的不同同态像，可以获得一系列由特定规范指定的特征的语义模型。可以引入额外的方程来表征这样的同质图像。J.A. Bergstra/Electronic Notes in Theoretical Computer Science 162（2006）7981• 具体的和抽象的特点是区别的，在某种形式的抽象功能抽象的活动，而具体的过程代数允许计数的每一步。对于具体的过程代数，可以使用应用于近似代数的投影极限构造来找到模型，这些近似代数被发现是有限过程的初始代数的同态图像，通过在固定数量的步骤之后切割每个过程这种投射极限构造为大多数ACP风格的进程代数规范提供了最简单的语义模型。投射极限可以使用初始代数语义和它们的近似代数来理解，并且不需要偏离（结构化的）操作语义或任何互模拟定义。然后可以证明，基于SOS的互模拟模型实际上是等价的。我认为投影极限模型的建设作为主要来源的直觉过程等价的情况下，具体的它可以在由于特征的复杂组合而难以开发适当的互模拟定义的情况下工作。一直很难准确地描述ACP风格的过程代数所捕获的内容。这在某种程度上是一个主观问题。我自己的观点是，ACP风格的进程代数打算以泛代数和等式逻辑的经典格式讲述（或者说是一个）此外，对替代成分的解释是非常重要的，因为替代成分的含义可能因上下文而异。从纯粹的内部选择的自主代理人的纯粹的外部选择感觉到一个键盘感应其用户，许多形式的或多或少的约束选择之间和ACP风格的过程代数应该构成一个媒介，这种范围内的机制的替代成分可以在某种程度上共存精心挑选的模型的公理系统。作为一个例子，可以提到公平抽象的处理，其中一个选择可以无限地经常重复以有助于其意义的事实。2进一步发展自从它被引入以来，ACP风格的进程代数已经在许多方面得到了发展，对此我将给出一个简要的综述。2.1时空一个丰富的家庭的定时扩展已被设计导致混合形式的进程代数。在这些时间代数中，使用了某种形式的变量绑定，特别是初始抽象和积分。已经证明，可以使用圆柱代数来处理大的总和（替代组合），但这些发展在可读性方面付出了代价。这方面有很大的发展空间。一个悬而未决的问题是重新设计真实空间ACP（三维空间中的定时ACP），使方程和验证与狭义相对论一致毕竟，如果A82J.A. Bergstra/Electronic Notes in Theoretical Computer Science 162（2006）79如果观察到通信协议正确地工作，那么从另一个惯性系统也应该认为它是正确的。对于协议的规范和验证，都应该假设洛伦兹不变性。然而，接下来的观察是，ACP似乎与狭义相对论不一致，如果要达到这一目标，需要进行重大修改。不同地说：ACP只涉及经典力学中的并发。2.2关于过程代数的非平凡的结果已经获得的因式分解的过程中的并行组件和一系列的结果已经获得有关的可判定性互模拟等价和其他等价的过程符号与递归或组合子，产生无限的行为（例如，正确的二元Kleene星，这是Kleene最初定义它的方式的重复2.3图式与SOS一个重要的发展是不同SOS格式的同余定理的图式。目前，关于ACP风格进程代数的大多数简单语义事实都可以从与算子定义形式相关的非常一般的性质中推导出来。在这一领域有足够的空间进行进一步的工作，因为就目前而言，使用显式图模型和专用互模拟定义比通过SOS的一般然而，这种基于SOS的Meta理论在很大程度上定义了理论发展和呈现的稳定终点，因此，它构成了一种发展，这种发展将遵循以老式风格完成的ACP家族的每个设计扩展。具有回溯互模拟的回溯条件构成了这种状态的一个当前示例。另一个例子是带信号的ACP。2.4真正的并发性和数据类型非交错进程代数已经被设计出来，关于ACP风格进程代数与抽象数据类型的交互，已经开发出了大量的信息。我一起讨论这些，因为已经确定，在ACP变体中建模真正的并发理论涉及以历史指针的形式引入自然数。其他实现真正并发的方法需要引入局部性，这些局部性也是数据的形式。从表面上看，人们可能会认为ACP与使用初始代数语义指定的抽象数据类型愉快地 但在一个更密切的解释，这是失败的情况下，因为ACP风格公理总是需要充分的信息，平等和不平等的类原子的行动，作为最重要的参数。此外，尽管在将流程和数据以规范格式PSF和μCRL组合方面有着丰富的经验，但仍然存在不对称性：流程代数部分对操作符集非常具体J.A. Bergstra/Electronic Notes in Theoretical Computer Science 162（2006）7983对于将要使用的过程，而数据部分对于要在数据上使用的运算符是完全自由的。因此，相同的事实必须一次又一次地从本质上相同的数据类型的边际变化中推导出来，并且未能出现一种令人信服的策略来积累数据类型的事实、定义和运算符。这一困难的真正性质以及最佳解决方案仍然很难理解。换句话说：可以理所当然地认为，一系列进程代数设计会导致可靠的进程理论，但抽象数据类型规范的理论无法提供数据理论。抽象数据类型理论存在于上述SOS一致性理论的图式学的抽象层次上。但是，要找到一个更具体的抽象数据类型理论已经证明是非常困难的。在组合的形式主义中，进程和数据的角色之间的差异的更深层次的原因可能是，在数据类型中隐藏一种复杂性已经变得很普遍，而这种复杂性在进程代数中根本不愿意出现。例如，具有过流和错误甚至错误恢复机制的有限堆栈在任何ACP风格的进程代数中都没有对应的机制。有人说，堆栈作为一种抽象数据类型的概念是令人敬畏的，因为堆栈不是一些很好理解的等式理论的模型。3如何进行？在各个方向上，ACP风格的进程代数的发展可以进一步推许多开放的问题和开放的结局仍然存在。将这些技术应用于协议和系统验证，无论是通过形式化的方程证明还是通过模型检查，都还有很大的进步空间。这一进展也可能导致有用的应用。很明显，ACP风格的进程代数与其他演算（如π演算和移动环境演算）之间的差异比人们预期的要大。移动环境似乎是如此的不同，以至于它不能被理解为一个在ACP之上设计的功能或任何合理的扩展。另一方面，对于移动性，这是一个未解决的问题。像π-演算中出现的那些移动特征可能有ACP风格的对应物，如果没有的话，这是一个相当有趣的事实，应该提供形式化和证明。3.1程序代数、线程代数与毛雷尔计算机我个人的计划是继续为程序、系统和计算机设计代数，非常接近于为ACP制定的路线，但强调不同的方面。程序代数及其相关的线程代数是该工作线的最新成果。当规范变得更复杂，语义问题变得更难分析时，与进程代数的联系就出现了。事实上，程序代数和线程代数是如此简单，因为已经作出了严格的限制。但当编写线程、程序和机器84J.A. Bergstra/Electronic Notes in Theoretical Computer Science 162（2006）79所得到的系统变得更加复杂，并且程序代数和线程代数的简化有时成为障碍而不是资产，这可以通过向进程代数的转换来消除。线程代数应该在编程语言语义学中找到它的应用，此外，在网格计算中，并发的主要形式是通过多线程的方式呈现的，在并发微处理器的理论中，不同形式的多线程，特别是微线程，有望为微处理器的摩尔定律的长期生存做出贡献在进行微处理器设计时，一定需要一些计算机（处理器、机器）理论。我得出的结论是，毛雷尔的计算机和计算机指令理论（从1967年开始，从那时起就被忽视了）提供了我所需要的格式。这个理论被故意设计成偏离图灵机，并且这样做是如此彻底，以至于需要由多线程驱动的Maurer计算机的无限并行组合多流水线处理器设计的详细语义研究，既有利于潜在的进一步处理器加速的系统化的解释，也有利于利用流水线组织的改进所需的编译器开发。幸运的是，Maurer计算机提供了程序代数和线程代数的完美匹配，并提供了有用的选项，可以将更大的系统描述转换为合适的进程代数3.2网格与Web现在我们都通过网络共享数据，下一阶段是通过网格共享处理。对网格计算的日益重视将导致大量新的和复杂的通信和安全协议。有了这个观察，进程代数的主要应用领域可能会停留在协议规范和验证领域，它的发展得到了最强大的工具的支持，这些工具可用于证明生成，存储和验证以及对越来越大的有限（甚至无限）模型进行模型检查。在我看来，网格在这个阶段是完全不可理解的，仅仅这个应用领域就为继续研究ACP风格的过程代数提供了足够的动力。42005年设计原理的有效性我仍然完全相信共同导致ACP和类似理论的成分的相关性但与此同时，其他理论在相关领域也被证明是非常有效的。机场核心计划的设计理据的分项数字是甚么从长远来看，决定这一问题的是激励应用程序的可见存在。在这方面，ACP及其数据类型扩展muCRL的扩展和应用程序的缓慢但稳定的建立是令人放心的，此时ACP风格的进程代数对我来说就像1982年Jan WillemJ.A. Bergstra/Electronic Notes in Theoretical Computer Science 162（2006）7985Klop和我开始了我们在这个领域的工作