理论计算机科学电子笔记106（2004）201-218www.elsevier.com/locate/entcs过程等价的一种共代数方法迹的共归纳原理Bartek Klin1奥胡斯大学2摘要基于测试和测试集的前序和等价过程的行为endofunctors提升到一类测试套件的余代数一般的框架是专门的情况下，有限分支标记的过渡系统。事实证明，来自所谓的van Glabbeek谱的大多数等价性可以通过结构良好的测试套件来描述。 作为一个直接的应用，共归纳证明原则，这些等价描述，特别是迹等价。关键词：范格拉贝克谱，余代数，余诱导。1介绍在作为变迁系统的并发进程理论中，考虑了进程上的各种操作等价和前序，对应于进程之间不同的“相似性”概念。 在非确定性的标记转移系统的标准情况下，最流行的概念包括互模拟等价、模拟前序、迹等价、故障等价等。这些概念在[3]中已经得到了深入的研究，统称为van Glabbeek谱。对于其他类型的系统，1电子邮件地址：mailto:klin@brics.dk2计算机科学基础研究（http://www.brics.dk），由丹麦国家研究基金会资助1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.029202B. Klin/Electronic Notes in Theoretical Computer Science 106（2004）201已知的等价包括各种弱互模拟等价、概率互模拟等价和许多其它等价。在coalgebraic方法的理论过程（cf。[15]作为主要参考），转移系统的概念被行为的概念参数化，建模为内函子B。系统被定义为B-余代数。例如，如果BX=Pf（A×X）onSet（对于一个固定的作用集A），B-余代数对应于有限分支标号转移系统。余代数方法允许人们抽象地描述几种变迁系统。考虑到进程代数中各种操作等价的重要性，对这些等价进行同样抽象的处理是必要的。在这个方向上已经做了几次尝试（见第7节），但即使在标记的过渡系统的情况下，没有一个覆盖了所有的等价和前序从范格拉贝克谱到目前为止。在文献[8，9]中，基于测试和测试集的概念，提出了一种新的处理等价的抽象共代数方法。在那里，等价和前序被建模为coalgebras行为endofunctors适当提升到一类测试套件TS。直观地说，如果两个过程不能通过给定测试套件中的任何测试来区分，则它们被不同的测试套件考虑，不同的概念的过程等效。这种一般的技术被应用到有限分支标记的转移系统的情况下，并从范Glabbeek谱的三个等价（迹等价，完成的迹等价和故障等价）的测试套件的特征。此外，还展示了如何将测试套件方法与[17]的双代数方法相结合，以系统地导出结构操作语义的同余格式。本文有两个新的贡献。首先，测试套框架被证明涵盖了其他三个等价的频谱：准备跟踪等价，模拟等价和互模拟等价。此外，通过Hennessy-Milner逻辑的各个片段中的测试和模态公式之间的对应，以比[9希望这能让读者相信，范·格拉贝克光谱中的其他概念也可以以类似的方式被特征化。其次，给出了提升行为内函子的所有余代数（而不仅仅是[8]中这就产生了新的，专门的共归纳证明原则的各种操作等价。B. Klin/Electronic Notes in Theoretical Computer Science 106（2004）201203P×例如，定义Tr-感知关系的概念，使得（1）迹前序是最大的Tr-感知关系，并且（2）Tr-感知关系具有足够的结构以便于证明给定的关系是Tr-感知的。这允许一个证明共归纳，两个给定的过程是跟踪等价的，通过显示任何Tr-感知的关系，将它们联系起来。因此，Tr-感知的关系连接到跟踪等价，以相同的方式作为互模拟连接到互模拟等价，或模拟到模拟等价。通过对TS上适当提升的内函子的余代数的仔细分析，得到了Tr-感知关系的概念。在第2节的概述之后，第3节回顾了测试套件的抽象框架。在第4节中，它专门用于行为BX=f（A X），以及来自van Glabbeek规范的几个等价物。trum与B的余代数有关，适当地提升到TS范畴。在第五节中，我们更详细地研究了这些余代数，从而定义了各种余诱导原理。一个简单的应用原则（对应于迹线等效性）见第6节。相关工作的简要说明见第7节。致谢。作者非常感谢Gordon Plotkin的灵感和鼓励，Pawel Sobocinski的许多讨论，以及匿名裁判的有用评论。2预赛在这一节中，我们提出了与标号迁移系统、运算等价和共归纳相关的标准概念和结果，主要来自[3]和[15]。定义2.1标号迁移系统（LTS）<$X，A，−→ <$X是一个集合X，一个过程，一个动作集合A，以及一个转移关系−→X×A×X。通常，我们会写ex−→axJinsteadof<$x，a，xJ<$∈−→。F或anyx∈X，在e定义条件下，初始值I（x）=，a∈A：x−→axJ，其中xJ∈X，.一个LTS<$X，A，−→ <$是有限分支的，如果对每个过程x∈X，有ar e onlyfinitelymay yyproposesxJ∈Xandactionsa∈Asuchchatx−→axJ.一个LTS，其底层图（通过忽略所有操作获得）是一个有根的，有向树被称为标记同步树。定义2.2给定一组动作A，考虑模态公式的集合FTr、FRdTr、FS和FBS，由以下BNF文法给出（此处a的范围204B. Klin/Electronic Notes in Theoretical Computer Science 106（2004）201⟨−→⟩|F±±±⊆×⊆×±±一在A上，并且Q在A的子集上的范围）：FTrφ：：= T|a|⟨a⟩φ|QFSφ：：= T| ⟨a⟩φ|φ φFBSφ：：= T| ⊥ |⟨a⟩φ|[a] φ|φ∧φ|φ∨ φ定义2.3给定LTSh =X，A，，过程和模态公式之间的满足关系=h归纳定义如下：X|= hT总是x |= hnever一X| = haφ XJ|= hφ对于某个xJ使得x−→ xJ一X|= h[a]φ XJ|= hφ对于所有xJ使得x−→ xJX|=hQ⇐⇒ I（x）=QX|= hφ1 x |= hφ1和（或）x |= hφ2公式BS的集合与上述解释一起被称为（无穷）Hennessy-Milner逻辑。定义2.4对于任何W∈ {Tr，RdTr，S，BS}，考虑相应的运算规则WXX和非线性等价函数cex=WXX，在给定的LTS h上定义如下：x±WxJ∈ FW. X| = hφ = xJ|= hφ）xφ=WxJφ（φ∈FW.X|=hφxJ|=hφ）给定LTS上的前序Tr和RdTr通常称为迹前序和就绪跟踪前序。相应的等价物以类似的方式命名。 TheepreordersS，下面更详细地考虑BS和等式BS=S，BS=BS。在下面的定义中，假设一个给定的LTS<$X，A，− → <$定义2.5关系R<$X×X是模拟，如果xRy意味着一• x −→ xJ。y −→ yJ。 xJRyJ.此外，如果xRy意味着• ∀y−→ yJ。x−→axJ. xJRyJ.那么R是互模拟。定义2.6过程x，y∈X是• 在模拟预排序中，如果存在模拟R使得xRy，一B. Klin/Electronic Notes in Theoretical Computer Science 106（2004）201205→• 模拟等效，如果存在模拟R、RJ，使得xRy和yRJx，• 互模拟等价，如果存在互模拟R使得xRy。命题2.7模拟前序确实是一个前序，它是给定LTS上最大的互模拟等价实际上是一种等价关系，它是给定LTS上最大的互模拟命题2.8在任何LTS中，关系±S等于模拟前序，关系R=S等于模拟等价，关系s±BS和B= BS与双模拟方程是正交的。余代数在抽象过程论中的应用是由Pf（A×−）-余代数（其中A是一个固定集，Pf：Set→Set是协变有限幂集函数）和有限分支标号转移系统之间的简单对应所推动的。事实上，<$X，A，−→ <$，考虑函数h：X→ Pf（A×X），定义为：a，xJ∈hxx−→axJ很容易检查这给出了1-1的对应关系。在下文中，我们将经常默默地使用这种对应，用它们对应的余代数来标识有限分支的通过改变内函子B，可以得到余代数与确定性自动机、带状态谓词的标记转移系统、概率转移系统等之间的类似对应关系（见[15]）。用于将转移系统表示为余代数的函子B通常称为行为内函子。这个概念只反映了使用B的上下文，并不限制所考虑的函子类众所周知，有限幂集函子Pf允许最终余代数[2]。特别是命题2.9对任何集合A，内函子BX=Pf（A×X）有一个最终余代数φ：<$B<$，其中<$是用A的元素边标记的（可能无限）有限分支同步树的集合，由互模拟等价表示。3过程关系的测试集方法在这一节中，我们回顾了测试套件方法[8]，以处理良好结构的关系，建模为余代数。该方法受到Plotkin未发表的想法的启发，Plotkin使用测试的拓扑来表示完全偏序的互模拟。206B. Klin/Electronic Notes in Theoretical Computer Science 106（2004）201∈−联系我们在第4节中，将展示这种方法如何允许从van Glabbeek谱表示操作前序和等价。表示2=tt，ff。对集合X的测试是函数V：X2. 集合X上的测试套件是X上的一组测试。在X上的所有测试集的集合，被（反向）包含部分排序，记为X。对于任何函数f：X→Y，定义单调重索引函数f：Y→X，f∈θ={V∈f：V∈θ}其中θ Y=θ。 很容易检查这给出了一个函子（）从Setop到 偏序集的范畴Pos在这个函子上，人们执行著名的Grothendieck构造（参见例如[5]），获得以下内容定义3.1测试套件类别TS定义如下：• TS中的对象是对<$X，θ<$，其中X是一个集合，θ∈X<$，• 态射f：。X上的每一个测试都可以用X的一个子集来识别。然而，我们坚持测试的函数表示，因为它将使进一步的发展（特别是下面提升的内函子BW的定义）看起来更自然。我们将用T和F来表示常为真和常为假的检验。我们还将谈到测试的并集和交集，用和表示，并以明显的方式定义。任何测试套件都包含两个规范的专门化关系：定义3.2设θ是任意集合X上的测试集。 专业化等价θ=θ和s_p_p_r_der≤θ由d定义θ={x，y∈X×X|V∈θ。Vx=Vy}≤θ={∈ X× X |V ∈ θ。 V x = tt Vy = tt}这是直接表明，测试套件态射保持特殊化前序和等价。有人说，如果p<$B<$=B<$p，则内函子B <$：TS→TS提升内函子B：Set→Set，其中p：TS→Set是明显的遗忘函子。任何函子B：Set→Set都可以通过多种方式提升为TS上的内函子，通过定义其在测试套件上的作用。就我们的目的而言，有一种特别有用的方法。这种结构良好的提升内函子的方法是基于测试构造函数和闭包的概念。直观地说，人们可能会将测试视为在过程上解释的公式。然后测试构造器对应于公式语言中的模态运算符B. Klin/Electronic Notes in Theoretical Computer Science 106（2004）201207→→XXXH.θh：X→BX可以被限制到B-代数方程组：θX，θx →BX，Bθ，如果HHφ∈→B，BWωW是最终的BW-余代数，其中ωW是ΦW。Ω和闭包对应于命题连接词。第4节中给出了支持这种直觉的更具体的例子定义3.3设B是集合上的闭函子。对集合B（2）的测试称为B-测试构造函数.定义3.4测试集闭包是一族单调函数Cl X：XX对每个集合X都有f，使得对任何函数f：XY，对于任何在Y上的测试集θ中，有Cl Xf<$θ= f<$Cl Yθ。命题3.5设B是集合上的闭函子。任何一组B-测试构造函数W3和任何闭包Cl都将B提升到TS上的一个内函子BW，定义为：BW<$B，θ<$=.BX，BWθ<$BWf=Bf其中对任意集合X，作用BW：X<$→（BX）<$是单调函数定义为BWθ=Cl BX{w <$BV|w∈W，V∈ θ}让BW：TS→TS定义如上。 对任意B-余代数h：X→BX，定义算子ΦW：X→X，ΦWθ =h<$BXθ它显然是单调的，因为h和BX都是单调的。BW-余代数对应于这类算子的预定点：一个B-余代数W WX且仅当θ<$ΦWθ。 在这种情况下，我们说θ把h提升到一个BW-余代数。遵循测试和模态公式之间的直观对应，BW-余代数是配备有在来自W的模态算子下和在由Cl定义的命题连接下闭合的性质（谓词）集的B最少这样的集合对应于在底层B-余代数上解释的某种模态逻辑。这种直觉将在第4节中再次得到证实。.命题3.6如果B有一个最终余代数φ：φ→Bφ，则φ：.，ωW最后的BW-余代数允许构造，对于任何B-余代数h：XBX，“提升h的最小BW-余代数“，即， 最小测试集θX升降机h到一个BW-余代数：[3]这个W与定义2.4中使用的W的关系将在4.2节中变得清楚208B. Klin/Electronic Notes in Theoretical Computer Science 106（2004）201→H→P×命题3.7在上面的符号下，对于任何余代数h：X BX，Φ W的最小不动点（或者等价地，X <$中将h提升到BW-余代数的最小元素）等于k <$ωW，其中k：X <$是h的余诱导扩张。在下一节中，我们将展示如何将过程上的各种已知等价和前序表示为测试集k<$ωW的特化等价和前序，以用于将行为提升到类别TS。4由测试集在这一章中，我们专门讨论第3节中描述的一般框架，以描述来自vanGlabbeek谱的运算等价和前序的各种概念 为此，fix闭函子BX = f（AX）为固定集合A。在下文中，将基于B-测试构造器的集合W的不同选择来提出B到TS的对于W，B的不同选择，W-余代数将通过特殊化关系与vanGlabbeek谱的运算等价和预序联系起来。对应关系将通过Hennessy-Milner逻辑的各个片段中的模态公式进行，说明测试和公式之间的对应关系，测试构造器和模态运算符之间的对应关系，以及闭包和闭包之间的对应关系。命题连接词4.1测试构造函数和闭包我们首先定义一些B-检验构造函数，用于表示来自van Glabbeek谱的关系。定义4.1对于任何a∈A，Q<$A，定义测试构造函数wa，w[a]，waQ：B2→ 2如下所示waβ=tta，tt∈β w[a]β=ffa，ff∈βw<$aQβ=tt <$$>w<$a<$β=tt且{a∈A：<$a，−<$∈β}=Q以下几组测试构造函数将非常有用：B. Klin/Electronic Notes in Theoretical Computer Science 106（2004）201209.Σ联系我们j=14.2定义Tr=w<$a<$：a∈ARdTr=Tr<${w<$aQ：a∈A，Q<$A}BS= Trw[a]：a ∈A我们还将考虑三种不同的闭包：定义4.3闭包ClT、Cl和Cl的定义如下：ClTXθ=θTClθ={nXVi：n∈N，Vi∈θ}Cl<$θ =，n mVij：n，m∈N，Vij∈θ，很容易检验上述方程是否确实根据定义3.4定义了闭合。最后，来自定义4.1的B-测试构造函数集合，与适当选择的闭包一起，沿着命题3.5的路线，将B提升到TS定义4.4对于W Tr，RdTr，TS上由B-检验构造函数集W和闭包Cl T诱导的内函子记为BW。TS上由B-检验构造函数Tr和闭包Cl_n诱导的闭函子记为BS。TS上由B-检验构造子BS和闭包Cl_n_n诱导的闭函子记为BS。4.2与模态逻辑的不难注意到，定义4.2中所示的测试构造函数集与定义2.2中所示的BNF语法中的模态构造函数相关。这不是巧合，事实上，定义2.2中的模态逻辑启发了定义4.1-4.3。这一小节致力于给出这些定义之间的形式对应。定义4.5设W∈ {Tr，RdTr，S，BS}，设h：X→BX是LTS。Xi=1i=1210B. Klin/Electronic Notes in Theoretical Computer Science 106（2004）201.- 是 的ΣΩ定义一个函数[−]h：FW→（X→2），归纳如下：[T]h=T[]h=F[aφ]h=waB[φ]hh[Qaφ]h=waQB[φ]hh[a]φ]h=w[a]<$B[φ]h<$h[φ1<$φ2]h=[[φ1]h<$[φ2]h[φ1<$φ2]h=[[φ1]h<$[φ2]h模态公式和试验之间的对应关系在定理4.6设W∈ {Tr，RdTr，S，BS}，h：X→BX是LTS.对于任何公式φ∈FW和任何x∈X，[φ]hx = ttx|= hφ证明模态公式的简单结构归纳Q上述对应关系将模态逻辑映射到最小测试套件，将余代数提升到内函子BW：定理4.7设h：X→BX是B-余代数，k：X→ BX是h的余诱导扩张.对于W∈{Tr，RdTr，S，BS}，{[φ]h|φ∈FW}= k<$ωW其中ωW取自最终BW-余代数φ： ，ωW→B，BWωW。定理4.7允许我们把给定余代数h：X→BX上的运算前序和等价描述为将h提升到TS上各种内函子的余代数的最小测试集的特化关系，如下所示。推论4.8设h：X→BX是B-余代数，k：X→ BX是h的余诱导扩张.对于W∈{Tr，RdTr，S，BS}，±W=≤k<$ωW和=W==k<$ωW比较定义2.4和3.2，并使用定理4.6和4.7。Q这个重要的推论给出了范Glabbeek谱的前序和等价的然而，甚至更强的对应关系之间的BW-余代数和运算关系可以显示，提供了一个完整的表征BW-余代数。在第5节中，我们提出了这种对应关系，然后在第6节中应用它来推导共归纳证明原理。B. Klin/Electronic Notes in Theoretical Computer Science 106（2004）201211X.ΣBX，BSθR±→是关于h：X→BX的严格自反和传递的模拟。.B_S-代数h：θ_X，θ_X→的S_p特殊化n_p序s≤θ专业化当量=B的θ- 余代数h：<$X，θ<$→ BX，BXθRBX，BBSθR是关于h：X的完全自反和传递的互模拟→C. BBS-代数h：<$X，θ<$→的S特殊化np序s≤θBX. 专业化当量= B的θ- 余代数h：<$X，θ<$→BX，BXθR5测试集余代数我们首先刻画了BS和BS-余代数的运算前序和等价性.其余的前序和等价的范Glabbeek频谱处理后。下面的两个定理证明了BS-余代数的特殊化前序是严格自反和传递的模拟（见定义2.5）。定理5.1对任意的BS-余代数h：<$X，θ<$→BX，BSθ，特殊化预序≤θ是h：X→ BX的自反传递模拟.定理5.2对任意余代数h：X→BX，以及h上任意自反传递模拟R，存在X上的测试集θR，使得≤θR = R和h：<$X，θR<$→。BX，B θR是一个有效的B-余代数.S SX证明（草图）假设h：X BX上的任何自反和传递模拟R，并考虑X上的以下测试套件：θR={V：X→2：V是R-上}其中V是R-上意味着对于任何x，y∈X，如果xRy和Vx=tt，则Vy=tt。 然后检查θR是否满足上述条件。QX轴。S是与h：X→BX上的自反和传递模拟R相关联的等价关系R<$R−1。BS-余代数的一个类似的特征可以用类似的方式得到：X公司简介.英国广播公司是与h：X→BX上的自反和传递互模拟R相关联的等价关系R<$R−1。从推论5.4和4.8可以很容易地推断出任何h：X BX上的互模拟预序BS是h上最大的互模拟，这是一个众所周知的结果，在命题2.9中陈述。这与通常的推导证明原理有关，该原理用于表明某些操作尊重双模拟等价性。许多例子证明使用这一原则，例如，在[15，第12节]。→212B. Klin/Electronic Notes in Theoretical Computer Science 106（2004）201→一一、、、XX.ΣBX，BWθ，关系≤θ是h：X→BX上的W-感知预序.xJSyJ∈X：<$y∈<$。y−→ayJ，I（x）=I（y）.X这暗示着，一个类似的特征BW-余代数的各种W可能会导致类似的证明原则，其他等价的范Glabbeek频谱。现在将介绍这样的特征，并且在第6节中显示了由此产生的证明原理给出了特殊化关系≤θ和θ=θ的充分特征化对于W∈ {Tr，RdTr}的BW-余代数，我们首先需要一些技术性的定义和结果。定义5.5一个关系S<$X×PX称为X上的拟预序，如果• 对于一个nyx∈X，xS{x}和x/S，• 对任意x，y∈X，n，χ<$X，如果xS <$，y∈n且ySχ，则xS（（n\ {y}）<$χ）.定义5.6设S是X上的拟预序。一个集合V<$X称为拟S-上集，如果对任意x∈V，且对任意X <$<$X使得xS <$，交V<$<$不为空.引理5.7设S是X上的拟预序，且f个任意元素x，y∈X. 若对每个拟S-上集Y<$X，x∈Y蕴涵y∈Y，则xS{y}.当Y={z∈X：z/S{y}}时，（s k e t c h）S h是拟S-上界. 以来y/∈ Y，也是x/∈ Y，因此xS{y}。Q定义5.8考虑一个LTS（一个B-余代数）h：X BX。 设a在A上的值域，Q在A的子集上的值域，x，xJ在X上的值域，以及n在X的子集上的值域。一个关系SX×PX称为• h上的一对多Tr-模拟，如果每当xS ≠且x−→xJ，则xJS{yJ∈X|y∈y−→ayJ}，h上的一对多RdTr-模拟，如果S是一个整数，h上的多Tr-模拟，并且如果每当xS ≠且x−→xJ时，则对于W∈ {Tr，RdTr}，关系R<$X×X称为h上的W-感知的，如果存在h上的一个多W-模拟S，使得xRy<$xS{y}.此外，如果S是一个拟前序，则R称为W-感知前序。下面的定理和推论刻画了BW-余代数的特殊化预序和等价性为相应的W-意识预序.T. heorem2005. 9LetW={Tr，Rd Tr}. F或anyBW-代数公式h：θX，θx→证明我们证明了W=Tr的情况，另一种情况类似。首先，回想一下说h：<$X，θ<$→BX，BTrθ是BTr-余代数等价于说θ<$h<$BTrθ。 等价地，T∈θ且对任意V∈θ和a∈A，也B. Klin/Electronic Notes in Theoretical Computer Science 106（2004）201213≤ ⊆→⟨ ⟩ →Xwa BV h∈θ。 定义SX×PX如下：xSV∈θ。（Vx=tty∈. V y= tt）显然x≤θy当且仅当xS{y}，因此足以证明S是一个拟前序和一个多Tr-模拟。S是一个拟前序的证明很简单。 为了证明它是一个e-by-mannyTr-模拟，考虑到ranyx∈X，Assumex−→axJ且xJ/S{yJ∈X|y∈y−→aV∈θ使得• VxJ=tt，以及yJ}。根据S的定义，存在一个检验• VyJ=ff对于所有y∈n，y−→ayJ。考虑一个测试VJ=waBVh。 显然VJx=tt，但对于每个y∈N，VJy=ff. SinceV∈θ，alsoVJ∈θ，hencex/S.Q定理5.10设W={Tr，RdTr}。对任意的余代数h：X→BX，以及h上的任意W-感知预序R，存在X上的测试集θR使得≤θR = R和h：<$X，θR<$→。BX，BθR是一个有效的B-余代数.W WX再次证明，我们证明了W=Tr的情况。另一个案例也是类似的。假设在h上的拟前序和一对多Tr-模拟S使得xRy当且仅当xS{y}。定义（比较定理5.2）θR={V：X→ 2 |V是拟S-上的}为了检查R≤θR，假设xRy，或等价地，xS{y}。 考虑任何V∈θR使得Vx = tt. 由于V是拟S-上的，所以Vy = tt.为了检验θRR，假设对于每个V：X2，使得V是拟S-上的，如果Vx=tt，则Vy= tt. 根据引理5.7，很容易得出：xS{y}，即xRy。检查h：X，θ足以证明• T∈θR，以及.BX，BTrθR是一个有效的BTr-余代数，它是• 对任意V∈θR，也有w∈BV∈h∈θR。第一个条件很简单，因为T对任何拟预序都是拟S-上的在X上。对于第二个条件，假设任何V∈θR，记为VJ=w<$a <$$> BV<$h。取任意x ∈X，X使得xS和VJx = tt。后一种假设这意味着存在anxJ∈X，满足atx−→axJ且VxJ=tt。由于S是一个一对多Tr模拟，这意味着XJS{YJ∈ X|214B. Klin/Electronic Notes in Theoretical Computer Science 106（2004）201一→BX，BTrθR是h：X→BX上的Tr感知的前序。Xy∈y−→yJ}且（由于V是拟S-上）存在y，yJ∈X使得y∈n，y−→ayJ且VyJ=tt。 ThenVJy=tt. SincexSwerechosen任意情况下，VJ是拟S-上的。QC. orollary5.11对于BTr-代数h：λX，θ→，Sp特殊化np重排序s≤θh上的迹前序±Tr是h上最大的Tr感知关系。6应用：迹进程的共代数语义的一个最有用的应用是共归纳证明原理，它基于这样一个事实，即任何LTS上的互模拟等价是它上的最大互模拟。因此，要证明两个进程是互模拟等价的，提供任何将它们联系起来的互模拟就足够互模拟关系的丰富结构允许人们以非常方便的方式使用这个证明原理。它的使用的许多例子可以在例如[15，第12节]中找到。第5节所示的结果允许人们将类似的推理应用于范·格拉贝克谱的其他等价性。推论5.11将迹预序刻画为最大的Tr-感知关系.事实证明，Tr-感知 关 系 在 推 理 迹 等 价 时 有 足 够 的 结 构 ， 类 似 于 在 推 理botbisimulationequivalence时的结构模拟。我们现在展示这样的“迹的共归纳原理”的一个例子考虑一个最终的B-余代数φ：<$B<$（回想命题2.9）。 在集合上，定义结合、幂等和交换二元运算+ byp+q=φ−1（φp <$φq）现在定义一个函数glue：→作为B-余代数α：α→B α定义为：αp =，.a，a，pJ<$∈φppJ<$：a∈A，其中，表示+到n的有限子集的明显扩展。使用[ 15，第11节]中介绍的共归纳定义的一p，.，p 正是p−→p1N一glue（p）−→对于任何a∈A。我胶（p1+···+pn）B. Klin/Electronic Notes in Theoretical Computer Science 106（2004）201215我、，pJ。 根据S的定义，p=glue对于某个指标集I，使得对每一个i∈I，qi∈ {\displaystyle qi}。 根据胶水的定义i∈I例如，如果k是所有有限分支标记同步树的集合，则有一 ·B·ab·glue（·zzc）=··zzaz··cz·定理6.1操作glue保持并尊重迹。换句话说，对于任何进程p∈n，p和glue（p）是迹等价的。证明这个定理的一个标准方法是对迹的长度使用归纳法。相反，我们使用余归纳证明原理来证明迹，如推论5.11所示。首先，我们证明了关系{xglue（p），p∈xglue：p∈xglue}是一个Tr-感知关系.考虑S×P，定义如下：pS{q1，.，qn}粘合胶。i∈Iqi = p对于某个I{1，.， n}。考虑到r ∈A，S是一个简单的Tr-模拟. ，p，pJ∈N和因此，有pJ=glue。i∈I，qi−a→qJqiJ<$pJSqJ∈N ：Nq∈N。q−→a这就结束了证明的第一部分。qJ，接下来，我们证明关系{p，glue（p）：p∈}包含在一个有意识的关系。考虑S×P，定义如下：pS胶（p + q）∈，其中q∈。为了证明S是一个一对多Tr模拟，考虑任何a∈A，p，pJ∈S，S∈SuchthatpS，p−→apJ。 这种方法是指p+q−→apJ。通过胶的定义，胶e（p+q）−→a由此可见，glue（pJ+ qJ），其中qJ∈ n.因此glue（PJ+QJ）∈，RJ∈θ ：θr∈θ. r−→aRJ，pJS，rJ∈S ：r ∈S。r−→arJ，而S是一个一对多的模拟，它结束了证明。QQI216B. Klin/Electronic Notes in Theoretical Computer Science 106（2004）201H7相关工作抽象测试套件的方法来处理等价是新颖的，但其他几种方法的抽象表示的操作等价是已知的。最流行的互模拟的余代数方法，基于余代数跨度[1，15]，专注于一个单一的，规范的概念等价的每一个行为的概念。在标号迁移系统的情况下，这个抽象概念专门用于互模拟等价。一些尝试已作出修改的余代数跨度的方法，以涵盖迹等价。在[14，16]中，基础范畴被改变为半格范畴。在[13]中，余代数态射的概念被改变了。这两种方法都将迹等价定义为适当范畴中的（跨度）互模拟。[13]中采用的方法与测试套件框架有一些相似之处.在这两种方法中，余代数建模过渡系统被提升到另一个类别。然而，这些提升似乎根本不同。在[13]中，提升是基于幂集单子上确定性行为的函子的分布律，从而利用了LTS的行为内函子此外，在所得范畴中，所讨论的余代数保持不变，但余代数morphism的概念发生了变化。在我们的抽象方法中，行为函子的结构没有以任何明显的方式使用，事实上，我们从来没有使用过这样的事实，幂集函子是一个单子。并且，在B-Tr-余代数范畴中，余代数态射来自于B-余代数的基本范畴，但余代数本身是不同的（它们配备了测试套件，并要求是某些算子的预定点我们的方法与[4，6]的方法有更强的联系，在[4，6]中，我们的内函子被规范地提升到二元关系和关系保持函数的范畴Rel，它是在Set上定义的。在[12]中，在递归定义域的上下文中使用了类似的技术，其中甚至定义了我们的算子ΦW的对应物。在测试套件方法中，行为内函子被提升到类别TS，它也是在Set上产生的，但比Rel具有更多的结构，因此允许表示例如，迹等价此外，在测试套件方法中，我们放弃了提升的规范性（实际上，可以使用任意的测试构造器集），从而允许表示更多的操作等价概念。上面提到的所有抽象方法都旨在定义特定等价的抽象概念，由行为概念参数化：双模拟等价[15，4]，模拟等价[6]或迹等价[14，13]。我们的目标是，在某种意义上，更温和的，我们的目标是一个抽象的和一般的定义一个行为良好的进程等价。这使我们能够涵盖许多B. Klin/Electronic Notes in Theoretical Computer Science 106（2004）201217更多的例子比其他方法，但阻止我们正式之间的连接，例如，不同行为概念的互模拟概念。与模态逻辑相关，测试套件方法提供了模态操作符作为测试套件构造器的抽象必须研究这个概念如何与自然关系的概念相联系，自然关系用于表示共代数逻辑中的模态算子[10，11]。必须指出的是，来自van Glabbeek谱的三个等价：可能的未来，可能的世界和2嵌套模拟等价不能在本文所示的测试套件框架中描述。这与描述这些等价的模态公式不能由只有一个非终结符的文法表示的事实有关。这个问题可以通过选择一组不同的测试值而不是2来规避（参见[7]）。引用[1] P. Aczel和N.门德勒一个最终余代数定理In D. H. Pitt等人，编辑，Proc. CTCS[2] M. Barr. 集合上闭函子的终余代数理论计算机科学，114：299[3] R. J. van Glabbeek线性时支时间谱I. Bergstra，A. Ponse和S. Smolka，编辑，过程代数手册。Elsevier，1999年。[4] C. Hermida和B.雅各布斯结构归纳和共归纳在虚构的设置。信息与计算，145（2）：107[5] B.雅各布斯范畴逻辑和类型理论。第141号在逻辑和数学基础的研究。北荷兰，阿姆斯特丹，1999年。[6] B.雅各布斯和J·休斯。余代数中的模拟。In H. Peter Gumm，编辑，电子笔记理论计算机科学，第82卷。Elsevier，2003年。[7] B. Klin. 行为良好操作语义的进程等价抽象方法。2004年，奥胡斯大学，金砖国家，博士论文。马上就来[8] B. Klin和P. Sobocinski。免费的语法格式：一种处理等价的抽象方法。In R. Amadio和D.Lugiez编辑，Proc.CONCUR 2003，LNCS第2671卷，2003年。[9] B. Klin和P. Sobocinski。免费的语法格式：一种处理等价的抽象方法。金砖国家报告RS-03-18，奥胡斯大学，2003年。[10] L. 莫斯共代数逻辑Annals of Pure and Applied Logic，96：177[11] D.帕丁森余代数模态逻辑中的语义原则。在Proc.STACS 2001，LNCS的第2010卷中。SpringerVerlag，2001年。[12] A. M.皮茨递归定义域的共归纳原理。Theoretical Computer Science，124（2）：195[13] J. Power和D.图里线性时间语义学的共代数基础。电子笔记理论计算机科学，29，1999。218B. Klin/Electronic Notes in Theoretical Computer Science 106（2004）201[14] J. Rutten和D.图里并发的初始代数和最终余代数语义。在J. de Bakker等人，编辑，Proc. 并发的十年-回顾和展望，LNCS的第803卷，第530-582页。Springer-Verlag，1994.[15] J.J.M. M.拉顿泛余代数：系统理论。理论计算机科学，249：3[16] D. 图里结构化操作规则的分类建模：案例研究。 在proc CTCS'97，LNCS第1290卷，第127-146页。Springer-Verlag，1997.[17] D. Turi和G.普洛特金数学运算语义学。 在诉讼12安妮。IEEE Symp.《计算机科学中的逻辑》，LICS '97，波兰华沙，1997年6月29日至7月2日，第280-291页。IEEE Computer SocietyPress，1997.
我的内容管理
展开
