马尔可夫双相似性：理论计算机科学中的马尔可夫链与马尔可夫过程代数的互模拟等价性

理论计算机科学电子笔记162（2006）87-99www.elsevier.com/locate/entcs马尔可夫检验和迹等价比马尔可夫双相似性更马尔科·贝尔纳多Universita`diUrbinoIstituto di Scienze e Tecnologiedellbernardo@sti.uniurb.it摘要等价性的概念通常用于将马尔可夫过程项联系起来，并减少它们的底层状态空间，这就是马尔可夫双相似性。原因是，除了是一个同余，马尔可夫双相似性是一致的，与普通的集总，一个确切的聚集马尔可夫链。在本文中，我们表明，两个非互模拟为基础的马尔可夫行为等价关键词：马尔可夫链，马尔可夫过程代数，互模拟1介绍为了说明性能方面，在过去的二十年中，代数过程演算已经扩展，使随机过程可以与它们的条款。在这一领域，重点主要是装备过程项与性能模型的形式连续时间马尔可夫链（CTMC）。在文献中已经提出了几种马尔可夫过程演算（参见，例如，[12，10，3]和其中的参考文献）。虽然他们对动作的表现形式有所不同，但持续与时间流逝分离的瞬时动作-以及对于同步规程-非对称对对称-这样的马尔可夫过程演算共享一个共同的功能：马尔可夫互模拟等价性。马尔可夫双相似性[12]是建立在[14，13]基础上的语义理论，已被证明可用于关联马尔可夫过程项并减少其底层状态空间。其基本思想是两个马尔可夫双相似过程项1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.07988M. Bernardo/Electronic Notes in Theoretical Computer Science 162（2006）87能够从功能和性能的角度模仿彼此的行为。马尔可夫双相似性成功的原因是它在代数方面和性能方面都具有一些很好的性质。首先，它是关于所有典型过程代数算子的同余[12]，从而允许组合推理和组合状态空间缩减。其次，它有一个健全和完整的公理化[11]，阐明了马尔可夫双相似性所依赖的基本方程定律第三，它与普通集总一致[12]，这意味着从性能角度来看马尔可夫双相似性的有用性。普通集总[5]是马尔可夫链的一个精确聚合概念，即处于普通集总马尔可夫链的宏观状态的稳态/瞬态概率是处于原始马尔可夫链的组成微观状态之一的稳态/瞬态概率之和。因此，只要两个过程项是马尔可夫双相似的，它们就保证具有相同的性能特征。在连续时间设置中，研究主要集中在分支时间等价性[1]上，因为它们与普通集总有关。只有最近的线性时间的等价性和测试方案已经调查，以及在连续时间的情况下。[4]在[8，6]的基础上提出了马尔可夫检验等价性。与马尔可夫双相似性不同，马尔可夫测试等价性考虑了模拟功能和性能行为的能力，而马尔可夫测试等价性依赖于通用的效率概念，它基于在一定的平均时间内执行测试驱动计算的概率。在[16]中，考虑了基于概率I/O自动机的过程代数语言的行为等价性，该过程代数语言相对于将实数与额定迹相关联的通用可观测量进行在文献[17]中，几个线性时间等价的马尔可夫变体--迹在[4，16，17]中定义的所有马尔可夫行为等价都比马尔可夫双相似性严格虽然这在实践中可能有助于攻击状态空间爆炸问题，但我们不知道这种基于非互模拟的马尔可夫行为等价性从性能的角度来看是否有用事实上，我们面临着以下公开的问题：是CTMC级的聚合所引起的这种等价的准确？换句话说，给定两个由这些非互模拟的马尔可夫行为等价之一相关的过程项，我们不知道它们是否具有相同的性能特征。本文的贡献是解决上述开放的问题表明，马尔可夫测试等价和马尔可夫迹等价诱导在CTMC水平的聚集严格粗糙比普通集总，仍然是准确的。这个结果确保了任何两个马尔可夫过程项M. Bernardo/Electronic Notes in Theoretical Computer Science 162（2006）8789测试或跟踪等效物具有相同的性能特征。另一个结果是，马尔可夫测试和跟踪等价性比马尔可夫双相似性聚合更多，同时保持聚合的准确性本文采用的证明精确聚集性的策略是：首先证明马尔可夫检验和迹等价具有可靠的完备公理化，然后证明马尔可夫检验和迹等价是同余。这两个副结果是为具有持续时间动作的基本马尔可夫过程演算提供的这确保了精确聚集性质的一般有效性，而不会使两个副结果的证明复杂化。一旦得到了马尔可夫检验和迹等价的公理化，我们将观察到，它们与马尔可夫双相似性的公理化不同，只是因为一个新的公理模式包含了马尔可夫双相似性的一个公理。因此，在证明精确的聚合属性时，有必要只关注应用这个新公理模式所产生的聚合本文的组织结构如下。在第2节中，我们介绍了一个基本的马尔可夫过程演算，我们回顾了马尔可夫双相似。在第3节中，我们以与[4]略有不同的方式给出了马尔可夫检验等价性的定义，然后我们证明了它是一个同余，具有健全和完整的公理化，并导出了一个比普通集总严格粗糙的CTMC级聚集，它仍然是精确的。在第4节中，我们以与[17]略有不同的方式给出了马尔可夫迹等价的定义，然后我们证明了与马尔可夫测试等价相同的同余，公理化和精确聚合结果。最后，在第5节中，我们报告了一些结论性意见。结果的证明可在[2]中找到。2马尔可夫过程演算与双相似性在本节中，我们将介绍一个带有持续动作的马尔可夫进程演算，它使用尽可能少的操作符生成所有CTMC：空项、动作前缀操作符、替代组合操作符和进程调用机制。在定义了我们称为MPC的演算的语法和语义之后，我们回忆了马尔可夫双相似性并展示了它在演算上的性质2.1语法在MPC中，每个动作都是持续性的，因此它被表示为一对，其中a∈AType是动作的类型，而λ∈R>0是表征动作持续时间的指数分布的比率。我们表示为Act=AType×R>0是MPC的动作集。与标准过程理论不同，这里我们假设所有的行为都是可观察的。90M. Bernardo/Electronic Notes in Theoretical Computer Science 162（2006）87Δ定义2.1MPC的过程项集合由以下语法生成：P：：=0|a<，λ>.P|P+ P|一其中A是通过（可能是递归的）方程定义的过程常数A=P。 我们用P表示MPC的封闭和保护过程项的集合2.2语义MPC的语义可以用通常的操作风格定义。作为一个结果，每个过程项的行为由一个多变迁系统给出，其状态对应于过程项，其变迁（每个变迁都有多重性）被标记为动作。从这样一个多转换系统的CTMC基础的过程项可以很容易地检索（i）丢弃的动作类型从转换标签和（ii）折叠所有的转换之间相同的两个状态到一个单一的转换，其速率是原始转换的速率之和。空项0不能执行任何动作，因此相应的标记多转移系统只是一个没有转移的状态。项.P可以执行类型为a且平均持续时间为1/λ的动作，然后表现为P：a，λ.P−−→P项P1+P2的行为与P1或P2相同，取决于P1或P2是否首先执行动作：a，λPJa，λJ1−→PP2−→PP+Pa，λJa，λJ12−−−→ PP1+P2−−→P其中可由P1执行的动作和可由P2执行的动作被认为是在竞争中，因此它们中的每一个都具有与其速率成比例的执行概率。最后，过程常数A表现为A的定义方程中的右侧过程项：a，λP−→PJa，λifA=ΔPA−→PJ2.3马尔可夫双相似性等价性的概念通常被用来在MPC等演算的过程项上进行推理，这就是马尔可夫双相似性。定义2.2等价关系B <$P × P是马尔可夫互模拟i <$，只要（P1，P2）∈ B，则对所有的动作类型a∈AType和等价类C∈ P/B：其中对于每个i= 1，2：rate（P1，a，C）=rate（P2，a，C）a，λrate（P i，a，C）={|λ |P J∈ C。P i−→ P J|}M. Bernardo/Electronic Notes in Theoretical Computer Science 162（2006）8791马尔可夫双相似性（Markovian bisimilarity）是所有马尔可夫双相似性的并集，记为Markovian bisimilarity。%满箱马尔可夫双相似性具有以下性质。首先，它是关于MPC的所有算子的同余。第二，它对MPC有一个合理而完整的公理化，包括以下四个公理：（A1）P1+P2=P2+P1（A2）（P1+P2）+P3=P1+（P2+P3）（A3）P+0=P（A4）.P+.P=.P第三，它与普通集总一致当P1与P2相乘时，P1和P2下面的两个CTMC通常是集总等价的.由于普通集总是一种精确的聚合，保证P1和P2具有相同的性能特征。更确切地说，除非我们考虑通过将通常可集总的状态区分为不同的奖励来区分它们的绩效度量，否则情况就是这样感兴趣的读者可以参考[3]以获得对这个问题的完整处理。3马尔可夫检验等价性在本节中，我们首先回顾[4]中给出的马尔可夫检验等价性的定义在此之前，我们需要提供测试的语法以及并行组合操作符。然后，我们继续证明马尔可夫测试等价是一个同余相对于MPC的运营商，有一个健全的和完整的公理化MPC的非递归条款，并导致CTMC级聚集严格粗糙比普通集总仍然是准确的。3.1测试形式化与并行组合测试是一个实体，它与过程项交互，以便公开后者的一部分行为。表示测试的最方便的方法是通过另一个过程项，它通过一个并行组合操作符与第一个过程项交互，该操作符在任何可观察的动作类型上强制同步。因此，过程术语和测试交互的语义模型仍然是一个带有动作标签的多转换系统。由于测试应该在有限数量的步骤中进行，对于测试形式化，我们限制自己处理有限状态和非循环的项，因此在测试中不允许递归换句话说，作为测试基础的标记的多转换系统必须具有有限的dag-like结构。为了表示测试通过或未通过的事实，作为测试基础的类dag语义模型的每个终端节点必须被适当地标记，以便确定它是成功状态还是失败状态。在进程演算级别上，这相当于用两个零操作符92M. Bernardo/Electronic Notes in Theoretical Computer Science 162（2006）87“f”（表示失败）。在测试语法中，将避免像s + f这样的歧义项，方法是用一组n元保护的替代组合运算符替换动作前缀运算符和二元替代组合运算符，其中n在整个N>0的范围内。在我们的马尔可夫框架中，过程项和测试的相互作用应该关于指数分布类是封闭的，即。它不应该引起其速率不能通过表示指数分布的正实数来表示的转变。这严格取决于所采用的同步原则基于[9]的术语，实现指数闭合的最简单方法是强制执行马尔可夫生成反应形式的通信[3]。因此，在测试中只能发生所谓的被动动作。被动动作没有与之关联的持续时间。 相反，它们被赋予解释为权重的正实数，用于在一组相同类型的被动动作中进行概率选择从测试的角度来看，这个想法是，在其任何状态下，一个过程项被测试生成的建议，通过在该状态下启用的指数时间的动作之间的比赛来执行的动作，然后测试的反应，概率选择一个被动的动作（如果有的话）的相同类型的建议指数时间的一个，以参与互动。定义3.1测试集T由以下语法生成ΣT：：= f|S|i∈I. 我不是其中I是一个非空的有限指标集，ai∈AType− {τ}，且wi∈R>0。下面的运算规则定义了P∈ P和T∈T的生成-反应相互作用：a，λP−→PJa，T−→TJ其中：a，λ·w/weight（T，a）P<$T−→PJ<$TJ阿杰，阿杰，weight（T，a）={|W |T.T −−→ T|}3.2等效性定义我们现在拥有了建立马尔可夫检验等价性定义的所有要素我们引入的第一个概念是计算过程项和测试的相互作用，这是一个最大的序列中的标记的多转换系统的过程项和测试的并行组成的基础上的过渡。由于先前对测试施加的限制，所有考虑的计算结果都将具有有限的长度。定义3.2P∈P和T∈T的相互作用系统是过程项P<$T，其中我们说：• 一个组态是一个标记的多跃迁系统的状态，该系统是P T的基础。M. Bernardo/Electronic Notes in Theoretical Computer Science 162（2006）8793rate（PT）t• 配置成功（相应地，失败）i验证其测试组件为“s”（分别为• 计算是一个最大的转换序列：a1，λ1a2，λ2an，λnP<$T−→P1<$T1−→. −→Pn<$Tn使得对于所有0≤i≤n− 1，配置Pi≠Ti既不成功也不失败• 计算成功（相应地）。失败），这是它的最后一次配置。一个既不成功也不失败的计算被称为中断。我们用C（P，T）和S（P，T）分别表示P和T的相互作用系统的计算和成功计算的多集。我们引入的第二个概念是效率的一般概念，它基于在给定的平均时间内执行测试驱动计算的概率。为了这个目的，回想一下CTMC的状态s执行转换所定义3.3设P∈ P，T∈ T，且c∈ C（P，T）。 c的执行概率和平均持续时间由c的长度归纳定义如下：⎧如果长度（c）= 0，则为1概率（c）=a，λ<$λ·prob（cJ）ifc<$P<$T−−→cJ速率t（PT）如果长度（c）= 0，则为 0时间（c）=a，λ其中：<$1+时间（cJ）， 如果c<$P<$T−−→cJa，λ率（P <0.01）|λ |a，P J，T J.PPj T J|}我们还提出：tT）=Σ−−−→对于所有的C C（P，T）和：概率（C）=c∈Cprob（c）C≤t={c∈C|时间（c）≤t}对所有的C<$C（P，T）且t∈R≥0.定义3.4设P1，P2∈ P.我们称P1是等价于P2的马尔可夫检验，记为P1<$MTP2，i对所有检验T∈T和平均时间t∈R≥0：prob（S≤t（P1，T））=prob（S≤t（P2，T））3.3同余性质在动作前缀和替代成分方面，《动作前缀》是一个一致性。定理3.5设P1，P2∈ P. 当P1≠MTP2时，则：(i) .P1≠MT.P2，对所有<的a，λ>∈ Act.(ii) 对所有P ∈ P，P1 + P<$MT P2 + P和P + P1<$MT P + P2.Q94M. Bernardo/Electronic Notes in Theoretical Computer Science 162（2006）874（A1）（A2）（A3）P1+P2=P2+P1（P1+P2）+P3=P1+（P2+P3）P+0=P（AJ）4Σ Σ。.P我i，j i，j i，j=i∈Ij∈Ji<本发明公开了一种复合材料，Σk∈I λk>。Σ Σi∈Ij ∈Ji.Pi，jk∈Iλk如果对所有i1，i2∈I：{bi1，j|j∈Ji1}={bi2，j|j∈Ji2} <${b1，b2， . . ，bn}并且对于所有h = 1，...，n：Σ Σ{|μi1，j|bi1，j=bh|联系我们|μi2，j|bi2，j=bh|}μhj∈Ji1j ∈Ji23.4可靠的和完全的公理化如[4]所示，RIMMB严格包含在RIMMT中，因此第2.3节的公理A1-A4对RIMMT仍然有效，但不完整。马尔可夫检验等价但不是马尔可夫双相似的过程项的示例如下：.& lt;b，μ>.P1+ .& lt;b，μ>.P2以及：。.λ1.PΣλ2+.P12λ1+λ21λ1 +λ22事实上，没有一个测试可以区分这两个术语，因为在这两个术语中，执行a-动作然后执行b-动作的平均时间是1/（λ1+λ2）+ 1/μ，并且概率是1/（λ 1 + λ 2）+ 1/μ 达到P1 （分别） P2）为λ1/（λ1+λ2）（分别 λ2/（λ1+λ2））。 通过相反，无法将.P1和.P2与。P1+. P2throughr o mbifP1/r o mbP2。表1Pnr上的BMT事实证明，上面的两个项构成了公理模式AJ包含A4，我们必须将其添加到A1-A3以获得一个健全的和完整的公理化的非递归的集合Pnr上P的过程条件。这样的公理化由表1中所示的公理集AJ给出，其中I和J定义了具有|我|≥2（如果Ji=0，则取其相应的和为0）。定理3.6对于上的BMT，演绎系统DED（AJ）是可靠的和完备的。Pnr，即对所有的P1，P2∈ Pnr：QAjP1=P2P1MTP2M. Bernardo/Electronic Notes in Theoretical Computer Science 162（2006）87954443.5精确聚合属性P ~nr-微分器上的P_2MT的公理化仅对P_2MB的公理化公理，因此我们可以集中在AJ上来研究在CTMC级别。 如果我们把AJ如以下重写规则：S1|我|S1S|我|一千一百零一，|J1||我|1.1升|我|、|J|我||PiS'克什托克年月11日s“克什托克|我||我|、克什托克|我Pi，j其中对于所有i1，i2∈I：j∈Ji1Σμi1，j=j∈Ji2μi2，jμ结果是AJ聚集体|我|两个国家合并为一个国家。 现在的问题这就产生了关于这种聚合是否准确的问题，即，该电台是否处于右侧的聚合CTMC的宏状态的静态/瞬态概率是处于左侧的原始CTMC的组成微观状态之一的静态/瞬态概率的总和。一个肯定的答案将意味着绩效评估工具包对绩效评估目的的有用性，即在以下过程中保持绩效衡量的价值：马尔可夫检验等价。定理3.7由BMT诱导的CTMC级聚集是精确的。Q4马尔可夫迹等价在这一节中，我们首先回顾了[17]中给出的马尔可夫迹等价的定义，然后证明了马尔可夫迹等价是关于MPC算子的同余，对MPC的非递归项有一个合理而完整的公理化，并导出了与马尔可夫测试等价相同的精确CTMC级聚集。4.1等效性定义与马尔可夫测试等价不同，在马尔可夫迹等价的情况下，给定一个过程项P∈ P，我们不再有与P相互作用的测试。相反，我们直接考虑孤立地进行的P的有限长度计算的多集Cf（P）定义4.1设P∈P且c∈Cf（P）. 与c的执行相关的迹通过对c的长度的归纳定义如下：⎧如果长度（c）= 0，则为εtrace（c）=a，λa·trace（cJ）如果c<$P− −→cJ96M. Bernardo/Electronic Notes in Theoretical Computer Science 162（2006）87rate（P）t4其中ε是空迹。定义4.2设P∈ P，c∈Cf（P），α∈AT型.我们说c与αitrace（c）=α相容。我们用CC（P，α）表示与α相容的P的有限长计算的多集。定义4.3设P∈ P，α∈A型，c∈ CC（P，α）。c的执行概率和平均持续时间通过对c的长度的归纳定义为：如下所示：⎧如果长度（c）= 0，则为1概率（c）=a，λ<$λ·prob（cJ）ifc<$P− −→cJ速率t（P）如果长度（c）= 0，则为 0时间（c）=a，λ我们还提出：1+时间（cJ），如果c<$P−−→cJ对于所有的C CC（P，α），并且：Σ概率（C）=c∈Cprob（c）C≤t={c∈C|时间（c）≤t}对所有C∈ CC（P，α）且t∈R≥0.定义4.4设P1，P2∈ P.我们说P1是等价于P2的马尔可夫迹，记为P1<$MTrP2，i对所有迹α∈AType<$p和平均时间t∈R≥0：prob（CC≤t（P1，α））=prob（CC≤t（P2，α））4.2同余性质结果证明，关于动作前缀和替代成分，CITMTr是一个一致性。定理4.5设P1，P2∈ P. 当P1≠MTrP2时，则：(i) .P1<，λ>.P2，对所有的 ∈ Act.(ii) 对所有P ∈ P，P1 + P<$MTrP2 + P和P + P1<$MTrP + P2.Q4.3可靠的和完全的公理化很容易看出，AMTr严格包含在AMTr中，因此公理A1-AJ表1中的“”仍然适用于CMTr，但不完整。给出了一个过程项是马尔可夫迹等价而不是马尔可夫检验等价的通过：以及：.& lt;b，μ>.P1+ .& lt;c，μ>.P2.Σ。 b<，·μ>.P + .P12λ1+λ21λ1 +λ22M. Bernardo/Electronic Notes in Theoretical Computer Science 162（2006）87974444（A1）（A2）（A3）P1+P2=P2+P1（P1+P2）+P3=P1+（P2+P3）P+0=P（阿JJ）4Σ Σ。.P我i，j i，j i，j=i∈Ij∈Ji<本发明公开了一种复合材料，Σk∈I λk>。Σ Σi∈Ij ∈Ji.Pi，jk∈Iλk如果对所有i1，i2∈I：Σ μi1，j=j∈Ji1Σj∈Ji2μi2，jμ事实上，以a开头可能跟有b或c的迹线都不能区分这两项，因为在这两项中，执行a-动作跟有b-动作或c-动作的平均时间是1/（λ1+λ2）+ 1/μ，而到达P1的概率（分别为1 /（λ 1 + λ 2）+1/μ）。P2）为λ1/（λ1+λ2）（分别λ2/（λ1+λ2））。相比之下，如果b/=c，则任何以被动a-动作开始，后面跟着被动b-动作或被动c-作用可以区分这两项，因为它增加了在ving。P1+< c，λ2/（λ1+λ2） ·μ>. P2分别从1/μ到（λ1 + λ2）/λ1·1/μ或（λ1 + λ2）/λ2·1/μ。表2Pnr上的MMTr原来上面的两个项构成了一个更自由的公理模式AJJ的最简单的例子，我们必须用它来代替更严格的公理模式AJ，以获得一个可靠的和完整的公理化的P编号这样的公理化由表2中所示的公理集A jj给出，其中 I和J定义了具有|我| ≥2（如果Ji=0，则相关数据取为0）。定理4.6推导系统DED（A_J_J）是可靠的和完备的在Pnr上，即对所有的P1，P2∈ Pnr：QAjjP1=P2P1MTrP24.4精确聚合属性通过查看公理模式AJ和AJJ的结构和速率约束，可以直接得出结论，这两个公理模式导致相同的CTMC级聚合，这是在第3.2节中描述的聚合。三点五定理4.7.Q推论4.8CTMC水平的聚集是精确的。Q98M. Bernardo/Electronic Notes in Theoretical Computer Science 162（2006）875结论在本文中，我们已经表明，马尔可夫测试和跟踪等价诱导在CTMC水平相同的聚集，这是严格粗糙比普通集总和准确。这确保了，无论何时两个过程项是马尔可夫检验或跟踪等价的，它们都具有相同的性能特征。另一个结果是马尔可夫测试和迹等价在状态空间减少方面改进了马尔可夫双相似性，同时保留了精确的聚合属性。从不同的角度看，本文的主要结论是：我们的知识在建立了精确集结的基本性质之后，进一步研究马尔可夫检验和迹等价的性质就变得有意义了除了合同和健全的和完整的公理化的动态运营商，我们已经在本文中，在理论方面，我们想调查的合同性质的平行组合，我们想得到的马尔可夫测试和跟踪等价的逻辑特征。在验证方面，设计一个算法来检查马尔可夫测试等价性的两个过程项的一个很好的起点可能是[7]中提出的经典测试等价性这需要马尔可夫测试等价性的更多表征，这可能受到[15]中提出的接受树模型的概率变体的启发。检查马尔可夫迹等价的两个过程项的问题已经在[17]中解决，其中设计了多项式时间算法。最后，根据本文证明的马尔可夫测试和迹等价的精确聚集性质，这在某种意义上扩展了普通的集总，理解由马尔可夫测试和迹等价引起的CTMC级聚集是否是可以获得的粗精确聚集或可以进一步扩展是有趣的。确认作者希望提到的是，在2000年与Mario Bravetti讨论结束时，提出了一个由马尔可夫检验等价性引起的CTMC级聚集引用[1] C. Baier，J. P. Katoen，H. Hermanns和V. Wolf，[2] M. Bernardo，M. Bernardo/Electronic Notes in Theoretical Computer Science 162（2006）8799[3] M. Bernardo和M.Bravetti，[4] M.贝尔纳多和W. R.李明，[5] P. Buchholz，[6] W.R. Cleaveland，Z.Dayar，S.A.Smolka和S.袁，[7] W.R.克里夫兰和M.C.B. Hennessy，[8] R. De Nicola和M.C.B. Hennessy，[9] R.J. van Glabbeek，S.A. Smolka和B. Ste Eschen，[10] H. Hermanns，[11]H. Hermanns和M. Rettelbach，71-87，埃尔兰根（德国），1994年。[12] 刘晓波，[13] K.G. Larsen和A. Skou，[14] R. Milner，[15] M. NunPleez， A1gebraicProgramming 56：117-177，2003.[16] E.W.斯塔克，W.R. Cleaveland和S.A. Smolka，[17] V. Wolf，M. Majster-Cederbaum和C. Baier，