马尔可夫链的（双）模拟关系：概率系统建模和性能评估

理论计算机科学电子笔记162（2006）73-78www.elsevier.com/locate/entcs马尔可夫链克里斯特尔·拜尔UniversitaütBonn，D-53117Bonn，Germany霍尔格·赫尔曼斯UniversitaétdesSaarlandes，D-66123Saarbruécken，Gerrmany约斯特-彼得·卡通RWTH Aachen，D-52074 Aachen，Germany维雷娜·沃尔夫曼海姆大学，D-68131曼海姆，德国摘要互模拟和模拟关系的形式化概念对于任何类型的进程代数都起着核心作用。这篇简短的论文概述了概率系统的互模拟和模拟关系的主要概念，由离散或连续时间马尔可夫链建模关键词：马尔可夫链，（弱）模拟，（弱）互模拟，时序逻辑1引言为了比较标记转移系统中状态的逐步行为，模拟和互模拟关系已被广泛考虑。它们在进程代数框架内的组合设计和推理以及抽象方面发挥着至关重要的作用。互模拟关系是要求两个双相似状态表现出相同的逐步行为的等价关系模拟关系是单向的要求，只要sJ模拟s，那么状态sJ就可以模拟所有s的逐步行为;但可能不是反之亦然。通常，（bi）模拟关系具有许多优良的性质，例如并行合成和过程代数的其他算子的同余性质，线性合成和过程代数的1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.07874C. Baier等人理论计算机科学电子笔记162（2006）73−→和分支时间逻辑;他们有健全和完整的公理化，高效的决策算法，并允许共归纳推理。在这篇简短的论文中，我们认为概率系统建模的行动标记马尔可夫链，并总结了（双）模拟关系的主要概念。马尔可夫链是一类重要的随机过程，在实践中广泛用于确定系统性能和可靠性特征，参见例如[28，20]。已经定义了各种具有操作马尔可夫链语义的过程代数，参见[27，17，9，23，22，30]的概述。基于Jonsson和Larsen [26]以及Larsen和Skou [29]的开创性工作，已经研究了离散和连续时间马尔可夫链的模拟和互模拟关系本文综述了时间抽象的完全概率系统（离散时间马尔可夫链）和连续时间马尔可夫链的分支时间关系的比较语义的结果我们跳过许多细节，这可以在上述文献中找到，并专注于互模拟和模拟关系的随机概念“行”是一种行为，一种行为。 我们假设τ∈Act是一个特殊的行动符号，用于不可观察的活动，即，这是一个复杂的计算过程。Ac\{τ}中的所有行为都是可见的。如果a是一个可见的动作，则symbola等于a，而τ=则是第二幕中的空词。2马尔可夫链动作标记离散时间马尔可夫链（简称DTMC）是一个标记的转移系统，其中每个状态都与一个概率分布相关联，该概率分布指定了动作和后续状态的概率也就是说，在任何一个州是在所启用的转换sasJ之间的概率选择。形式上，DTMC是一个元组D=（S，P），其中S是一个可数的状态集，P：S×Act×S→[0， 1]Σ是满足sJ∈S，a∈Act的概率矩阵P（s，a，SJ）= 1，对所有s ∈ S.我们认为DTMC是时间抽象模型。DTMC这个名字具有历史意义原因（离散）定时解释适用于所有状态变化都发生在等距时间点的设置。相比之下，CTMC被认为是时间感知的，因为它们具有明确的时间参考，以确定系统在时间上的随机演化的过渡率的形式 形式上，CTMC是元组C=（S，R），其中S如前所述，并且速率矩阵R是分配对任何三元组（s，a，sJ）一个非负实数，使得R（s，a，SJ）收敛。如果R（s，a，SJ）= 0，则不存在从s到SJ的a-标记的转移，否则从s到SJ的a-转移具有速率λ=R（s，a，SJ），这大致意味着1/λ是转换sasJ的平均延迟。在s中花费的平均时间−→J不执行任何操作的情况下的最大值是1/E（s），其中E（s）=sJ∈S，a∈Act R（s，a，s）是即所谓的状态s的退出率。 为了简单起见，我们假设所有的状态都有至少一个传出转换，即，对于所有状态s，E（s）>0。通过动作a从s移动到sJ的时间抽象概率是P（s，a，sJ）=R（s，a，sJ）/E（s）。那么，（S，P）是一个DTMC，称为C的嵌入DTMC。sJ∈ S，a∈ActC. Baier等人理论计算机科学电子笔记162（2006）73753强互模拟[29，27，17，11，23]而在非概率设置中，两个状态的互模拟等价要求一个状态的任何转换具有另一个状态的至少一个匹配转换，概率互模拟考虑 对于DTMC，互模拟等价表示coars-在状态空间上测试等价性，使得对于所有的s1和s2，所有的动作a所有互模拟等价类C，我们有P（s1，a，C）=P（s2，a，C），其中P（s，a，C）=0sJ∈CP（s，a，SJ）表示s通过a移动的概率，转换到C中的状态。类似地，对于CTMC，互模拟等价表示状态空间上的粗等价性，使得对于所有的s1和s2，所有的动作a并且所有互模拟等价类C，我们有R（s1，a，C）=R（s2，a，C），其中拉吉R（s，a，C）=sJ∈C R（s，a，s）表示从s通过动作a到C州。在这个意义上，CTMCC的互模拟等价性比其嵌入的DTMC的互模拟等价性更好，DTMC也比通过忽略概率获得的标记转移系统中的标准互模拟等价性更此外，在标号trans-mitted中，互模拟等价具有类似的性质sition系统。它们充分满足概率过程演算的复合算子的几个同余性质[17，23]，具有完整的公理化[27]，通过CTL-类分支时间逻辑[2，4，15]的逻辑刻画，共代数刻画[16，8]和多项式时间决策算法[24，3，12]。4弱互模拟[5，7]而在强（bi）模拟中，所有可见或不可见的步骤都被认为是从内部不可观察的步骤中抽象出来的弱（bi）模拟。在非概率环境中，存在弱互模拟的几个概念，这些概念在潜在的通过考虑τ-转移的累积概率效应，可以给出马尔可夫链的相应概念例如，模拟对于DTMC，MilnerPr（s1， τaτ， C）=Pr（s2， τaτ， C）其中Pr（s，τa τaτb， C）表示通过τaτb中 的 动作 等 式 从R移 动 到C状 态 的概 率。我不想让你在没有准备好的情况下离开，因为没有-DTMC的观测等价性与分支互模拟方程uivalence′alavanGlabbeekanddWeijland一致[18]。Roughlyspeaking，branching互模拟被定义为观测互模拟等价，除了在τ- 前缀中 的目标状态必须等于τ-前缀中的目标状态和τ-后缀中的目标状态对于DTMC，分支互模拟和观测互模拟等价，它们可以用（1）局部概率条件和（2）全局可达性条件来刻画76C. Baier等人理论计算机科学电子笔记162（2006）73局部概率条件要求对任何等价类B∈S/d条件概率P（s，a，C）1−P（s，τ，B）从s经由动作a移动到某个等价类C，只要执行可见动作或导致某个其他等价类的不可见动作（即， （a，C）/=（τ，B）），对所有状态s∈B都成立，其中P（s，τ，B）1.<的需要一个可达性条件来区分发散状态和非发散一个。形式上，它要求如果有一些状态s∈B可以执行可见的动作或可以到达另一个等价类BJ，那么这对B中的所有状态都成立。观测等价性的后一个特征可以很容易地适用于CTMC，其中我们可以处理（1）嵌入DTMC中的局部概率条件和（2）通过要求R（s1，a，C）=R（s2，a，C）（对于所有s1∈cs2和（a，C）∈Act×（S/c））来细化可达性条件的速率条件。其中τorsi∈/C，i = 1，2。 弱互模拟等价有一个简单的表征：Ctmc是上的粗等价，状态空间使得R（s1，a，C）= R（s2，a，C），对所有s1∈cs2，a∈Act和所有等价的无约束的.虽然BCLd和BCLc是相当强的等价关系，但它们是保留时间类CTL逻辑的所有分支时间属性的粗糙关系[14，7]。[1]中提出了DTMC弱互模拟的一个粗略概念，它依赖于τ-跃迁的非确定性跃迁关系和可见动作的概率选择。DTMC或CTMC的弱互模拟等价的局部特征允许使用与强互模拟算法[24]类似的思想并在多项式时间内运行的决策算法。5模拟关系[26，13，7]对于概率系统，模拟关系的形式定义比标记转移系统更复杂。原因是必须比较概率分布而不是单个状态。我们跳过细节，只提到正式的强模拟依赖于（1）概率的局部条件和（2）CTMC的附加速率条件。局部概率条件（1）可以通过所谓的权重函数[25，26]来形式化，该权重函数结合了状态的片段，或者替代地通过向上闭合集合的定量标准：如果s1由s2模拟，则对于所有动作a，P（s1，a，C↑）≤P（s2，a，C↑），是的。这里，C↑表示C的向上闭包，即模拟状态t∈C的所有状态u的集合。弱模拟的正式定义更为复杂，因为它依赖于识别可观察跃迁的适当片段，重新定义了强模拟的局部概率条件和速率条件，C. Baier等人理论计算机科学电子笔记162（2006）7377问。对于弱互模拟，需要一个附加的可达性条件来适当地处理发散然而，（强或弱）模拟等价在标记转移系统是粗糙的比（强或弱）互模拟等价，他们同意马尔可夫链。虽然这些定义相当复杂，但有限状态马尔可夫链的多项式时间决策算法依赖于网络流算法[3]或线性规划[6]。6结论本文简要介绍了马尔可夫链模型上的模拟和互模拟关系。在[7]中提供了它们的特征和性质的比较讨论，包括分支时间逻辑PCTL[19]和CSL [4]引用[1] S. Andova和J. Baeten。概率进程代数中的抽象。系统构造与分析的工具与算法，LNCS 2031，pp。204[2] A. Aziz，V. Singhal，F.巴拉林河Brayton和A.桑吉瓦尼-文森泰利它通常工作：随机系统的时间逻辑。计算机辅助验证，LNCS 939，pp。155[3] C.拜尔湾Engelen和M.塞德尔鲍姆少校概率过程的双相似性和相似性判定。J. of Comp. and System Sc. ，60（1）：187[4] C. Baier，B.R. Haverkort，H.赫尔曼斯和J. - P·加藤连续时间马尔可夫链的模型检验算法。IEEE软件工程学报，29（6）：524[5] C. Baier和H.赫尔曼全概率过程的弱互模拟。计算机辅助验证，LNCS 1254，pp。119-130，1997年。[6] C. Baier，H.赫尔曼斯和J. - P·加藤概率弱模拟在多项式时间内是可判定的。Inf. Proc. Lett. ，89（3）：123[7] C. Baier，J. P. Katoen，H.赫尔曼斯和沃尔夫。马尔可夫链的比较分支时间语义。出现在《信息与计算》中[8] C. Baier和M.Z.奎亚特科夫斯卡概率过程的域方程，计算机科学中的数学结构，10（6）：665-717，2000。[9] M. Bernardo和R. Gorrieri。扩展马尔可夫过程代数Concurrency Theory，LNCS 1119，pp. 315-330，1996年。[10] M. Bernardo和R.克里夫兰马尔可夫过程的检验理论。Concurrency Theory，LNCS 1877，pp. 305[11]P. Buchholz.有限马氏链中的精确和普通集总性。J.应用概率，31：59-75，1994.[12] S. Derisavi，H. Hermanns和W.H.桑德斯马尔可夫链中的最优状态空间集总。 Inf. Proc. Lett. ，87（6）：309[13] J. Desharnais。 标记马尔可夫过程 博士论文，麦吉尔大学，1999年。[14] J. Desharnais，V. Gupta，R. Jagadeesan，P. Panangelan.弱互模拟是合理的，完整的PCTL重复。Concurrency Theory，LNCS 2421，pp. 355-370，2002年。[15] J. Desharnais，P. Panangelo.连续随机逻辑刻画了连续时间马尔可夫过程的互模拟性. J. 逻辑与代数进展，56：99[16] E.P. De Vink，J.J.M.M.拉顿概率转移系统的互模拟：共代数方法，ICALP，LNCS 1256，pp 460-470，1997。78C. Baier等人理论计算机科学电子笔记162（2006）73[17] R.J. van Glabbeek，S.A.斯莫尔卡湾Ste daughen.概率过程的反应、生成和分层模型。信息计算，121：59[18] R.J. van Glabbeek，W.P. Weijland.互模拟语义学中的分支时间和抽象。J. ACM，43（3）：555-600，1996.[19] H. Hansson和B.琼森关于时间和可靠性的推理逻辑。Formal Aspects of Computing6：512[20] B.哈弗科特计算机通信系统的性能。基于模型的方法。约翰·威利父子公司1998年[21] H.赫尔曼 交互式马尔可夫链 LNCS 2428，2002年。[22] H.赫尔曼斯大学赫尔佐格和J. - P·加藤用于性能评估的进程代数。理论计算机科学，274（1-2），2002年。[23] J·希尔斯顿 一种性能建模的合成方法。 剑桥大学出版社，1996年。[24] T.玄湖田概率过程的若干等价关系。基金信息，17：211-234，1992.[25] C. 琼斯 概率非决定论 爱丁堡大学博士论文。1990年[26] B. Jonsson和K.G.拉森概率过程的具体化和细化。IEEE Symp.论Comp.Sc.中的逻辑，pp. 266-277，1991年。[27] C.- C. Jou和S.A.斯莫尔卡概率过程的等价、同余与完备公理化Concurrency Theory，LNCS 458，pp.367[28] V.G.库尔卡尼 随机系统的建模与分析。 查普曼大厅，1995年。[29] K.G. Larsen和A. Skou.通过概率测试进行互模拟。信息与计算，94（1）：1-28，1991.[30] N.洛佩斯，M。努涅斯概率过程代数及其等价的概述。随机系统的验证程序。目前的研究指南。计算机科学讲义2925，第89-123页