马尔可夫链代数在CTMC中的扩展及性能评估模型

理论计算机科学电子笔记162（2006）107-112www.elsevier.com/locate/entcsYMCA- 为什么是马尔可夫链代数？-马里奥·布拉韦蒂Di parti mentodiScienzedee ll' I n for o r m a z i o ne，Universi a `d i Bo l o g n a，Mura Anteo Zamboni 7，I-40127 Bologna，Italy.电子邮件地址：bravetti@cs.unibo.it霍尔格·赫尔曼斯德国萨尔大学计算机科学系，Dependency Systems Software，66123Saarbruecken，德国;和特文特大学，形式方法和工具P.O. Box 217，7500 AE Enschede，荷兰电子邮件地址：hermanns@cs.uni-sb.de约斯特-彼得·卡通RWTH Aachen，软件建模和验证，Ahornstrasse 55，D-52074，Aachen，Germany;和University of Twente，Formal Methods and Tools，P.O. Box 217，7500 AE Enschede，荷兰电子邮件地址：katoen@cs.rwth-aachen.de摘要马尔可夫链被广泛用于确定系统的性能和可靠性特征。绝大多数应用考虑连续时间马尔可夫链（CTMCs）。这篇笔记激发了并发理论如何扩展（而不是扭曲）到CTMC。我们提供了交互式马尔可夫链的代数设置的核心动机。因此，这本笔记最好被命名为YIMC。关键词：马尔可夫链，进程代数，并发理论连续时间马尔可夫链（CTMCs）是一种广泛使用的性能评估模型。它们可以被认为是标记的过渡系统，其中的过渡标记-负指数分布的速率-指示系统从一个状态演化到另一个状态的速度。数值算法允许以相对容易和舒适的运行时间并且以定量精确的方式计算给定CTMC的重要特性。使用概率模型检查技术，还可以1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.108108M. Bravetti等人理论计算机科学电子笔记162（2006）107λIMC是进程代数的简单扩展。IMC包含CTMC的代数，其中互模拟与集总性一致。查过了有几种软件工具可用于支持CTMC的规格化、数值分析和模型检查。本说明不涉及分析，但与CTMC的过程代数框架的建模和分析反应系统的集成。交互式马尔可夫链代数（IMC）是经典过程代数的一种扩展，它可以描述随机时滞。任何这样的延迟都由负指数分布来指定。基本概念是给进程代数增加一个延迟前缀。这种简单的扩展--延迟和动作之间的明确分离--产生了一种以精确和模块化的方式描述CTMC的具体形式主义，类似于典型现代系统的层次性质整合营销传播的理论是由一系列设计原理驱动的，我们将在后续文章中简要讨论它通过一个算子（λ）.P扩展了传统的进程代数，其中λ是任意的正实值，且.前缀运算符，P是进程代数项。直觉，（λ）。P在表现出P的行为之前延迟一个以速率λ呈指数分布的时间。 另一方面，在时间单位为1−e−λ·t或为implle：it时，P的概率为平均1时间单位演化为P。IMC以保守的方式扩展了进程代数，即，已建立的复合运算符的含义不会改变。IMC是一个保守的扩展，因为基本进程代数片段的操作语义、等价关系和等式理论保持不变。无论是CCS，π演算，CSP，ACP，μ-CRL还是. . .作为一个基础并没有什么不同。我们使用LOTOS，基本片段如下所示：P：：= a.P|P + P|X|记录X.P|P||SP其中a是一个动作，S是一组动作，+和||S是标准选择和平行组合。注意，最后一个基本原理也可以表述为CTMC的代数是与（标准）正交的IMC的一个片段。M. Bravetti等人理论计算机科学电子笔记162（2006）107109IMC自然支持相位型分布。IMC支持随机时间约束的约束导向过程代数片段，其特征在于以下等式定律：（B1）P+Q=Q+P（B2）（P+Q）+R =P+（Q+R）（B3）P+0=P（B4）（λ+μ）.P =（λ）.P+（μ）.P公理（B1）到（B3）是众所周知的，也是进程代数的标准公理（B4）是一个区别法则，可以看作是传统的选择幂等公理（P+P=）的马尔可夫设置的替代。P）。它反映了选择的分辨率由（统计独立的）指数分布的最小值建模。这些公理与处理经典进程演算上的递归的标准定律一起，可以被证明形成CTMC片段的合理和完整的公理化，由下式给出：P：：=（λ）.P|P + P|X|记录X.P|P||CUP相型分布可以被认为是指数分布的矩阵推广，并且包括经常使用的分布，诸如Erlang、Cox、超指数分布和次指数分布。直观地说，相位型分布可以被认为是具有单个吸收状态（一旦达到就永远不会离开的状态）的CTMC直到该吸收CTMC吸收的时间决定了相类型分布[9]。在IMC方面，相位类型分布可以通过显式地指定CTMC使用 求和 、递 归和 终止（ 0）， 如在 IMC项Qgivenbyy （ λ ） 中。 X.（μ）。 （μ）。 X+（λ）。0的情况。相位型分布的概率密度函数是非常有趣的，因为相位型分布可以近似任意接近的任意分布[9]（即，它是连续分布集合的稠密子集）。换句话说，IMC可以用来表示任意分布，通过选择适当的吸收马尔可夫链，并（机械地）在IMC中编码。(The在[11]中创造了面向约束的术语。）这个属性可以通过组合来丰富现有的具有随机时序约束的非时序规范。因此，时间约束的描述可以以模块化的方式进行，也就是说，作为通过与不定时的（或以其他方式受时间约束的）过程并行运行来约束行为的分离过程这是由一个经过运算符[6]促进的，该运算符用于对特定动作施加相位类型的分布式时间约束。这个的语义110M. Bravetti等人理论计算机科学电子笔记162（2006）107IMC增加了CTMC的非确定性和交互性。IMC有一个很好理解的等式理论。运算符是通过转换成IMC的基本运算符来定义的-事实上，它只是“语法糖”。由于IMC的组成性质，重要的性质（例如，全等结果）直接传递给该运算符。延迟是作为两个动作之间的时间约束而施加的，并且如果同时发生某种动作，则延迟可以被“中断”。也就是说，elapse运算符是具有四个参数的运算符，在语法上表示为[在S延迟D通过Q，除非B]：• 确定时间约束的持续时间的相位型分布Q，• - 一组动作S（开始），其确定延迟（由Q控制）何时开始，• - 必须延迟的一组动作D（延迟），以及• 一组动作B（中断），可以中断延迟。因此，在此之前，[n{a}delay{b}yQQ（modelingga phase-typedistribution）betwenandb. 很明显，该算子背后的直觉是，它用用于以适当的方式初始化和重置时间约束的某些同步势来充实链Q。时间约束是通过并行组合的方式施加在进程P上的，例如在P||SDB[在S上延迟D乘Q，除非B]。交互式马尔可夫链可用于指定CTMC，但由于非确定性的存在（从标准进程代数继承），IMC的基础模型更丰富。事实上，它是连续时间马尔可夫决策链的类[10]，CTMC的严格超集。非确定性是进程代数的重要组成部分之一，因此也是IMC的重要组成部分见[4，第5章]的声音和完整的等式特征的强和弱双相似性的完整演算，包括递归和开放的条款。M. Bravetti等人理论计算机科学电子笔记162（2006）107111结论简而言之，一个经过深思熟虑的基本代数算子的选择使IMC成为一个具有独特的一组区别性质的微积分。整合营销传播的理论在[4，5]中得到了发展;另见[1]。值得注意的是，像PEPA [7]或EMPAgr [2]这样的结石特别是，它们不是进程代数的保守扩展，因为延迟和动作是扭曲的而不是分离的。延迟和动作的分离允许将动作同步视为标准进程代数，也是获得更一般分布的进程代数框架的关键原则之一[3，8]。引用[1] M.布拉维提重新审视交互式马尔可夫链。电子笔记理论Comput. Sci. ，68（5），2002.[2] M. Bravetti和M.伯纳多具有概率、优先级和时间的进程代数的合成非对称合作。电子笔记理论Comput. Sci. 39（3），2000年。[3] M.布拉韦蒂河Gorrieri。交互广义半马尔可夫过程理论。Theor. Comput.Sci. 282（1）：5-32，2002.[4] H.赫尔曼交互式马尔可夫链和对量化质量的追求。LNCS 2428，2002年。[5] H. 赫尔曼斯大学赫尔佐格和J. -P. 加藤用于性能评估的进程代数Theor.Comput. Sci. ，274（1-2）：43 - 86，2001.[6] H.赫尔曼斯和J. - P·加藤自动合成马尔可夫链生成一个简单的老电话系统。计算机科学Prog. ，36（1）：97[7] J·希尔斯顿一种性能建模的合成方法。剑桥大学出版社，1996年。[8] P.R. D'Bagio，J.- P.Katoen和E.布林克斯玛随机系统的代数方法（扩展抽象）。编程的Chapman Hall，pp. 126[9] M.F.中性。随机模型中的矩阵几何解-数学方法约翰·霍普金斯大学出版社，1981年。[10] M.L. 普特曼马尔可夫决策过程：离散随机动态规划。约翰·威利父子出版社，1994年。112M. Bravetti等人理论计算机科学电子笔记162（2006）107[11]C.A. Vissers，G.斯科洛，M. van Sinderen和E.布林克斯玛在分布式系统设计中使用规范风格。Theor. Comput. Sci. ，89（1）：179