连续时间概率KLAIM: 分布式编程与概率语义的定量分析

理论计算机科学电子笔记128（2005）27-38www.elsevier.com/locate/entcs连续时间概率KLAIMAlessandra Di Pierro意大利比萨大学信息学系克里斯·汉金1英国伦敦帝国理工学院计算机系Herbert Wiklicky1英国伦敦帝国理工学院计算机系关键词：分布式编程，概率语义，连续时间马尔可夫链1介绍设计支持网络编程的语言是实现分布式和移动计算形式化的必要步骤。一个抽象的语义框架的存在构成了对这种系统进行形式化分析的基础。KLAIM范例[5]通过引入基本概念和原语提供了这样一个语义框架，这些基本概念和原语解决了相互作用的定位进程的协调的关键方面。我们扩展了这一基本范式的概率结构，目的是引入一个语义的网络定量分析的基础一般而言，定量分析例如，概率分析允许建立系统的安全性高达1所有这些都是由EPS RCp rojectS 77066A“计算资源的量化分析”提供资金的。1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.11.04028A. Di Pierro等人/理论计算机科学电子笔记128（2005）27S∈S（物理）站点v∈瓦尔（基本）价值观L∈Loc（逻辑）局部性e∈Exp（基本）表达式L ∈禄寿（一般）地点一 ∈Proc（预定义）过程X∈V ar（值）变量u∈LV ar（局部）变量Q∈维尤配置环境X∈PV ar（过程）变量表1句法类别给定表示系统实际上有多脆弱的容差因子这与定性分析相反，定性分析通常可用于验证给定系统的绝对安全性。在分布式环境中，定量分析在考虑涉及以不同时钟运行的进程之间的异步通信的定时问题时也具有很大的实际用途在安全设置中，这些问题是相关的例如用于分析和预防拒绝服务攻击，这涉及到时间关键型操作的延迟[9]。在我们的概率版本的KLAIM中，我们称之为pKLAIM，我们以多种方式引入概率。在局部层次上，我们引入概率并行和选择算子。此外，我们使用的概率分配环境相关联的物理站点上的分布与逻辑的地方。此外，我们将速率与每个节点相关联;这决定了节点活跃的频率。另一种方法是将概率与每个节点相关联，表示该节点上的进程被选择执行的机会。我们已经研究了这样一个变量在较早的文件[6]中详细。2pKLAIM的结构pKLAIM的语法基本上基于最初在[5]中给出的KLAIM语法，并参考表1中的语法类别。pKLAIM中的工艺术语根据表2中的规则形成。与原始KLAIM语言的主要区别是选择的概率加权和局部并行性。在网络层次上，转移概率是时间的函数;特别是，它们受某个特定速率给定的参数指数分布的支配。语法定义见表4。差异A. Di Pierro等人/理论计算机科学电子笔记128（2005）2729ęP：：=nil空进程|a.Paction prefixni=1|+ npi：Pi概率并行pi：Pi概率选择i=1||XA（P，l，e）过程变量进程调用a：：=out（t）@l发送元组|in（t）@l接收元组|read（t）@l检查元组|eval（P）@l远程评估|newloc（u）新位置表2工艺流程t：：=t1，t2元组|eexpression tuple|Pprocess tuple|llocality tuple|! x表达式模板|! u局部性 模板|! X工艺模板表3 KLAIM元组N：：=s：：λP 节点|N1ǁ N2composition表4网络拓扑在标准KLAIM的网络语法之间是执行速率λ，其是根据连续时间马尔可夫链模型确定网络的行为的正实数。我们将在第3.2节中形式化这个模型，在那里我们定义了pKLAIM的操作语义。我们利用概率分配环境，使我们能够||30A. Di Pierro等人/理论计算机科学电子笔记128（2005）27将逻辑位置与所述物理站点集合上的概率分布相概率分配环境被正式定义为部分映射：Q：位置→距离（S），其中Dist（S）是物理站点上所有分布的集合。我们将这个定义推广到物理站点集合S，定义Q（s）为这样一种分布，它将概率1分配给s，将概率0分配给所有其他sJ∈S。我们用φ表示在所有l∈Loc上定义的概率分配环境。分层过程允许用外部分配环境Q扩展内部分配环境σ（如在标准KLAIM中），定义为概率分配环境：⎧σi（σ·Q）=否则，只要l有一个内部分配σ，我们就可以根据分布σ（l）随机地将l与一个可能的位点标识在一起;只有当σ=φ时，我们才都将l分配给Q（l）。3pKLAIM的操作语义pKLAIM的操作语义是通过KLAIM的两个操作语义级别的概率版本定义的在局部层次上，每个节点上的过程本质上表现为离散时间马尔可夫链，而全局网络更新被建模为根据节点上的速率确定的转移概率而演变的链。因此，在全局水平上，每个节点表现为具有速率λ的泊松过程。这定义了pKLAIM的操作语义，根据网络作为局部同步和全局异步的系统3.1本地语义局部跃迁关系P1行动 P2布吕普定义见表5。与KLAIM的原始语义一样，我们使用标签动作来描述演化中执行的活动;因此，例如o（t）@l指的是在由l指定的元组空间中发送元组t的动作，而r（t）@l是在由l指定的元组空间中消费元组t的动作。遵循[5]中的约定，我们使用额外的- 不是pKLAIM语法的一部分-在A. Di Pierro等人/理论计算机科学电子笔记128（2005）2731PJę·σpnnn输出（t）@l.Po（t）@lP输入（t）@l.Pi（t）@l P读取（t）@l.Pr（t）@l Pφ1φ1φ1eval（Q）@l.Pe（Q）@lPnewloc（u）@l.Pn（u）@l PPµPJφ1PµPJφ1Pµ PJJJ.J.ępjępi=1pi ：PiµJp·pjji=1pi ：Piµp·pjj/=i=1Pi| PJP{σ}µPJ{σ}P[Q/X，l/u，e/x]µPJ布吕普A（Q，l，e）µPJ其中P<$A（X，u，x）布吕普表5局部结构语义学T[[e]]=E[[e]]T[[P]]=P{Q}T[[l]]n=s，其中hp=Q（l）（s）T[[！x]]=！XT[[！X]]=！XT[[！u]]=！uT[[t1，t2]]=T[[t1]]，T[[t2]]表6概率元组评价操作语义;例如，我们使用元组评估与标准KLAIM略有不同，因为我们必须考虑到分配环境是具有站点的位置的概率标识。每次我们计算一个位置l时，我们可能会得到另一个位置。 如果p∈Q（l），则e表示概率p∈Q（l）（s）. 元组的求值函数在表6中定义，其中E [[e]]表示封闭表达式的求值机制。表7中的元组匹配（使用模板）与标准KLAIM中的定义完全相同我们将也写X Y表示匹配（X，Y）。3.2全局语义分析我们将为pKLAIM定义一个连续时间语义，它依赖于状态变化（转换）不会发生在规则空间（如+||32A. Di Pierro等人/理论计算机科学电子笔记128（2005）27match（v，v）match（P，P）match（s，s）match（！x，v）match（！X，P）match（！u，s）匹配（et1，et2）匹配（et3，et4）匹配（（et1，et3），（et2，et4））匹配（et1，et2）匹配（et2，et1）表7概率元组匹配离散时间模型）;相反，从一个状态到另一个状态的跳跃以某些实数指定的速率发生。根据连续时间马尔可夫链模型，这些速率确定了从网络的一种配置到另一种配置的转换之间的指数分布时间（参见例如[16，14，1]）。在我们的模型中，每个节点可以在任何时候独立地发起网络更新该参数在节点语法中由上标λ指定我们假设这些速率与时间无关，因此每个节点都即发起更新，经由所谓的泊松过程（参见例如，[14，第2.4节]）。pKLAIM的全局语义定义见表8。 过渡关系rztij 两个网络配置Ni和Nj的z标记为速率tij，其作为发起更新的节点的触发速率与更新中所涉及的节点中发生的局部转变的归一化概率之间的乘积而获得。需要对局部转移概率进行归一化，以考虑节点“不活动”的可能性，速率tij允许我们计算在时间t从网络配置Nj全局转移的概率，假设我们在时间t= 0开始于状态Ni，简单地说：P（N（t）= N j|N（0）= N i）=（exp（tT））ij哪里tij=Tij=QijPij，对于i=ijΣtii=Tii=−jQijPijPij是局部离散概率，Qij是与A. Di Pierro等人/理论计算机科学电子笔记128（2005）2733发起从Ni到Nj的全局更新的节点。例3.1考虑以下简单的三节点pKLAIM网络：l：：λ1（1out（t）@l2+输出（s）@l）* λ2in（x）@ l .[x]l：：λ3out（u）@ l.1φ3232 2φ2 3φ2其思想是，位置l2处的节点可以通过执行inaction并将此令牌替换为'body' [ x ]中的每个x出现来消耗单个令牌我们对“身体”的具体形式不感兴趣[x][x ][x]@self，等等。要消耗的令牌可以源自位置11或13处的两个节点中的任一个。直观地说，很明显，它将取决于速率λ1和λ3，哪个令牌将首先被放置在节点l2，以及它将被消耗的速率λ2换句话说，在l1和l2之间存在同时，在l1处的选择构造中，记号s和t之间也存在为了说明这些不同的随机元素是如何相互作用的，以及我们在一段时间t后可能得到什么样的网络配置，我们首先必须枚举所有可达配置，如图1所示。34A. Di Pierro等人/理论计算机科学电子笔记128（2005）27ęęęęPo（t）@lPJs，p∈（σ·Q）（l）et=T[[t]]σpsσ·ęs：：λPrzps·p·λzs：：λPJ|出口，出口Po（t）@lPJAlberta，pn ∈（σ·Q）（l）et=T[[t]]1σ1p12s21 1σ1·ę1s：：λ1P波长：λ2P rzps2·p·λ1zs*λ1PJs*λ2P| out(et)1ę112ę221ę112ę22Pi（t）@lPJσs，p<$∈（σ·Q）（l）Po（et）@selfPJt[t]1σp11s2φp22σ·ęs：：λP|Przp1·ps·p2·λzs：：λPJ[et/T[[t]|PJę1 2ę1σ·ę2Pi（t）@lPJσs，p<$∈（σ·Q）（l）Po（et）@selfPJt[t]1σ1p112s21 12φp22σ1·ę1s：：λ1Ps：：λ2Przp1·ps2·p2·λ1zs ：：λ1PJ[et/T[[t]][商务英语*λ2PJ1ę112ę221ę11σ·ę2ę22Pr（t）@lPJσs，p<$∈（σ·Q）（l）Po（et）@selfPJt[t]1σp11s2φp22σ·ęs：：λP | Przp1·ps·p2·λzs：：λPJ[et/T[[t]]]的一种|PPr（t）@lPJę1Alberta，p2∈（σę• Q）（l）P1o（et）@selfσ·ęPJ2t[t]1σ1p112s21 12φp22σ1·ę1s：：λ1Ps：：λ2Przp1·ps2·p2·λ1zs ：：λ1PJ[et/T[[t]][商务英语*λ2P1ę112ę221ę11σ·ę2ę22Pe（Q）@LPJ∈s，p∈（σ·Q）（l）σpss：：λPrzps·p·λzs：：λPJ|QPe（Q）@lPJσs，p<$∈（σ·Q）（l）1σ1p12s21 1s：：λ1P波长：λ2P rzps2·p·λ1zs*λ1PJs*λ2P|Q1ę112ę221ę112ę22n（u）@selfσ1pPJsJ∈S s/=sJs：：λPrzp·λ zs：：λPJ[sJ/u]sJ：：λ无[sJ/self]·s：：λPrzpzs：：λPJę1ę1s：：λP|Przp·λ zs：：λPJ|PPA. Di Pierro等人/理论计算机科学电子笔记128（2005）2735ę1 2ę12表8全局连续时间结构语义36A. Di Pierro等人/理论计算机科学电子笔记128（2005）273λ13λ3BCBCBCBC1C（i） l 1：：λ1（lout（s）@l 2 + 2out（t）@l 2）l 2：：λ2 in（x）@l2。[x]l3：：λ3out（u）@l 2φ3 3φ φ（ii）l 1：：λ1 nil<$l 2：：λ2 in（x）@l 2. [x]|out（s）l 3：：λ3 out（u）@l 2φ φ φ（iii）l 1：：λ1 nil<$l 2：：λ2 in（x）@l 2. [x]|out（t）l 3：：λ3 out（u）@l 2φ φ φ（四）l 1：：λ1（1out（s）@l 2 +2out（t）@l 2）=l 2：：λ2 in（x）@l2。[x]|out（u）nil 3：：λ3 nilφ3 3φ φ（v）l1：：λ1nill 2：：λ2[s]l 3：：λ3out（u）@l 2φ φ φ（vi）l1：：λ1nill 2：：λ2[t]l 3：：λ3out（u）@l 2φ φ φ（vii）l1：：λ1（1out（s）@l 2+2out（t）@l 2）l 2：：λ2[u]l 3：：λ3nilφ3 3φ φ(viii)l 1：：λ1nil<$l 2：：λ2 in（x）@ l 2. [x] |out（s）|out（u）nil3：：λ3 nilφ φ φ(ix)l 1：：λ1nil<$l 2：：λ2 in（x）@ l 2. [x]|输出（t）|out（u）nil3：：λ3 nilφ φ φφ φφ φφ φφ φ图1.一、可达网络配置的枚举基于这个枚举，我们可以指定矩阵Q，它包含关于全局网络配置之间的转移率的所有信息，以及包含离散转移概率的矩阵P。 根据Q和P，我们可以直接构造图2中给出的矩阵T。0 −λ1B-λ31 12 11λ30 0 0 0 0 0 0 0 0CB0 −λ2−λ 30 0λ 20 0λ 30 0 0 0 0CBCB0 0 −λ2−λ30 0λ20 0 λ30 0 0 0CB000−λ1 − λ200λ21λB32λ10000 CCB0000−λ30000λ3000CB00000 −λ30000λ300CBT =BBB000000 −λ1000011λ1λC2 2C1CB000000−λ20B2λ20λ20CCB0000000−λ201λ201λ2CB2 2CB CB0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 00 0 0 0 0 0 0BB0000000000000 CCB@0000000000000 C一0000000000000图二. 组合转移率矩阵T如果我们指定λ1、λ2和λ3的具体值，我们可以计算出网络配置N（t）在未来任何时间t为N j的概率，如果我们从某个初始配置N i开始，为P（N（t）= N j|N（0）= N（i）=（exp（tT））ij。我们还可以看看长期行为，即如果我们等待（相对）长时间，网络会发生什么。对于λ1、λ2和λ 3的不同值，12（十）l1：：λ1零ǁl 2：：λ2 [s]|out（u）第3章：：λ3nilφ（Xi）l1：：λ1零ǁl 2：：λ2 [t]|out（u）第3章：：λ3nilφ（xii）l1：：λ1零ǁl 2：：λ2 [u]|out（s）第3章：：λ3nilφA. Di Pierro等人/理论计算机科学电子笔记128（2005）2737λ3我们得到不同的行为，如下面的例子。λ1= 1，λ2= 1，λ3= 1。 在这种情况下，所有节点都以大约相同的速度运行。我们以下列概率达到最后四种配置之一1P（N（1000）= N x|N（0）= N（i）= 61P（N（1000）= N Xi|N（0）= N（i）= 31P（N（1000）= N xii|N（0）= N（i）= 61P（N（1000）= N xiii|N（0）= N（i）= 3在任何其他配置中结束的概率（实际上）为零。λ1= 1010，λ2= 1，λ3= 10 −10。在这里，中间节点以正常速度运行，而第一个节点非常快，第三个节点非常慢。在这种情况下，我们以概率到达中间节点Nv和Nvi之一1P（N（1000）= N v|N（0）= N（i）= 32P（N（1000）= N vi|N（0）= N（i）= 3其他的概率是（间接地）零。我们没有达到最终配置的原因是第三个节点非常慢，它的令牌u在1000个时间步内没有到达中间节点。λ1= 1010，λ2= 1，λ3= 1。最后，我们看看第一个节点非常快而其他节点以正常速度运行的情况。最后的配置结果与第一种情况相同，但概率不同1P（N（1000）= N x|N（0）= N（i）= 41P（N（1000）= N Xi|N（0）= N（i）= 21P（N（1000）= N xii|N（0）= N（i）= 121P（N（1000）= N xiii|N（0）= N（i）= 6连续时间模型将真正的并发实现为几个transi，38A. Di Pierro等人/理论计算机科学电子笔记128（2005）27这些事情似乎是“平行”发生的。事实上，两个转换实际上永远不会在同一时刻发生，因为这种可能性为零。然而，在一个时间单元之后，我们可以观察到发生了两个或更多个转换。这使我们可以避免考虑然而，我们可以要求两个in中4结论我们已经提出了一种将概率引入协调语言的方法。我们的建议已经在KLAIM语言的背景下，我们介绍了在本地（或过程）级别和网络级别的概率概率在进程级别的自然作用是调度并行线程和决定选择操作符。我们使用速率来确定节点活跃的频率。该信息有助于网络更新的概率。本文介绍的KLAIM的概率版本与最近文献中提出的各种概率编程语言和概率过程演算密切相关。在这些方法中，我们也提到了离散时间方法-例如PCCS [8，12]，PCCP [7]等 随着连续时间的逼近-例如PEPA [10]，随机π演算[15]。性能分析的工作通常基于概率过程演算，例如Hillston本文提出的工作的长期目标之一是沿着类似的路线，在经典的程序分析的语义为基础的方法对性能分析的发展我们还旨在更密切地研究我们的工作与最近的概率验证和模型检查工作的关系，例如PRISM [13]和deAlfaro [4]。我们在这里考虑了一个基于泊松过程的模型，泊松过程是连续时间马尔可夫链的一些最简单的例子可以考虑更复杂的连续时间行为，但这可能需要比仅速率更多的参数来描述时间分布[1]。该语言还可以被扩展以便允许概率和速率的动态变化，即，允许取决于时间的速率和概率。最后两个扩展需要进一步的工作。A. Di Pierro等人/理论计算机科学电子笔记128（2005）2739引用[1] Bause，F.另外，Kritzinger，“随机Petri网-理论导论”，Vieweg Verlag，2002年，第二版。[2] Bergstra，J.，A. Ponse和S.Smolka，editors，[3] Bernardo，M.和R. Gorrieri，A tutorial on EMPA：A theory of concurrent processes withnondeterminism ， priorities ， probabilities and time ， Technical Report UBLCS-96-17 ，Department of Computer Science，University of Bologna（1997）.[4] de Alfaro，L.， 论文，斯坦福大学计算机科学系（1998年）。[5] 德尼古拉河，G. Ferrari和R. Pugliese，KLAIM：A kernel language for agents interactionand mobility，IEEE Transactions on Software Engineering 24（1998），pp. 315-330[6] Di Pierro，A.，C. Hankin和H. Wiklicky，Probably KLAIM，in：R. D. Nicola，G. Ferrari和G.Meredith，editors，Proceedings of Coordination 2004，number 2949 in Lecture Notes inComputer Science（2004）.119-134[7] Di Pierro ， A. 和 H. Wiklicky ， Quantitative observables and averages in ProbabilisticConcurrent Constraint Programming，in：New Trends in Constraints，number 1865 inLecture Notes in Computer Science（2000）.[8] Giacalone，A.，C.- C. Jou和S. Smolka，概率并发系统的代数推理，在：IFIP WG 2.2/2.3编程概念和方法工作会议论文集（1990年），pp. 443-458[9] Gollmann，D.，“Computer Security,” John Wiley[10] Hillston，J.，PEPA：Performance enhanced process algebra，Technical Report CSR-24-93，University of Edinburgh，Edinburgh，Scotland（1993）.[11] Hillston，J.，“A Compositional Approach to Performance Modelling,” Cambridge UniversityPress,[12] Jonsson，B.，W. Yi和K. Larsen，685[13] Kwiatkowska，M.，G. Norman和D.帕克，概率符号模型检验与PRISM：一种混合方法，在：J。P. Katoen和P.Stevens，editors，Proceedings of TACAS52比66[14] Norris ， J. ， “MarkovChains,”CambridgeSeriesinStatisticalandProbabilisticMathematics, Cambridge University Press, Cambridge,[15] Priami，C.，Stochasticπ-calculus，Computer Journal 38（1995），pp.578-589。[16] Tijms，H.C.的方法，