交互式马尔可夫链并发系统的设计,验证及评判

1、Concurrency includes parallel and distribution.进程代数成了现今复杂系数形式刻画与分析的要紧工具, 比较闻名的有 :CCS(calculus ofcommunication system),CSP(communicating sequentialprocesses),LOTOS(国 际 标 准 化 组织,language of temporal ordering specifications).假设随机变量D1 和 D2 别离知足参数为lambda 1 和 lambda 2 的指数散布 ,那么 :PD1<=D2= lambda 1 / (la

2、mbda 1+lambda 2);关于存在竞争的状态 si(非吸收态 ),其在时刻 t 内转移到状态j的概率为 :s(1-exp(-lamdba i t) lambda ij / lambda i.注意在上面的式子中 ,若是令 t- ->infinity,能够再次取得从状态si转移到状态js 的概率为 :lambdaij/ lambda .这一转移概率事实上刻画了一个与该CTMC 相关的 DTMC,称之为内嵌的iDTMC(embedded DTMC),它的转移概率矩阵为 P=(pij)n×n.在性能评判领域里马尔可夫分析要紧关切的几个性能气宇：1 抵达一个吸收状态的平均时刻MT

3、A;2 第一次抵达某个特定状态s 的平均时刻 MTFP(s);3 在一个给定的时刻t 系统处于一个特定的状态s 的概率 PXt =s.4 系统在长时刻运行后稳固在某个状态s 的概率 limt->infinityPX =s (假定该马尔可夫链能达t到一个平稳状态 )Steady-state analysisTransient analysisChapman-Kolmogorov 向前方程： P(t)=P(t) R.解此微分方程，有Runge-Kutta method, 或基于归一化 (uniformization) 的方式CTMC 的极限散布知足以下方程：pi=pi P(t)利用转移率矩阵

4、R，上式能够简化为：pi R=0，Chapter 3:IMC: Interactive Markov chains ：经典的进程代数模型和持续时刻马尔可夫链模型的结合;进程代数与标记转移系统动作集合 Obs=a,b1,c, 系统内部执行的运作tao not in Obs令： A=Obs并 tao 表示所有动作的全集概念 设 a in A， A belongs to Obs, Var表示一个进程变量的集合，x in Var。 大体进程代数BPA由以下语法产生：P:= 0|P;P|P+P| AA|x| 1 0 表示中止进程2 是动作前缀操作，表示系统先执行动作a，然后执行进程 P3 P1;P2 是

5、顺序操作4 P1+P2 是选择操作；这种选择的非确信性是并发系统的一个重要特点，也是与传统顺序相较的一个重要区别特点5 P| AP 是并发操作， 也是进程代数中最重要的一个操作，它代表了两个进程的并发执行，其中 A belongs to Obs 中的动作是两个进程需要同时执行的动作，即需要同步的动作。若是 A=emptyset，那么 P12不需要同步任何动作，现在称12为异步并发执行和 PP和 P的，并将 | empty set 简记为 |.另外，为书写方便，关于只一个元素的集合，省略a为 a.6 PA 是隐藏操作，或叫做抽象操作，行为与P 类似，唯一的不同是进程PA 中那些在集合 A 中的动

6、作都被看成内部动作（通过更名为tao），即外部将再也不可观看到。7 x 和 是为了支持递归操作而引入的操作符，其中x 代表一个进程变量，是递归表达式，其中变量 x 可能在进程 P 中显现形成一个递归函数。称被递归算子 限制的变量 （如x| 中的 x）为约束（ bound ）变量，没有被递归算子限制的变量称为自由（free）变量。自由变量能够通过替换来实例化 （ instantiated ），而约束变量那么是不受变量替换的阻碍，因经约束变量的名字能够被以为是无关紧要的。一个进程表达式中的某项若是没有自由变量，那么称该项为闭项 (closed),反之称为开项 (open) 。关于递归表达式，要求递

7、归项是良性护卫的 (well-guarded) ，这一条件保证了递归项的语义模型与它的指称函数的不动点相对应而且是唯一的。递归表达式的引入使得进程代数的表达能力更壮大，更适合描述一些特定的系统。默许优先级 (高 - ->低 )：.;+|进程代数作为一种严格的形式刻画方式，除要有严格概念的语法结构外，还需要有严格概念的语义模型。（ SOS， structural operational semantics ）采纳下面的表达方式前提 1前提 2 前提 n-(条件 )结论称为一条规那么：若是条件成立的话，该计划能够应用，而且当前提1 到前提 n 都知足时，结论成立。 其中规那么中的前提与结论都

8、具有P- -(a)- ->P,表示进程 P 能够执行动作a，同时演变成进程 P。表 BPA的结构化操作语义略，其中PQ/x 表示将进程P 中所有进程变量x 的显现都替换成进程Q 取得的进程；- -(a)- ->：标记转移系统（Labeled transition system, LTS）LTS要紧关切的是系统在发生状态转移时所执行的动作，因此是基于动作（action-based ）的系统模型。它的形式概念如下：概念一个 LTS是一个四元组 (S,Act,- ->,s0)，其中：1 S 是非空的状态集合；2 Act belongs to A 是动作集合；3 - ->S&#

9、215;Act× S 是状态转移关系；4 s0 是初始状态。LTS通经常使用图形来表示，能给出一个进程代数直观而且精准的执行进程例:aS2bS1S4bS3a该 LTS表示了如此一个进程的行为 : 由此可见 , LTS能给出一个进程代数直观而且精准的执行进程 .下面考虑两个进程并发执行的操作进程,先考虑不需要同步的情形 ,假设 P1=,P2=,那么 P1|P 2是如何执行的呢 ?依照 BPA 的结构化操作语义,很容易患出与上图相同的模型,这说明 ,在 LTS表示的操作语义模型说明下, 能够得出 |= 如此的结论 ,而这确实是 两个系统并发执行的交织语义明白得 ,即将两个并发执行的进程看

10、做是两个进程中的动作依照任意可能的交叉顺序执行,因此说 LTS是一个交织语义模型.关于需要同步的情形 ,例如 ,假设 P1=+, P2=+,那么 P1| c P2的 LTS模型如以下图 :aS2bS1cS4bS3a由上图能够看出,需要同步执行的动作由两个进程同时执行(当两个进程都预备好执行该动作时 ),而不需要同步的动作那么能够依照异步并发的执行方式任意交叉执行.将上述情形推行到一样的情形,设P=sumi aiPi, Q=sumjbjQj,在交织语义下,有下面的展开定律:P| Q = suma(P |Q) +sumbj not in Ab(P|AQ) +sumai=bj in Aa (P |Q

11、 )Aai not in Ai iAjjiiA j上式给出了两个并发执行的进程严格的交织语义说明,也是进程代数理论中一个重要的等式,若是一个进程代数中许诺该式成立,那么称交织语义的进程代数；假设不许诺该式成立,那么称该进程代数为真并发语义的进程代数,如用事件结构 (eventstructure) 作为语义模型的进程代数 .在交织语义下,任何大体进程代数表达式都能够展开表示为仅包括前缀操作(.)与选择操作 (+)的形式 ,即:P=.+.+=sumai in Act ai 1ai2ain0 因此 ,在交织语义下 ,进程代数的推理能够变得相对简单 .例 设 P=+|+, 那么依照展开定律 ,能够将

12、P 展开如下 : P=+|+=a.()+b.()+c.()+d.()=带标记的持续时刻马尔可夫链LTS 要紧用于刻画并发系统行为特点,关注的是系统在发生状态转移的时候所执行的动作,状态本身的信息并非是它所关切的,而性能评判领域经常使用的马尔可夫链模型那么要紧关切的是系统所处的状态信息,因此 ,在用马尔可夫链进行系统的性能评判时,人们常常采纳稍作修改的马尔可夫链模型 .Labeled CTMC:假定 AP 是所有原子命题的集合,那么 :Labeled CTMC是一个四元组 (S, - ->, L, alpha0),其中 :S 是状态空间集合 ;- - -> belongs to S&

13、#215; R+× S,是状态转移关系 ,称为马尔可夫转移；(虚箭头 )L: S |- -> 2AP 是标记函数 ,用于给每一个状态标上该状态所知足的原子命题的集合;alpha0 是初始散布 .s- -()- ->s.概念中的 L 称为标记函数 ,它是用来给CTMC 的状态增加一些附加信息的,这些附加信息是一些原子命题的集合 .不失一样性 ,假设不同的状态知足不同的性质,那么这些原子命题的集合就能够够用于区分不同的状态,即每一个状态都能够由它上面标记的原子命题的集合来唯一标识 .如此一来 ,带标记的 CTMC要紧关注的确实是每一个状态上的不同信息了,因此称如此的系统为基于

14、状态的 (state-based)系统 .例:c1S1bS0S332S2ca4S4上图表示一个带标记的CTMC.其中 AP=a,b,c,每一个状态所知足的原子命题标在状态旁,状态间的转移仍然保留虚线箭头的形式,关于单元素集合 ,一样采纳了省略花括号的简写方式.(带标记的 )CTMC的语言层次的刻画模型有排队网逻辑刻画有持续随机逻辑CSL及其变体等 .,随机 Petri 网 ,随机活动网,随机进程代数等；交互式马尔可夫链IMC结合 LTS与 CTMC:随机进程代数模型:SPA(stochastic process algebra): SPA模型在结合LTS和 CTMC 时都有一个一起的特点-它们

15、都是将两个模型不同转移关系(动作转移与概率转移)融合在一个转移关系中 ,即将 :-a->( 实线 ),与 -()->(虚线 ) 组合成一个单一的转移关系(a,)->,其含义是系统发生该状态转移的延迟时刻知足参数为 的指数散布 ,同时在发生状态转移时系统将执行动作a.由于将两种转移关系合二为一 ,在这种模型中,系统在不同的状态转移之间选择执行的动作将再也不是确信的,因为事实上每一个动作执行都由一个确信的概率散布(由参数为的指数散布确信 )来决定 ,也确实是说 ,非确信被概率散布所取代 .但是非确信性关于并发系统来讲是个超级重要的特点,它有助于模拟很多用其他方式不能表达的重要概念

16、,例如 :1. 实现自由(非确信性 )2. 调度自由(交织语义模型下非确信性概念的一个经典的利用,几个并发执行的进程在交织语义明白得下能够看成是在这些进程之间自由地选择执行)SPA 模型将动作与时刻延迟绑定在一个转移关系上,处置带有同步动作的并行操作时就会碰到一些很棘手的问题 .例:进程 P1 在动作 a 和 c 之间选择 ,同时动作 a 与 c 的执行别离知足参数为与 1；进程 P2 在动作 b 和 c 之间选择 ,与 21c 2;在交织语义下 P |P ,由于指数散布的无经历性 ,a,b 的散布参数不变；但指数散布并非在最大值运算下封锁,即两个知足指数散布的随机变量的最大值再也不知足指数散

17、布 .因此 ,动作 c 的执行所知足的延迟散布再也不是指数散布,即同步以后动作c 上的散布参数phi 无法简单确信下来(事实上已经跳出了SPA的范围 ). SPA模型总的来讲在处置同步并发的时候并非那么令人中意.总之 ,SPA模型中有以下两大问题是不能专门好解决的:1.非确信性再也不是真正意义上的非确信性,而是被随机散布所代替;2. 带同步的并发操作在 SPA 模型并非能专门好地表示出来 ,因为指数散布在最大值运算下并非封锁 .IMC 确实是为了解决 SPA这些不足而提出来的另外一种结合LTS与 CTMC 的模型 .交互式马尔可夫链IMC 与 SPA不同 ,它保留两种转移关系而不是将它们合二为

18、一.一个 IMC 是指一个五元组 (S,Act, ,->,s0),其中 :S 是一个非空的状态集合 ;Act belongs to A 是一个动作集合 ;belongs to S× Act× S 是动作转移关系 ;-> in S× R+× S 是马尔可夫转移关系 ,知足 :For all s1,s2 in S, |(-> (s1× R×s2)|<=1注 :对马尔可夫转移关系要求知足的条件说明,任意一对状态之间最多只有一个马尔可夫转移关系 .若是存在多个如此的转移关系,依照指数散布的性质,能够简单地将这几个转移关

19、系合为一个 ,取得的转移为原先各个转移之和.另外 ,与转移率矩阵R 有一点小小的区别是,在马尔可夫转移关系 ->,许诺到自身的转移,它表示系统通过参数为的指数散布延迟后仍然停留在原状态 (或转移到自身状态 ).这一修改并非阻碍IMC 的随机行为 ,可是却更适合于通常的状态转移说明 .S0 是初始状态 .以下 ,记 R(s,s)为状态 s 转移到 s的转移率 .s 上的总转移记为E(s)=sumsin S R(s,s).定理任何一个LTS都与一个IMC 同构 ,任何一个CTMC都与一个IMC 同构 .在 IMC 中 ,由于动作转移与时刻延迟是分离的 ,因此这些动作转移之间的选择就能够够仍然

20、保留 LTS的非确信性说明 ,如此 IMC 解决了 SPA模型中非确信性不能保留的问题 .IMC 采纳最大前进假设(maximal progress assumption): 内部动作 (即动作 tao)的执行不许诺时刻延迟的发生 ,即假设系统内部动作要执行的话 ,该动作的执行是当即的 ,不许诺其他延迟转移发生 .因此 ,若是一个内部动作转移与马尔可夫转移一起存在于一个状态的时候 ,马尔可夫转移可被忽略 .可是关于外部动作 (即 Obs 中的动作 )a,它的执行是依托环境的 ,或说它是环境交互的一个动作 ,因此是有可能被延迟的 ,假设在一按时刻内系统没有执行动作 a(或与环境进行动作 a 的交

21、互 ),那么系统能够选择执行马尔可夫转移 .最大前进假设普遍用于很多实时进程代数中 ,它反映了内部动作具有比外部动作更高的优先级.IMC 模型中 ,动作与延迟时刻的分离使得咱们在考虑同步执行的动作时没必要考虑延迟时刻,因为它们并非参与同步.需要同步的动作的执行时刻发生在并发执行的所有组件都预备好执行该动作的时候,换句话说 ,IMC 将同步动作的延迟隐式地实现为最大散布,因为只有动作转移需要同步 ,因此同步的发生意味着该动作的所有延迟都已经完成.而关于不需要同步的动作转移和马尔可夫转移,它们那么是依照经典的交织语义来执行的,注意到由于马尔可夫性,马尔可夫转移也是能够任意交叉执行的.IMC 很明确

22、地域分了非确信性和概率,保留了并发系统中非确信性那个重要概念带同步动作的并发执行下,简单而优美地解决了同步动作的随机散布问题.,同时 ,IMC在例:S0 - ->s1as2S0 - ->s1as2| a:S0 - ->s1 - ->s3s3as4S0 - ->s2 - ->s3IMC 的代数刻画概念 令 a in Act, A belong to Obs, in R+, x in Var, 那么交互式马尔可夫链进程代数 IMPA 由以下语法产生 :P:=0|(其中 ,新增加的 ().P 称为延迟前缀操作指数散布时刻延迟,它事实上对应了).P|P;P|P+P|

23、P AP|PA|x| ,表示系统在执行进程 IMC 模型中马尔可夫转移,P 之间需要通过一个参数为的.可见 IMPA 是 BPA一个超集 .例 令 P,Q in IMPA,那么以下是合法的IMPA 表达式(1) a.().().b.().0(2) +().Q(1) 的直观含义是 :系统第一与动作 a 进行交互 ,执行动作 a,然后 ,系统再进一步与动作 b进行交互之前将有两次延迟 ,第一次知足参数为 的指数散布 ,第二次知足参数为 的指数散布 .在系统执行动作 b 以后 ,系统通过一个参数为 的指数散布延迟后中止 .(2) 式是 IMPA 中一个典型的表达式 ,它反映了 IMC 系统中动作转移与马尔可夫转移之间的彼此关系 .(2)式代表了系统在一个动作转移与马尔可夫转移之间进行选择,这种