拓扑学与Hennessy-Milner逻辑在模态转换系统中的应用

理论计算机科学电子笔记161（2006）3-23www.elsevier.com/locate/entcs精化的拓扑分析迈克尔·胡特1英国伦敦帝国理工学院计算机系摘要一个模态转换系统有一类实现，即它的最大精化。这个类确定满足性和有效性判断，以及它们的合成近似，用于Hennessy-Milner逻辑的公式。利用拓扑学，我们证明了这些判断的结构性质：精化是实现类的反向包含，Hennessy-Milner逻辑通过有效性判断来表征精化，实现类是拓扑闭集，Hennessy-Milner逻辑在这些类上具有紧性定理，模态转换系统之间的鲁棒一致性度量是可定义的。特别地，Hennessy-Milner逻辑的每个公式都是Hennessy-Milner逻辑公式的有限析取，其有效性检查可简化为模型检查。保留字： 拓扑，精化，有效性，模型检验，模态转换系统1介绍1.1写这篇论文本文是松散的基础上，在第三届爱尔兰会议上的数学基础的计算机科学和信息技术在三一学院，都柏林，爱尔兰，2004年7月22日至23日的邀请谈话本文中讨论的所有技术成果均已在[14，15，18]中发表或已在其他地方提交[19]。然而，我们认为，讨论作为这些出版物的基础和统一的研究方案是有价值的，因为它创造了一个机会，以非正式的方式提出相当技术性的问题，并侧重于概念问题。这样的阐述也使我们能够以一种容易接近的、希望是动机良好的方式提出开放的研究问题。1 电子邮件：M. doc.imperial.ac.uk1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.04.0224M. Huth/Electronic Notes in Theoretical Computer Science 161（2006）31.2报告研究的动机拓扑学可以被看作是一种将数学技巧和见解从有限集合和函数扩展到无限集合的方法，其中这种扩展的约束和特殊性是研究的主题。这种有偏见的观点拓扑是适合我们的研究对象在这里。精化被理解为数学模型类上的二元关系。模型和它们允许的实现之间的实现关系被这种理解包含在将模型M与它们的所有“最大”的精化I在计算机科学的许多领域都可以找到对模型进行优化的需求。我们仅举两个例子，这两个例子都包含在本文讨论的技术改进概念中。例1.1（i）程序抽象：从程序P的操作语义可以构建状态和行为M的数学模型[26]。由于M可能有无限多或“太多”的状态，我们可能想把M抽象成一个“更小”的模型A，然后分析A。当M中所有可能的行为在A中也可能时，模型M应该精化A，这是M的安全模拟[5，4]。(ii)具体化：设计与实现的区别在于，状态或行为的某些方面尚未决定或已知。Microsoft .NET框架中的组件，例如，可能有一个main方法，它将启动执行，但如果组件是Web浏览器的音频插件，则可能没有这样的方法[9]。组件的任何实例要么有main方法，要么没有。但是组件的“设计模板”不会规定是否存在这样的方法。实现应该是设计的细化，这样所有可选或未指定的方面都已经确定。本文证明了拓扑对于证明关于精化的结构性质是有用的，因为它使我们能够证明限制于某类有限状态模型的精化的这些性质通过这种对精化的拓扑分析所获得的见解具有潜在的重要应用和后果，我们提到了两个模型之间的一致性度量，对实现类的满足性检查可能减少到模型检查，以及Hennessy-Milner逻辑和有限多个模型的常见这里介绍的工作也可以被视为相关工作链的统一：• de Bakker Zucker [8]的过程的度量语义，它解决了完备度量空间上的递归方程，• 一个用于系统的未指定和细化的框架，由Larsen Schloss在[25]中提出• 域理论建模过渡系统及其细化，这是M. Huth/Electronic Notes in Theoretical Computer Science 161（2006）35Abramsky在[1]中对部分互模拟进行了计算，• Lawson在[24]中首先提出了将经典拓扑空间表示为Domain的极大点空间。这种统一，以及它所提供的拓扑手段，可以用来确定对精化结构的理解，特别是• 时态逻辑的紧性定理，• 一种针对规格不足的一致性措施• refinement的实现是实现的逆包含，以及• 多个模型的集体模型检查我们概述了这些见解的性质和证明，但1.3文件概要在第2节中，我们介绍了本文中研究的模型及其改进概念，并提到这些模型具有很强的表达力。在第3节中，我们讨论了[15]中发展的完全抽象和通用的精化域模型在第4节中，我们证明了我们的域模型的极大点集，配备了由Scott拓扑诱导的拓扑，是一个Stone空间和互模拟等价类集的模型。这就导致了Hennessy-Milner逻辑在模型实现集上的紧性定理。在第5节中定义并研究了两个模型之间的一致性度量，其中实现集的紧凑性允许我们证明这些概念的鲁棒性。在第6节中，我们给出了一个证明，证明模型之间的精化只不过是各个实现集合的保留包容：一个模型M精化一个模型N，并且M的所有实现也是N的实现。因此，我们认识到，有效性检查是对Hennessy-Milner逻辑的某个公式集的模型检查，该公式集通过析取生成整个逻辑。最后，第7节结束。有关工作的说明，请参阅文献[14，15，18，19，132模态转换系统和精化在这一节中，我们定义模态转移系统，它们的共归纳精化，指出这种形式主义的表达性，并给出表征精化的时间逻辑的近似2.1模型例2.1[[18]]图1显示了一个“pub行为”的模态转换系统从状态“Waits”开始，保证事件“newpint”可以导致其他两个状态中的任何一个，如从“Waits”开始的两个实心转换所指示的。的6M. Huth/Electronic Notes in Theoretical Computer Science 161（2006）3饮料饮料会谈饮料会谈订单订单纽品脱等待纽品脱Fig. 1.一个指定pub行为的模态转换系统[18]。实线表示Ra-转变，虚线表示Rc\Ra-转变。从“Drinks”到“Talks”的虚线转换在本文中，我们固定了一组有限的事件。 模态转换系统M是一个元组(1)（Ra，Rc）• 其中k是状态空间，例如图1中的{Drinks， Talks， Waits}，• Ra由所有实线组成，[25]中的必须转换，•Rc\Ra包括所有虚线，[25]中的可能过渡• 表示所有“不存在”的• 存在关于转移关系的一致性条件：Ra<$Rc。作为一种特殊化，模态转换系统M有两种契约保证：保证Ra的元素被实现，而保证不实现R ×Act×R\Rc的元素后者是一种间接保证，因为Rc是契约可能行为的论域。该等担保须就再融资作出诠释例如，图1中的（Drinks， newpint， Talks）/∈Rc意味着事件'newpint'不能从任何细化'Drinks'的2.2细化这种对保证和可能性的理解暗示了对细化的共归纳定义[23，7，6]。一个关系Q<$$>× <$$>是一个模态转换系统的精化，如（1）i <$（s，t）∈Q意味着(i) 若（s，α，SJ）∈Ra，则存在（t，α，TJ）∈Ra且（SJ，TJ）∈Q(ii) 若（t，α，TJ）∈Rc，则存在（s，α，SJ）∈Rc且（SJ，TJ）∈Q。所以对于某些精化关系，t精化s（或等价地，s抽象t）i ∈（s，t）∈QQ.我们说，s和t是等价的，如果每个都是另一个。例2.2[[18]]在图2的右边，我们看到图1中模态转换系统的改进。的关系Q={（Drinks， BobDrinks），（Drinks， TomDrinks），（Waits，Waits），（Talks， BobTalks），（Talks， TomTalks）}M. Huth/Electronic Notes in Theoretical Computer Science 161（2006）37饮料饮料饮料饮料饮料谈判命令订单会谈会谈鲍勃饮料鲍勃谈话订单订单newpint等待纽品脱纽品脱等待纽品脱BobDrinks精炼饮料，订单纽品脱纽品脱TomTalks refines Talks.汤饮料会谈TomTalks饮料Q={（Drinks， BobDrinks），（Drinks， TomDrinks），（Waits， Waits），（谈话，鲍勃谈话），（谈话，汤姆谈话）}图二.左边是图1的模态转换系统。右边：这个模态转换系统的一个细化，由关系Q证明。是模态转换系统中的一个细化，模态转换系统是图2中左侧和右侧系统的联合。模态转换系统是基于事件的，因此模型的建模和分析似乎仅限于事件的概念。但事实并非如此。Godefroid Jagadeesan [10]已经证明，在实践中使用的大多数3值形式主义在PTIME和LOGSPACE中相互转换，使得模型和时态逻辑公式的转换保持并反映了模型检查的结果。两个突出的这样的形式主义是• Bruns Godefroid [3]的部分Kripke结构，它是元组（R_n;R_ n× R_n;L_a，L_c：AP→ P（R_n）），其中我们有2值转移（s，s_J）∈R，并且对于每个q∈AP，有3值状态命题L_a（q）<$L_c（q），并且• Kripke模态转移系统[14]是一个三元组（n;Ra，Rc<$ n×Act× n;La，Lc：AP→ P（n）），其中有三值转移Ra<$Rc和三值状态命题La（q）<$Lc（q），q∈AP.在这些模型中，s∈La（q）表示因此，[10]中的结果确保了我们的域模型和随后提出的拓扑见解捕获了所有这些精化形式主义，无论它们是基于事件的，基于状态的还是两者兼而有之。2.3时态逻辑创建规范的模型可能是设计的重要组成部分。 给定这样的模型，我们可能希望分析它，以便调试或验证设计。为此，我们使用一个简单的时间逻辑，Hennessy-Milner逻辑[17]。虽然这种逻辑没有固定点，但它对于有界测试、验证和模拟活动来说足够有表达力。给出了Hennessy-Milner逻辑的语法8M. Huth/Electronic Notes in Theoretical Computer Science 161（2006）3语法（2）φ：：= tt | ¬φ| ⟨α⟩φ| φ∧φ其中α的范围是有限的一组事件Act。 有两种判断：• S| = aφ，其意图是说“φ是在s处的sserted”，并且• S| = cφ，这意味着“φ在s处可能是不相容的”。第一个判断低于有效性判断(3)V（s，φ）={s的所有实现都满足φ}。第二个过度近似了双重满意度判断(4)S（s，φ）={ s满足φ的一些实现}我们回到精确度的损失和减轻它的可能性，这篇论文的结尾。判决的语义|= a和|= c是组成的，由下式给出：• S| = mtt• S| = m<$φ i（not s| =<$mφ，其中<$a = c且<$c = a）• S| = m（对于某些（s，α，SJ）∈ Rm，SJ| = mφ）• S| = mφ1φ2i φ（s| = mφ1和s| = mφ2）其中m∈ {a，c}。析取φ）的缩写，框模态[α]表示对于每个α∈Act的α。从上面的定义中，我们可以读到析取和盒子模态的语义：• S| = mφ1φ2i φ（s| = mφ1或s| = mφ2），以及• S| = m[α] φ i <$（对于所有（s，α，sJ）∈ R<$m，sJ| = mφ）。请注意，框模态的通用量化器在与判断模态双重的模态中的转换范围内例如，如果我们检查s| = a[α] tt，我们需要查看标记为α的s中的所有Rc-跃迁。[[18]]第一章：第一章(i) 我们有会谈|= cdrinkstt as（Talks，drinks，Drinks）∈Rc. 因此，会谈|= a¬⟨drinks⟩tt. 我们也有会谈|= adrinkstt，因为没有x，其中（谈话，饮料，x）∈Ra. 因此，会谈|= a在标记的转换系统上，重复式是一种同义反复。(ii) 我们都有一个这样的|=a[newpint][talks]（drinkstt<$drinkstt）as：• （Waits， newpint， Drinks）（Drinks， talks， Talks）是一个Rc路径，识别单词• Talks|=a按第（i）项的规定，这个例子所传达的直觉是，模态转换系统M“is”（5）[δ1][δ2]。 . [δn]（<$α <$φk<$$> α<$φk）M. Huth/Electronic Notes in Theoretical Computer Science 161（2006）39对于α，δ i ∈ Act和适当的Hennessy-Milner逻辑φ k，=语义学。|适格性意味着φk的集合必须足够大以刻画精化。例如，我们可以选择Hennessy-Milner逻辑的所有公式作为φk，因为Larsen已经证明[23]，使用我们的符号，以下陈述对于模态转换系统的状态s和t(i) statet修饰states(ii) 对于Hennessy-Milner逻辑的所有φ，|= aφ表示t| = aφ(iii) 对于Hennessy-Milner逻辑的所有φ，|= cφ隐含s| = cφ。这个结果推广了互模拟的相应结果，因为对于标记迁移系统，精化是互模拟，|=a等于|= c，并且是标记迁移系统上的Hennessy-Milner逻辑的熟悉的语义，其中标记迁移系统（R，R）被解释为模态迁移系统（R，R，R）。这种逻辑特征的另一个重要结果是，|= aφ在上述第（ii）项s的修正下是合理的，而判断t| = cφ在上面第（iii）项的t的抽象下是合理的，其中t的抽象是一个状态u，使得t限定u。3细化的域模型3.1作为隐喻在本节中，我们使用Scott读者可能希望查阅简短的附录A，了解域理论的基本术语和符号[2]。域D具有作为模态转换系统D的自然解释，使得D是普适的：所有模态转换系统都有细化-等价嵌入 域D也是完全抽象的：定义域D是D中的最大加细关系，它是D中所有加细的并集。这两个属性，以及两个拓扑结构的D，是确保本文中提出的结果的关键成分例3.1图3显示了区间域及其排序：[r，s]≤[rJ，sJ] i（r≤rJandsJ≤s）。在这种情况下，我们说[rJ，sJ] refines [r，s]。区间整环很好地说明了我们期望整环D的整环模型所具有的一些性质。(i) 如果实数x∈ [0，1]表示为区间[x，x]被看作区间的可能实现，则[r，s]有{[x，x]|x∈ [r，s]}作为一组实现。既然我们可以用[r，s]来标识该集合，因此很明显[r，s]由[rJ，sJ]来定义，[rJ，sJ]的所有实现也是[r，s]的实现。(ii) 普适性：区间域I对于最坏/最好情况抽象是普适的。[0， 1]的子集 如果我们用区间[X，X]，后者在I中，并且I的任何元素都是至少一个这样的X的抽象。10M. Huth/Electronic Notes in Theoretical Computer Science 161（2006）3[0， 0][r，r][RJ，RJ] [x，x][sJ，sJ][秒，秒][1， 1][rJ，sJ][r，s]区间域[27]I ={[r，s]|0 ≤r≤s≤ 1}[0， 1]图三. 区间整环及其阶的一个图解描述：[r，s]≤[RJ，SJ] i <$（r≤RJandSJ≤s）.(iii) 完全抽象：如果精化关系意味着实现的反向包含，则I上的顺序准确地捕获了精化关系，这是由于上面的第（i）项。(iv) 作为极大点空间的经典空间具有欧几里得拓扑的集合[0， 1]作为拓扑空间同构于由I的Scott-或Lawson-拓扑导出的拓扑中的I的极大元的集合。(v) 可计算结构的稠密性：具有有理端点的区间近似区间到I内的任何精度。(vi) 一致性度量：由c（[r，s]，[rJ，sJ]）= [max（r，rJ），min（s，sJ）]的映射c：I×I→I，其中如果x /≤ y，则[ x，y ]被理解为，通过检查它的输出是否彼此一致来告诉我们它的输入是否彼此与之不同的是，3.2域模型[15]我们的目标是为模态转换系统设计一个域模型D，并将它们的精化与max（D）中的元素对标记转换系统具有类似的事实特别地，我们希望确保加细是完备的，并且存在有意义的单调一致性测度c：D×D→I。域模型D[15]是作为以下方程的初始解、ω-代数解和双有限解D获得的：（六）D=α∈ActM[D]其中M[D]是Heckmann Gunter [12，11]的混合幂整环。M[D]的元素都是对（L，U），其中L= ↓L和U= ↑U是Lawson闭的，并且（L，U）满足混合条件（七）M[D]上的阶由下式给出：L= ↓（L <$U）。(8)（L，U）≤（LJ，UJ）i <$（L<$LJUJ <$U）M. Huth/Electronic Notes in Theoretical Computer Science 161（2006）311α所以L集在M [ D]中以递增序列增长，U集在M[D]中以递增序列收缩例3.2[[18]]下面是D的一些元素：•D=（{}，D）α∈Act∈D模拟了一个• （{}，{}）α∈Act∈max（D）模拟死锁，因为它不可能参与任何事件;这本质上是一个标记转移系统。条件（7）证明是Ra<$Rc的有序版本，因为我们可以使D成为模态转换系统[15]。这背后的想法是，集合L编码Ra-后继者的集合，U编码Rc-后继者的集合，如递归（6）中那样按事件排序递归模式(9)d=（（da，dc））α∈Actα α从（6）导出定义元组D=（D;Ra，Rc），其中(10) Ra={（d，α，DJ）∈ D × Act × D |dJ∈da}Rc={（d，α，DJ）∈ D × Act × D |dJ∈dc}α所以da（dc）是d（分别）的Ra-后继者（Rc-后继者）的集合，α α α αα∈Act。一个小细节值得注意：我们有Ra/Rc，因此D不是模态的过渡制度但是，如果我们将与前面相同的加细定义应用于可能不满足Ra<$Rc的系统，则D根据（7）与模态转移系统（D;Ra<$Rc，Rc）是加细等价的[15]。因此，对于D，只要我们指的是模态跃迁系统（D;Ra<$Rc，Rc），我们就有权写D注3.3我们不知道不满足Ra <$Rc的系统（R; Ra，Rc）在（R; Ra，Rc）有某个标号的转移系统作为加细时是否与某个模态转移系统加细等价。也就是说，我们不知道混合条件（7）对于实现类的非空性是否也是必要的（而不仅仅是足够的）。D [ 15 ]的普适性表明，对于任何初始状态为i的模态转换系统M，|M，I| n ∈D，使得（M，i）和（D，n| M，I|其中，对于具有初始状态i的模态转换系统M，我们写（M，i），并且其中，精化意味着初始状态对初始状态的精化。这个结果可以证明如下，完整的证明请参见[15]：(i) 对于每个n≥0展开和截断（M，i）作为深度≤n的树，(ii) 用文法表示三值过程代数中的截断项(11)p：：= 0 | ⊥ | αtt.p| αβ.p|p + p（α∈Act）其中子句p+p中的p都不允许是k，(iii) 将（M，i）实现为2这一事实在[15]中得到了证明，对于图像有限模型，其中对于所有s∈A，α∈Act，m∈ {a， c}，{sJ∈ N|（s，α，SJ）∈ Rm}是有限的。12M. Huth/Electronic Notes in Theoretical Computer Science 161（2006）3饮料{|0|}=（（{}，{}））α∈Act{|⊥|}= 0（）在|αtt.p|}a，{|αtt.p|}c）=（↓{|p|联系我们|p|）的文件α α（）在|αβ.p|}a，{|αβ.p|}c）=（{}，↑{|p|）的文件α α（）在|αv.p|}a，{|αv.p|}c）=（{}，{}），αβ，v∈ {tt，τ}β β{|p + Q|联系我们|p|}m{|Q|}m，γ ∈ Act，m ∈ {a，c}γ γ γ见图4。D.过程术语的指称语义它将0解释为死锁，将0解释为universal stub，将+解释为[12]的混合并集，并按照预期的方式进行前缀（加上↓和↑的饱和度）。γ∈Actγ∈Act饮料BobDrinks会谈BobTalks订单订单汤饮料等待TomTalks纽品脱等待订单纽品脱纽品脱纽品脱汤饮料汤饮料会谈TomTalks饮料图五.向左：图2中“TomDrinks "深度1的截断我们观察到两种叶子：通用存根和死锁。(iv) 通过图4中进程代数项的指称语义将截断p嵌入到D中，(v) 在D中使用连续性/紧性参数来实现细化等价。为了便于说明，图4中给出了D中过程项的表示。示例3.4[[18]]图5显示了图2中状态'TomDrinks'的深度1的截断示例我们观察到两种叶子：通用存根，这里是接下来，我们可以证明D的完全抽象[15]，说D上的序是D上的最大加细关系，它是所有加细关系的并集：对于所有d，e∈D，我们有d≤ei（D，e）加细（D，d）。为了证明这一点，我们(i) 证明D上的阶≤是D内的一个精化，它被硬连接到D和D的定义中，并且(ii) 使用精化的逻辑特征来证明d/≤e意味着（D，e）不精化（D，d）：(a) K（D），D的紧元素的集合，序生成D，因为后者是会谈订单饮料M. Huth/Electronic Notes in Theoretical Computer Science 161（2006）313代数sod/≤e蕴涵k≤d和k/≤e，其中k∈K（D）(b) 对于每个k∈K（D），存在一个Hennessy-Milner公式φk，使得对于所有f∈ D：k ≤ f i <$f |= aφk(c) 因此D| = aφk和e| = aφk意味着e不通过第7页第（ii）项在D中细化d。关于这个证明的更多细节，我们再一次参考[15]。4加细的紧性定理4.1极大点拓扑空间在本节中，我们定义了Scott-拓扑、Lawson-拓扑和Stone空间，定义了X= max（D）上的诱导拓扑τX，并给出了（X，τX）是Stone空间和标号迁移系统模互模拟的商空间的证明。后者然后给我们一个实现类的紧性定理。我们写(12)X= max（D）={d ∈ D |e∈ D：d ≤ e对于D的极大元素的集合，这里需要三个拓扑。(i) D的Scott拓扑是(13)σD={↑k|k∈ K（D）}并且是T0，使得K（D）是所有截断的图像有限树的嵌入的集合[15]（或者，等价地，意义的集合{|p|对于（11）的所有过程项p）。(ii) Lawson拓扑是(14)λD={↑k\ ↑l| k，l∈ K（D）}[2]是一个很好的例子。(iii) 最后，劳森条件，一个在max（D）上的Scott-和劳森-拓扑之间的一致性条件，是至关重要的：(15)τX={Umax（D）|U∈ σD}在X上等于{Vmax（D）|[24 ][25][26][27][28][29]让我们回想一下，（X，τX）是一个Stone空间[20] i <$τX是紧的，Hausdor <$，零维的，其中• 紧凑 是指： 对于所有U X与XXF有一个有限的F U，• 豪斯多尔 平均值：对于所有x且O≠OJ={}，且xJ在X中存在O，OJ∈τX，其中x∈O，xJ∈OJ，• 零维意味着：每个U∈τX是τX-开（即τX的元素）和τX-闭（即τX的补元素）的集合的并集。14M. Huth/Electronic Notes in Theoretical Computer Science 161（2006）3KK4.2极大点空间的紧性应用Lawson条件，可以看到↑k max（D）={m ∈ max（D）|对任意k ∈ K（D），k ≤m}是τX-开和τX-闭的.利用这一点，很容易证明τX是零维的，Hausdor是零维的。由于λD是紧的，它表明max（D）是λD-闭的（因此是τX-紧的）。这是我们利用最大化的一套完整的测试。我们把有限的词的集合写在有限的事件的集合上。·对于Δ = δ1δ2. δn∈ Act，α ∈ Act，k ∈ K（D），我们定义了检验公式Δ， α=[δ1][δ2].. . H_（n+1）-M_（n+1）-L_（n +1）（十六）如前所述。对于所有d ∈ D，我们有（D，d）|= aφki k ≤ d• 对于m∈ {a，c}和φa Hennessy-Milner逻辑公式，我们写(17)[|φ|] m={d ∈ D|（D，d）|= mφ}。• 我们形成了一组通过所有测试的点，|= a语义：（十八）C=Δ，α|] a|Δ ∈Act，α∈Act，k∈K（D）}.{|克我们的计划是证明(i) 对于Hennessy-Milner逻辑的每个公式φ，[|φ|] a是λD-闭的，并且(ii) C= max（D）。如果这个计划成功，max（D）是λD-闭的，因为λD-闭集的交集。对于上述两个项目的充分证明，我们参考[18]，只勾勒了论点的结构：我们表明，(i) [|φ|在强归纳假设下，Hennessy-Milner逻辑的所有公式φ在φ上的互结构归纳下都是λ D -闭的(19)“[|φ|] c及[|φ|] a是λD-闭的和λD-开的，”(ii) max（D）<$C;当C是λD-闭的时，证明了标号转移系统的嵌入集在C中，且在max（D）中稠密，(iii) Cmax（D），通过利用（D，≤）的精细结构，并且d∈C通过所有测试d| =aΔ，α。因此，（X，τX）是一个Stone空间。我们还可以证明这个Stone空间是标号迁移系统模互模拟的商空间[18]：(i) 嵌入（M，i）→|M，I|将初始状态指定为max（D）的转换系统标记为映射，(ii) 任意（D，d）（d∈max（D））与标号转移系统等价，则ea∈ec=ec∈ max（D），对所有α∈Act和e是可达的α α α从d经由Rc，以及M. Huth/Electronic Notes in Theoretical Computer Science 161（2006）315K(iii) 我们有集合的双射（20）X=α∈ActC[X，τX]其中C[X，τX]表示X的τX-紧子集集，所以xα是α-后继集的τX-紧集，x=（xα）α∈Act∈X.因此，我们的模态转换系统的域方程在D的极大点空间上给出了一个Stone空间方程。4.3时态逻辑的一个紧性定理与精化我们现在可以陈述这些结果的第一个结果，一个加细的紧性定理。定理4.1（[18]）设（Mk，ik）是有限多个具有各自初始状态i和Γ的模态转移系统，一组Hennessy-Milner逻辑公式使得对于Γ的所有有限子集，Hennessy-Milner逻辑公式满足而不是定义所有i k的带标签的转移系统。然后有一个像有限标号的转移系统（L，l）使得l精化所有ik且l满足Γ的所有公式。该定理的证明仅在[18]中针对单个模型进行了表述，它依赖于τX的紧性以及每个↑ τ X|Mk，ik|λ max（D）是λD-闭的，因此τX-闭。例4.2[[18]]如果我们只有一个模态转换系统（M1，i1），i1=D，则上述定理是Hennessy-Milner逻辑和标号转移系统的熟悉的紧性定理，因为所有标号转移系统都是精化的。我的天5精炼的一致性度量5.1两个一致性措施在这一节中，我们提出了模态和标记转换系统的度量，定义了模态转换系统的两个一致性度量，并证明其中之一是一致性的鲁棒乐观度量这两个指标是从文献中熟悉的对于任何枚举k0，k1，. K（D）定义(21) dD（d，e）= inf {2 −n|X（x，y）= inf{2 −n}|{i ≤ n：ki≤ x i <$ki≤ y}。关于这些度量值得注意的一点是，实际需要需要增加模态深度φkn（n≥0），因此在这两个度量中，更接近的模型需要更多的估计（即模态深度）来通过测试区分它们。从标准域和度量理论，我们得知dD诱导λD，dX诱导τX.16M. Huth/Electronic Notes in Theoretical Computer Science 161（2006）3D的实现xy zeDc1（d，e）= 0 asy是普通精炼元素c2（d，e）=dX（x，z）CITD见图6。两个模态转换系统d和e有一个共同的精化。假设在模态转换系统中，状态(22)s和t是一致的i，并且t具有共同的细化。现在可以定义两个一致性度量[18]：(23) c1（d，e）= inf{dX（x，y）|x∈ ↑d max（D），y∈ ↑e max（D）}c2（d，e）= sup{dX（x，y）|x∈ ↑d max（D），y∈ ↑e max（D）}.度量c1背后的直觉是，我们试图分别选择d和e的实现，以便最小化这些实现之间的距离对偶地，在c2中，我们寻求最大化这个距离.因此，区间[c1（d，e），c2（d，e）]是d和e与映射(24)（d，e）›→[c1（d，e），c2（d，e）]：D×D→I是单调的 d和e的不一致程度c2（d，e）不小于c1（d，e）。5.2共同改进从τX的紧性，我们推断测度c1是鲁棒的。也就是说，我们可以证明，(25)c1（d，e）= 0 i ∈d和e有一个共同的精化。后者是PTIME [13]中的决策问题，但可能更难证明c1的非零下界。这与决定互模拟在PTIME中，而Kanellakis Smolka已经证明，确定有界互模拟n是PSPACE完全的[22]。例5.1图6示意性地描述了c1和c2的含义。紧性保证了如果d和e分别有实现序列（xi）i≥0和（yi）i≥0，使得序列（dX（xi，yi））i≥0的极限为0，则d和e有公共的精化。M. Huth/Electronic Notes in Theoretical Computer Science 161（2006）317⟨|N，t|⟩⟨|N，t|⟩⟨|M，s|⟩⟨|M，s|⟩{|我，我|⟩|（L，l）∈I[M，s]}{|我，我|⟩|（L，l）∈I[N，t]}健全性：假定不完全性（N，t）refines（M，s），所以I[N，t]I[M，s]（N，t）但I[N，t]=I[M，s]见图7。左为《易经》，右为《易经》。右：一个假设的不完整的细化的说明。6实现的细化已完成6.1问题定义在本节中，我们证明了实现的精化的可靠性，概述了实现的精化的完整性的证明，推导了精化的新的逻辑对于这些见解的详细说明和他们的充分证据，我们参考[19]。实现类(26)I[M，s]={（L，l）labelledtransitionsystem|（L，l）refines（M，s）}（ M ， s ） 的 是 所 有 定 义 （ M ， s ） 的 标 号 转 移 系 统 （ L ， l ） 的 类 由 于refinement_m_t是一个定义了i[N，t ]的函数，其中v_r（N，t）refines_s（M，s）。这一含义抓住了合理性，因为它规定逐步细化不能引入新的实现。相反的含义也应该是真的：实现的反向包含应该是一种细化：(27)如果I[N，t]等于I[M，s]，则t（N，t）等于s（M，s）。例6.1图7说明了精化的可靠性和假定的不完全性。6.2校样草图我们可以通过下面的公式证明(i) 对于当s和t是由dy（11）生成的过程代数项的表示时的情况证明了这一点。这是一个使用I[N，t]S[M，s]来设计s和t的细化博弈中的大小获胜策略的规则，改编自Stirling18M. Huth/Electronic Notes in Theoretical Computer Science 161（2006）3K有γ∈Act的预固定γ∈的个数;(ii) show w in g that“↑|N，t|⟩∩m ax(D)⊆↑⟨|M，s|对于所有（M，s）和（N，t），(iii) 证明了这使用了项（i），一个紧性参数，以及{d∈ D |↑dmax（D）由Hofman-Mislove定理[16]证明了对于k∈K（D），↑k} ∈σD6.3这个证明这种完备性的一个结果是，对于基于满足性或有效性检查的语义，细化也在逻辑上由Hennessy-Milner逻辑表征。从健全的|= a表示细化，|= c对于抽象，我们得到了含义(28) S| = aφ⇒V（s，φ）s| = cφ<$S（s，φ）对于所有模态转移系统的所有状态s和Hennessy-Milner逻辑但这些蕴涵的逆命题一般都是错误的。 例如，所有的εΔ，α都是标记转移系统上的重言式，我们看到模态Ka过渡系统满足所有这些公式关于|= i这些系统是基本上被标记为过渡系统。我们现在可以证明一个新的逻辑特征化。定理6.2（[19]）设t和s是模态转移系统的状态。那么以下内容都是等价的：(i) t细化 s(ii) 对于Hennessy-Milner逻辑的所有φ，判断V（s，φ）蕴涵判断V（t，φ）(iii) 对于Hennessy-Milner逻辑的所有φ，判断S（t，φ）蕴涵判断S（s，φ）。第（ii）项和第（iii）项通过对偶性是等价的。（i）意味着（ii）由（28）和第7页的（ii）项得出。为了证明（ii）意味着（i）我们再次使用加细的完备性和（28）。例6.3图8显示了判断t的精确度的潜在损失|= aφ/有效性判断V（t，φ）。这种精度损失在域D中由集合V φ|[|φ|] a.加细的完备性具有明确的逻辑意义，因为我们可以证明它等价于这样一个事实，即对所有k∈K（D），φk都不损失精度：[|φk|] a= V φ。定理6.4 [[19]]模态转移系统的修正对于实现i是完备的，对所有k∈K（D），我们有判定V（s，φk）和s| = aφk对于所有模态转换系统的所有状态s都是相同的。M. Huth/Electronic Notes in Theoretical Computer Science 161（2006）319同极大元集[|φ|] a={d∈D|D| = aφ}包含在VφVφ={d∈D|V（d，φ）}Vφ∈σD的Hofman-Mislove定理CITD一图8.第八条。 基于s的语义的潜在精度损失示意图|= φ大于基于有效性判断V（s，φ）。6.4一些研究问题由于集[|φ|] a对Hennessy-Miler逻辑的所有φ都是λD-闭集，我们可以推论[|φ |A是集合的有限并集[|φk|[题意]因此，关于|= a，每个φ是Hennessy-Milner逻辑公式的有限析取，对于该逻辑公式，对实现类的有效性检查是定理6.4的模型检查。这引发了几个问题：• 其中Hennessy-Milner逻辑的附加φ为Vφ= [|φ|] a？对于这些φ，有效性检查可简化为在恒定时间和空间中的模型检查• 其中Hennessy-Milner逻辑的φ是VφλD-闭的，因此形式为[|ψ| Hennessy-Milner逻辑的一部分？对于这些φ，有效性检查可归约为模型检查，但这种归约可能具有非平凡的复杂性。• 关于集合的拓扑复杂性，我们能说些什么呢？|φ|] a和V φ，如果φ在模态μ演算公式上的范围[21]？• 最后，能否使用Wadge约化[30]和（相对）空间理论[28]为前一项的集合开发一个描述性的集合论，这样的描述是否与模态μ演算层次结构的表达性结果有关？7结论本文提出了一个域模型D，它构成了模态转换系统D的状态空间，使得模态转换系统D对所有模态转换系统都是普适的，而模态转换系统D是完全抽象的，域的阶是D上的最大精化关系。这是与Radha Jagadeesan和David Schmidt的联合工作，已经在[15]中报道过。然后证明了D的极大点空间是Stone空间，实际上是标号迁移系统模互模拟的商空间，从而得到了模态迁移系统之间的鲁棒一致性测度和Hennessy-Milner逻辑上这类系统实现类的紧性定理这项工作也在其他一些地方报道过。20M. Huth/Electronic Notes in Theoretical Computer Science 161（2006）3详细信息[18]。最后，我们概述了[19]中的