产品形式CTMC模型检验及其组合约束的分解语义

理论计算机科学电子笔记250（2009）21-37www.elsevier.com/locate/entcs产品形式CTMC的组合模型检验保罗·巴拉林i1和和ra'sHorva'th2摘要乘积形式马尔可夫链（Product form Markov chain）是一类组合马尔可夫模型，可以证明其受益于稳态分布的分解解（即稳态分布由组分稳态分布的乘积给出）。在本文中，我们专注于Boucherie产品过程，一类特殊的产品形式连续时间马尔可夫链。我们证明了导致该类中的产品形式结果的组合约束也可以在模型检查问题中利用，从而导致连续随机逻辑的片段的分解语义。关键词：组合随机模型检验，乘积型马尔可夫链1介绍连续随机逻辑（CSL）[1，2]已被证明是一种有价值的语言用于表示连续时间马尔可夫链（CTMC）模型系统的性能和可执行性要求。 CSL属性通过适当的模型检查算法针对CTMC模型进行验证。 有限状态模型的模型检查程序对模型的大小很敏感。在文献中可以找到相当数量的工作，旨在增加模型检查的适用性方面的模型的尺寸。至少有三种不同类型的方法来解决所谓的状态空间爆炸问题：压缩状态空间表示（即符号模型检查）;通过抽象减少状态空间维度;通过分解原始模型减少状态空间（即组合模型检查）。例如，符号模型检查（对于非概率[10]和概率[9，6]系统）使用特定的数据结构（BDD，MTBDD）来获得状态空间的紧凑表示另一方面，模型中的抽象1英国格拉斯哥大学计算科学系，paolo@dcs.gla.ac.uk2.Informatica，Uni versit`adiTorino，Ital y，horvath@di.unito.it，由MIUR通过PRIN项目Famous和EEC项目Crutial提供部分支持。1571-0661 © 2009 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.08.00322P. Ballarini，A.Horváth/Electronic Notes in Theoretical Computer Science 250（2009）21→× →→检查的目的是寻找一个抽象的，因此减少，版本的模型，这证明是等价的，从某些角度来看，原来的。 相反，在给定的时序逻辑中，对属性的复合验证涉及当给定的模型通过复合获得时对公式的真值的分析 一系列的子模型。在这方面，我们的目标是研究通过验证φ本身或其他公式来推断公式φ的真实性的可能性。非概率系统的模型检查的组合方法已经得到了广泛的研究（例如，参见CTL组合模型检查[7]和模块检查[11]）。如果在非概率系统的成分验证方面已经做了很多工作，就我们所知，概率系统属性的成分验证仍然是一个主要未探索的研究领域。在本文中，我们考虑概率系统的CTMC域，我们解决了关于它的组合验证问题具体地说，我们考虑了CTMC的组成框架，即Bouche- rie乘积过程[3]，其中K维CTMC作为K个分量CTMC的乘积获得Boucherie框架适合于建模系统，其中一些并行进程竞争一些互斥的共享资源。由于对共享资源的互斥访问，除了隐式同步之外，不考虑进程之间的显式同步。通过对合成规则施加互斥和强阻塞两个约束，Boucherie证明了产品-过程M的稳态分布由M本文研究了Boucherie过程族的CSL模型检验问题。我们表明，CSL语言的子集的成分验证可以在Boucherie产品过程中进行。 因此，给定一个涉及K维过程M的CSL公式φ，我们说明如何导出一个涉及M的某些分量的等价公式（e）φJ（的集合）论文的其余部分组织如下。第二节The Boucherie组成框架的形式化描述和一个例子，这将在整个文件中提到，是目前。第三节简要介绍了CSL逻辑，并证明了它的一个子集的组合验证。第四节讨论了我们应用所提出的方法所得到的好处。最后，第5节总结了本文所做的工作，并说明了未来工作的指导方针。CTMC基础知识。 我们介绍有关CTMC的基本概念/符号。它们将用于本文的其余部分给定一组原子命题AP ={a，b，c . . . }标记的CTMC表示为M=（S，Q，L），其中S是状态的有限集合，Q：SSR≥0是速率矩阵，其中Q（s，s）= 0，并且L：S2AP是标记函数。转移率Q（s，sJ）>0当且仅当存在从s到sJ的转移，并且转移s sJ的延迟由指数分布决定，其参数是转移率Q（s，sJ）。任何状态s使得Q（s，SJ）= 0，对所有SJ∈S都称为吸收。的总和P. Ballarini，A.Horváth/Electronic Notes in Theoretical Computer Science 250（2009）2123Σ∈.ΣE（s）E（s）⊆−≤≤⊂∈≤≤∈⊂∩∅联系我们∈i=1通过P（s，sJ，t）=Q（s，sJ）·1−e−E（s）·t. P（s，sJ）=Q（s，sJ）从状态s出发的输出转移率称为s的退出率，记为E（s）=SJS Q（s，SJ）。当Q（s，SJ）>0时，sJ，则从s开始的不同转换之间存在竞争。在这种情况下给出了在t个时间单位内从s到SJ（SSJM的转移概率矩阵在valI=[a，b]之间的时间内离开状态s ∈ S的概率R≥0记为eI（s）=（e−a·E（s））e−b·E（s））。CTMCM的稳态分布（即，表示长期处于某种状态的概率的分布）被表示为πM（或者当表示M在论述的上下文中不相关时简单地表示为π对于K > 1个CTMC的集合，下标k将用于指代集合中的第k个（1 kK）CTMC（例如，Mk=（Sk，Qk，Lk），APk，Pk，πMk）。2Boucherie产品形式在[3]中，Boucherie引入了一个组合CTMC，M，适合于对多个共享资源上的并发进程之间的竞争建模。 这样的模型被描述为K遍历的集合 CTMCs，Mk，1KK，每个 它们具有有限的状态空间Sk、转移矩阵Qk和唯一的稳态分布πk。一个索引集，N>0，表示共享资源。竞争资源i的组件nts的集合由Ui表示。 我们假设对于每个资源iI，Ui至少包含两个组件（否则资源不会被共享）。集合Cki1，...，K表示与组件k竞争资源iI的组件，并且RkI指示组件k竞争的资源。对于给定的k和iI，Aki表示M k的状态集合，其中资源i被组件k使用。假设对于任何分量k和任何两个资源i和j，k0表示k 3不使用共享资源的状态集。产品过程M的特征在于两个条件。条件1：每个转换只能改变一个组件的状态没有同步）。条件2：资源是互斥和强阻塞的，也就是说，如果组件k持有资源i，则其所有kJ∈Cki）是阻塞的。在这些假设下，Boucherie证明了，状态s=（s1，...，sk，.，sK）是产品形式的，即，它可以计算为π（s1，...，sk，.，sK）=GK 其中πi（si）表示描述组分i的CTMC中状态si的稳态概率。为归一化常数G的有效计算，见[12]。 状态空间S，是通过从乘积k∈KSk中减去表示违反互斥条件（这些状态的集合将由ME表示）和对应于循环阻塞的状态的集合（这些状态的集合3为了更直观，我们用i= 0表示非共享资源，而在[3]中，i= 1用于表示非共享的。代表了嵌入的24P. Ballarini，A.Horváth/Electronic Notes in Theoretical Computer Science 250（2009）21Ykik=1ki--国家将由CB表示）。因此，S被正式定义为：KS=Sk\（ME_CB）（2.1）k=1集合ME可以计算为ME=kii：i∈IJ：JUi，|J|≥2Kk=1其中J=如果k∈J，则Aki，否则DJ=Sk，即，每一个状态，其中一个给定的资源是必须排除至少由两个组件使用的，因为它违反了条件相互排斥。为了识别CB中的状态，我们引入以下符号。一个给定的资源的所有操作情况将由向量表示|r1， . ，rK|其中ri∈I（即，组件i使用资源Ri）或Ri= 0（即，组件I不使用共享资源）。 然后系统处于循环阻塞状态，|r1， . ，rK|如果存在分量索引i1，...，iC，2 ≤C≤K，使得ri1∈Ui2，ri2∈Ui3，.，riC−1∈UiC，且riC∈Ui1。表示的向量集循环阻塞将由CBr表示。 则CB=r：r∈CBrKk=1 Akrk.非同步和强阻塞约束Boucherie框架反映在M的速率矩阵Q上。对于两个状态，s =（s1，...，sk，.，sK）和sJ=（sJ1， . ，sJk， .. . ，sJK），Q（s，sJ）=0，如果s和sJ在多于一个的分量nt中发生差异;如果s和s j仅在分量k中发生差异并且分量k在s中未被阻塞，则Q（s，sJ）= Qk（sk，sJk）;如果s和sj仅在分量k中发生差异并且分量k在s中被阻塞，则Q（s，s j）= 0。在这项工作中，我们扩展了Boucherie框架，假设状态的组件k标记原子命题从APk。为了方便起见，我们进一步假设集合APk（1≤k≤K）是成对不相交的。该组M的原子命题是AP=K APk。作为一个例子Boucherie过程，我们考虑的流行的哲学家用餐问题的随机版本。在这样一个模型中，K个哲学家围坐在一张桌子周围，桌子上放着K根筷子（或叉子），每个哲学家与右边的邻居分享右边的筷子，与左边的邻居分享左边的筷子。哲学家的行为被描述为一个由两个活动组成的无限循环：思考和进食。为了吃饭，哲学家必须有两只筷子，一旦他开始思考，他就会松开M1M2M3吃1吃2吃3Fig. 1. 三个用餐哲学家和相应的CTMC本文讨论K = 3的哲学家的情形，其中forkk，k∈1，2，3，表示Mk和M（k+1）mod（K）共享的资源.此外，我们使用的资源吃k之间共享Mk和它的两个邻居。既然我们是M1M2M3第1A10条think1叉车1s2A20think2Rfork2Lfork2s3A30think3Rfork3Lfork3DP. Ballarini，A.Horváth/Electronic Notes in Theoretical Computer Science 250（2009）21258>>.- 是的 Σ|||−||| − ||−× × ∪ ××>A11={Rfork1}资源1状态忙叉国全部免费1已使用2 使用3 使用（t1t2t3）（Lf1t2t3），（Rf1t2t3），（t1Lf2t3）. （t1Rf2t3），（ t1t2Lf3 ） ， （ t1t2Rf3 ） . （ e1t2t3 ） ， （ t1e2t3 ） ，（t1t2e3），（Lf1Rf2t3），（Lf1Lf2t3），（Rf1Rf2t3），（Rf1t2Lf3），（Rf1t2Rf3），（t1Lf2Lf3），（t1Lf2Rf3），（t1Rf2Rf3）. （e1Rf2t3），（e1t2Lf3），（Lf1e2t3），（t1e2Rf3），（Rf1t2e3），（t1Lf2e3）.表1三位用餐哲学家的状态考虑到3个哲学家，只有这样我们才有一个单一的食物资源，这是他们三个人共享的工艺/资源竞争和相应的CTMC见图1。分量Mk的状态根据资源占用用标签thinkk、Rforkk、Lforkk和eatk（我们使用tk、Rfk、Lfk和ek转换率都假定为1。哲学家S1=A10<$A11<$A13<$A14状态空间A10={think1}无资源状态M1：A13={Lfork1}资源3状态A14={eat1}资源4状态R1={fork1，fork3，eat}共享资源C11={M2}，C13={M3}，C14={M2，M3}竞争过程M2：S2=A20<$A21<$A22<$A24A20={think2}A21={Lfork2}A22={Rfork2}A24={eat2}R2={fork1，fork2，eat}C21={M1}，C22={M3}，C24={M1，M3}M3：S3=A30<$A32<$A33<$A34A30={think3}A32={Lfork3}A33={Rfork3}A34={eat3}R3={fork2， fork3，eat}C32={M2}，C33={M1}，C34={M1，M2}组合CTMCM的状态空间S由（2.1）式直接得到。对应于违反互斥的状态是至少两个哲学家使用资源eat或至少一个分叉被两个相邻哲学家使用在这个例子中，循环阻塞也很容易识别当每个哲学家都有相应的右叉或左叉时，这些哲学家被阻塞，这些状态由下式给出： A11一名22一名33一名13一名2132分 最后，我们报告说，三位哲学家的例子ME= 40，S=kSkME= 6440 = 24 也就是说，组成的CTMC由表1中列出的24个状态组成。>>：>>>>><8>>：>>>>><8>>：26P. Ballarini，A.Horváth/Electronic Notes in Theoretical Computer Science 250（2009）21SXk=13Boucherie过程的组合CSL模型检验连续随机逻辑（CSL）[1，2]，是一种形式语言，用于表达一个系统的属性建模在一个标记的CTMC。给定一个原子命题集合AP，一个标记的CTMC模型M=（S，Q，L）可以用CSL公式表示的性质来验证。CSL状态公式（φ）和路径公式（ψ）的语法是φ：= a|TT| ¬φ|φ∧φ| Sp（φ）|Pp（）（3.1）：= XIφ| φU Iφ（3.2）其中a∈AP，p∈[0， 1]，n∈ {<，≤，>，≥}且I∈R≥0是一个非空区间.CSL公式的语义根据两个概率度量来定义稳态概率和路径概率。πM（s，φ）表示给定s为起始状态，从长期来看达到φ为真的状态的状态s满足稳态公式<$p（φ）i <$πM（s，φ）<$p。类似地，ProbM（s，）表示M中初始状态s满足的路径的概率（其中建立在标准Next和Until路径算子的时间有界扩展上[8]）。路径公式Pp（s）由状态siProbM（s，s）p满足。形式上：S|=ttfor alls ∈ Ss |= φJφJJi s |= φj s |= φJJS|=ai <$a ∈ L（s）s |=<$φ i s |= φS|= S <$p（φ）i <$πM（s，φ）<$p s|= P p（s）iProbM（s，s）p下面我们给出计算时间有界Next公式的概率测度的公式（3.3）（取自[2它将在其余部分中提到概率（s，XI（j））=eI（s）·P（s，sJ）（3.3）S'|=本文考虑K维标号Boucherie CTMCM =（S，Q，L）的状态根据它们的投影进行标记，即：L：S → 2AP：L（s）= K Lk（sk）。我们考虑到一个受限制的CSL语法中，嵌套的概率运算符是不允许的。结果语法由下式给出φ：：=φ|ξ|ϕ|ω|φ ∧ φ |<$φ：：= Pp（XI（）） ：：= Sp（）：：= TT|一|ψ∧ψ |<$ω：：= Pp（U）状态公式φ可以根据它们所建立的原子命题来分类。 一个状态公式φ，其中所有的原子命题属于同一个分量，将被称为单分量公式。一个状态公式，φ，其中原子命题涉及一个以上的分量， 将被称为全球公式。我们观察到，简单布尔公式的组合语义（M）是M的“分解”标记的直接结果例如用P. Ballarini，A.Horváth/Electronic Notes in Theoretical Computer Science 250（2009）2127--→对于三维Boucherie CTMC，我们有（s1，s2，s3）|= a1a2a3当且仅当S1|= 1a1，s2|= 2a2和s3|= 3a3。下面我们介绍k-移动的概念并设计它的概率（引理3.1）. 我们将转换Q（s，sJ）称为k移动，如果它对应于组分k的状态变化。我们观察到，在状态s=（s1，...，sk，.，sK），记为pk（s），由下式给出：pk（s）=8个PEk（sk）j∈B（s）Ej（sj）如果k∈B（s）（3.4）：0ifk∈B（s）其中B（s）={k∈{1， .. . ，K}：i∈Rk，kJ∈CkiskJ∈Akji}是在s中被分块的复合物nts的集合。我们将把B（s）= 0的状态s称为全局非阻塞状态与部分阻塞状态相反，其中B（s）= 4。注意式（3.4）指出， 使得k的竞争者中的一个正在使用k正在竞争的资源。 如果不是这样，那么观察到k-移动的概率取决于取决于剩余组件中有多少组件可以自由移动（即，不被阻止，因为它们竞争的资源之一正被其他人使用）。 注意如果K是唯一的非阻塞分量（即，B（s）=k），则这样的概率等于1。下面的引理说明了组合过程的嵌入转移概率与组件的嵌入转移概率之间的关系。引理3.1从状态s到sJ的k -移动的概率等于对应的k-投影（sksJk）的概率，由在s中观察到k-移动的概率加权。（即，Boucherie过程M的嵌入转移矩阵P，是其k-投影的因子P（s，sJ）=Pk（sk，sJk）·pk（s）（3.5）在本节的其余部分中，我们报告在几种情况下，可以用组合的方式来决定组合过程的给定状态是否满足状态公式。特别地，我们考虑三种类型的公式：第3.1节处理单分量直到公式;第3.2节讨论单分量下一个公式;第3.3节考虑全局下一个公式。从本质上讲，我们表明，给定上述三种类型之一的路径公式，路径满足它的概率可以计算的一些导出公式的组件。对于涉及稳态算子的公式，由于组合过程中状态的稳态概率是乘积形式的，因此它们的评估是直接的。[4]请注意，S相应地被划分。28P. Ballarini，A.Horváth/Electronic Notes in Theoretical Computer Science 250（2009）21⊆s，XI（k）=pk（s）·概率ksk，Xpk（s）（丹麦文）pk（s）pk（s）pk（s）3.1单组分Until公式下面的定理提供了一个组合过程和它的组件之间的关系为untimed路径。定理3.2考虑K个分支之一上的有限无时路σk。 在k-投影为σk的组合CTMC中观察到路径σ k的概率等于在CTMC M k中观察到路径σk的概率，即，概率{σ：Projk（σ）=σk}=概率k {σk}。直觉上，定理3.2成立，因为在Boucherie过程中，一个组件可以在给定的时间内阻止另一个组件，但它不能改变另一个组件选择下一个状态的方式。在附录中给出了形式证明定理3.2不能推广到任何时间路径。考虑三位哲学家的模型和路径σ=（think1，think2，think3），[1，2]，（Rfork1，think2，think3）。由于在状态（think1，think2，think3）中任何哲学家都可以移动，并且由于哲学家2和3中的任何一个都可以移动到哲学家1被阻塞的状态中，因此σ的概率不等于M1中路径（think1），[1， 2]，（Rfork1）的概率。另一方面，存在其概率可以在单个分量上计算的路径。例如，在一个示例中， 因为只有哲学家1可以进入（吃1，想2，想3），我们有Prob（（吃1，想2，想3），[1，2]，（想1，想2，想3））= Prob1（（想1），[1，2]，（吃1））。下面的定理是定理3.2的直接推论。定理3.3对于一个状态s =（s1，...，sk，.，sK）和一个单分量不定时的Until公式ωk，则（第1条，...，sk，.，sK）|= ωksk|= kωk作为定理3.3的结果，可以简单地在所涉及的分量上检查单个分量直到公式。最后，我们简要地指出，定理3.3也可以推广到嵌套的单分量路径公式，只要公式中没有Next算子3.2单组分Next配方现在假设我们有一个单独的分量，下一个公式XI（k）指的是分量k。下面的定理表明，针对组合进程检查XI（k）等价于检查组件k上的类似Next公式。定理3.4对于s=（ s1，. sk，. sK）K维Boucherie CTMC的状态，I =[a，b]R+，时间有界单分量的概率测度“”1·I«其中1·I=a，b，是一个移动的时间间隔。Prob+（1−pk（s））·eI（s）·P robk（sk，k）（3.6）P. Ballarini，A.Horváth/Electronic Notes in Theoretical Computer Science 250（2009）2129≡--⊆−--−tt如果：aij∈APl， l/=ksl|=aijK>_^ξ（s）=一（3.7）证据 见附录二Q上述结果表明，在Boucherie框架中的时间Next属性的推理可以以分解的方式进行。特别地，由I对M限定的单分量Next公式的验证归结为（在最坏的情况下）具有移动的边界区间I j的相同Next公式的验证。直觉上，这种时间转移可以解释为对并发性降低的（随机）补偿：当我们将注意力从状态（S1，.，sK）到其在M k上的投影sk，我们基本上减少了启用的转换的数量，因此在给定延迟内离开s k的可能性增加。例3.5让我们考虑3个用餐哲学家，并假设我们对以下概率感兴趣：从M的初始状态（t1t2t3）开始，在一步中，资源叉1被M1占用，延迟时间间隔为I =[2，5]。在CSL中，这可以通过公式Rf1X[2，5]（Rf1）表示。为了描述M1的概率测度与M1分量（即M1）之间的Prob1（t1，t1））和wrt合成的CTMCM（即， 我们参考图2，图2示出了M1和M的路径的展开（满足X（Rf1）的路径是非虚线的路径）。由于E （t1t2t3）=6且eI（t1t2t3）=（e−2·6e−5·6），则通过应用（3.3）式wrt M，我们有概率（t1t2t3，X[2，5]（Rf1））=（e−12e30）1/6。另一方面，对于M1，E1（t1）=2且eI（t1）=（e-2·2e−5·2），则由式（3.3）可知，概率1（t1，X[2，5]（Rf1））=（e−4e10）1/2。 由于分量M1在t1t2t3中没有被阻挡，并且1步的概率是p1（ t1t2t3）= 1/3，那么P rob（ t1t2t3 ， X[2 ， 5]（Rf1））=1/3·1/2（e−3·4−e−3·1 0）=p1（t1t2t3）·Prob1（s1，X[6，15]a1）。3.3Global Next公式设k是一个全局公式（即，包含原子命题的公式， 指至少2个不同的分量），以析取范式书写：=ijaij。每个合取词ij都是一个（可能被否定的）原子命题，一个组件（即，aij∈APk，对于某个k）。我们考虑下一个公式XI（X），其中I=[a，b] R+是连续的时间间隔。 给定状态s=（s1，. sK），则对于每个分量Mk，我们定义（状态依赖）公式8><<$tt，如果ij：aij∈APl， li=ksl|=aij>：i：a ij'，aij'∈APl，l=lM1k，sl|=ai j'j：ai j∈APkMT11 1t1t2t31 11 1 1 1LF1RF1Lf1t2t3Rf1t2t3t1Lf2t3t1Rf2t3t1t2Lf3t1t2Rf3图二、满足单分量Next公式的路径IJ否则30P. Ballarini，A.Horváth/Electronic Notes in Theoretical Computer Science 250（2009）21111 1 1 1∧∧∧|∧∧||∧|||∧ ∧ ∧ ∧ ∧ ∧ ∧∧≡ ∨∨M1M2M3Mt1t2t3LF1RF1LF2RF2LF3RF3Lf1t2t3Rf1t2t3t1Lf2t3t1Rf2t3 t1t2Lf3 t1t2Rf3图三. 满足全局下一个公式的其含义如下。假设要移动的是组件k，则组合模型的下一个状态将满足k，当且仅当组件k的下一个状态将满足k。让我们考虑三维CTMC的状态（s1，s2，s3）和公式：一个2B1一个3的1C1C2D2D3C3b2，假设s1=a1b1c1，s2=a2，s3=c3d3。如果没有一个进程被阻塞，则必须考虑三种不同的移动。• 1-move：因为s3=a3，s2=d2，s2=b2，所以无论我们认为1-move是什么，在合成过程的下一个状态中，都不会满足。因此，<$1（s1，s2，s3）=<$tt。• 2-move：由于组件1和组件3，下一个组合状态肯定会满足a1b1a1c1d3c3。 因此，当且仅当分量2的下一个状态满足（c2≠ d2）或b2，则下一个组合状态满足d2。它的结果是<$2（s1，s2，s3）=（c2<$d2）<$b2。• 3-move：由于组件1和组件2，下一个组合状态肯定会满足a1a2b1a1c1。因此，当且仅当分量3的下一个状态满足3，则下一个组合状态满足1。因此，3（s1，s2，s3）= a3。如果k移动发生，为了满足X1，分量k的下一个状态必须满足X1，.，sK），并且跃迁必须发生在I内。结果定理如下。定理3.6对于一个状态s =（s1，. sk，. sK），时间有界全局Next公式（XI）的概率测度分解如下：概率（s，XI）=k∈XB（s）1我pk（s）概率k（sk，Xpk（s）k（s1， . ，sK））（3.8）证据这个定理的证明可以构造为定理3.4的证明。Q例3.7让我们再次参考三位用餐哲学家，假设我们 我们感兴趣的概率，从初始状态，任何哲学家的第一步将是抓住他的右叉与延迟[2， 5]。这由全局下一个公式（X[2，5]（Rf1））捕获Rf2Rf3））。 图3示出了在每个组件M k的初始状态和合成过程M的初始状态处生成的路径的展开（非虚线表示满足k（X[2 ，5]（Lf1<$Lf2<$Lf3））的路径）。通过应用（3.3）式，我们直接T31 1T11 1T21 1P. Ballarini，A.Horváth/Electronic Notes in Theoretical Computer Science 250（2009）2131k=1X∧≡∧|{ }|∀ ∈ {}P rob（t1t2t3， X[2，5]（Rf1 <$Rf2<$Rf3））=1/2·（e−2·6−e−5·6）。现在我们应用定理3.6。注意，在初始状态t1t2t3，每个组件都可以自由移动。由式（3.7），我们有：Rf1（t1t2t3）= Rf1，Rf2（t1t2t3）= Rf2，Rf3（t1t2t3）= Rf3。由于在t1t2t3中k步移动的概率是pk（t1t2t3）= 1/3，对所有k∈{1，2，3}，式（3.8）的右ht端为S<$31/3·Probk（tk， X[2·3，5·3]Rfk）. 以来Probk（tk， X[6，15]Rfk）=1/2·（e−6·2−e−15·2）则我们有一个31/3·P robk（tk， X [6，15]Rfk）=1/2（e−6·2−e−15·2）k=1=Prob（t1t2t3，X[2，5]（Rf1<$Rf2<$Rf3））3.4全局（不定时）直到公式在本节中，我们考虑引用多个组件的Until公式，例如公式（（think1认为2）Ueat3）指的是 哲学家M3赢得了与M1和M2的竞争。 不幸的是，在这种情况下，组合语义的推导（类似于为单组件Until和Next公式演示的语义）并不是一件容易的事情。 事实上，如果单分量Until公式的分解语义是分量CTMC的独立性的直接结果，那么当我们必须查看必须同时满足多个分量的条件的路径时，这种独立性的好处就会丢失，就像全局Until公式的情况一样然而，通过观察以下性质，可以提出对整体Until公式进行分解验证的可能性：假定σ是一个整体Until公式，σ是M中满足它的一条路径，那么，对于由σk表示的每个分量k，σk的k-投影满足从σ k导出的单分量Until公式σk。例如，在一个示例中，如果Ueat（（think1think2）Ueat3），则可以导出以下单组分Until公式：1并且，σ=σ=σk=σk， K一二三 不幸的是，我们实际上是在寻找一种相反类型的蕴涵，即：我们想证明，如果存在Rankk公式，那么针对分量Mk验证它们就等价于针对M验证Rankk。要做到这一点，我们需要推导出一个聚合模型，描述如何组合每一个Rankk的（局部）概率，使得它们的组合等价于M中Rankk的概率。这种聚合模型的推导是一项艰巨的任务，我们还没有一个解决方案为了克服这一困难，我们提出了一种替代方法。而不是看一个（分解）语义等价直到公式，我们看看我们是否可以利用固有的组合描述的CSL模型检测算法本身内的Boucherie CTMC。对于标记CTMCM=（S，Q，L）的状态s，通过以下递归函数[2]计算满足s中的非定时Until公式（φ U32P. Ballarini，A.Horváth/Electronic Notes in Theoretical Computer Science 250（2009）218><|>：P8>|：|≤≤K||1，如果s=0概率（s，φU））=s '∈S P（s，sJ）·Prob（sJ，（φ U））如果s |= φ0否则上述功能可适用于Boucherie CTMC，1，如果s =0P rob（s，（φU））=>pk（s）Pk（sk，sJk）·P rob（s.sJk，（φ U））0否则其中s.s.j.k表示通过用s.j.k代替s.k从s获得的状态。上述等式表明，可以建立涉及Boucherie CTMC的Until公式的概率，而不必求助于组合模型的概率转移矩阵P。还要注意的是，在求和中，我们只考虑那些s.sJk=φ的状态，这允许检查成分的方式，这些状态的组合模型的递归必须被计算。结果，直到公式的模型检测算法的存储器需求可以相对于“非组合”方法降低3.5Timed Until公式我们在3.1节中已经证明，可以在不考虑模型的其他分量的情况下验证关于分量Mk的当公式被计时时，必须考虑其他组件阻塞的方式，因此在给定的资源分配情况下，组合模型的瞬态行为可以以乘积形式计算因此，如果一个公式只满足资源分配不变的路径，那么组合验证是可能的。这是很少的情况下，因此我们必须计算概率的路径沿瞬态概率不是产品的形式。然而，即使在这种情况下，我们也可以利用模型的模块化结构来存储Q，即组合模型的速率矩阵。特别地，可以基于分量的速率矩阵Qi，1，1，K在矩阵上计算Q的条目。这种基于Kronecker代数的方法（例如，参见[5]的详细信息），如果组合模型很大，则可以节省大量内存有了模型的紧凑表示，可以应用大型结构化CTMC的模型检查技术[4]。模型的状态空间可以划分为宏观状态。每个宏状态的特征在于由向量r1，...，其中，如果组件j不使用任何共享资源，则rj = 0，并且rj>0指示资源rj正被组件j使用。然后，组合模型的马尔可夫链的速率矩阵可以被构造为块矩阵，其中块（i，j）包含从宏状态i的状态到宏状态j的状态的转移。在继续描述Q的块之前，我们引入以下符号。Qi，j是Qk的子矩阵，其中行根据P. Ballarini，A.Horváth/Electronic Notes in Theoretical Computer Science 250（2009）2133KKK我n（Q˛˛˛˛1吉吉1˛˛123我123另外两个处于思考阶段，可以计算为Q3，30 0Q0，0，我们年q1I2I3，Q1见式（3.11）。我˛˛˛˛到A ki中的状态和根据A kj中的状态的列。 0 i ii是0，尺寸的特征矩阵|阿ki| ×|阿ki|，respectivevely.必须区分两种类型的块，因为可能发生两种类型的转换：要么是宏状态内部的转换，要么是导致不同宏状态的转换。 描述宏状态内部转换的块 被给定为MAi，其中Ai=（Qri，ri，如果组分i未被阻断0（3.9）i=1ri如果组件i被阻塞其中是Kronecker sum算子。 描述从宏状态r1， . ，rj， . ，rn到宏状态r1， . ，rjJ， . ，rn是Oi=1Bi，Bi=里，里Ri我如果i=j如果i=j（3.10）哪里Kronecker乘积算子作为一个例子，我们考虑一个稍微复杂一点的哲学家用餐的模型。特别地，哲学家的每个状态将由相应的马尔可夫链的2个状态表示。对应于哲学家i的链的速率矩阵，1≤i≤ 3，用Qi表示为：0qi，12 qi，13 qi，14qi，15qi，160 0qi，210qi，23 qi，24qi， 25qi， 260 0˛ ˛000Q˛i，3400Qi，37qi，3800qi，43000qi，47qi，48qi，56qi，57qi，580qi，67qi， 68˛ ˛qi，71 qi，7200000qi，782000年，81年，82年 ，0年，0年 ，qi，870在状态1和2中，哲学家认为，在状态3-4中只有左叉，在状态5和6中只有右叉，在状态7和8中吃。让我们考虑几个Q块。所有哲学家思考的宏观状态内部的转变可以写为Q0，0Q0，0Q0，0，其中Q0，0给定在宏观国家内部的转变，哲学家1有他的左叉，因为哲学家2是封闭的，Q3，3是（3.11）式中的从每个人都思考的宏观状态到哲学家1拥有他的权利（资源1）的宏观状态的转变由下式给出：0、1个000、1个Q0， 0=0qi，12˛Q3，3=10q1，34˛Q0，1=q1，15q1，16（3.11）2009年1月1日，210日，19 9 9年q 1，25 q1， 26现在让我们考虑过程的嵌入式DTMC的转移矩阵P。请注意，P在很大程度上取决于各个组件的转移速率，因为“快”组件比“慢”组件移动的概率更高。根据组件的嵌入DTMC，Pi，1≤i≤K，我00 00 000 00qi，6534P. Ballarini，A.Horváth/Electronic Notes in Theoretical Computer Science 250（2009）21−Σ| |−||≡转换速率不能恢复。因此，P不能基于单个嵌入式DTMC构建然而，我们仍然可以计算P的元素，而不需要存储整个矩阵，因为P=I（diag（Q））-1Q，其中diag（Q）是Q的对角矩阵。4关于分解模型检验到目前为止，我们已经看到，验证某种类型的CSL公式对a Boucherie CTMCM等价于根据分量CTMC M k验证某些推导公式。这种方法的明显优点是，如果组件过程小于组合过程（几乎总是这种情况），那么通过模型检查来验证大型Boucherie过程可以从中受益。虽然这种分解方法的优点的精确评估在很大程度上取决于所考虑的模型和公式检查，我们可以做一些一般性的考虑。如果针对M验证公式φ等价于针对Mk验证导出公式φJ，则增益由状态空间维数差给出 S差异越大，增益越大。通过BoucherieCTMC状态空间（2.1）的定义，我们观察到M中的状态数（因此差异|S| −|SK|）de p在下面的翼上结束。• K：Boucherie框架的维度（即，部件的数量）：尺寸越大，增益越大• C：框架的竞争水平：这反过来又取决于两个方面：共享资源的数量（I），以及它们之间的竞争分布（即 集合Aki）。 我们可以说，由两个进程共享的资源比由三个进程共享的资源具有更低的竞争水平。类似地，我们可以说，一个进程只在单个状态中占有共享资源的框架，比一个进程通过许多不同的状态占有共享资源的框架具有更低的竞争水平。因此，框架的竞争水平越大，收益就越大让我们考虑3个用餐哲学家的例子，假设我们有兴趣确定哲学家1（在某个点）吃东西的概率是多少，这对应于CSL单分量公式101（真U吃1）。由于定理3.2，我们知道直接在4态CTMCM1上验证B1是足够的，而不是针对24态M，这意味着大约83%的状态空间增益最后，我们观察到，在某些情况下，φ对M的验证对应于若干φJk对Mk的验证（例如Global Next）。为了评估这种情况下的增益，我们需要考虑我们必须在每个组件上验证的φJk如果φ的分解导致nk公式φJk，必须针对分量Mk进行验证，则在这种情况下，decom posedverification是：（|S| −k∈{1. K}nk·|SK|）. 例如，正如我们之前所看到的，全局下一个公式（X[2，5]（Rf1<$Rf2<$Rf3））是P. Ballarini，A.Horváth/Electro