马尔可夫链和马尔可夫再生过程的向后解：形式化及应用

可在www.sciencedirect.com在线获取理论计算机科学电子笔记296（2013）7-26www.elsevier.com/locate/entcs马尔可夫链和马尔可夫再生过程的向后解：形式化及应用埃尔维奥湾Amparore1和苏珊娜·多纳泰利2意大利托里诺大学信息技术研究所摘要在本文中，我们调查的计算，和随机解释，向后概率马尔可夫链（瞬态和稳态概率来自向后Kolmogorov方程）及其扩展的情况下，马尔可夫再生过程（MRP）。然后将研究扩展到的情况下，非遍历设置，这照亮了一个实质性的差异之间的前向解决方案的过程（基于前向Kolmogorov方程）和向后的。我们将阐明后向解在计算吸收概率和随机逻辑的模型检查，如CSL和CSLTA，通常需要稳态解，非遍历的CTMC和MRP。 此外，我们表明，算法的计算满足CSL公式（这是CSL模型检查器中的标准实践）的整个状态集可以可以看作是连续时间马尔可夫链（CTMCs）的后向概率计算的情况。然后将MRP的向后计算插入到无矩阵求解技术的上下文中，允许处理的MRP的大得多的大小比标准的方法的基础上的计算和解决方案的嵌入式马尔可夫链。关键词：随机模型检验，向前和向后，Kolmogorov，MRP1引言从任何性能评估书籍的第一章开始，我们就可以了解离散时间马尔可夫链（DTMC）和连续时间马尔可夫链（CTMC）的向后和向前查普曼柯尔莫哥洛夫方程。但是书中剩下的大部分主题只涉及前向解（从初始状态到目标状态），而对后向解（从目标状态回到可能的初始状态）的关注非常有限。因此，我们无法找到正式的设置来处理非遍历（可约）的后向概率。1电子邮件：amparore@di.unito.it2电子邮件：susi@di.unito.it1571-0661 © 2013 Elsevier B. V.在CC BY-NC-ND许可下开放访问。http://dx.doi.org/10.1016/j.entcs.2013.07.0028例如Amparore，S.Donatelli/Electronic Notes in Theoretical Computer Science 296（2013）7系统，或更复杂的随机过程，如马尔可夫再生过程（MRP）。已知可约CTMC的前向概率的计算需要两个步骤：每个递归类都是单独求解的，并且使用从给定初始状态进入每个类的概率来规范化该解或分销。正如我们将在本文中显示，向后解决方案也有有趣的特点，不需要一个两步程序。本文回答的第二个问题是，用于马尔可夫链的相同方法是否可以应用于可约和不可约马尔可夫再生过程（MRP）。MRP的解决方案通常基于其嵌入的离散时间马尔可夫链（EMC）的稳态概率，该离散时间马尔可夫链（EMC）建立在多个从属CTMC的解决方案上，每个MRP状态一个CTMC。由于构建和存储EMC的成本，这种方法通常不适用：实际上，即使对于非常稀疏的MRP，所产生的EMC通常也非常密集。[13]中提出了一种不同的无矩阵方法，后来在[7]中进行了扩展，该方法不需要显式构造EMC，但代价是更复杂的解决方案模式。在本文中，我们将得出结论，我们确实可以回去处理MRP（遍历和非遍历）时，即使在更复杂的情况下，矩阵自由的解决方案。这些结果有一些明显的应用，例如计算吸收概率（从每个状态到达集合的概率随机Petri网（SPN）[ 2 ]或确定性SPN（DSPN）[ 1，19 ]的“最终”状态）最近的一个应用来自连续时间马尔可夫链（CTMC）的随机模型检查（或者更准确地说，随机逻辑的模型检查随机模型检查允许检查状态s是否满足给定条件的概率，该条件通常在CTMC中源于s这些逻辑中最流行的是CSL[8][9]。CSL识别两种固定类型的路径，由NeXt和Until路径运算符指定，以及必须沿着所考虑的路径满足的时间约束的附加条件（定时Until和定时neXt）。时间neXt的计算是非常直接的，我们将不在本文中考虑它，但要检查CTMC中的单个状态s是否满足时间Until，则需要两个CTMC的级联（通常是瞬态）解，通过使某些状态吸收（如[9]中所证明的）从原始CTMC获得级联意味着第一个的解被用作第二个CTMC的初始分布。[9]中的方法基于CTMC的前向Kolmogorov方程在时间t的解（前向解）。当我们需要计算Sat（k）时，一次求解一个状态是不够的，Sat（k）是满足公式k的整个状态集，如在嵌套CSL公式的计算中所要求的，因为必须重复相同的计算，将每个单个状态作为CTMC的初始状态在[15]中，给出了一个算法，该算法同时计算满足条件的整个状态集，例如Amparore，S.Donatelli/Electronic Notes in Theoretical Computer Science 296（2013）79它从“目标”状态开始在本文中， 我们将[15]中的算法所做的计 算形式化为CTMC 的向后Kolmogorov方程，并且我们写下允许证明向后和向前计算产生相同Sat集的方程，但是当必须计算整个满足状态集时，向后更有效。MRP出现在随机逻辑的模型检查中，如CSLTA。CSLTA在[11]中被定义为CSL的扩展（以及具有动作的CSL [14]），以允许通过单个时钟定时自动机识别的定时路径的更丰富的表征[3]。在[11]中还表明，CTMC的CSLTA公式的模型检验需要计算到达集合的概率在一个（可约的）马尔可夫再生过程中的吸收状态。同样，嵌套公式需要计算整个Sat集，然后问题就出现了，我们是否可以在可约MRP的解决方案中向后走文献综述。除了经典的不可约马尔可夫链的向后和向前柯尔莫哥洛夫方程外，我们几乎没有找到向后解的工作。与吸收概率的计算有明确的关系[17]，尽管它通常不明确。我们发现没有扩展的情况下，可减少DTMC/CTMC和以前的工作在所有的向后解决方案的MRPs。尽管CTMC的后向和前向概率的大多数基本结果肯定已经在各种书籍和论文中提出，但我们无法找到对这些主题及其对模型检测算法的影响的全面处理。[15]中的工作肯定是与本文最相关的先前工作，因为它提供了本研究的主要动机。本文主要研究基于判定图的CSL符号模型检测。标题的 [15]中的算法是目前在PRISM [18]和MRMC [16]等工具中实现的算法。对于CSLTA模型检查，[10]中的工作使用了一种迭代方案，该方案基本上是嵌入式DTMC的向后解决方案，但该目标需要构建嵌入式DTMC，这具有时间和空间成本，我们将通过提出无矩阵向后解决方案来避免本文的结构如下。第二节和第三节分别给出了DTMC和CTMC的后向和前向求解方法不可约链和可约链都被考虑。第4节应用了问题的向后和向前解决方案10例如Amparore，S.Donatelli/Electronic Notes in Theoretical Computer Science 296（2013）7Σ ΣΣΣ ΣΣCSL模型检查，以证明它们在计算的解决方案方面是等价的，但是如果需要整个Sat集，则向后更快（如[15]中第5节回顾了马尔可夫再生过程（MRP）的定义，并推导了不可约和可约MRP的前向和后向解，而第6节将推导扩展到MRP的无矩阵解，第7节将其应用于CSLTA。第8节结束了论文。2DTMC的前向和后向求解在本节中，我们描述了不可约和可约DTMC的瞬态和稳态概率的向前和向后计算我们用D ={Y n|n∈ N}是定义在有限状态空间S上的时间齐次离散时间马尔可夫链（DTMC）。设P是D的随机矩阵。DTMC的动态行为可以根据前向概率或后向概率分布来描述，基于前向和后向Chapman-Kolmogorov方程[23，p.342]。对于给定的初始固定状态i，前向概率给出了t个时间单位后系统演化的行为。在n步后处于状态j的概率，知道在时间0时状态是i，表示为：πD（i，j，n）= Pr{Y n= j|Y0= i}（1）当我们考虑初始分布α而不是单个初始状态时，由α约束的前向状态概率的向量πD（α，t）变为：πD（α，n）（j）=α（i）·πD（i，j，n）（2）i∈S方程（2）服从正向Chapman-Kolmogorov方程（对于时间齐次情况），其中n≥0：πD（α，n）=α·Pn（3）向量πD（α，n）的第j个元素是到达状态j从初始分布α开始的n步。当我们需要计算从每一个其他状态i经过n步到达固定状态j的概率时，我们需要重新计算上面的公式|S|ii是状态i的指示符向量。后向概率表示系统以状态i，假定在步骤n在给定的目的地状态j中被观察到：i，j，n）= Pr{Y0= i|Y n= j}（4）如果我们现在考虑在步骤n处的目标状态集合上的测量向量ρ，则我们可以引入表示由目标向量ρ调节的后向概率的后向概率向量ωD（ρ，n）：D（ρ，n）（i）=ρ（j）·j∈S例如Amparore，S.Donatelli/Electronic Notes in Theoretical Computer Science 296（2013）711.- 是的Σ/P=⎡⎢TF1· · ·Fm⎤⎥⎥...向量n =D（ρ，n）并不表示概率分布：事实上，它的和不等于一，而且每个n都是一个独立的p= n的量。 当ρ=ij时，则向量D（ρ，n）给出了从每个可能的初始状态i经过n步到达固定状态j的概率。方程（5）由反向Chapman-Kolmogorov方程控制：ρD（ρ，n）=Pn·ρ（6）并且重要的是观察到前向概率和后向概率通过以下关系联系在一起：πD（α，n）·ρ = α·Pn·ρ=α·Pn·ρ，故可简单证明.通常，静态行为被定义为：πD（α）= limπD（α，n）=α· limPn（8）n→∞n →∞D（ρ）= limn→∞n →∞再一次，向前和向后是通过以下方式联系在一起的：πD（α）·ρ=α·δD（ρ）（10）对于不可约DTMC，πD（α）总是存在的，它是唯一的且与α无关（πD（α）=πD（αJ））.较少人知道的是，向量D（ρ）依赖于ρ（D（ρ）=D（ρJ）），并且向量的每个元素都有相同的值D（ρ）[k]=D（ρ）[l]，并且D唯一地依赖于ρ。 注意，当ρ = is时，则值正好是πD（α）·is，因此向后计算稳态概率的整个向量具有额外的成本：|S|.可简化的DTMC。当D是可约的时，它的随机矩阵P可以被重新排序为上三角块形式（可约范式）：0 R1···0好吧.. . .. ⎥⎦00 ···Rm状态空间S被划分为瞬态集ST和m个集递归状态SRi（递归类）。子矩阵T是瞬态ST的子随机DTMC。每个矩形子矩阵Fi是从ST进入第i个递归类的概率矩阵。每个正方形子矩阵Ri是第i个递归类的DTMC。我们现在推导出lim的结构→∞如等式（8）和（9）中，当P为n12例如Amparore，S.Donatelli/Electronic Notes in Theoretical Computer Science 296（2013）7=M我我-是的Σ我Σ0J·F1·limRn···J·Fm·limRn⎢好吧M1. . ..可还原的 P的权力是：TnΛ1（n）···Λm（n）0n0Rn···0⎥P=I，P. . .⎥好吧 ..⎦n−10 0··· Rn其中Λi（n）=<$TkFiRn−k−1且Λi（0）= 0。k=0P的n次幂揭示了一个可约过程的众所周知的结构在n步之后：过程在瞬时类ST中停留k步（k≤n），然后发生单个Fi转换并将过程移动到第i个递归类SRi中，之后过程在SRi中停留剩余的（n-k-1）步。瞬态前向和后向概率然后可以使用上面导出的Pk的表达式从等式（3）和（6）重写;方便的是将用于递归和瞬态的部分分开，以获得：πDT（α，n）=αT·TnπDRi（α，n）=αT·Λi（n） +αRi·RnT（ρ，n）=nΛi（n）·ρRii=1n+Tn·ρT（十一）Ri（ρ，n）=Rn·ρRi令J=∞k=0Tk·e是一个矩阵，其中n次J（i，j）可以被解释为从状态i到状态j的离散步的平均数，而不离开过渡集。注意到，由于J=∞k=0Tk=（I-T）-1，则有可能计算（12）中的ny在（I-T）中，而不是直接计算与J的乘积，即：x = b·J⇒解：（I-T）·x = b x = J·b⇒解：x·（I-T）=b对于R中的任何测度向量b，|S|空间考虑到LimnTn= 0，使用J的定义，我们可以重写Pn→a∞s的极限速度n→n∞100limRn→∞.n→∞···0⎥limPn =n→∞0 0···limRnn→∞⎥⎦1M1⎥例如Amparore，S.Donatelli/Electronic Notes in Theoretical Computer Science 296（2013）713我πDRi（α）=. αT·J·Fi+αRi·limRnΣ ΣΣFi·limRn·ρRi我由此，（11）的极限行为导致：πDT（α）=0好吧i=1n→∞Σn→∞我（十二）DRi（ρ）=limRn·ρRin→∞因此，观察到向量πD（α）在每个瞬态中为零（正如预期的那样，因为我们在长期内没有发现系统处于瞬态）。此外，给定一个递归类SRi，由于向量αT·J·Fi可以解释为从集合ST长期进入SRi的概率，则递归类的元素的概率πDRi（α）可以通过乘以稳定的每个递归类（lim）→∞Rn）通过加权向量。对于后向概率，我们可以观察到与ST（ρT）相关的ρ值对过渡态的概率（πDT（ρ））和重现态的概率（πRI（ρ））都没有影响。这确实是一个事实的后果，从长远来看，国家不会成为目标。此外，还可以在递归类上计算递归状态的稳态后向概率孤立地（在等式中所有的量都只涉及递归类 SRi（ρ））。如前所述，同一递归类的所有状态都具有后向概率的值相同更有趣的是过渡状态的后向概率y的情况，其中通过与矩阵Fi（从ST到达SR i的一步概率）和矩阵J（过渡行为）相乘，将每个递归类的概率y对于可约马尔可夫链，两个关系式（7）和（10）仍然成立，这可以通过用（12）和（11）项扩展它们来容易地证明请注意，当ρ是一组吸收状态的指示向量时，则通常称为3CTMC的前向和后向求解给定连续时间马尔可夫链（CTMC）M={X t|t∈ R}，具有有限状态空间S和无穷小生成元Q，其演化由前向/后向Kolmogorov微分方程[17，th. 2.3]。在时间t处于状态j的概率，知道在时间0状态是i，表示为：πM（i，j，t）= Pr{X t= j|X0= i}（13）或者，以向量形式：πM（α，t）（j）=α（i）·πM（i，j，t）（14）i∈SnT（ρ）=J·我14例如Amparore，S.Donatelli/Electronic Notes in Theoretical Computer Science 296（2013）7Σ ΣΣ.- 是的Σ-是的其中α是时间0时的概率分布向量（14）是前向Kolmogorov方程的解dπM（α，t）dt=πM（α，t）·Q（15）进入条件πM（α，0）=α.对于t≥0，（15）的解为：πM（α，t）=α· eQt（16）后向概率给出了M在时间0处于状态i的概率，假设在时间t处于状态j，则为：n（i，j，t）= Pr{X0= i|X t= j}（17）或者，以向量形式：M（ρ，v）（i）=ρ（j）·j∈S其中ρ是在时间t处的目标状态上的测量向量。由此产生的向量是后向Kolmogorov方程的解：d<$M（ρ，t）dt=Q·M（ρ，t）（19）退出条件为<$M（ρ，t）=ρ。 （19）的解为：M（ρ，t）= eQt·ρ（20）前向和后向公式由以下关系联系在一起：πM（α，t）·ρ =α·M（ρ，t）（21）等价于：α·eQt·ρ = α·eQt·ρ，并且：πM（α）·ρ=瞬态测量（16）和（20）的计算可以以多种方式进行[21];流行的均匀化方法也可以用于向后概率，导致两个以下泰勒级数展开的解决方案Kolmogorov方程的一阶常数系数ODE：πM（α，t）=α·eQt=α·∞e−qt（qt）nU你好！n例如Amparore，S.Donatelli/Electronic Notes in Theoretical Computer Science 296（2013）715-是的Σn·n=0（二十三）M（ρ，t）=eQt·ρ=∞e−qt（qt）nUρ你好！n=0其中q=− maxi∈SQ（i，i）且U=1/qQ+I是Q的一致化矩阵。像往常一样，U是在1/q的时间步长之后的平均行为的随机矩阵。用πM（α）和πM（ρ）表示平稳的前向和后向向量 关于CTMC存在许多成熟的算法用于计算CTMC的极限行为。Σ16例如Amparore，S.Donatelli/Electronic Notes in Theoretical Computer Science 296（2013）7Q=1M我我∞我⎡⎢TF1·· ·Fm⎤⎥TnΛ1（n）···Λm（n）e⎥.==R可还原CTMC。当马尔可夫过程M是可约的时，它的无穷小生成元Q可以写成可约范式：0 R1···0...（二十四）好吧.. . . . ⎥⎦00···Rm对于DTMC，我们导出了lim的结构，→∞eQ测试以显示如何导出trans-i-静态和静态（向前和向后）公式。 Q的幂是：0n=0Rn···0⎥Q=I，Q. . .⎥好吧 ..⎦n−10 0··· Rn其中Λi（n）=<$TkFiRn−k−1且Λi（0）= 0。Qt的指数则为k=0eTtΘ1（t）···Θm（t）∞qntn0eR1t···0..eQt = 你好！n=0好吧.. ..Rt项Θi（t）定义为：00 ··· emΘi（t）=θ Λi（n）tn n−1TkFiRn−k−1tnFiRktn+k+1你好！n=0你好！n=0k=0n=0k=0i（n + k+1）！最后一个因素可以重写：tn+k+11吨n k=x（n+k+1）！ 你好！k！0因此，项Θi（t）可以重新表述为：（t-x）dxΘi（t）=θTn ·Fi· .Σ∞KtXn0（t−x）dx =你好！n=0k！k=0不客气。Σ∞=Tnxn· Fi· .Σ∞Rk（t-x）kDx =0n=0Tx0不=∞∞∞∞=.K例如Amparore，S.Donatelli/Electronic Notes in Theoretical Computer Science 296（2013）717我我dx（25）你好！R（t-x）k！k=0最后一个方程可以解释如下：过程最初在瞬态类ST中经过x个时间单位，然后发生一次Fi跃迁，之后过程在第i个递归类中花费剩余的时间（t-x）·Fi·e18例如Amparore，S.Donatelli/Electronic Notes in Theoretical Computer Science 296（2013）7-是的∫··t→∞···St→∞t→∞t→∞t→∞t→∞10W·F1·lim eR1t···W·Fm·lim eRmt0用于ST和SRi状态划分的瞬态前向和后向方程然后可以被重写为：πMT（α，t）=αT·eTtπMRi（α，t）=αT·Θi（t） +αRi·eRitMT（ρ，t）=MΘi（t）·ρRii=1n+ eTt·ρT（二十六）MRi（ρ，t）=eRit·ρRi通过定义术语：W=∞eTx dx（27）0其是瞬态中的预期逗留时间矩阵，可以通过按部分积分来重写Θi（t）的极限limΘi（t）=<$∞eTxdx·Fi· lim eRit=术语lim→∞=W Fi lim eRit（28）t→∞eRit是第i个递归类的平稳随机矩阵因此，可约马尔可夫链的极限行为是lim eQt=0.00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000t→∞. .好吧...⎥⎦0 0limeRmtt→∞由于T至少有一行的行和为负，因此，极限运动→∞eTt 倾向于0。 所以limt→∞eQt具有T个状态的列−1零，积分（27）等价于：W=−T，因此，W可以被计算为T中的线性系统的解。πM（α）和πM（ρ）的平稳表达式为：πMT（α）=0πMRi（α）=. αT·W·Fi+αRi·lime Rit不不例如Amparore，S.Donatelli/Electronic Notes in Theoretical Computer Science 296（2013）719-是的t→∞MMT（ρ）=W·Fi·limeRit·ρRi（二十九）i=1t→∞Ri（ρ）=limeRit·ρRi并且对它们的离散对应物（12）所做的考虑也适用于（29）。4应用于CSL模型检查我们现在显示的作用，CTMCs的向后和向前的概率在CSL模型检查CTMCs中发挥作用。为了本文的目的，我们集中Σ20例如Amparore，S.Donatelli/Electronic Notes in Theoretical Computer Science 296（2013）7UΦ¬你... sUΦ·。SΣ..ΣΣ关键操作员直到。CSL 的 一 个 U_n_t_a_λ （ ΦU [t ， t′] ） 形 式 ; 如 果 M 的 路 径 集 合 的 概 率 从 s（P_a_t_h_s_M（s））开始并满足ΦU [t，t′] s_d_a_λ，其中a ∈{<，≤，≥，>}是一个比较算子，则对于CTMC M的一个状态s，这个U_n_t_a_λ形式为P_d_a_λ（Φ U [t，t ′ ]）。M的一条时间路径满足ΦU [t，t′]ii fii s in an-statt e at im e u∈[t，tJ]，且nuJ∈ [0，u）该路径只通过Φ-状态。公式θ的模型检验有两种变化：给定一个状态s，确定该状态是否满足公式θ（记为s| = θ），或确定满足θ的状态集Sat（θ）<$S假设U nt il formu l a=（ΦU [t，t′]），状态s满足mulaPdaλ（λ）的CSL，如果ProbM（s，λ）da λ，其中ProbM（s，λ）= Pr{σ∈PathsM（s）|σ| =}是所有从s开始并满足的路径σ的概率测度。因此，对CSLUntil公式的模型检验归结为计算从给定状态开始的一组路径的 概 率 。在[8]中，数量ProbM（s，）被证明是可测量的，而[9]表明ProbM（s，）的计算可以用最多两个CTMC的（瞬态/稳态）解来完成，通过使某些状态吸收从原始模型M导出。.求解方法的核心是修正CTMC的思想，通过针对特定CSL公式Φ的基于SAT的滤波算子M[Φ]获得。标记CTMCM [Φ]是通过吸收M中满足Φ的所有状态而获得的。Sat集的计算公式取决于Φ I的时间间隔I的形状。 间隔I可以是I= [0，t]、I= [t，t]或I= [t，tJ]，其中0]i<$，tJ−t，t基于后向πM（ρ，v）概率的Prob公式与基于前向πM（α，t）概率的Prob公式是镜像的：区间Until情形仍然是分两步计算的，但是在后向方法中求解两个修改链的顺序是颠倒的。产品型号：ForwardUntil计算：向后直到计算：M[<$Φ]M[<$Φ]M[<$Φ]M[<$Φ]s0Φs1.40.3.7S21s00s1.40.3.7S2s0.7s1s 200=Prob（s，）0s0.70s1s 2s00.7.30.3一点四秒二=P rob（1.3S3Φ，φ0.3.30S3.30.31S311.31S3.3.概率S3为每个初始状态Ψ（一）α0=isπtπt'iΨ（b）（c）ρt'= i联系我们（d）（e）其中：πt=πM[<$φ]（α0，t）αt=IΦ·πtπt'=πM[<$Φ]（αt，t′−t）其中：t=M[<$Φ]（ρt'，t′−t）ρt=IΦ·t'0=图1. CSL公式ψ= ΦU[t，t']Ψ在简单模型上的数值分析概率对于国家××22例如Amparore，S.Donatelli/Electronic Notes in Theoretical Computer Science 296（2013）7.- 是的[t，t][Φ]..ΣΣ′[t,t][ΦΨ]Φ[Φ]U··−s.- 是的 Σ..ΣΣM[¬Φ]M[¬Φ∨Ψ]ΦJ=ξI·ξi，t−t，t·i =sΨ为了更好地解释后向和前向方法之间的关系，图1说明了基于πM和πM方法的数值分析，用于mulaπ=ΦU [t ， t′]π的u n til。 初始CTMC显示在左侧（a）。图1的中间部分说明了初始状态s的Prob（s，n）的前向计算：在时间t对修改后的CTMC M [<$Φ]进行瞬态分析（b），然后将处于（<$Φ）状态的概率设置为零，并将所得向量用作链M [<$Φ]在时间t j-t的瞬态分析（c）的初始分布。然后，通过与i的叉积，将计算出的概率在所有i个状态上相加。 沿着时间轴看，我们可以观察到，使用时间t的行为作为时间t j − t的瞬态解的初始向量，导致计算系统在时间t j的行为，并导致将πt′称为由（c）的解产生的向量的结果。图1的右边部分说明了使用后向公式一次计算整个Prob（Rk）向量模型检查器首先计算目标向量i上时间tJ−t的后向概率，将其视为修改后的CTMCM [<$Φ]（d）中时间tJ在所得到的向量Put中，将<$Φ状态归零，以产生测量向量Pt。最后，在时间t对M[<$Φ]（e）进行后向概率分析，使用ρt作为退出条件，得到向量ρ0。满足公式的状态集然后通过取所有状态来建立，其对应的条目是da λ。然后通过以下定理很容易将前向和后向模型检查联系起来定理4.1对于给定的初始状态s，l，Pdaλ（Φ U [t，t′]λ）满足的路径概率的前向和后向计算得到相同的结果.为了证明这个定理，用关系式（21）重新表达每个Prob公式是足够的，它连接了前向和后向概率：概率M（s，Φ U[0，t]）= i·πM[<$ΦU]is，t= πM[<$ΦU]i，t·is==概率M（ΦU[0，t]Ω）·is概率M（s，Φ U ）= iΦ·πM<$is，t =<$M<$iΦ，t·is==概率M（ΦU[t，t]Ω）·is概率M（s，Φ n）=iπM<$ i，t，tJt==πM[<$Φ]。是的。IΦ·M[<$ΦM].i，tJ−t==ProbM（ΦU [t，t′]）·is这证明了对于每个初始状态s的关系。Q5MRP的前向和后向求解我们现在考虑马尔可夫再生过程（MRP）的前向和后向平稳分析MRP是随机过程，其中击发时间可以具有一般分布（一般事件）。触发时间呈指数分布的事件称为指数事件。更新时间是一个时间点，其中每个随机变量g的值占（启用）gen的年龄例如Amparore，S.Donatelli/Electronic Notes in Theoretical Computer Science 296（2013）723∈gg所有事件均为零。在更新时遇到的进程状态称为再生点。 当一般事件被限制为每个状态最多启用一个时，随机过程是马尔可夫再生过程，其可以在马尔可夫更新序列（MRS）上描述。定义5.1[马尔可夫更新序列]设S是MRP的有限离散状态二元随机变量序列{|n∈ N}称为马尔可夫更新序列，其更新点Yn∈ S在更新时间Tn∈ R≥0i ∈时遇到：• 0= T0

下载后可阅读完整内容，剩余1页未读，立即下载