资源描述：
《交互式马尔可夫链-并发系统的设计,验证与评价》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。
1、Concurrencyincludesparallelanddistribution.进程代数成为了当今复杂系数形式刻画与分析的主要工具,比较著名的有:CCS(calculusofcommunicationsystem),CSP(communicatingsequentialprocesses),LOTOS(国际标准化组织,languageoftemporalorderingspecifications).假设随机变量D1和D2分别满足参数为lambda1和lambda2的指数分布,则:P{D1<=D2}=lambda1/(lambda1+lambda2);对于存在竞争
2、的状态si(非吸收态),其在时间t内转移到状态sj的概率为:(1-exp(-lamdbait))lambdaij/lambdai.注意在上面的式子中,如果令t-->infinity,可以再次得到从状态si转移到状态sj的概率为:lambdaij/lambdai.这一转移概率实际上刻画了一个与该CTMC相关的DTMC,称之为内嵌的DTMC(embeddedDTMC),它的转移概率矩阵为P=(pij)n×n.在性能评价领域里马尔可夫分析主要关心的几个性能度量：1．到达一个吸收状态的平均时间MTA;2．第一次到达某个特定状态s的平均时间MTFP(s);3．在一个给定的时间t系
3、统处于一个特定的状态s的概率P{Xt=s}.4．系统在长时间运行后稳定在某个状态s的概率limt->infinityP{Xt=s}(假定该马尔可夫链能达到一个平稳状态)Steady-stateanalysisTransientanalysisChapman-Kolmogorov向前方程：P’(t)=P(t)R.解此微分方程，有Runge-Kuttamethod,或基于归一化(uniformization)的方法CTMC的极限分布满足以下方程：pi=piP(t)利用转移率矩阵R，上式可以简化为：piR=0，Chapter3:IMC:InteractiveMarkovcha
4、ins：经典的进程代数模型和连续时间马尔可夫链模型的结合;进程代数与标记转移系统动作集合Obs={a,b1,c,…}系统内部执行的运作taonotinObs令：~A~=Obs并{tao}表示所有动作的全集定义3.1.1设ain~A~，AbelongstoObs,Var表示一个进程变量的集合，xinVar。基本进程代数BPA由以下语法产生：P::=0
5、a.P
6、P;P
7、P+P
8、
9、AP
10、PA
11、x
12、μx.p1．0表示中止进程2．a.P是动作前缀操作，表示系统先执行动作a，然后执行进程P3．P1;P2是顺序操作4．P1+P2是选择操作；这种选择的非确定性是并发系统的一个重要特征
13、，也是与传统顺序相比的一个重要区别特征5．P
14、
15、AP是并发操作，也是进程代数中最重要的一个操作，它代表了两个进程的并发执行，其中AbelongstoObs中的动作是两个进程需要同时执行的动作，即需要同步的动作。如果A=emptyset，则P1和P2不需要同步任何动作，此时称P1和P2为异步并发执行的，并将
16、
17、emptyset简记为
18、
19、
20、.此外，为书写方便，对于只一个元素的集合，省略{a}为a.6．PA是隐藏操作，或者叫做抽象操作，行为与P类似，唯一的不同是进程PA中那些在集合A中的动作都被看成内部动作（通过改名为tao），即外部将不再可观察到。7．x和μx.p是为了
21、支持递归操作而引入的操作符，其中x代表一个进程变量，μx.p是递归表达式，其中变量x可能在进程P中出现形成一个递归函数。称被递归算子μ限制的变量（如x
22、μx.p中的x）为约束（bound）变量，没有被递归算子限制的变量称为自由（free）变量。自由变量可以通过替换来实例化（instantiated），而约束变量则是不受变量替换的影响，因经约束变量的名字可以被认为是无关紧要的。一个进程表达式中的某项如果没有自由变量，则称该项为闭项(closed),反之称为开项(open)。对于递归表达式，要求递归项是良性护卫的(well-guarded)，这一条件保证了递归项的语义模型与
23、它的指称函数的不动点相对应并且是唯一的。递归表达式的引入使得进程代数的表达能力更强大，更适合描述一些特定的系统。默认优先级(高-->低)：.;+
24、
25、进程代数作为一种严格的形式刻画方法，除了要有严格定义的语法结构外，还需要有严格定义的语义模型。（SOS，structuraloperationalsemantics）采用下面的表达方式前提1∧前提2∧…∧前提n--------------------------------------(条件)结论称为一条规则：如果条件成立的话，该规划可以应用，并且当前提1到前提n都满足时，结论成立。其中规则
