共代数互模拟和模拟的理论计算机科学电子笔记

可在www.sciencedirect.com在线获取理论计算机科学电子笔记286（2012）323-336www.elsevier.com/locate/entcs共代数互模拟与模拟的表达性刻画托比·威尔金森1，2英国南安普敦大学摘要在以前的论文中，我们介绍了内部模型的共代数模态逻辑，并显示了他们如何表达双模拟。 在这里，我们通过丰富预序集来扩展这项工作，在这样做时，导出包含互模拟和模拟表达性的表征关键词：丰富逻辑连接;预序集;余代数;互模拟;模拟。1引言在[15]中，给出了一个抽象的范畴论的表示性的刻画。这种特性是根据模态逻辑的内部模型，这些模型也在[15]中介绍过。在本文中，我们将这项工作扩展到包括互模拟和模拟。我们的新特征是通过丰富[13]的预序集来实现的，因此每个余代数的载体都正是这种关系给出了我们的模拟概念。这个想法首先在[6，7]中提出，其中作者丰富了Pos（偏序），但我们通过注意（如[13]）将其推广到包含互模拟，集合可以被视为具有离散前序-即 Set Setoid=DiscSetoid（离散setoid）。事实上，我们比这更进一步，并观察到，通过丰富Preord（前序），Pos，Setoid（setoids）和DiscSetoid，我们可以分别进行模拟，其中相互模拟是互模拟，相互模拟和互模拟1由EPSRC博士培训账户支持的研究。2电子邮件地址：stw08r@ecs.soton.ac.uk1571-0661 © 2012 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2012.08.021324T. Wilkinson/Electronic Notes in Theoretical Computer Science 286（2012）323，，关于双模拟的余代数模态逻辑的表达性的概念表明，两个状态在逻辑上等价当且仅当它们在逻辑上等价。这里逻辑上等价意味着 因此，存在着对与所有理论的集合相关联的等式关系以及与每个余代数的载体相关联的等式关系的隐含依赖。 正是这一点，我们推广，而不是使用这些对象现在携带的前序关系为了简洁起见，我们总结了我们需要的[15]中的重要思想，并应参考进一步的细节。本文的概要如下。在第2节中，我们概述了我们工作的框架。在第3节中，我们定义了预序集。在第4节中，我们回顾了[15]中的定义和我们需要的结果，并在第5节中定义了我们广义的表达性概念第6节包含了我们的主要特征结果，最后在第7节中，我们通过众所周知的表现性结果来模拟有限分支标记的迁移系统作为例子。2双邻接框架越来越多地，标准的方法，以共代数模态逻辑是制定它在一个双附加框架[10，8，5]。在[12]中，这被扩展到一个丰富的设置，其中丰富是在一个对称的monoidal闭范畴，是完全的和上完全的。我们使用的这个丰富的版本，以及在本文的其余部分，所有的范畴，函子等都应该被假设为丰富的。SLzAP该框架由两个范畴A和X以及两个逆变函子P和S形成一个对偶附加，即存在一个自然同构Φ：A（−1，P（−2））<$X（−2，S（−1））这样的双附加通常被称为逻辑连接[14]，我们用以下方式表示单位和计数：ρ：idAPSσ：idXSP范畴X表示一个状态空间的集合，在这些状态空间上，一个广义转移系统的集合被定义为一个内函子T的余代数。类似地，类别A表示要添加模态运算符的基本逻辑的集合。 这些都是通过一个内函子L引入的，相应的模态逻辑是L-代数。的语义zX，不T. Wilkinson/Electronic Notes in Theoretical Computer Science 286（2012）323325这些模态逻辑分两个阶段给出。首先，对偶附加给出了基逻辑在状态空间中的语义，其次，给出了一个自然变换δ：LPPAPPT根据T[9，11]引入的转换结构给出了模态算子的语义。文献中有许多非丰富情形的例子，例如参见[5]，在例3.4中我们将给出一个丰富的例子。3预序集回想一下预序集和单调函数的范畴Preord，其对象是由集合和该集合上的预序关系 组成的 对。类似 地， 范畴Pos （ 偏序集 合）、 Setoid（ setoids ） 和DiscSetoid（离散setoids）对于对象对具有由集合和分别在该集合上的偏序、等价关系或相等关系组成的对象对。在[13]中，这些例子被统称为预序集，它们对模拟的共代数分析有重要意义，我们稍后会回来讨论我们可以通过下面的定义来考虑这些例子，其中“R型”关系类型是固定的，并且范畴SetR中的每个对象都必须有该类型的关系。定义3.1范畴集合R对于由集合X组成的对象对（X，RX）和RX具有X上的R型二元关系。态射是R-保持函数，即。f：（X，RX）→（Y，RY）是态射当且仅当对所有x，x×∈XxRXx×<$f（x）RYf（x×）明确地说，我们有以下四种情况：(i) 如果R是前序类型，则SetR是前序。(ii) 如果R是偏序类型，则SetR是Pos。(iii) 如果R是类型等价关系，则SetR是Setoid。(iv) 如果R是类型相等，则SetR是DiscSetoid（显然与Set同构）。很容易证明，从集合R到集合的遗忘产生了极限和极限-（X，RX）和（Y，RY）的乘积由（X×Y，RX×Y）给出，其中（x，y）RX×Y（x×，y×）惠xRXx×和yRYy×，最终对象是（1，R1），其中1是单点集，R1=1×1。也很容易证明二元积和最终对象形成对称monoidal范畴的张量和单位。为了使集合R也是闭的，我们需要内部hom对象[（X，RX），（Y，RY）]使得[（Y，RY），−]右伴随于−×（Y，RY）。[（X，RX），（Y，RY）]的明显定义是所有R-保持326T. Wilkinson/Electronic Notes in Theoretical Computer Science 286（2012）323从X到Y的函数，f R[（X，RX），（Y，RY）]g惠<$x∈X f（x）RY g（x）此外，我们可以定义附加的单位η（X，RX）：（X，RX）→[（Y，RY），（X，RX）×（Y，RY）]由η（X，RX）（x）=fx：（Y，RY）→（X，RX）×（Y，RY），其中fx（y）=（x，y），以及伴随函数的计数ε（Z，RZ）：[（Y，RY），（Z，RZ）]×（Y，RY）→（Z，RZ）通过ε（Z，RZ）（g，y）=g（y）.因此，我们有以下命题。命题3.2范畴集合R是闭范畴。在本文的其余部分，我们做了以下假设。假设1范畴A和X对于某个固定的关系类型R在集合R上是丰富的。此外，范畴A和X是具体范畴，即 对象是具有某种附加结构的集合，并且携带R类型的关系，并且态射具有潜在的R-保持函数。我们这样做有两个原因。首先，在集合R上丰富是[6，7]方法的明显推广，其次，为了研究表达性，我们需要访问X中对象的各个状态例3.3在R是类型等式的情况下，则集合R上的扩充只是普通的范畴论，因此我们从文献中得到了所有逻辑连接的例子，例如参见[5]。下面的例子是我们的主要例子，当我们讨论表达性时，它将突出显示。例3.4在集合R上，在MSL（与top相交的半格）和集合R本身之间有一个丰富的逻辑连接。要看到这一点，我们需要观察MSL的对象带有两个内置的前序。第一个是众所周知的偏序，定义为x≤y惠x=xy，第二个是等式。在下文中，如果类型R表示前序或偏序，那么MSL的对象应该被认为具有标准偏序，如果R表示等价关系或相等，那么它们应该被认为携带相等关系。函子P：SetR→MSL将对象（X，RX）发送到其右R-闭子集的交半格。一个子集U<$X是右R-闭的，如果x∈U且xRXy蕴涵y∈U.P（X，RX）是按包含或相等排序的，这取决于类型R。函子S：MSL→SetR将交半格A发送给它的过滤器集合，也是根据类型R按包含或相等排序。T. Wilkinson/Electronic Notes in Theoretical Computer Science 286（2012）3233274模型、内部模型和R-模型在[15]中，我们引入了L-代数的模型和内模型的概念.我们在下面总结这些定义，并将它们扩展到集合R上的富集的情况。定义4.1[模型]对于L-代数（A，α），我们定义Mod（A，α），即（A，α）的模型范畴，对象由对（（X，γ），f：X→S（A））其中（X，γ）是T-余代数，f是态射，使得XfS（λA）S（α）JCγSL（A），，δAJCT（X）TS（A）T（f）上下班这样的f被称为理论图。这里δ：TSSL定义为δ=SLρδb S其中ρ是逻辑连接的单位，δb是逻辑连接下δ的附属物。Mod（A，α）的态射g：（（X1，γ1），f1）→（（X2，γ2），f2）由T-余代数态射g：（X1，γ1）→（X2，γ2）给出，使得f1=f2<$g.与范畴Alg（L）和CoAlg（T）一样，范畴Mod（A，α）在集合R上是丰富的，并且每个同态宾语上的（R型）关系是集合R中基础同态宾语上的对应关系.定义4.2[内部模型]给定X中的单态类M，我们定义IntModM（A，α）为Mod（A，α）的全子范畴，其中理论映射在M中，并写G：IntModM（A，α）→Mod（A，α）对应的包含函子。我们通过类M参数化，因为有时我们需要M具有额外的性质，例如，M的成员被保留由T.在[15]中，这被利用为吉里函子，它不保持所有的单态，但保持它们的一个特定子类328T. Wilkinson/Electronic Notes in Theoretical Computer Science 286（2012）323在[15]中，内部模型被用来验证互模拟的表达性。正如我们将在第6节中看到的那样，为了简化模拟，我们将需要下面的广义定义。定义4.3[R-模型]范畴R-Mod（A，α）是Mod（A，α）的全子范畴，其中理论映射是R-相关的。一个函数f：X→Y是R-自相关的，如果对所有x，y∈X，如果f（x）RYf（y）则xRX y.我们写H：R−Mod（A，α）→Mod（A，α）对于相应的包含函子。应该注意的是，如果类M的单态也是R-如果M（A，α）是R − Mod（A，α）的一个全子范畴，则M的态射对应于R关系型的嵌入，IntModM（A，α）是R−Mod（A，α）的一个全下面的定义对于我们描述表现力的特征非常重要，我们将广泛使用它。定义4.4我们说Mod（A，α）中的模型X通过IntModM（A，α）中的内部模型I分解，如果在Mod（A，α）中存在态射g：X→G（I类似地，如果在R−Mod（A，α）中存在态射h：X→H（J），则X通过R-模型J在R −Mod（A，α）中因子分解。在以后的章节中，我们还需要模型的共极限。因为我们是在一个丰富的设置工作，一般情况下是加权colimits，但我们将仅需要圆锥余限，即对应于普通范畴意义上的余限的那些。然而，我们不能忘记，中介morphism和cocone（对于固定的图和对象）的homobject必须与对象同构在集合R中，而不仅仅是集合。从相应的结果可直接得出下列两个定理[15]。 这是因为创建的余限被保留，并且类型R的关系在从图到对象的cocone集合上，对应于集合R中的底层。定理4.5遗忘函子U：CoAlg（T）→ X产生小的圆锥极限。定理4.6遗忘函子U：Mod（A，α）→ X产生小的圆锥极限。5表现力为了开发一个涵盖互模拟和模拟的表达性概念，我们首先需要扩展逻辑等价和行为等价的概念定义5.1给定两个模型X1，X2在Mod（A，α）中，状态x1∈X1，x2∈我们说x1和x2是逻辑R相关的，如果f1（x1）RS（A）f2（x2）T. Wilkinson/Electronic Notes in Theoretical Computer Science 286（2012）32332922其中f1和f2分别是X1和X2的理论映射定义5.2给定Mod（A，α）中的两个模型X1，X2，以及状态x1∈X1，x2∈X2，我们说x1和x2是行为R相关的，如果在Mod（A，α）中存在一个cosspan使得f1（x1）RX3f2（x2）.X1f1FX=3，，X= 2为了证明这些定义是正确的，我们首先考虑类型R是相等的情况。 在这种情况下，逻辑上的R相关简单地变成相等理论，正如预期的那样。对于行为R相关的定义，我们看到从Mod（A，α）到CoAlg（T）的遗忘函子产生了CoAlg（T）中的行为等价的通常定义，但除此之外，X的遗忘函子产生了一个条件，即理论映射是相容的。这是因为我们正在处理任意的L-代数3，而不仅仅是初始的L-代数，并且类似于[2]中互模拟的定义。因此，当类型R表示相等时，我们有互模拟的情况，如[15]中所示在类型R表示前序的情况下，我们想把x与y行为上R相关的定义解释为x被y模拟。为什么会这样呢？在余代数中接近模拟的通常方法是通过一种称为关系子的东西[4，3，13]。在函子F：Set→Set的情况下，F-关系子是满足某些附加性质的函子Γ：Rel→Rel。利用这一点，可以定义F-余代数的Γ-模拟的一般概念。此外，与F和Γ相关联的是函子T：Preord→Preord[4，引理5.5]和[13，定义11]，由下式给出：T（X，RX）=（F（X），Γ（RX））在一定条件下[4，定理9.4]，最终T-余代数是最终F-余代数，其预序由Γ-相似关系给出. 这个最终T-余代数刻画了F-余代数的Γ-相似性，因为每个集合都带有一个离散的预序（等式）. 因此，对于每一个F-余代数，都有一个对应的T-余代数，给定两个F-余代数，这两个F-余代数上的Γ-相似关系由对应于最终T-余代数的唯一态射余跨度下的状态象上的预序给出[3，注21]。在我们的一般框架中，对于初始L-代数，每个T-余代数都有一个唯一的理论图，使其成为模型。 因此，如果存在最终T-余代数，它是一个模型，而且每一个其他的模型因子都唯一地通过它，因此它是最终的模型Z。所以对于任何模型的cospanX1f1FX=3，，X= 2使得f1（x1）RX3f2（x2），存在唯一的模型态射g：X3→Z，这给出g<$f1（x1）RZg<$f2（x2）.因此，如果T由如上所述的F-关系子给出，则我们的[3]使用任意L-代数可以直接处理命题变量，而不是将其作为零模。330T. Wilkinson/Electronic Notes in Theoretical Computer Science 286（2012）323相似性的概念与Γ-相似性是一致的因此，我们的模拟概念可以看作是接受模拟的F-关系子概念，并将其扩展到Mod（A，α）中的任意余跨距，而不仅仅是以最终T-余代数为目标的余跨距，还扩展到任意函子T，而不是由集合上的函子F和F-关系子Γ产生的函子。通过丰富来接近共代数模拟的想法首先出现在[7]中，尽管作者在Pos上丰富，而不是Preord。也是在[7]中，第一次建立了预序集上的富集和模拟的关系子方法之间的联系例5.3考虑例3.4的逻辑连接，其中我们将类型R固定为前序。然后逻辑上R相关对应于理论的包含。为了从行为上解释R相关，我们可以考虑集合R上有限幂集函子的推广。我们定义Pfin（X，RX）=（Pfin（X），RPfin（X））哪里URPfinn（X）V惠x∈ Uy ∈V.xRX y(this可以看出是[13]的Sim关系的一个例子）。 利用这个，我们可以定义T（X，RX）=Pfinn（（X，RX）×（X，RX））使T-余代数成为有限分支标号变迁系，标号来自于n。 此外，我们假设R是等式关系。 然后我们看到，对T-余代数γ：（X，RX）→T（X，RX），γ必保R的事实意味着xRX y意味着对所有（l，z）∈γ（x），存在（l，z×）∈γ（y）使得zRXz×，这将被看作是x由yy模拟的通常概念.R型的其他两种情况是模拟的变化，总结如下：(i) 如果R是类型前序，那么我们有模拟。(ii) 如果R是类型偏序，那么我们有相互模拟是互模拟的模拟(iii) 如果R是类型等价关系，那么我们有相互模拟。(iv) 如果R是类型相等，那么我们有互模拟。类型R决定了我们具有哪种行为关系，例如模拟或互模拟，但正是函子T的定义，特别是它在余域上定义R关系的方式（实际上可能通过关系子），决定了T-余代数的模拟实际上意味着什么。下面的结果是X中的态射是保存。命题5.4给定Mod（A，α）中的两个模型X1，X2，状态x1∈X1，x2∈X2，如果x1和x2行为上R相关，则x1和x2逻辑上R相关。T. Wilkinson/Electronic Notes in Theoretical Computer Science 286（2012）323331最后，我们的表现力定义如下。定义5.5L-代数（A，α）对Mod（A，α）是R-表达的，如果对Mod（A，α）中的所有模型，状态是逻辑R-相关的当且仅当它们是行为R-相关的。6表现力的表征在[15]中，我们给出了一个抽象的，范畴论的，互模拟的表达性的特征。在这里，我们将其扩展到包括模拟。实际上，这些变化是最小的，只不过是把IntModM（A，α）替换为R-Mod（A，α），把内射函数替换为R-反射函数。下面的定理给出了R-可表达性的充分条件定理6.1给定一个L-代数（A，α），如果下列成立：(i) Mod（A，α）中的每个模型都通过R-Mod（A，α）中的某个模型进行因子分解，(ii) 对于R−Mod（A，α）中的每一对I1，I2，存在一个cosspan I1→ I3<$ I2，R−Mod（A，α），则（A，α）是Mod（A，α）的R-表达式。证据取Mod（A，α）中的任意一对模型X1和X2然后这些因子分别通过R-模型I1和I2，并假设存在一个R-模型I3，使得在R−Mod（A，α）中存在一个cosspanI1→I3<$I2因此X1和X2都通过I3分解.具体来说，模型（（X1，γ1），f1）和（（X2，γ2），f2）通过R-模型（（I3，3），m3）通过T-余代数态射g1：（X1，γ1）→（I3，3）和g2：（X2，γ2）→（I3，3）因子化，使得f1=m3<$g1和f2=m3<$g2。现在假设两个状态x1∈X1和x2∈X2对于（A，α）是逻辑R则f1（x1）RS（A）f2（x2），这意味着m3<$g1（x1）RS（A）m3<$g2（x2），由于m3是R相关的，g1（x1）RI3g2（x2），并且x1和x2在行为上是R相关的。相反的方向由命题5.4给出。Q除了假设1之外，对于下面的几个结果，我们还需要对范畴Mod（A，α）做出假设。这些假设包含了我们证明结果所需要的精确的范畴论性质，然而，在推论6.5中我们将看到，这些假设实际上是从关于范畴X和函子T的更基本的假设中得出的。每当我们需要这些额外的假设时，这将在相关命题、引理或定理的前提中指明。假设2给定一个L-代数（A，α），范畴Mod（A，α）有小的推出，一个因子分解系统（EMod（A，α），MMod（A，α）），并且是EMod（A，α）-cowell-powered的，其中MMod（A，α）是Mod（A，α）中那些具有R-相关底层函数的态射的子类，EMod（A，α）是Mod（A，α）中那些具有满射底层函数的态射的子类.332T. Wilkinson/Electronic Notes in Theoretical Computer Science 286（2012）323利用假设2，我们可以证明定理6.1的逆命题。最困难的部分是证明（A，α）对Mod（A，α）的表达性意味着所有模型都通过R-模型因子化。定理6.2给定一个L-代数（A，α），假设命题2的条件成立，如果（A，α）对Mod（A，α）是R-表达的，则Mod（A，α）中的每个模型都通过R-Mod（A，α）中的R-模型分解。证据证明是相当长的和技术性的，但本质上与[15]的双模拟版本因此，我们将只勾勒出轮廓：(i) 观察到所有模型态射都有一个（EMod（A，α），MMod（A，α））-因子分解。(ii) 对于一个模型（（X，γ），f），使用Mod（A，α）是EMod（A，α）-共幂的，来取<（（X，γ），f）的EMod（A，α）-商对象的推出（（e j > I j，f），f ff）。(iii) 构造一个模型满态h：（（X，γ），f）→（（ Ij，j），f†）.(iv) 利用因子分解系统的对角化性质来表示wh，pj∈EMod（A，α）对所有j∈J.(v) 使用MMod（A，α）中的态射具有R-自反的底层函数来表明ff f具有R-自反的底层函数。(vi) 注意，这使得（Ij，ff）是R-模型.Q推论6.3给定一个L-代数（A，α），并有以下假设：(i) 假设2的条件成立，(ii) Mod（A，α）有二元余积，如果（A，α）对于Mod（A，α）是R-表达的，则对于R-Mod（A，α）中的每对I1，I2在R − Mod（A，α）中存在余跨距I1→ I3<$I2.证据给定两个R-模型I1和I2，由于它们也是模型，所以它们的余积存在，并且根据定理6.2，余积因子通过一个R-模型，例如I3，这导致I1和I2之间的明显余跨距。Q从定理6.1，6.2和推论6.3中，我们得到了我们的主要表达性结果- 一个抽象的，范畴论的，R-表达性的表征。定理6.4给定一个L-代数（A，α），并有下列假设：(i) 假设2的条件成立，(ii) Mod（A，α）有二元余积，（A，α）对Mod（A，α）是R-表达的当且仅当(i) Mod（A，α）中的每个模型都通过R-Mod（A，α）中的R模型进行因子分解，T. Wilkinson/Electronic Notes in Theoretical Computer Science 286（2012）323333(ii) 对于R−Mod（A，α）中的每一对I1，I2，存在一个cosspan I1→ I3<$ I2，R−Mod（A，α）.334T. Wilkinson/Electronic Notes in Theoretical Computer Science 286（2012）323假设2的条件是由关于范畴X和函子T的适当条件得出的。本质上需要的是X有足够的余极限，并且X有一个适当的因子分解系统，其单态被T保持。推论6.5给定一个L-代数（A，α），并有以下假设：(i) X是一个具体范畴（在集合R上），它有小的锥上极限，有一个因子分解系统（EX，MX），并且是EX-cowellpowered的，其中MX被选为X中那些具有内射和R-反射的底层函数的态射的子类，EX被选为 X中那些具有满射的底层函数的态射的子类，(ii) T保持MX，即m∈ MX<$ T（ m）∈ MX，（A，α）对Mod（A，α）是R-表达的当且仅当(i) Mod（A，α）中的每个模型都通过R-Mod（A，α）中的R模型进行因子分解，(ii) 对于R−Mod（A，α）中的每一对I1，I2，存在一个cosspan I1→ I3<$ I2，R−Mod（A，α）.证据我们必须证明定理6.4的前提成立。首先，我们通过定理4.6观察到Mod（A，α）具有小的圆锥余极限。为了证明X的因子分解系统提升到Mod（A，α），我们注意到在[5]中观察到，如果T保持MX，并且MX的成员是单态的，则X的因子分解系统提升到CoAlg（T），并且很容易看出这扩展到Mod（A，α）。最后，Mod（A，α）是EX-余幂的，因为EX中的态射是满射，这确保了给定Mod（A，α）中的一个跨距，其中底层态射在EX中，Mod（A，α）中的两个如此定义的EX-商对象之间存在同构，当且仅当，X中的底层EX-商对象Q7仿真实例为了更好地说明R模型的实际情况，我们将把众所周知的结果转换到我们的框架中，即语法给出的逻辑L3 φ：：= tt |φ ∧ φ|其中 l∈ φ是表达有限分支标记的过渡系统的模拟。这继续例5.3，类型R再次被固定为前序。我们的目标是定义一个L和δ，使得L是初始L-代数，那么任何T-余代数都有一个唯一的理论映射，使它成为L的模型。为T. Wilkinson/Electronic Notes in Theoretical Computer Science 286（2012）323335LLI任何这样的模型（X，RX），γ），f），我们将其因子分解如下FZeroz_（X，RX）e（I，RI） mS（CHL）S（=）JCγJcT（e）ζJcT（m）SL（），，δ∗LT（X，RX）T（I，R）TS--我是T（f）其中（I，RI），m）是L的R-模型。我们首先使用遗忘函子U：MSL→SetR及其左伴随F：SetR→MSL来定义模态，它创建了具有顶元素的自由交半格。特别地，F（X，RX）是变量集X上的通常的自由交半格F（X），其中关系RF（X）由等式关系给出，等式关系由[x]RF（X）[y]惠xRXy扩展，对所有x，y∈X。函子L则定义为L（A）=Fl∈<$U（A），我们选择δ如下δ（X，RX）：LP（X，RX）→PT（X，RX）TLP（X，RX）<$→ Pfin（（R，R）×（X，RX））[V l] LP（X，RX）→ {W ∈ Pfin（（R，R））×（X，R X））|<$（l，x）∈W.x ∈V l}[Vl1<$Vl2]LP（X，RX）<$→δ（X，RX）（[Vl1]LP（X，RX））<$δ（X，RX）（[Vl2]LP（X，RX））其中，符号Vl指示V来自UP（X，RX）的副本，L. 这对应于模态算子l，对于每个l∈，其中如果存在从状态到a满足的状态的l转换，则在该状态下满足l a。 从我们得到δA→SL（A）V→ {[W] L（A）∈L（A）|V∈δS（A）<$L（ρ A）（[W] L（A））}其中ρ A（a）={s ∈ S（A）|a∈ s}是逻辑连接的单位，因此δS（A）<$L（ρA）：L（A）→PTS（A）TL（A）→ Pfin（（S，R）×（S（A），RS（A）[a l] L（A）<$→ {V∈ Pf in（（n，Rf）×（S（A），RS（A）））336T. Wilkinson/Electronic Notes in Theoretical Computer Science 286（2012）323|<$（l，s）∈V.al∈ s}[al1<$al2]L（A）<$→δS（A）<$L（ρA）（[al1]L（A））<$δS（A）<$L（ρA）（[al2]L（A））其中符号a1再次指示a来自U（A）的由l索引的副本。回到我们的计划，我们接下来需要做的是通过一个R-反射态射M。我们使用众所周知的结果来做这一点，即轩尼诗-T. Wilkinson/Electronic Notes in Theoretical Computer Science 286（2012）323337×米尔纳逻辑（Lwith negation）是有限分支标记转移系统的互模拟的表达。具体地说，使用一个函子U：X → X，它给每个对象分配离散前序（换句话说，忘记当前前序），任何模型（X，R X），γ），f）都可以通过满射T-余代数态射e：（X，γ）→（I，γ）来表示，其中I是Hennessy-Milner逻辑的超滤子（最大相容集）的子集。然后有一个明显的函数m：I→US（A），它通过抛弃所有包含否定的公式将Hennessy-Milner逻辑中的超滤波器映射到L中的相应滤波器，此外，U（f）= m e。 思考这个问题的方法是，L中的过滤器列出了过渡系统中状态可以做的所有可能的未来事情，而Hennessy-Milner逻辑中的超过滤器明确地添加了它不能做的所有事情。注意：众所周知，互模拟与互模拟不同，因此m显然不是单射的。现在S（A）是按包含排序的，很容易看出我可以被给定，一个预序RI，使得e是R-保持的，并且m是R-保持和R-反射的。具体地说，我们可以通过包含顺序对I的超滤子在它们的否定自由子集上进行排序。此外，由于e是满射，所以（（I，U（m）），U（m））是L的模型。剩下要证明的是，m保持了前序RI，因为如果是这种情况，则（I，RI），m），m）是L的R-模型。很容易看出，如果T保持R-自映射态射，δ-自映射态射L 是令人尊敬的。 前者不是很∗很难证明，所以剩下的就是证明δL是R-反射的。事实上，对任意L-代数（A，α）证明了这一点。为了使这一假设成立，V/RT S（A）V×，V/RT S（A）V×惠（l，s）∈V。<$（l，s×）∈V×eitherll×或s/RS（A）s×现在，我们的计划是找到[al]L（A）∈L（A），使得al∈s，并且对于所有的（l×，s×）∈V×，ll×或al/∈s×。 如果不存在（l×，s×）∈V×使得l=l×，则我们可以取al=（TA）l.如果不是这种情况，则存在一个有限的对集合（l，s×）∈V×使得s/RS（A）s×。 N w s/RS（A）s×意味着s/RS×，所以有可能找到s的一个元素，它不在任何s中（成对地做，然后取交-我们可以这样做，因为V×是有限的）。因此，δA（V）/δA（V×），即δA（V）/RSL（A）δA（V×），以及δAβ是R-反射的。因此，我们证明了每个L因子的模型都通过一个R-模型.此外，本发明还由于集合R有余积，根据定理4.6，作为模型的任何一对R-模型的余积都存在，并且由于任何模型因子通过R-模型，这产生R-模型的余跨度。因此，我们已经满足了定理6.1的前提，因此我们可以得出结论，正如预期的那样，L对于有限分支标记转移系统的模拟是有表现力的。确认作者要感谢Corina C irstea的许多有趣的讨论和她的宝贵指导。特别感谢Alexander Kurz的分享338T. Wilkinson/Electronic Notes in Theoretical Computer Science 286（2012）323未出版的版本[7]。引用[1] Ad'amek，J.，H. Herrli ch，G. E. Stre cker，“Abstract and Concrete Categories，”Wiley NewYork，1990.[2] Blackburn，P.，M. de Rijke，Y.维内马，[3] C.，C.，Amodularapproachtodefiningandcharterisingconceptsof simulation，InformationandComputation204（4）（2006），469[4] Hughes，J.，B. Jacobs，Simulations in coalgebra，Theoretical Computer Science327（1-2）（2004），71-108.[5] Jacobs，B.，A. Sokolova，模态逻辑的示例表达性，逻辑与计算20（5）（2010），1041[6] K.，A. Kurz，J. Velebil，Expressivity of Coalgebraic Logic over Posets，CMCS 2010 Shortcontributions，CWI Technical report SEN-1004，2010，16[7] K.，A. Kurz，J. Velebil，Expressivity of Coalgebraic Logic over Posets，未出版的扩展版本，2011。[8] Klin，B.，超越集合的共代数模态逻辑，理论计算机科学电子笔记173（2007），177[9] Kupke，C.，A. Kurz，D. Pattinson，Algebraic Semantics for coalgebraic logics，Electronic Notesin Theoretical Computer Science106（2004），219[10] Kupke，C.，A. Kurz，Y. Venema，Stone coalgebras，Theoretical Computer Science327（1-2）（2004），109-134.[11] Kupke，C.，A. Kurz，D. Pattinson，Ultrafilter extensions for coalgebras，Lecture Notes inComputer Science3629（2005），263[12] Kurz，A.，J. Velebil，Enriched Logical Connections，Applied Categorical Structures（online first），2011，http://dx.doi.org/10.1007/s10485-011-9267-y网站。[13] Levy，P.，Similarity Quotients as Final Coalgebras，Lecture Notes in Computer Science6604（2011），27-41.[14] Mislove，M.，D. Pavlovic，J. Worrell，Testing Semantics：Connecting Processes and ProcessLogic，Lecture Notes in Computer Science4019（2006），308[15] 威尔金森，T.，共代数模态逻辑的内部模型，计算机科学讲义7399（2012），238