进程代数中的同余格式技术及其应用

理论计算机科学电子笔记128（2005）3-37www.elsevier.com/locate/entcs从双代数语义到同余式Bartek Klin1天气-奥胡斯，丹麦摘要一个通用的和抽象的框架来定义各种过程等价的同余格式该框架扩展了图里和Plotkin的双代数技术与抽象的coalgebraic的方法来处理等价，基于一个概念的测试套件。所得到的技术说明完成跟踪等价的例子而不是提供正式的证明，该文件是引导读者通过的过程中得出的一致性格式的测试套件的方法。关键词：进程代数，结构操作语义，同余格式，双代数语义1介绍进程代数是研究复杂计算系统的形式化描述的领域，特别是那些具有通信、并发执行组件的复杂计算系统。自20世纪80年代以来，它一直是理论计算机科学的一个成熟和深入研究的领域（例如[4，8，18，21，29]）。传统上，它的主要目标是为并发和网络计算机系统的规范和验证开发形式主义，并为并发编程语言提供语义。其中最著名的传统进程代数是ACP [7]，CCS [28]和CSP [11]。最近，进程代数的方法已经应用于计算机科学的其他领域，在分布式，动态和移动的形式化方法1电子邮件地址：klin@brics.dk1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.09.0384B. Klin/Electronic Notes in Theoretical Computer Science 128（2005）3系统（例如，π演算[14，30]，移动环境演算[12]），密码协议的安全性（spi演算[1]），甚至计算分子生物学[13，33]。在正式描述系统和过程时，必须考虑三个关键方面：语法、行为和过程（也称为行为、观察或操作）等价性。过程结构指的是过程的结构，反映了这样一个事实，即将各种系统描述为由较小的子系统组成是自然和方便的。在简单的情况下，进程是代数签名上的任意项。更复杂的句法现象包括变量绑定和结构一致性，其中两个句法上不同的术语被识别并表示相同的过程。行为指的是进程可能采取的操作类型。在可转移过程代数中，允许过程从一个指定的集合中非确定地执行外部可观察的动作。人们还考虑确定性，概率和/或定时行为，执行不可观察动作的能力，与状态，输入和输出相关的特征过程等效描述的是那些行为应被视为“相同”的过程。 这个概念显然取决于所选择的过程行为的概念，但即使对于一种行为，人们也可以考虑许多不同的过程等价物，适用于不同的目的。最完善的方法，以正式表示的进程代数，涵盖所有三个方面，上述，是结构操作语义[32，2]。在那里，过程的行为被建模的过渡关系的过程中提出的一些符号性质的条款。转换关系又由遵循过程的句法结构的推理规则诱导。这种方法的直观吸引力，重要的是，它的内在支持建模非确定性行为，使其成为一个自然的框架，正式描述的进程代数。一般来说，一组操作推理规则归纳出一个转换系统，即，一组过程及其上的转移关系。根据规则的形式，这可以是一个简单的标记转移系统（LTS），一个具有不可观测步骤的LTS，一个概率转移系统，一个定时转移系统等。基于转移关系的结构，人们可以定义过程上的许多不同的等价和前序。在LTS的情况下，对各种可能的过程等价进行了最深入的研究，包括互模拟等价[31]、模拟等价、跟踪等价、测试等价等（全面的处理，参见[17]）。对于其他过渡B. Klin/Electronic Notes in Theoretical Computer Science 128（2005）35系统和过程行为，最彻底研究的过程等价包括弱/延迟/分支互模拟等价（例如[16]）、概率互模拟等价[26]、定时互模拟等价[3]和许多其他等价。为了使过程等价的概念实际上有用，它必须是组合的（或者，换句话说，它必须是一致的），即，它必须被所选择的进程代数的语法构造所尊重。这对于任何类型的关于过程的归纳推理都是必要的，例如，对于系统组件的指定和验证。对于特定的进程代数，所选择的进程等价的组合性的证明可能是相当苛刻的。因此，它是可取的，以显示一般的结果，这种持有整个类的过程代数。在结构操作语义学的框架下，对这些结果的搜索导致了各种同余格式的发展。全等格式是对结构化推理规则的句法形式的限制，其保证特定的过程等价组合。最流行的同余格式之一是GSOS [10]，这是一种对推理规则形式的限制，可以保证从这些规则生成的LTS上的互模拟等价性。许多其他的一致性格式已经被定义为各种行为和过程等价的概念（参见[2]和其中的参考文献，以及[5，23]）。然而，为一个给定的过程等价概念定义一个一般的全等格式往往是一项困难的任务。考虑到越来越多的不同的编程范例和过程行为，它是可取的，有一个通用的框架，为给定的语法，行为和过程等价的概念构建一致格式。为了提供这样一个框架，必须提出语法、行为和等价性的抽象概念，涵盖大多数众所周知的例子。Turi和Plotkin在[35]中开发的一个这样的框架被称为bial-geopolitan语义学。它基于经典的语法代数方法和行为的共代数方法[34]，包括互模拟等价的共代数跨度方法。在[35]中，我们展示了如何以抽象的方式导出GSOS作为互模拟等价的同余格式。将相同的方法应用于其他类型的行为，Bartels [6]导出了概率转移系统上概率互模拟等价的一种新的同余格式，Kick [23]导出了定时转移系统上定时互模拟的格式。原双代数方法的通用性受到特征的限制的余代数跨度方法的过程等价，它只涵盖了一个单一的概念等价的任何给定的概念的行为。在[25，24]中，6B. Klin/Electronic Notes in Theoretical Computer Science 128（2005）3双代数方法已被修改，以适应其他众所周知的等价。而不是共代数跨度的方法，提出了一种新的框架建模过程的等价性，基于简单的概念测试和测试套件。这一点，当结合原来的双代数框架图里和Plotkin，给出了一个框架，推导出许多不同的过程等价的同余格式。本文的目的是尽可能直观地解释原始的双代数技术及其测试套件的扩展。为了展示一些具体的例子，并证明这个抽象的框架确实会导致新的结果，本文集中在通常考虑的行为标记的非确定性，并在两个特定的过程等价：互模拟等价和完成的跟踪等价。前者用于解释Turi和Plotkin的原始技术，后者用于说明测试套件方法。完全迹等价的选择是基于这样一种观点（见[2]），即找到它的一般同余格式是非常困难的。因此，一个合理的一般格式的成功推导证明了抽象双代数方法可以带来一些具体而有用的结果。这篇文章的内容和风格的动机是一些人向我表达的感觉，即双代数测试套件方法是复杂的，难以理解的。特别是，[24]中所示的导出同余格式的正确性的形式证明不可否认不是很有启发性，并且它们对格式的实际推导过程提供了很少的见解。这使得任何人都很难将这种方法适应他们最喜欢的行为和等价物。出于这个原因，我决定省略掉双代数和测试套件技术的介绍中几乎所有的形式证明。相反，我试图在推导全等迹格式的每一步中提供尽可能多的直觉。我希望这种直觉会使测试套件方法更容易理解和使用。为了全面、详细和完全正式地介绍这里概述的思想，建议读者参考[24]。在[25]中，我们已经与Pawel-Sobocin′ski共同完成了框架和格式的初步版本虽然所有相关的定义都被召回，但读者应该具备结构化操作语义和并发理论的基本知识。[17]和[2]应该足够熟悉了。在整个文件中，范畴理论的基本概念被使用。假设读者熟悉基本概念，如范畴，函子，自然变换，B. Klin/Electronic Notes in Theoretical Computer Science 128（2005）37∈−→概念，初始对象，最终对象，产品，余产品和拉回。[27]的第一章，以及其他许多书，包含了这些的定义。本文的结构如下。第二、三节简要回顾了结构操作语义学领域的一些概念和结果。在第4节中，图里和Plotkin的原始双代数方法被勾勒出来，连同它的GSOS格式的抽象表示。在第5节中，描述了各种过程等价的抽象测试套件方法。在第六节中，将这种方法与双代数方法相结合，给出了一个关于同余格式的抽象定理。该定理是spece- cialised的情况下，完成跟踪等价，并引导读者通过的过程中推导的一个同余格式的等价。文章最后附有一组练习和一系列值得思考的开放性问题。众所周知： 我 很 感 谢 PiotrHo Mushman、Pawe-lSobocin'ski和DanieleVaracca对本文草稿的评论。2标记的过渡系统和工艺等效性操作描述通常基于标记变迁系统的概念。定义2.1标号迁移系统（LTS）<$X，A，−→ <$X是一个集合X，一个过程，一个动作集合A，以及一个转移关系− →X×A×X。所有y代替f<$x，a，xJ<$∈−→onewritesx−→axJ。AnLTSX，A，−→称为无限分支，如果对于每个过程x∈X，manyprocessesxJ∈X且actionsa∈Asuchtatx−→axJ.对于anyx∈X，a∈A，其中x/−→a表示存在noxJ∈Xsuchthatx−→axJ. Moreover，x/−→意味着s有x/−→a，对所有a∈A。许多前序和等价在标号迁移系统中的过程上被定义为了说明的目的，本文集中在其中两个：互模拟等价和完全迹等价。在[17]中详细研究了许多其他等价关系互模拟等价通常基于经典的互模拟概念来在以下两个定义中，假设LTS<$X，A，−→ <$。定义2.2一个关系R<$X×X是互模拟，如果xRy意味着对任何a∈A，• 对于任意xJ X，如果xaXJRyJ，以及xJthenthereexistsyJ∈Xsuchthaty−→ayJ和8B. Klin/Electronic Notes in Theoretical Computer Science 128（2005）3∈−→∈• 对于任何yJ X，如果yaxJRyJ.yJthenthereexistsxJ∈Xsuchthatx−→axJ和过程x，yX是互模拟等价的，或互模拟相似的，如果存在一个互模拟R使得xRy。很容易证明，在任何LTS互模拟等价确实是一个等价关系，它是LTS上最大的互模拟。对于有限分支的LTS，互模拟的另一种表征可以使用以下的有限Hennessy-Milner逻辑给出。当且仅当它们满足完全相同的公式时，过程才被认为是等效的从逻辑。定义2.3给定一组动作A，考虑模态公式集FBS，由BNF文法给出：φ：：= T |⊥ ||[a] φ |φ ∧ φ |φ ∨ φ其中a的范围超过A。给定LTSh =<$X，A，−→ <$，满足关系式|= h⊆ X × FBSis defined inductively as follows:X|= hT总是X|= hneverh→xJXJ最后，等式B =BSX×X由给定的LTShy定义：x<$= BSxJ<$$>（<$φ∈FBS. X|=hφxJ|=hφ）Hennessy-Milner逻辑[19]的可靠性和完备性结果是：在一个有限的branchingLTS中，关系B=BS是等价的模拟等价性一旦回忆起Hennessy-Milner逻辑，在LTS上定义其他已知等价的最简单方法是通过该逻辑的适当片段。这就是我们如何继续定义完整的迹等价。X|=aφ⇐⇒一X J|=hφ对于某个x J使得x −X |=h[a] φ⇐⇒一XJ|=hφforallxJsuchthatx−→X|=hφ 1<$φ2⇐⇒X|=hφ 1和x |=hφ 2X|=hφ 1<$φ2⇐⇒X|=hφ 1或x |=hφ 2B. Klin/Electronic Notes in Theoretical Computer Science 128（2005）39F定义2.4给定一组动作A，考虑模态公式FCTr，由BNF文法给出：φ：：= T|∅| 其中a的范围超过A。给定LTSh =<$X，A，−→ <$，满足关系式|= h⊆ X × FCTris as in Definition 2.3, with the additional case:X| = hx−→在给定LTSh的情况下，X上的等式T=CTr定义为：xφ= CTrxJφ（φ∈FCTr. X|=hφxJ|=hφ）（2.1）上述逻辑确实可以被看作是Hennessy-Milner逻辑的一个片段，因为在任何LTS中，一个过程满足公式[a]当且仅当它对所有的动作a都满足公式[a]。以CTr结尾的公式通常被称为有限的、部分的迹（或简称迹），以结尾的公式被称为完整的迹。3结构操作语义与- mats的在结构化操作语义学中，过程通常是某些特征上的闭项，标号迁移系统是由推理规则集导出的。Asignatureisaset语言结构，以及一个函数：N→N。 对于给定的变量集合X，对于m f（x1， . . . ，xar（f）），其中f∈ndx1， . . ，xar（f）∈X.给定一个签名n和一个集合X，X表示为T<$X。TX中的下标如果与上下文无关或清楚，则省略。T0的元素（在本文中，0表示空集）被称为T上的闭项对于一项t∈TX和一个函数（代换）σ：X→Y，tσ表示TY中的项，它是由t同时用σ（x）替换每个x∈X而得到的为了定义推理规则，假设一个固定的、可数无限的变量集合，其范围为x 1，x 2，.。，y1，y2，. ................. 基于来自于Escherichia coli的变量构建的术语是typebortt，tJ等，与通常的符号t、TJ等相反在下面，固定一组任意的动作A。 作为签名的礼物，一个正性的正态-正态-负态-负态10B. Klin/Electronic Notes in Theoretical Computer Science 128（2005）3α表示为t/−→a，其中t，tJ∈T ∈ a∈A。一个非感染性的规则ρveris一个表达式H，其中H是一组正的正文字，α是正的正文字。于是H的元素称为ρ的前提，α称为ρ的结论。ρ的结论的左侧和右侧分别称为ρ的源和目标 如果规则ρ的源具有f（x 1，x 2，. ，xn），我们说ρ是f的规则。一个在环上的转移系统规范是一组在环上的规则。例3.1基本进程代数就是一个变迁系统规范的例子。假设一组动作A，其语法由BNF文法t：：=零|αt |t + t而BPAover ESTA的转换系统规范是一组规则αx−α→xx−α→xJx+y−α→xJy−α→yJx+y−α→yJ其中α的范围超过A。当在上面的语法上呈现术语时，尾部的nil被省略。这是一个相当简单的例子;特别地，上述规则中的所有前提都是肯定的。如何从上述规则中归纳出一个有标签的过渡系统是很清楚的。首先，一个可证明的正文字的概念是以一种直截了当的方式定义的。所有可证明文字的集合构成一个LTS，它包含了过程上的闭项，并以正的闭文字作为变迁。请注意，当负前提存在时，如何以有意义的方式将LTS与转换系统规范相关联可能不太清楚（参见[2]）。如果LTS可以从一组规则中导出，那么可以定义各种等价（例如，互模拟等价，完全迹等价）之间的封闭项之间的诱导LTS作为相应的等价。这种等价性标识了其作为过程的行为在某种意义上是相同的术语。然而，为了使等效在实践中有用，它应该是一致的：定义3.2设k为任意签名。一个等价关系R<$T0×T0是一个连续环，如果对于一个yf∈ N，其中har（f）=n，并且对于一个yt1，tJ1，t2，tJ2， . . ，tn，tJn∈T0，当vertiRtJi（i=1，2， . . . ，n），则nf（t1，t2， . . ，tn）Rf（tJ1，tJ2， . . . ，t，J，n）。事实证明，即使对于非常简单的语言，许多有趣的等价也不是同余。此外，如果一个特定的等价是一个给定语言的全等，这是可以相当苛刻的证明。 这就是为什么 寻找过渡系统专用的同余格式是值得的B. Klin/Electronic Notes in Theoretical Computer Science 128（2005）3111n阳离子，即，语法限制的规则集，保证特定的等价诱导LTS是同余。最流行的一种全等格式是GSOS [10]。下面的定义假设了一个固定的签名。定义3.3[GSOS]如果每个规则ρ∈Λ的形式为，xaijy：i≤n，j≤m，n，xbik ：i≤n，k≤n，−→i−→ij我我我 Cf（x，.，x）−→ t在ρ nndn=ar（f）中，如果语言c o n t，则xi∈fndyij∈fn都是不同的，并且是唯一出现在ρ中的变量。此外，如果对于每一个f ∈N，Λc都包含无穷多个f或f的规则，则Λ是象有限的。GSOS格式中的任何跃迁系统规范Λ都诱导出上面所描绘的LTS。如果Λ是像有限的，那么诱导的LTS是有限分支的（详见[2]）。如[10]中所示，互模拟等价于alence=BS保证与诱导LTS一致。在其它换句话说，GSOS是互模拟等价的同余格式。互模拟等价和其他已知等价的几个其他同余格式已经被定义（详细的调查，见[2]）。然而，在一段时间内，为完整的迹等价定义一个通用格式的任务显得非常困难。这一观点得到了以下看似简单和无辜的规则的例子的支持，但对这些规则来说，完全痕迹等同并不是一种一致。例3.4假设A={a，b}，用封装运算符{b}的运算规则扩展BPA：{b}x−→a（x）−→ay{b} （y）很容易检查BPA 的上述扩展是否不考虑完 全 事务。 实际上，aa+ab<$=CTra（a+b）but<${b}（aa+ab）/±CTr<${b}（a（a+b）），因为<$a <$<$b是<${b}（aa+ab）的完全迹，但不是<${b}（a（a+b））的完全迹。例3.5假设A={a，b}，用一组二进制同步合成规则x扩展BPAx−α→xJy−α→yJx×y−α→xJ×yJ12B. Klin/Electronic Notes in Theoretical Computer Science 128（2005）3其中α的范围超过A。这里很容易看出aa×（aa+ab）/±CTraa×a（a+b），因为ar是aa×（aa+ab）的完全迹，而不是aa×（a（a+b））的完全迹然而，完整的迹等价对于BPA来说是一个全等，甚至对于一些看起来更复杂的规则集来说也是如此，特别是涉及到否定前提：例3.6使用二进制顺序组合的规则集合扩展BPA;：x−α→xJx;y−α→xJ;y其中α的范围超过A。x/−→a对于a∈Ay−α→yJx;y−α→yJ，对于这种语言，完全迹等价是全等的证明被留作练习。上面的例子有点令人沮丧。似乎很难确定封装和同步组合规则的语法特征，该语法特征防止完成的跟踪等价成为一致性，因为这些规则实际上非常简单。然而，在下面的部分中，将导出一个不包括这些示例的全等格式，并且仍然足够通用以涵盖例如，顺序合成操作符。事实上，本文承担了一个更大胆的任务，并提供了一种方法，推导出同余格式的任何给定的概念的等价与足够的结构。新的格式完成跟踪等价出现作为一个特殊的情况下，这种一般的方法。要做到这一点，需要更抽象地看待标记的转换系统、运算等价和转换系统规范。基本范畴理论证明是达到这一目的的有用工具。4数学运算语义学我们首先简要介绍了美丽的抽象框架定义的图里和Plotkin [35]和所谓的双代数语义或抽象GSOS。它允许他们重新定义GSOS格式，并以抽象的方式重新证明其互模拟等价的同余性质。在下面的章节中，将修改该方法以涵盖其他过程等价，特别是完整的跟踪等价。任何带标号的跃迁系统<$X，A，−→ <$X都可以看作是一个函数h：X−→ P（A×X）B. Klin/Electronic Notes in Theoretical Computer Science 128（2005）313一P ×− P ×− P×−P× −P× −（其中P是幂集结构），通过简单的对应关系，a，yx−→y当P被视为集合和函数范畴Set上的协变幂集内函子时，上述函数称为函子（A）的余代数，或简称（A事实证明，用其他内函子（在本文中称为行为内函子）代替（A） 这导致了泛余代数作为抽象的过渡理论的发展系统（详细介绍见[34]）。形式上，对于集合上的任何内函子B，具有载体X的B-余代数是函数h：X→BX。 一个从g：X→BX到h：Y→BY的余代数态射是一个函数f：X→Y，使得下图交换：XfYGhJBXBfBY很容易看出，B-余代数和它们的态射形成一个范畴，其恒等式和合成继承自Set。过程的共代数方法最重要的成就之一是互模拟的抽象定义：定义4.1设h：X→BX是余代数。h上的（span）互模拟是一个关系R<$X×X，使得存在一个余代数结构r：R→BR，使投影π1和π2成为余代数态射：X，π1Rπ2XhrhJ，J，JBXBπ1 BRBπ2BX事实证明，对于B=（A），该定义专门针对LTS上互模拟的对于B的其他选择，它专门针对其他众所周知的定义（详细信息参见[34]）。在余代数方法的许多技术发展中，要求所选择的行为函子B保持弱拉回，并且在B-余代数范畴中存在最终对象（最终B-余代数）。不幸的是，（A））不承认final余代数。 因此，为了充分利用共代数方法的力量，将注意力限制在有限分支的LTS上是很方便的。很容易看出，这样的系统是正确的-14B. Klin/Electronic Notes in Theoretical Computer Science 128（2005）3P × −P→ →→给闭函子f（A）的余代数，其中f是协变有限幂集函子。这个行为函子允许final余代数并保持弱回调（详细信息见[34]），并且以下发展适用于任何进一步的假设。下一步是为余代数的载体配备某种句法结构，因为在结构操作语义的上下文中，LTS中的过程是某些句法上的术语。表示简单语言的语法的常用技术是将签名表示为多项式（即，仅由常数、和和积构建）在Set上的内函子。任何签名都确定一个内函子（也有点草率地表示为内函子，这不应导致任何混淆），定义为：X=Xf∈ar（f）哪里和分别表示不相交并积和卡里积。 例如，基于一组动作A的基本进程代数BPA的签名对应于内函子X = 1+（X +. + X）+X × X`|一|我的天x其中，1是单例集，+表示不相交并，×表示实数产品 那么，在签名上给集合X赋予代数结构就是提供一个函数g：X−→X用范畴术语来说，它被称为代数。 来自代数g的态射：<$XX到一个代数h：YY是一个函数f：XY使得下图为通勤路线：X ΣYGhJfY和余代数一样，余代数和它们的态射形成一个范畴。如果k是多项式的（正如它是从上面的签名导出的情况），那么初始k-代数：总是存在的，其中T0是所有闭项的集合，并且是明显的代数结构XB. Klin/Electronic Notes in Theoretical Computer Science 128（2005）315−P × −定义3.2中的同余概念可以推广到由签名得到的闭函子的任意代数定义4.2设λ是一个签名，h：λX→X是集合上相应多项式内函子的代数。 等价关系R <$X×X是h上的同余，如果对任意的余积注入f：Xn→ <$X，且对任意的x1，y1，x2，y2，.，xn，yn∈X，当xi Ry i（i = 1，2，.，n）则h（f ∈x1，x2，. ，xn <$）Rh（f ∈y1，y2，. ，y n）。很容易看出，当h是初始的n-代数n：nT 0→T 0时，上面的定义特别适用于定义3.2。代数框架也允许在签名上表示项。形式上，给定任何集合X，闭函子X+容许初始代数，且上的以X为变量的项集是初始（X+ −）-代数的载体。这个构造（从X到那个载体）可以扩展到Set上的一个内函子，记为T，或者简称为T，如果是不相关的或者从上下文中是清楚的。特别地，环上闭项集T0是初始的λ-代数的载体.在范畴术语中，函子T被称为由T自由生成的单子。在[35]中，Turi和Plotkin提出了双代数的概念，将其作为具有强加于过程的句法结构的转移系统的抽象表示。集上函子B的双代数是一对具有公共载体的B-代数和B-余代数：GX−→ X−h→BX然后，他们展示了如何从分配律中推导出给定λ和B的双代数，即，形式的自然变换λ：λ（Id×B）=λBT其中T是由n自由生成的单子。 为了本文的目的，这个抽象结构在技术上如何工作并不重要（详细信息，见[35]）;可以说，上面的任何λ都会产生一个带有载体T0的双代数：T0−BT0其中λ是初始的λ-代数，hλ是由λ导出的余代数结构。注意，hλ的载体是签名上的闭项的集合回想一下，当B=f（A）时，那么hλ只是一个有限分支LTS。因此，人们有一种从某些抽象实体导出LTS的方法16B. Klin/Electronic Notes in Theoretical Computer Science 128（2005）3分配律 [35]的一个中心结果表明，这些分布律实际上对应于像有限GSOS格式的跃迁系统规范，并且从λ抽象构造hλ专门用于从这些规范归纳LTS：定理4.3在签名上的具有一组动作A的图像有限GSOS格式的跃迁系统规范Λ与自然变换之间存在（本质上1-1）对应λ：<$（Id× Pf（A× −））=<$Pf（A×T−）对于任何这样的转移系统规范Λ，由对应于Λ的自然变换λ导出的余代数hλ就是由Λ导出的LTS。这个定理的完整证明在[35]中是隐式的，但可以在[6]中找到。在这里，对于如何从一组规则Λ导出自然变换λ给出一些直觉就足够了固定一组任意的动作A，一个签名，多项式内函子，以及GSOS规则的像有限集Λ，其具有来自A的动作。任务是定义一个变换λ，就像定理陈述中那样。对于给定的集合X，分支函数λX的定义域是集合<$（X× Pf（A×X））这个集合的元素是仅由单个主语言构造（比如f）构建的项r，其中变量来自X，并且每个变量x配备有一个有限的对集合，这些对可以被视为源自x的可能转换。有了这些信息，就可以确定可以进行哪些转换根据规则Λ从r中得到，通过依次寻找Λ中f的每个规则ρ，并试图用X的元素替换来自ρ的变量，使得ρ的源变量映射到r中的变量，并且ρ的所有前提都由r提供的转换集满足。如果可以做到这一点，那么ρ就可以被“激发”，并且由此产生的转换（即，一对标签和一个术语）被添加到λX的结果中，λ X是Pf（A×TX）B. Klin/Electronic Notes in Theoretical Computer Science 128（2005）317∈比克1∈n更正式地说，一种语言可以用一个字母yn和一个字母X（GSOS格式中的一个规则ρ）来表示tructf，xaijy：i≤n，j≤m，n，x/−→：i≤n，k≤n，i−→ij我我我Cf（x，.，x）−→ t定义映射ρX：（X× Pf（A×X））n→ Pf（A×TX）如下：ρX存在一个置换σ：n→X满足(i) σ（xi）=xi(ii) <$i≤n<$j≤mi<$aij，σ（yij）<$∈βi(iii) i≤n(iv) tσ=t然后，给定图像有限GSOS格式的规则集Λ，可以通过定义具有元数n的函数fX：（X×Pf（A×X））n→Pf（A×TX ）来定义函数λX：λfX：nxi，βi<$i≤n<$→ρΛf的ρρX<$xi，βi<$i≤nΛ的形象有限性确保了这个函数是良好定义的，即它只返回有限集合。最后，λX由fXQ例如，考虑过渡系统规范BPA（例3.1）为Λ（假设a，b，c∈A），并取X={λ，λ}。考虑如下的r1，r2，r3∈P（X×Pf（A×X））：r1=，{a，，b，}+，{a，}r2=a，{b，，c，}r3=零然后，上面描述的构造产生λX r1={λa，λ b，λb，λc，λa，λ c}λX r2={λa，λ b}λX r3=λ18B. Klin/Electronic Notes in Theoretical Computer Science 128（2005）3P × −在[35]中证明了GSOS的同余性质是以下结果的特殊情况：定理4.4对于任何自然变换λ：λ（Id×B）=λBT（其中B允许最终余代数且保持弱拉回）hλ：T0→BT0上的最大跨度互模拟是T0上的一个同余关系.这一点，专门针对B = f（A）的情况 ）并与The- orem4.3相结合，意味着image-finite GSOS是一种用于双模拟等价的同余格式。然而，定理4.4的重要性在于，它可以应用于其他行为内函子B，因此，它作为导出对应于各种行为的跨度互模拟的等价的同余格式的一般方法在[6]中，这种方法已被应用于概率转移系统，得到了一个同余格式对于概率互模拟，以及[23]中的定时转移系统，其中获得了定时互模拟的同余格式。然而，这种方法的一般性，是有限的跨度互模拟方法的过程等效的范围对于任何行为内函子，只有一个单一的，规范的概念等价的基础上跨度互模拟可以覆盖。一种方法是找到另一种更一般的过程等价的共代数方法，在普通LTS的情况下，它将涵盖更多的概念，而不仅仅是互模拟等价（特别是完全迹等价），但仍然允许证明定理4.4的对应部分以获得同余性质。5测试套件在本节中，基于测试和测试套件的简单概念，提出了一种用于过程等价性的余代数跨度方法的替代方法。示出了过程等价的一个绝对定义，其专门用于LTS上的大多数已知等价，特别是完成的迹等价。 在第6节中，这将与双代数方法相结合，产生对于给定的等价概念导出同余格式的一种方法。从概念上讲，测试套件方法是基于从模态逻辑中获得的直觉：如果两个过程不能被任何测试从给定的测试套件中区分出来，则它们被认为是等效的。通过改变所考虑的测试套件，可以获得不同的等价概念。相关的测试套件获得的LTS问题的共代数结构B. Klin/Electronic Notes in Theoretical Computer Science 128（2005）319→--⟨⟩∨∧测试套件方法与余代数跨度方法不同，因为要在余代数h上找到等价，并不构造余代数的跨度，而是用额外的结构丰富h，并要求h保持该结构。在[20，22]中使用了这种一般方法，其中煤- gebras在其载体上配备了二元关系。相反，在我们的方法中，余代数配备了测试套件。从现在开始，记为2= tt，ff。关于集合X的测试是一个函数V：X二 、集合X上的测试集（记为θ：X<$2）是一组测试集在X上。集合X上的所有测试集的集合，通过包含部分排序，记为X。显然，X上的任何测试V都可以用以下子集来识别：× ×：{x∈X：Vx=tt}从这个角度来看，X上的测试套件是X的子集的族。特别地，任何拓扑都是其载体上的测试套件。 保持直觉是有用的考虑到解释，但为了进一步开发的技术方便，坚持功能定义。测试套件TS的类别定义如下：• TS中的对象是对X，θ，其中X是一个集合，θ：X2是一个测试套件，• 态射f：<$X，θ<$→ <$Y，<$<$是函数f：X→Y，使得{Vf：V∈θ}θ为了得到一些直觉，请注意TS中的态射被定义为完全像拓扑之间的连续态射，当拓扑被视为测试套件时。T和F表示恒真和恒假检验。 人们还谈到了测试的并集和交集，用和和以明显的方式定义。在第6节中，将使用TS中的分类产品和联产品它们的定义如下：X，θX，θ哪里θ={[V，VJ]：V∈θ，VJ∈θ}θ={Vπ1：V∈θ}{VJπ2：VJ∈θ}20B. Klin/Electronic Notes in Theoretical Computer Science 128（2005）3→⊕×⊗×∧ ×→{→ ∈}→（这里[V，VJ]：X+Y 2表示V和VJ的配对）。检查所需的通用属性作为练习。 它也将是有用的考虑另一种测试套件的构造。对于测试套件θ：X<$2，测试套件θ0<$：X×Y<$2定义为：θ0<$={<$$>（V×VJ）：V∈θ，VJ∈<$}（5.1）其中：2 2 2是逻辑与运算符。很容易看出0是关联的，因此在适当的时候省略了它的括号直觉上，给定测试套件θ：X2和θ：Y2， θ是X + Y上的测试套件，包含由使用X上的θ和Y上的θ的测试的情况定义的测试，θ包含X Y上的测试，其由X上的θ的测试或Y上的θ的测试组成;最后，θ0是X Y上的测试套件，其由通过在X上从θ执行测试并同时执行一个测试，从Y开始，当两个测试都接受时接受。让它在一个新的空间X上运行。在X上的S_p_cialisationeequivalence_p=θ是定义为θ={x，y∈X×X|V∈θ。Vx=Vy}这是直接的，并留下作为练习，以表明测试套件态射保持专门化等价。为了给Set上的闭函子B的余代数配备测试集，充实B以作用于范畴TS是有用的。 有人说，如果p<$B<$=B<$p，则内函子B <$：TS→TS提升内函子B：Set→Set，其中p：TS→Set是明显的遗忘函子。提升给定函子B：Set Set的TS上的内函子由它们的动作确定，即，函数族BX：X（BX）：X集 如果这样的家庭满足某种温和的条件（详见[24]），则B定义为：BX，θ=BX，BX θBf=Bf是TS上的闭函子，它显然提升了B。在下文中，类似于BX，X的表达式将表示TS上的一些对应的闭函子B，X的作用。任何函子B：Set→Set都可以通过多种方式提升为TS上的内函子，通过在测试套件上定义其动作BX就我们的目的而言，有一种特别有用的方法。这种结构良好的提升内函子的方法是基于测试构造函数和闭包的概念。直观也就是说，人们可以把测试看作是根据过程解释的公式。然后，测试构造函数对应于公式语言中的模态运算符，闭包对应于命题连接词。B. Klin/Electronic Notes in Theoretical Computer Science 128（2005）321∈→ P×→→定义5.1设B是集合上的闭函子。对集合B2（即函数w：B2→ 2）的测试称为B-测试构造函数，或者简单地称为测试构造函数，如果B是不相关的或者从上下文中是清楚的。例5.2在本文的运行示例中，B2=Pf（A×2）。对Pf（A×2）的检验可以看作是将多个检验的结果结合起来的一种方法。例如，对于任何a∈A，都有一个测试构造函数w，定义为waβ=tta，tt∈β如何使用这样的测试构造函数？ 假设LTS h：Xf（AX），以及X上的测试V。功能BV_（60）h：X→B2，应用于一个进程x X，首先计算x在h中的后继者集合（以及相应的动作），然后对每个后继者应用测试V。然后可以将其结果提供给测试构造器w_a_c，从而获得测试waBVh：X→2它检查对于给定的进程x，是否存在x的a-后继满足测试V。细心的读者现在应该已经注意到，在定义2.3中，测试构造函数wa和模态构造函数wa之间存在着直观的对应关系。本文中提到的其他测试构造函数是w[a]，其中a∈A和w∈ A，定义为：w[a]β=ffa，ff∈βwβ=ttβ=定义5.3测试集闭包是一个（大）单调函数族Cl X：XX被集合X索引，使得对于任何函数f：X是的，对于任何测试集θ：Y<$2，ClX{V∈f：V∈θ}={VJ∈f：VJ∈ClYθ}例5.4测试套件闭包在概念上比测试函子简单，因为它们不依赖于任何行为内函子。他们只是22B. Klin/Electronic Notes in Theoretical Computer Science 128（2005）3XXXP × −.Σh：<$X，θ<$−→。BX，Bθθ.Σ选择一些结构下的封闭测试套件闭包的例子有：ClTXθ=θ{T}Cl<$Xθ=，.V∈V：θ，显然，Cl是任意并下的闭包，Cl是有限并和交下的闭包。上面的证明满足定义5.3的要求的直接证明作为练习。我们现在准备好定义一种结构化的方法，从设置为TS。定理5.5设B是集合上的闭函子.任何B测试构造器集合W，连同任何测试套件闭包Cl，都将B提升到TS上的内函子BW，定义为：BW<$B，θ<$=. BX，BWθ<$BWf= Bf其中对任意集合X，作用BW：X<$→（BX）<$是单调函数定义为BWθ=ClBX{w <$BV|w ∈W， V∈θ}很容易检验如上定义的BW确实是一个函子，显然它将B提升到TS。作为