通用进程代数——理论计算机科学电子笔记的研究与应用

理论计算机科学电子笔记162（2006）65-71www.elsevier.com/locate/entcs一个通用进程代数乔斯·C·M Baeten埃因霍温理工大学数学与计算机科学系计算机科学系形式方法组，P.O. Box 513，NL-5600 MB Eindhoven，荷兰电子邮件地址：josb@win.tue.nl马里奥·布拉韦蒂Di parti mentodiScienzedee ll' I n for o r m a z i o ne，Universi a ` d i Bo l o g n a，Mura Anteo Zamboni 7，I-40127 Bologna， Italy.电子邮件地址：bravetti@cs.unibo.it摘要三种经典的进程代数CCS、CSP和ACP在各自的技术机制中存在着一些问题。这不仅是由于它们的经营者不同，而且也是由于一直（现在仍然）与它们合作的社区的术语和“思维方式”。在本文中，我们将首先讨论这些差异，并试图澄清术语和概念的不同用法。然后，作为讨论的结果，我们定义了一个通用进程代数，其中三个进程代数的每个基本机制都由一个运算符表示，并且可以用作底层公共语言。我们展示了采用这样一种语言而不是三种更专门的代数之一的优势的一个例子：产生有限状态行为的完整公理化。保留字： 进程代数，CCS，CSP，ACP1引言在过去的25年里，进程代数的大量研究工作始于进程代数CCS [13]、CSP [11]和ACP [7]理论的引入。尽管这些进程代数在概念上相似，但它们是从不同的观点出发发展起来的，并产生了不同的方法：CCS在很大程度上是基于从操作观点出发的基于观察性双模拟的进程通信理论; CSP是作为一种实用并发语言的理论版本而诞生的，仍然基于操作语义，然而，操作语义被解释为W.R. T。一个更简单的理论基础上的痕迹比互模拟;最后，ACP从一个完全不同的角度来看，并发系统，根据一个1571-0661，由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2005.12.07766JCM Baeten，M.Bravetti/Electronic Notes in Theoretical Computer Science 162（2006）65纯数学代数观点，因为方程组（ax-ioms）的解在所考虑的代数的签名上，以及操作语义和互模拟（在这种情况下，考虑分支互模拟的不同概念）被视为仅仅是代数可以被定义并且公理可以被应用的可能模型之一这种差异反映了开始与他们合作（并经常保持合作）的不同社区的不同“思维方式”。本文旨在指出这样的差异，这往往反映在不同的社区内的不同术语的使用，并在创建一个统一的过程代数视图的手段。这种差异的影响乍一看很容易被低估。然而，当涉及到在三种不同的背景下处理有关递归和过程变量处理的相关机制时，需要进行澄清和比较。我们的研究具体体现在进程代数的共同理论的发展。特别是，我们使用了一个称为TCP+REC的进程代数，它的定义方式是，三个进程代数的运算符中涉及的每个基本机制 这个想法是TCP+REC：（i）是一种基本的共同语言，可用于表达任何的三个进程代数;（ii）可以被用来作为一种手段，为正式比较的三个各自的方法;（iii）可以用来产生新的结果，在进程代数理论的背景下，由于其一般性（例如，以产生一个公理化，这是完整的有限状态过程）。本文的其余部分组织如下。在第2节中，我们重点介绍CCS、CSP和ACP中有关过程变量递归和处理的在第3节中，我们提出了TCP+ REC。在第4节中，我们提出了基于TCP+ REC的有限状态过程的公理化结果。2过程变量和递归ACP过程代数中假设的不同观点，例如，CCS过程代数在公理化中引起了过程变量的不同技术处理。在CCS中，公理被认为是可以通过使用元变量P来表达的项之间的方程（例如，在P+P=P中，代表任何项。其含义是，根据所考虑的等效概念（例如CCS的观测一致性），由“=”左边的术语生成的模型在=的左边和右边的项可以包括自由变量X（它们可以是所谓的开放项）。在这种情况下的意义如下：对于自由变量的任何替换，左边的项通常，不同的元变量E用于在开放项上进行范围调整，而P仅在封闭项上进行范围调整：即。自由变量X不出现的术语（或者如果它们出现，则它们受约束，例如递归运算符，如recX.E）。注意，在本文中，“过程”一词在ACP中，公理被认为是过程变量JCM Baeten，M.Bravetti/Electronic Notes in Theoretical Computer Science 162（2006）6567（表示为代数假设的模型中的任何过程）通过代数的签名中的运算符组合（例如，在x+x=x中）。请注意，这里与CCS的情况不同，过程一词用于表示模型中所考虑的任何元素（例如转换系统模分支互模拟）。这样的过程变量的行为类似于元变量P的CCS只有当所谓的术语模型是假设：模型中，每个元素是由所考虑的过程代数的签名的操作符组成的术语生成/表示。在ACP中，不考虑CCS的自由变量X然而，请注意，这并不妨碍使用开放项进行“推理”的可能性：这在ACP公理化中是通过替换其他公理中的公理来完成的。与ACP和CCS之间的这种差异相关的是使用“演算”一词与CCS不同的是，在ACP上下文中，只有在引入绑定运算符时才使用微积分这个词，以强调我们在存在此类运算符的情况下离开纯代数域。最后，我们想观察到，CCS语境中的“完全公理化”概念一旦解释了这些基本的区别，下面我们将集中讨论在三个过程代数中表达递归的不同方式 设V是一组变量，范围在过程上，范围在X，Y上。 根据ACP设置中常用的术语，递归规范E=E（V）是一组方程E={X = tX|X∈V}，其中每个tX是所讨论的签名上的项和来自V的变量。 递归规范E（V）的解是元素集合{yX|X ∈V}，使得E（V）的方程对应于等价元素，如果对所有的X∈V，用yX代替X。通常，我们感兴趣的是一个特定的变量X∈V，称为初始变量。这种递归规范的保护性准则确保了理论的优选模型中的唯一解，而无保护规范将有多个解。例如，无保护规范{X= X}将有每个元素作为解，例如。 如果考虑过渡系统模观测同余，则无保护规范{X = τ.X}将有多个解，因为任何以τ-步为唯一初始步的过渡系统都将满足这个方程。就受保护的递归规范而言，虽然在CCS中，唯一解可以通过使用递归运算符“recX.P“来表示，但在ACP中，没有显式递归运算符，这是不可能的因此，在CCS中，解的唯一性由两个标准公理（展开）recX.t=t{recX.t/X}（F old）tJ= t{tJ/X} ⇒ tJ=recX.t如果X在t这实际上使得有可能得到解决方案，在ACP中，这个属性是68JCM Baeten，M.Bravetti/Electronic Notes in Theoretical Computer Science 162（2006）65用所谓的“原则”来表达。递归定义原理，对应于展开公理，指出每个递归规范都有一个解（无论它是否被保护）。递归具体化原理，对应于折叠公理，指出每个受保护的递归具体化最多有一个解。就无保护递归规范而言，进程代数ACP、CCS和CSP以不同的方式处理它们。在ACP中，出现在无保护递归规范中的变量被视为（约束）变量，而不是过程。在CCS中，递归规范是通过所谓的“常数“进行的，范围为A，B，.. t算子，其中t是包含变量X的项，从解的集合中将选择在所生成的转变系统中具有最少转变的解因此，为方程{X=X}选择的解没有跃迁（这是ACP术语中的死锁过程δ），而为{X=τ.X}选择的解只有一个到自身的τ-跃迁，这个过程与观测同余中的τ.δ是双相似的在CCS中，这种行为由无保护递归（FUng）recX的三个公理表示。（X+t）=recX.t（WUng 1）recX. （τ.X+t）=recX.τ.t（WUng 2）recX. （τ. （X + t）+s）= recX。（τ.X+t+s）这使得有可能将每个无保护的递归指定转换为有保护的递归指定（实际上，WUng1和WUng 2可以由一个公理表示，如我们在[5]中所示）。值得注意的是，如果无保护性仅由τ动作（弱无保护性）引起，如在{X=τ.X}中，而不是由在等式的右侧可直接执行的变量引起（完全无保护性），如在{X=X}中，则在ACP中，可以通过隐藏运算符获得与CCS中的recX.t相同的效果：例如，可以通过以下方式在ACP中获得{X=τ.X}τ{a}（X）其中X = a.X（在ACP中“τ I（t）”是隐藏运算符）。 这种技术使得在ACP中也可以“推理”弱保护递归，但是是通过隐藏运算符以一种间接的方式。更准确地说，在ACP中，可以通过添加一组更复杂的条件方程来表达公理WUng1和WUng2的类比，称为CFAR（集群公平抽象规则），在[15]中引入。CFAR是KFAR（Koomen的公平抽象规则）的推广然而，请注意，CFAR和KFAR与上述公理不同，也适用于分支互模拟，而不是米尔纳的观测一致性。最后，在CSP中，处理无保护递归规范的方式是这样的，一个解决方案将像在CCS中一样被选择，但是一个不同的：最不确定的一个。因此，CCS和CSP都使用最小不动点构造，但相对于不同的排序关系。在CSP中，为方程{X=X}选择的解是混沌过程，一个对所有过程x都满足x+x=x的过程（对于具有这样一个过程的ACP的扩展，参见[3]）。JCM Baeten，M.Bravetti/Electronic Notes in Theoretical Computer Science 162（2006）65693通用进程代数TCP+REC代 数 TCP+REC 是 代 数 TCP[1 ， 2] 的 扩 展 ， 其 又 通 过 包 含successfultermiminatitionschedule和pref ixingaCCS来扩展A CP。代数TCP在一组动作A（不包括特殊的内部动作τ）上参数化，并被赋予序列“tj·tjj“，隐藏“τ I（t）"，restrictio n（其中假设通信函数γ计算通信动作的类型）。 此外，它还包括左合并“T J T JJ“和同步合并“Tj|tJJ“运算符，用于公理化并行组合。TCP +REC除了考虑TCP之外，还考虑递归运算符REMAX|E（其中E = E（V）是一个重cursive specification和X是V中的变量，用作初始变量），与CCS类似，它计算（非保护）方程组的最小定点解，并扩展了[9]中引入的类似算子，使递归算子可以嵌套在递归算子内。X|E递归包含CCS recX.t运算符（通过取E={X = t}获得）和ACP中表达递归的标准方式（其中通常仅通过方程组E考虑保护递归）。此外，在CCS的背景下，运营商|E可用于直接表示Milner在[12，14]中考虑的（标准）方程组（即包含自由变量的方程组E）的解，并用于证明具有保护递归项的强互模拟和观测同余的公理化的完备性。这个进程代数是通用的，在这个意义上，所有常用进程代数的特征都可以嵌入其中。在下文中，我们使用了[10，4]（CSP外部选择的翻译是由于Pedro D'Eklio，Rob van Glabbeek也开发了我们考虑一个对应于CCS的子理论，见[13]。这是通过省略签名元素、·、来实现的，|.接下来，我们通过将参数集分离到以下三个 元素来专门化参数集 A ：asetofnamesA、 asetofco-namesA和a set如果比较Ac，则a∈ A 的 比 较 值是a ∈And的比较值恰好一个ac∈ Ac。通信函数γ被专门化为具有如 下 的 完 全 可 定 义 的 复 合 运 算符：γ（a，a′）=γ（a′，a）=ac，以及CCS并行复合运算符|CCS可以由以下公式定义：X|CCSy = τAc（x<$y）。我们考虑一个对应于ACPτ的子理论，见[8]。这是通过对每个a∈A定义一个新的常数a，a = a. k，然后省略签名元素k，.，ρf.我们考虑一个对应于CSP的子理论，见[11]。非确定性选择算子H可以定义为：xH y = τ.x + τ. y。就CSP并行复合算子而言，我们将参数集A具体化为两部分：一个名字集A和一个通信集Ac，使得对于每个a∈ A，恰好有一个ac∈Ac.通信函数γ专门用于具有唯一定义的通信γ（a，a）=ac，并且70JCM Baeten，M.Bravetti/Electronic Notes in Theoretical Computer Science 162（2006）65此外，我们使用具有f（ac）=a的重命名函数f。然后，x<$Sy，其中x和y是仅使用A上的名称的过程，S<$A，可以由下式定义：x<$Sy=ρf（<$S<$（Ac−Sc）（x<$y））其中我们使用“Sc“来表示名称集合{ ac|a∈S}和“−“表示集合的差。 就CSP外部选择算子Q而言，我们进一步将名称集A具体化为三部分：一个名称集B，以及两个名称集B1和B2，使得对于每个a ∈ B，恰好有一个名称a1∈ B1和一个名称a2∈ B2. 通信功能γ没有改变（没有进一步改变）。通信已添加）。最后，我们使用具有FJ（a1）=a和FJJ（a2）=a的重命名函数FJ和fjj。然后，xQy，其中x和y是仅使用B上的名称的过程，可以由下式xQy =ρfJ<$fJJ （ （ ρfJ−1 （ x ） <$ρfJJ−1 （ y ） ） <$B1<$B2（B1<$$>+B2<$$>））其中，给定一组名称B和一个过程x，ΣrecX. （x+a∈Ba.X）。第4章公理化非稳态过程正如我们在[5]中所示，通过使用TCP+REC的限制版本，可以解决为具有静态算子的过程代数开发地面完全公理化的开放问题CCS平行和限制）对有限状态过程模观测同余，从而扩展了米尔纳的结果，该结果适用于没有静态算子的CCS。注意，如果我们考虑完全CCS的签名，我们有米尔纳的公理不再足以摆脱无保护递归。换句话说，即使两个CCS项都是有限状态的，它们也可能不被一个公理化所等同，这个公理化包括标准CCS公理（没有recX.t递归运算符的CCS公理）加上无保护和保护递归的公理。例如：（（recX.a.X）|（recX.a.X））\a凡“|“和“\“分别表示CCS并行组合和限制。这样一个项的模型只有一个状态，有一个τ自环，但不能通过米尔纳公理化等同于等价项recX.τ.X或τ。为了应用折叠公理和摆脱静态运算符，不能去除无保护的原因。特别地，我们考虑TCP+REC f，其中在TCPX中，|E = E（V），我们要求V中的变量（由操作符绑定）在E中是“串行”的：即我们不允许这样的变量出现在E中的静态操作符范围内，如隐藏，限制，重新标记和并行组合操作符或排序操作符的左侧。通过考虑关键公理τI（τX|X = t）=X|X = τI（t） 如果X在测试中是串行这允许隐藏运算符（唯一可以生成无保护递归的静态运算符）与递归运算符交换。JCM Baeten，M.Bravetti/Electronic Notes in Theoretical Computer Science 162（2006）6571引用[1] JCM 贝滕嵌入untimed到定时进程代数：显式终止的情况。Mathematical Structures in Computer Science，13（4）：589[2] JCM Baeten，T. Basten和M.A.雷尼尔通信过程的代数。 剑桥理论计算机科学。剑桥大学出版社，2005年。[3] JCM Baeten和J.A.伯格斯特拉带有命题信号的进程代数。Theoretical Computer Science，177（2）：381[4] JCM Baeten，J.A. Bergstra，C.A.R.霍尔河Milner，J. Parrow，and R.德·西蒙尼。进程代数的多样性。ESPRIT基础研究行动3006，CONCUR，1991年。[5] JCM Baeten 和 M. 布 拉 维 提 过 程 a l geb r a 中 有 限 状 态 过 程 的 一 个 基 础 完 备 公 理 化 。InMart'enAbadianddLucadeAlfaro，editors，ProceedingsCONCUR' 0 5， v o l um e 365 3 of LectureNotes in Computer Science ，pages 248-262. Springer Verlag，2005.[6] J. A. Bergstra和J. W.克洛普 利用进程代数验证交替位协议。Wolfgang Bibel和Klaus P. Jantke编辑，Proc. Mathematical Methods of Specification and Synthesis of Software Systems，LNCS第215卷，第9-23页。Springer，1986年。[7] J.A. Bergstra和J.W.克洛普同步通信的进程代数。 Information and Control，60（1/3）：109[8] J.A. Bergstra和J.W.克洛普抽象的通信进程代数。Theoretical Computer Science，37（1）：77[9] J.A. Bergstra和J.W.克洛普一个完整的推理系统，经常过程与沉默的举动。在F.R. 德雷克和J.K.Truss，editors，Proc. 逻辑讨论会'86，第21-81页。1988年北荷兰[10] R.J.范格拉贝克。关于CCS和CSP方法的说明。Theoretical Computer Science，177（6）：329[11]C.A.R.霍尔 通信顺序进程。 普伦蒂斯·霍尔1985年[12] R.米尔纳一类规则行为的完整推理系统。Journal of Computer. 系统科学，28（3）：439-466，1984.[13] R.米尔纳 通信和并发。 普伦蒂斯·霍尔1989年[14] R. 米尔纳有限状态行为的观测一致性的完整公理化。信息与计算，81：227[15] F.W.凡德拉格通过进程代数验证两种通信协议。技术报告报告CS-R8608，CWI Amsterdam，1986年。