混合逻辑：混合计算树逻辑的模型检查方法的发展与应用

理论计算机科学电子笔记112（2005）61-76www.elsevier.com/locate/entcs混合逻辑迈克尔·胡特1英国伦敦帝国理工学院计算机系摘要通过两个相关的主题，我们提出并发展了混合逻辑的定量版本的数学基础：混合计算树逻辑的关系抽象技术和混合Kripke结构，作为计算树逻辑的模型检查框架的扩展，具有命名、绑定和检索状态的能力;以及标记马尔可夫链的混合扩展上的混合概率计算树逻辑的语法和语义，其中混合Kripke结构的关系抽象技术应该是可转移的。保留字：混合逻辑，模型检验，概率系统，抽象。1介绍混合逻辑（参见例如http://www.hylo.net）增强了基本模态和时域逻辑，具有将名称绑定到模型中的唯一状态的能力。这种扩展在必须跨空间或时间跟踪状态或其他对象的应用程序中是一种重要的功能。 如果我们认为一个混合逻辑作为一个临时逻辑丰富的语法条款的查找和绑定的名称，这是很自然的问题是否建立模型检查方法可以适应，或保留，在这种混合设置。 除了Franceschet Rijke [10]的工作之外，令人惊讶的是，很少有人关注将模型检查扩展到混合时态逻辑。我们也不知道1电子邮件：M. doc.imperial.ac.uk1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.01.02362M. Huth/Electronic Notes in Theoretical Computer Science 112（2005）61∈∈任何关于定量或概率模型的混合逻辑的工作。注意，本文只讨论命题时态逻辑。因此，本文通过为计算树逻辑的混合扩展[4]定义两个模型检查主题，在这个方向上迈出了适度的第一步：关于混合计算树逻辑的所有属性的定性模型的合理关系抽象;以及概率系统和概率计算树逻辑的扩展[12]。这些主题之间的联系是双重的：(i) 概率可以被看作是定性信息的一种抽象形式，减少了系统2的确定性;(ii) 定性系统的关系抽象技术有望在未来的工作中移植到概率混合系统中。2混合计算树逻辑我们定义了计算树逻辑的混合版本[4]及其模型。定义2.1（i）具有签名Obs的Kripke结构是元组M =（M，R×M，L：Obs→P（M）），其中Obs是原子可观测量的集合。(ii) 一个签名为Obs = AP + Nom的混合Kripke结构是一个元组M =（M，R×N，L：Obs→P（N）），其中AP和Nom分别是原子命题和名词的不相交集合，使得对于所有n∈Nom，集合L（n）只包含一个元素。(iii) 我们写（M，i）来表示M的状态i是M的初始状态。一个混合克里普克结构由一个状态集合、一个状态转移关系R和一个标记函数L组成，其中，对于每个可观测的o∈Obs，L（o）表示o成立的状态集合;见图1。由于对L的约束，这些模型不仅仅是Kripke结构：所有名词nNom只在模型的一个状态下成立，而原子命题pAP可能不成立，只在一个或多个状态下成立。 在本文中，我们提出了一个混合扩展的计算树逻辑的具体属性，因为这准备了一个混合扩展的概率计算树逻辑[12]，但本文的定理3.6适用于完全命题μ演算[15]。对于签名Obs=AP+Nom，计算树逻辑的适当片段是(1)φ：：= φ|O| ¬φ|φ∧φ|EXφ|E [φUφ] |AF φ[2]同时，概率可以被看作是“0 - 1”非决定论的具体化。M. Huth/Electronic Notes in Theoretical Computer Science 112（2005）61633n2，qp，qn1，n3ps3s2s0s 1图1.一、 具有签名Obs ={p，q}+{n1，n2，n3}的混合Kripke结构M。一个状态s被标记为ois∈L（o）。在这种情况下，我们也写（M，s）|= 0。其中o∈Obs。时间模式EXφ、E[φ1Uφ2]和AFφ分别表示“在某个下一状态φ”和“在某个每个混合Kripke结构M也是一个Kripke结构如果我们“忘记”标签函数上的约束，则会出现结构。所以满足关系（M，s）|= φ是Kripke结构的常见公式（例如[7]）。通常，我们把）写成φ，把）写成φ→。从Kripke结构到混合Kripke结构限制了类因此改变了满意度和有效性的概念我们讨论两个标准的例子，从文献。实施例2.2（i）对于计算树逻辑公式(2)EX（n<$p）<$ EX（n<$q）→ EX（p<$q）我们可以认为n、p和q是原子命题，它们在任何状态、一种状态或多种状态下都是真的。然后我们可以很容易地在克里普克结构中找到这个公式为假的状态。如果我们把n看作是混合克里普克结构中的一个名词，这个公式是有效的。因为如果前提为真，则由n命名的唯一后继状态s（即L（n）={s}）满足p且满足q，因此存在满足p<$q的后继状态。（ii）利用名词，还得到了公式与转移关系性质之间更丰富的对应理论。公式n→ <$EXn，仅在名词和克里普克框架上解释，表示转移关系R是不相关的;已知这个性质不能在克里普克框架上的模态逻辑中表达。混合模型的分析受益于用标准混合算子增强计算树逻辑，我们在这里为分支-3一个Kripke框架F=（R，R）类似于一个Kripke结构M=（R，R，L），除了我们不能控制选择标签函数L，所以（R，R）|= φ i对于所有L，（φ，R，L）|= φ。64M. Huth/Electronic Notes in Theoretical Computer Science 112（2005）61¬¬↓↓时间逻辑控制设CTL（@）是具有满足算子@的计算树逻辑的扩展(3)φ：：= φ|O| ¬φ|@ nφ|φ∧φ|EXφ|E [φUφ] |AFφ其中o∈Obs和n∈Nom。@nφ的意图是(4)（男，女）|=@ nφi（M，sJ）|对于L（n）={sJ}，注意，（M，s）|= @ nφ要么在M的所有状态下成立，要么不成立。该算子是自对偶的：@nφ和@nφ在混合Kripke结构上语义等价在混合克里普克结构中，标记函数L将所有的名词绑定到一个唯一的状态。将名词视为参数，我们可以将它们绑定到计算公式的唯一状态。考虑CTL（↓），它将运算符↓ n.φ添加到计算树逻辑中，其语义需要标记|=与底层混合Kripke结构的标记函数L。对于计算树逻辑或CTL（@），（M，s）的求值|= Lφ不改变L。对于CTL（↓），标号函数L改变，用于评估形式为↓n.φ的子句。定义2.3设L[n<$→s]是标号函数，其中L[n<$→s]（o）=L（o），对于所有o∈Obs，其中on且L [n <$→s]（n）={s}。 然后我们(5)（男，女）|= L↓ n.φi（M，s）|= L[n <$→s]φ。我们得出结论，混合模型M上CTL（↓）的模型检查是检查（M，s）|=Lφ，初始标记函数为M，但其中对形式为↓ n.的子公式的检查的求值静态地更新L。在混合逻辑中，绑定器n.φ允许人们通过检查来表示状态s属于循环（在时序逻辑中不可(6)（男，女）|= L↓ n。E [<$U n].如果我们将模型检查的标记算法看作一个抽象机器，那么@nφ对应于“位置”n的查找在目前的状态下。最后，考虑CTL（Bidder），它为位置添加了一个绑定器，这似乎与Kripke满意关系中固有的局部性原则相反|=：(7)（男，女）|= L<$n.φi <$对于某些sJ∈ <$：（M，s）|= L[n<$→SJ] φ。这个操作符缺乏局部性意味着没有纯自底向上的标记算法可用于模型检查。例如，检查（M，s）|=你好@nE[Un]保持i，模型M包含某个循环，不一定M. Huth/Electronic Notes in Theoretical Computer Science 112（2005）6165↓∃通过s;类似的问题出现在对↓n.φ的自底向上评估中。接下来，我们用CTL（@，↓）等来扩展CTL，并列出所有的操作符。例2.4在图1的混合克里普克结构中，检查（M，s0）|= L@n2EX <$p成立，因为（M，s3）|= LEX <$p.支票（M，s0）|= L↓n2。<$EXn2成立，因为（M，s0）|= L[n2<$→s0]<$EXn2，其成立为（s0，s0）/∈R.支票（M，s0）|= Ln1. @n1<$p EX p成立，例如， （M，s0）|= L[n1<$→s3]@n1 <$p <$EX p.3混合模型模型检测的状态爆炸问题，即模型的状态空间的大小通常是原子命题数量的指数，对模型检测在现实和可扩展问题中的应用提出了重大挑战[7]。这是加剧了这一事实，即增加运算符或计算树逻辑使模型检查问题PSPACE-完全，虽然增加名词和@单独不改变检查的线性复杂性在模型的大小[10]。抽象被认为是减轻状态空间爆炸效应的关键技术.它的标准方法[6]通过“安全模拟”抽象模型，使得在抽象模型中为真的线性时间时态逻辑或计算树逻辑的通用片段（“对于所有路径”）的公式在具体模型中也为真。然而，抽象模型的反例通常是虚假的，因为它们不能反映具体模型中的真正错误。三值模型检验[8，2]通过安全和实时模拟的“混合”来抽象具体模型这里付出的代价是，模型检查可能会有第三个结果值但是我们获得了自由组合这些路径量化器的能力，例如。就像验证安全属性一样通过诉诸公平性假设（通过路径的“移除”获得），在抽象（通过路径的“添加”获得）上在本节中，我们使用混合Kripke结构M=（R，L），其特征为Obs=AP+Nom，一组设计为bstratestestesisaconcreteinstanceoft）。我们来定义一个hybridmodelM=（R，R，L）[4]在Bruns Godefroid66M. Huth/Electronic Notes in Theoretical Computer Science 112（2005）61∈| ¬∈\\根据对M的实际情况的分析，摘要M.为我们假设ρ分别是左全和右全：（八）s ∈t∈一个实际相关的示例是将某些分区的目录设置为索引，并将其列在索引中。这样的划分可以由一组有限的公式（例如，来自程序代码的布尔值保护）。B跟踪结构的M值表示所有的V值，（M值，t）|=φ，and在抽象模型（M，s）中的一个基本模型中的所有回归方程s，（M，t）=φ，（9）<$φ∈CT L（@，↓，<$）<$（s，t）∈<$×<$>：sρt&（M<$，t）|=φ（M，s）|=φ 。由关系ρ引入的抽象放松了混合逻辑的约束，并以3值形式表示它们。定 义 3.1 具 有 签 名 Obs=AP+Nom 的 3 值 混 合 Kripke 结 构 是 元 组 M=（M，Ra，Rc，La，Lc），其中（M，Ra，La）和（M，Rc，Lc）是具有签名Obs的Kripke结构，其受到以下约束：(i) Ra=Rc;(ii) 对于所有o∈Obs，La（o） <$Lc（o）;并且(iii) 对于所有n Nom，La（n）至多包含一个元素;如果是，则La（n）=Lc（n）.关于Ra和La的直觉，已经由Larsen在[17]中对标记转移系统表示过，它们表示“必须”-信息（“定义”、“必然如此”等），而R c R a和L c（o）L a（o）表示“可能”-信息（“可能”如果La（n）是非空的，我们力La（n）=Lc（n），因为Lc（n）\La（n）中没有元素可以有不同于s∈La（n）的元素的精化，在下面定义3.4这种对“可能”和“必须”信息的解释因此，我们可以在一般情况下定义3值混合Kripke结构的抽象，允许3值模型检查的增量抽象和细化方法，如[11]所示。定义3.2对于一个三值混合Kripke结构A=（R，Ra，Rc，La，Lc），其中符号Obs=AP+Nom，一个集合N，以及一个左全和右全关系ρ×ρ，我们定义一个元组Aρ=（Ra，Ra，Rc，La，Lc）：• （t，TJ）∈R_ai ∈R_a，r_e是某个s_Jρt_j，其中h（s，SJ）∈R_a;• （t，tJ）∈Rci对于某些（s，sJ）∈Rc，我们有sρt和sJρtJ;M. Huth/Electronic Notes in Theoretical Computer Science 112（2005）6167∈Xp，qs0S4pQy和zS1S2S3图二.形状图。节点是堆中的单元。名义值集由那些指向堆中单元的程序标识符x、y和z组成。 因为没有一个人能指出一次一个单元，我们有混合堆模型。• t∈La（o）i对于llsρt，我们有s ∈La（o）;且d• t∈ L<$c（o）i <$对于某些sρt，我们有s∈ Lc（o）。Example3. 图3的3值混合Kripke结构A以此方式从图2中的混合Kripke结构A获得。 为了看到这一点，我们设置ρ={（s0，t0），（s1，t1），（s2，t2），（s3，t2），（s4，t2）}.则ρ是左全和右全。 在图中，两个转换（s0，s1）和（s1，s2）被建模为实线，因为ti仅与si相关，i= 1， 2;对于出于同样的原因，它们的标签x和p被分别保留为t 0和t 1中的“必须”信息。 从t2到t1有一条虚线，因为（i）有一个跃迁（s3，s1），s3ρt2，和s1ρt1;（ii）s2ρt2，但没有从s2到某个s的跃迁，其中sρt1。类似地，我们考虑了从t2到其自身的虚线过渡.在t2处没有标签是“必须”-信息，并且除了x之外的所有标签都是“可能”-信息。例如，对于y，这是因为s3满足y，但s4不满足， 并且两者都通过ρ与t2 相关。这个例子表明，混合模型和逻辑可以表达形状图[19]。 注意对n个s的La和Lc 的 定 义 ： 如 果 A 是 一 个 hybridKripke 结 构 ， 则 n 个La （ n ）={t}i{s∈k}|sρt}=La（n）;且Lc（n）contains所有s o ρt的t，其中s0∈Lc（n）. 因此，如果我们想在抽象上验证φ，并且NNom是在φ中偶数个否定下出现的名词的集合，那么对于每个n N，s n∈L（n）必须被抽象为单例。这因为N与N相比将非常小，例如7对10- 7。在我们能够证明抽象定义3.2中A的定义（9）我们需要提出满意度关系|=对于3值混合68M. Huth/Electronic Notes in Theoretical Computer Science 112（2005）61LLLLLLLLC一一个cX的t0pp？，q？y？，t1t2图3.第三章。3值混合Kripke结构是图2的混合Kripke结构的抽象。实线和可观测量o分别包括Ra和La（o）虚线和可观察到的？包括Rc\Ra和Lc（o）\La（o）。Kripke结构M在两种模式下，“a“（a serted）和“c“（cconsistent），其中（M，s）|=和（M，s）|=分别表示“φ必须保持在M中的状态s“和“φ可以保持在M中的状态s”。 如果M =（R，R，L）是一个混合Kripke结构，则（R，R，L，L）是一个3值混合Kripke结构，使得|=和|=是平等的，所以定义|=正式为M。我们还正式定义了抽象和细化定义3.4LetA=（λ，Ra，Rc，La，Lc）和Aλ=（λ，Ra，Rc，La，Lc）是两个具有签名Obs = AP + Nom的3值混合Kripke结构。(i) 设r×t是一个参数，t∈Q，i ∈（s，t）蕴涵(a) 对所有ll（t，TJ）∈Ra，re是某个（s，SJ）∈Ra且h（SJ，TJ）∈Q;(b) 对所有l l（s，SJ）∈Rc，re是某个（t，TJ）∈Rc且h（SJ，TJ）∈Q;(c) 对所有llo∈Obs，t ∈La（o）蕴涵s ∈La（o），且d(d) 对llo∈ Obs，s∈ Lc（o）蕴涵t∈ Lc（o）.(ii) 我们说t（A，t）abstracts（isrefineddby）（A，s）如果re是一个refinement其中（s，t）∈ Q。(iii) 对 于 s∈N ， n∈Nom ， 标 号 L[n <$→as] 是 标 号 函 数 对 （ L[n<$→as]a，L[n <$→as]c），其中（La，Lc）（n除外），其中L[n <$→as]a（n） =L[n<$→as]c （n） ={s};实验L [n <$→cs]是实验函数对（L[n<$→cs]a，L[ n <$→ cs] c），其中等式（La，Lc）不含n ， 其中L [ n <$→cs]c（n）=Lc（n）<${s}且L[n<$→as]a（n）={}.(iv) 我们的定义|=a和|=c，用于3值混合Kripk结构，其中m∈{a，c}，<$a=c，且<$c=a：• （A，s）|=m;• （A，s）|=mois∈Lm（o）;• （A，s）|=m<$φi（A，s）|=<$mφ;• （A，s）|=m@nφi∈ re是某个SJ∈Lm（n），其中h（A，SJ）|=mφ;M. Huth/Electronic Notes in Theoretical Computer Science 112（2005）6169LLLLL›→›→L↓∃LLLLLL[n]→s]LL[n]→s]LLLLLLLLLL• （A，s）|=m↓n。φi（A，s）|=mmφ;• （A，s）|=mn。φi∈ re是某个sJ，其中h（A，s）|=mmJ φ;• （A，s）|=mφ1<$φ2i <$（（A，s）|=mφ1和（A，s）|=mφ2）;• （A，s）|=mEXφi<$re是某个（s，SJ）∈Rm<$h使得t（A，SJ）|=mφ;• （A，s）|=mE[φ1Uφ2]i，其中re是某个0≤j，其中hs=s0，使得对于ll，k∈{0，1， . . . ， j−1}我们有（sk，sk+1）∈Rm和（A，sk）|=mφ1，and（A，sj）|=mφ2;and• （A，s）|=mAFφi如果s = s 0，则re不为无穷大方程（si）i≥0，对于llk≥0，（sk，sk+1）∈R<$m且（A，sk）|=mφ。备注3.5跳转到任意状态以继续模型检查的评估的能力意味着（9）不能仅仅通过表明抽象状态t确实抽象了具体状态s来保证。 声音抽象成为一个全局属性，因为我们需要左全和右全精化关系，谢天谢地，它们在复合和子状态空间划分下是封闭的。L[nat]在A中的收敛是n到t的“must-bind”，L [ n]在A中的收敛是n到t的“must-bindcs]是n与s的“可能”-结合。这两个动作保守地约束了A中n的未抽象的Theorem3. 6（i）LetA=（A，Ra ，Rc，La，Lc）且Ab=（Ab ，Rba，Rbc，Lba，Lc）是两个具有签名Obs=AP+Nom的设Q为全左全右全右整数，（s，t）∈Q. F或所有的公式φ∈CT L（@，↓，<$），我们有（A<$，t）|=aφ隐含（A，s）|=aφ;and（A，s）|=cφ蕴含（Aφ，t）|=cφ。（ii）对于左全和右全ρ，LetA是3值混合Kripke结构，并且A由定义3.2中的A定义。 当A是一个3值的混合Kripk结构时，对于所有的sρt，（A_p，t）都是抽象的s（A，s）. 特别地，第（1）项适用。证据第（2）项是根据第（1）项的结构得出的。我们用φ上的结构归纳法证明了（1）。我们关注子句o、@nφ、n.φ和n.φ，因为其余子句的证明是标准的（参见例如：[8、2、14]）。• 考虑o。· Let（A，t）|=ao。 T∈L∈a（o）. From（s，t）∈Qweinfers∈La（o）whichimlies（A，s）|=ao。· Let（A，s）|=co. s∈Lc（o）. From（s，t）∈Qweinfert∈Lc（o）whicimplies（A，t）|=co.• 考虑@nφ。· Let（A，t）|=a@nφ。 这是一个有tj∈L∈a（n）且d（A∈，tJ）的问题|=aφ。70M. Huth/Electronic Notes in Theoretical Computer Science 112（2005）61LLLLL||LL ∃|||LLL[n→s]LL[n→s]LLL[n→s]LLC由于Q是right-total的，所以存在一些sj，其中h（SJ，TJ）∈Q，SOTJ∈L∈a（n）.设ssJ∈La（n）. By归纳法，（SJ，TJ）∈Q且（Aj，TJ）|=aφ意味着（A，sJ）|=aφ。 当N∈La（n）时，满足s（A，s）|=a@nφ。L· 令（A，s）|= LL@nφ。这是一个sJ，其中hsJ∈Lc（n）且d（A，sJ）|=cφ。由于Q是左全的，所以存在某个tJ使得（sJ，tJ）∈Q，所以sJ∈Lc（n）设tJ∈L<$c（n）. By归纳，（SJ，TJ）∈Q且（A，SJ）|=cφ隐含（A，tJ）|=cφ。 但t∈L_（？）c（n）满足s（A_（？），t）|=c@nφ。• 考虑↓n.φ。· Let（A，t）|=a↓n. φ。 Then（A，t）|=aφ。IfeeplaceLwthL[n<$→at]LL[n›→at]且L在A和A中（分别）有L[n<$→as]，则asummptions第（1）款的规定暂停执行。通过归纳，（A，t）=aL[n›→at]因此，φ意味着（A，s）|=aaφandso（A，s）|=a↓n. φ。· Let（A，s）|=c↓n。φ。 Then（A，s）|=ccφ。Iferep laceLwthL[n<$→ct]L其中L[n→cs]在L[n→s]A和A（分别），第（1）款的规定暂停执行。 通过归纳，（A，s）|=c因此，cφ意味着（A，t）=cL[n›→ct]• 考虑φn.φ。φ和so（Aφ，t）|=c↓n.φ。L[n→s]·Let（A，t）|=an. φ。这是一个J∈h（A∈，t）=a的问题L[n›→atJ] φ。以来Q是right-total的，存在一些sj，其中h（SJ，TJ）∈Q. 我想让L.L.L[n] →atJ]和L，其中L[n]→asJ]分别在A和A中，假设m（1）仍然成立。By感应，（A，t）=aL[n›→atJ] φ因此隐含s（A，s）|=aaJ φ和so（A，s）|=an。φ。·Let（A，s）|=cn. φ。 ThenthereissomeesJwith（A，s）|=ccJ φ。SinceQ是左-total，这里t是某个tJ，其中th（sJ，tJ）∈Q。分别在A_n和A中表示L_n与L_n[n<$→ctJ]和L_n与L[n<$→csJ]，位置m（1）s，直到保持。By感应，（A，s）|=ccJφthereforeimplies（A，t）=cL[n›→ctJ] φ和so（Aφ，t）|=cn.φ。L[n→s]让我们重新考虑图2的混合Kripke结构A和图3的抽象A。(i) Wehavee（A，t2）|=a@xE[x <$pU<$x]sin ce我们有（A，t0）|=aE[x<$pU<$x]，而后者在t0→t1→t2时由R_（？） s4ρt2，定理3.6使得（A，s4）|= L@xE [x<$p U <$x]。(ii) 最后，我们有（A，t2）|=cE[yU<$p]sin cet2∈L<$c（p）\L<$a（p），但ut不M. Huth/Electronic Notes in Theoretical Computer Science 112（2005）6171L有（A，s4）|=cE[yU<$p]尽管事实上s4ρt2。Thediredroughtof因此，模型检验结果的传递是依赖于模式的定理3.672M. Huth/Electronic Notes in Theoretical Computer Science 112（2005）61Obs是一组原子观测量;对于所有s∈n，ΣsJ∈R（s，sJ）= 1;4混合标记马尔可夫链混合逻辑丰富了时态逻辑及其模型，使其能够命名并跟踪模型中的状态。对于Kripke结构和计算树逻辑，这种丰富需要对标签函数的多重性约束（在基于抽象的模型检查中必须放松）以及向计算树逻辑添加标准混合运算符在从定性混合逻辑转向定量和概率逻辑的过程中，出现了几个问题：(i) 混合算子如何或应该如何推广到定量或概率环境？(ii) 模型检查后端及其数据结构（例如MTBBD [5，1]和Kronecker表示[18，9]）的使用是否受到混合运算符的影响，如果是，如何影响？(iii) 定性混合模型的关系抽象技术是否能顺利地转移到定量或概率环境中？(iv) 在概率计算树逻辑的混合扩展上，对标记马尔可夫链的混合扩展进行模型检测的复杂性是多少它比非混合设置的更差？在本文中，我们集中在第一个问题，并且仅在有限状态标记的马尔可夫链和概率计算树逻辑的设置中没有定义4.1（i）一个带有签名Obs的（有限状态）标记马尔可夫链设M=（λ，R： λ×λ→[0，1]，L：Obs→Pλ（λ）），其中λ是有限的;L1和L2具有与Kripke结构相同的解释。（ii）具有签名Obs = AP + Nom的混合（有限状态）标记马尔可夫链是元组M =（M，R：N × N→ [0，1]，L：（AP → P（N））+（Nom× N→ [0，1]）），其中（N，R，L|AP）是一个有限状态标记的马尔可夫链5; AP和Nom分别是原子命题和名词的不相交集合;对所有n∈Nom，s∈NL（n，s）= 1。在混合标记马尔可夫链中，标记函数L有一个和类型：在标记马尔可夫链的情况下，L（a）表示那些原子可观测值a∈AP保持的状态;而λs.L（n，s）是状态空间中标称n的概率分布;参见图4，图1中的混合克里普克结构的一个版本作为混合标记马尔可夫链。5 我们写L|AP表示L对类型AP→P（n）的限制。M. Huth/Electronic Notes in Theoretical Computer Science 112（2005）6173关于我们Σ∈如果检查（M，s）|= L@ ±p.φ保持，如果φ{L（n，sJ）|（M，sJ）|= Lφ} ±S3n2= 0。93S2n 3 = 0。13n 1 = 0。55n 1 = 0。45n 3 = 0。87s0s1n2= 0。07见图4。一种混合标记马氏链，其特征码为Obs=p，q+n1，n2，n3. 名词的概率在相应状态旁边描述。例如，L（n3，s0）= 0。87和L（n3，s3）= 0。我们将标称值作为函数λs进行概率处理。L（n，s）是每个标称值nNom的状态集上的概率分布。 这种类型是感兴趣的，因为它模型的概率不确定性的一个可观察的代理但它也允许我们保留混合对数的初衷，通过选择λs，L（n，s）为点分布δ sj， 将1赋值给sJ0到所有其他国家。或者，可以选择其他定量的度量（风险、成本等），使得s∈L（n，s）不再为1。这种选择的统一点是，关于名词的信息往往是不确定或不完整的。现在我们讨论一个合适的混合概率时态逻辑。概率计算树逻辑（无(10)φ：：= φ|一|¬φ|φ∧φ| [X φ] ±p|[φ U φ] ±p是由于Hansson Jonsson [12]，其中a∈AP，p∈[0， 1]，±∈ {≥，>}。下面，我们将标记马尔可夫链上的概率计算树逻辑的熟悉语义扩展到我们的混合设置。这种解释提出了混合算子@nφ、↓n.φ和n.φ的概率变体：np？这种解释类似于[Xφ]±p的解释，只是状态马尔可夫链，例如在PRISM模型检查器中实现的[16]。然而，这种解释与条件概率的作用不一致：L（n，SJ）是nQ0的情况。5p，q0的情况。640的情况。50的情况。010的情况。36p0的情况。9974M. Huth/Electronic Notes in Theoretical Computer Science 112（2005）61n|↓|n∃SJthat “nominal（11）（男，女）|=L@±p。φ i∈L（n，sJ）|（M，sJ）|=L[n <$→δ]φ} ±p 。与定性情况不同，@±pφ的检查静态地改变了子公式检查的标记函数。虽然这需要对现有的概率模型检查算法进行调整，但好消息是，连续将n的标记信息解析为在标记马尔可夫链中发现的定性可定性检验（M，s）=Ln.φ成立i ∈（M，s）=L[n<$→δs]φ成立.考虑到这一点，我们也可以将概率分布而不是点分布分配给概率检验的延续(12)（男，女）|= L↓（n，δ）.φi（M，s）|= L[n <$→δ]φ。定性检查（M，s）|= L<$n.φ对某些s j ∈ φ保持i <$，检查（M，s）|=L[n <$→δsJ]φ成立。如果我们设置J={δ sJ|sJ∈ <$}，这是一般概率检查的一个实例(13)（男，女）|= L<$（n，<$J）.φ i <$ 对于某些δ∈ <$J：（M，s）|= L[n<$→δ]φ。对于这个运算符（n，J），我们可能必须限制j的范围，以便使它可计算，甚至可行。我们判断这样的概率计算树逻辑的扩展是潜在的巨大用途。比如说使用概率分布来模拟代理的存在的想法建议在安全方面的应用。概率混合算子的这种普遍性可能不尊重混合时间模式的原始意图。比如说，(14)（男，女）|= L↓（n，δ）。[<$U（n <$）] ≥. 9999检查由n命名的节点是否在概率为至少的概率循环上（在该概率循环上，n为真至少一次）。9999只有当概率分布δ不涂抹这样一个节点的位置，即只有当δ是δsJ的形式，对于某些sJ∈π。使用点分布，概率混合逻辑因此能够表示概率的概率递归跟踪集。5混合概率计算树逻辑我们将我们的讨论总结为混合概率计算树逻辑的建议：定义5.1设Obs = AP + Nom是混合标记马尔可夫链的一个签名，并表示包含所有点分布的一类离散概率分布。 然后，在Obs和Obs上的混合概率计算树逻辑，没有“有界直到”，定义为：M. Huth/Electronic Notes in Theoretical Computer Science 112（2005）6175n∈|⊥|n3（十五）φ：：= φ|一|¬φ|φ∧φ| [X φ] ±p|[φ U φ]±pn±p|@±p.φ| ↓（n，δ）.φ|（n，其中，a ∈ AP，n ∈ Nom，p ∈ [0，1]，± ∈ {≥，>}，δ ∈ N，且n ∈ J∈N。在（M，s）中导出了定性算子↓n.φ和<$n.φ| = L↓n.φ被解释为（M，s）|= L↓（n，δ s）.φ;和（M，s）|= Ln.φ as（M，s）|= L（n，{δ s|s∈ φ}）.设M=（M，R，L）是一个带特征码Obs的混合有限状态标记马尔可夫链。 我们定义（M，s）|对于混合概率计算树逻辑的所有φ，L = Lφ。给定s∈S，设Path（s）是M中从s开始的无限路径的集合，其中s→sJ的转移发生在i <$R（s，sJ）>0。给定混合概率计算树逻辑的φ，φ1和φ2以及一些π路径，我们定义• π |=LXφi（M，sJ）|=Lφ，其中π=s → SJ →. . ;• π |=Lφ1U φ2i存在某个k ≥ 0，使得π的第一个k − 1个状态s i（M，s i）|= Lφ1且第k个状态s k满足（M，s k）|= Lφ2。因此，我们通过互感定义了混合概率计算树逻辑的某些路径公式和所有状态公式上的=L，就像对概率计算树逻辑所做的那样[12]。a、否定和合取的语义定义与Kripke结构相同。路径公式和混合运算符的语义是• （男，女）|= L[X φ] ±pi <$那些π ∈路径的 集 合 的 概 率 ，π |= LXφ为±p;• （男，女）|= L[φ1U φ2] ±pi那些π ∈ Path（s）的集合的概率，π |= Lφ1U φ2为±p;• （男，女）|= Ln±pi ∈ L（n，s）± p;• （男，女）|= L@±p.φ i{L（n，sJ）|（M，sJ）|= L[n <$→δ]φ}± p;nsJ• （男，女）|= L↓（n，δ）.φ i（M，s）|= L[n <$→δ]φ;以及• （男，女）|= L<$（n，<$J）.φ i <$对于某些δ∈ <$J，我们有（M，s）|= L[n<$→δ]φ。请注意，对于所有混合有限状态标记的马尔可夫链，=L都有很好的定义，因为谓词上的所有路径公式（混合概率计算树逻辑的特定公式为真的状态集）通过序列空间上的标准测度构造产生可测路径集[20上面给出的路径公式的语义与概率计算树逻辑相同。例5.2为了说明混合概率计算树逻辑的语义，我们检查（M，s3）|= L@>0。1 [<$U n3] ≥0。01号。 为此，我们需要-76M. Huth/Electronic Notes in Theoretical Computer Science 112（2005）61n3一个周期是0。01·0。64分。5·（|¬⊥∞i= 0（0. 64分。5）i）=0。00948529. . .这是当L（n3，s）> 0时，我们有（M，s）|= L[sU n3] ≥0。01;然后对所有这些L（n3，s）求和，并检查该和是否> 0。1 .一、这里只有s0和s2是相关的。• 在M中的一个t状态s0，具有一个b-1函数L[n3<$→δs0]，不≥ 0。01 so（M，s0）|= L[sU n3] ≥0。01不成立，这意味着L（s0，n3）=0。第87章没有贡献• 在M中的状态s2处，具有标号函数L[n3<$→δ s2]，s2在循环上的概率为0。64分。5+0。64分。五点零。01= 0。3232，等于0。0 1，所以（M，s2）=L[s <$→δs2][Un3]≥0. 01成立，这意味着L（s2，n3）= 0。13是唯一的贡献者。从0. 13> 0。1，我们得出结论，（M，s3）|= L@>0。1 [<$U n3] ≥0。01保持。6结论我们提出了命题混合逻辑，作为命题时态逻辑的增强然后，我们为混合Kripke结构和计算树逻辑的混合版本提供了一个合理的关系抽象技术。我们进一步提出并讨论了混合标记马尔可夫链的定义以及在这种混合设置中概率计算树逻辑的语法和语义。我们的混合Kripke结构的抽象技术应该可以转移到混合标记马尔可夫链和定量混合模型，也许沿着[13]的路线。致谢我们对混合逻辑的阐述深受http://www.hylo.net/上的介绍性文章以及Chris Hankin、Sebastian Nanz和Herbert Wiklicky的评论的启发我们感谢匿名评审Joost-Pieter Katoen和Prakash Panangelo的建设性意见，这些意见有助于形成本文的最终版本。引用[1] C.拜尔E. M.作者声明：Clarke，V. Kwiatkowska和M.瑞恩概率过程的符号模型检验。在Proc.ICALP[2] G. Bruns和P. Godefroid.基于三值时态逻辑的部分状态空间模型检测。 在proc 第11届计算机辅助验证会议，计算机科学讲义第1633卷，第274-287页。Springer Verlag，1999年7月。M. Huth/Electronic Notes in Theoretical Computer Science 112（2005）6177[3] G. Bruns和P. Godefroid.广义模型检验：关于部分状态空间的推理。在Proc. of CONCURSpringerVerlag，2000年8月。[4] E. M. Clarke和E. A.爱默生分支时序逻辑同步骨架的综合。In D. Kozen，编辑，程序逻辑研讨会，LNCS第131号。Springer Verlag，1981年。[5] E. M. Clarke，M. Fujita和X.赵离散函数的表示，第93-108页，多终端二元决策图和混合决策图一章. Kluwer学术出版社，1996年。[6] E. M. Clarke，O. Grumberg和D. E.久了模型检查和抽象。 ACM Transactions on ProgrammingLanguages and Systems，16（5）：1512[7] E. M. Clarke，O.Grumberg和D.A. 佩尔德。模型检查。麻省理工学