（基础数学专业论文）随机进程代数的等价性判定计算.pdf

摘要 随机进程代数( s p a ) 是一种功能与性能相结合的并发系统模型，是通过给 经典进程代数模型中的动作发生附加上一个随机变量值，来反映在系统的运行 中，动作出现的时间延迟规律而得到的模型。它既能够描述系统的功能，又能 够对系统运行的性能进行评价，很多涉及资源共享的系统，例如，大型计算、客 户一服务器结构、网络等都可以用这种随机模型作精确的形式化描述。随机进程 代数中应用最广泛的是马尔可夫进程代数，在马尔可夫进程代数中，动作出现 的随机延迟时间是满足指数分布的随机变量。本论文主要研究了马尔可夫随机 进程代数的各种操作语义模型，在这些语义模型下的等价性概念的定义，以及 对马尔可夫随机进程的等价性进行判定的计算算法。主要包括以下三方面的内 容： 1 马尔可夫链代数上的模拟等价判定。马尔可夫链代数是进程间只有时间 延迟转移的进程代数，连续时间马尔可夫链( c t m c ) 代数是并发系统性能评 价最早使用的模型。通过状态转移的马尔可夫链分析，可给出系统的性能指标 的刻画。在一个c t m c 代数模型上的互模拟等价关系是以状态间满足的转移概 率值为基础定义的，这和c t m c 上的聚集等价关系一致，所以给出了基于状态 的“聚集块”的等价块划分算法，并给出了算法的复杂度分析。 2 交互式马尔可夫链( i m c ) 代数上的等价性判定。交互式马尔可夫链代数 是通过正交结合经典的进程代数和连续时间马尔可夫链代数得到的随机进程代 数模型。本文研究了i m c 上的互模拟等价的计算，计算算法的主要思想是对动 作和概率转移分别进行划分细化计算，最终得到一个递减关系链的不动点，从 而得到互模拟等价。并在c t m c 模型的弱模拟等价定义的基础上提出了i m c 上 强( 弱) 模拟等价的概念，并且给出了判定模拟前序关系的计算算法，算法的主 要思想是通过求解一个线性方程组，判定两个状态的马尔可夫模拟关系，并去 掉所有不能进行模拟的状态对。 3 一般随机进程代数上的等价性判定。一般随机进程代数是指既有动作 随机进程代数的等价性判定计算 转移，又有带随机时间延迟的动作转移的进程代数。这种进程代数的一个 关键点是如何定义两个并发进程中同步马尔可夫动作转移的随机延迟分布 咖( a ，p ，p ，q ) ，不同的函数定义对应了不同的随机进程代数模型，我们研究了 ( a ，p ) = 札时的随机进程代数中的互模拟、模拟等价性概念的定义和判定算 法，这些算法是i m c 上各种判定算法的改进。即，对马尔可夫转移进行判定时， 要区分收敛状态和发散状态，同时要对每一个马尔可夫动作转移进行( 互) 模 拟判定。 关键词：随机进程代数( s p a ) ，互模拟等价，模拟等价，算法 a b s t r a c t s t o c h a s t i cp r o c e s s e sa l g e b r a s ( s p a ) a r ec o n c u r r e n ts y s t e mm o d e l sw i t hb o t h f u n c t i o n a ls p e c i f i c a t i o na n d p e r f o r m a n c ee v a l u a t i o n i ti sap r o c e s sa l g e b r aw h e r e a c t i o no c c u r r e n c e sm a yb es u b j e c tt oad e l a yt h a ti sd e t e r m i n e db yar a n d o m v a r i a b l e s p am a yf o r m a l l yb eu s e dt os p e c i f yt h eb e h a v i o ra 8w e l la se v a l u a t e t h ep e r f o r m a n c eo fas y s t e m ah t l g ec l a s so fr e s o u r c e - s h a r i n gs y s t e m s s u c h a sl a r g e - s c a l ec o m p u t e r s ，c h e n t - s e r v e ra r c h i t e c t u r e s ，n e t w o r k s c o na c c u r a t e l yb e d e s c r i b e db yu s i n gs u c hs t o c h a s t i cs p e c i f i c a t i o n f o r m a l i s m s m a r k o v i a np r o c e s s a l g e b r a sa r es t o c h a s t i cp r o c e s sa l g e b r a sw h e r ed e l a y sa r eg o v e r n e db ye x p o n e n - t i a ld i s t r i b u t i o n s ，w h i c hh a v eb e e n 稍d e l yu s e di nt h es p a i nt h i st h e s i s ，w e i n v e s t i g a t et h eo p e r a t i o n a ls e m a n t i c s ，n o t i o n so fe q u i v a l e n c ei ns t o c h a s t i cp r o - c e & qa l g e b r a ，a n dt h ea l g o r i t h m so fc o m p u t i n ge q u i v a l e n c ef o rd i f f e r e n tt y p e so f m a r k o v i a np r o c e s sa l g e b r a s w ef o c u so nt h ef o l l o w i n gt h r e et o p i c s ： 1 t h eb i s i m u l a t i o n sa n dp r o o r d e r sc o m p u t i n go nm a r k o v i a nc h a i na l g e b r a i nm a r k o v i a nc h a i na l g e b r a ，ap r o c e s si sd e l a y e df o ra ne x p o n e n t i a l l yd i s t r i b u t e d t i m e c o n t i n u o u st i m em a r k o v i a nc h a i n ( c t m c ) a l g e b r ai st h ee a r l i e s tp e r f o r - m a l c ee v a l u a t i o nm o d e l 8o fc o n c u r r e n c ys y s t e m st h a ta r eu s e d b ya n a l y s i n g s t a t e st r a n s i t i o no fm a r k o vc h a i n ，w ec a ng i v et h ep e r f o r m a n c ed e s c r i p t i o no fc o n - c u r r e n c ys y s t e m s o nac t m ca l g e b r am o d e l ，b i s i m u l a t i o ne q u i v a l e n c ei sd e f i n e d b a s e do nt h et r a n s l a t i n gr a t eb e t w e e ns t a t e s ，w h i c hi sc o i n c i d e sw i t hl u m p a b i f i t y , a ne l e m e n t a r yn o t i o nf o rt h ea g g r e g a t i o no fm a r k o vc h a i n s ，s ow eg i v eap a r t i t i o n r e f i n e m e n ta l g o r i t h m i cf o re q u i v a l e n c ec l a s s e sw h i c hi sa c t i o n b a s e dl u m p a b i l i t y e q u i v a l e n c e ，a n dg i v et h ec o m p l e x i t ya n a l y s i n go fo u ra l g o r i t h m s 2 t h eb i s i m u l a t i o n sa n dp r o o r d c r sc o m p u t i n go ni n t e r a c t i v em a r k o vc h a i n ( i m c ) a l g e b r a i n t e r a c t i v em a r k o vc h a i n s ，w h i c hc o m b i n ec l a s s i c a lp r o c e s sa l - g e b r am o d e l sw i t hc o n t i n u o u s - t i m em a r k o vc h a i n so r t h o g o n a l l y , a r es t o c h a s t i c p r o c e s s e sa l g e b r a sm o d e l s i nt h i st h e s i s ，w ei n v e s t i g a t et h ea l g o r i t h m so fb i s i m u - 随机进程代数的等价性判定计算 l a t i o ne q u i v a l e n c ec o m p u t i n go ni m c t h em a i ni d e a so fo u ra l g o r i t h m sa r ep a r - t i t i o nr e f i n e m e n ts a t e so fs y s t e m sb yu s i n ga c t i o na n dp r o b a b i l i t yt r a n s i t i o n s ，r e - s p e c t i v e l y , u n t i lt h ef i x e d - p o i n t so fs u c c e s s i v e l yf i n e rr e l a t i o n sa r er e a c h e d b a s e d o nt h ew e a ks i m u l a t i o nd e f i n i t i o no fc t m cm o d e l s ，w eg i v et h es t r o n g ( w e a k ) s i m u l a t i o ne q u i v a l e n c ed e f i n i t i o na n dc o m p u t i n ga l g o r i t h m sf o rt h e mo ni m c t h ec e n t e rp o i n t so fo u rm g o r i t h m sa r e ，b yr e s o l v i n gal i n e re q u a t i o n ss y s t e m ， r e m o v i n ga l ls t a t ep a i r sw h i c hh a v er i os i m u l a t i o nr e l a t i o ni ns y s t e m s 3 t h eb i s i m u l a t i o n sa n dp r o o r d e r sc o m p u t i n go ng e n e r a ls t o c h a s t i cp r o c e s s e s a l g e b r a ( s p a ) a ng e n e r a ls t o c h a s t i cp r o c e s s e sa l g e b r ac o n t a i n sa c t i o nt r a n s i - t i o u so fp r o c e s s e sa l g e b r aa n dm a r k o v i a na c t i o nt r a n s i t i o n s ，w h i c ha c t i o ni s t r a n s i t i o n e da f t e rad e l a yd e t e r m i n e db ya ne x p o n e n t i a ld i s t r i b u t i o nr a n d o m v a r i a b l e t h em a i nc h a r a c t e r i z a t i o no fs p ai 8h o wt oc o m p u t et h er e s u l t i n gr a t e ( a ，p ，p q ) i ne a s eo fs y n c h r o n i s a t i o no fm a r k o v i a na c t i o nt r a n s i t i o n s t h es p a m o d e l sd i f f e r sf r o mt h ed e f t n i t i o no f 西f u n c t i o n i nt h i st h e s i s ，w ei n v e s t i g a t e ( b i ) s r m u l a t i o ne q u i v a l e n c et h e n o t a t i o n so ns p am o d e sw h e r e j i ( a ，p ) = 札a n d g i v e st h ed e c i d i n ga l g o r i t h m sf o rt h e m t h e s ed e c i d i n ga l g o r i t h m sa r em o d i - l y i n ga l g o r i t h m sf r o mt h o s eo fi m c s ，i e w eh a v et os e p a r a t et i m e - c o n v e r g e n t f r o mt i m e - d i v e r g e n ts t a t e s ，a n dd e c i d eb i ( s i m u l l a t i o n ) f o re v e r ym a r k o v i a na c t i o n t r a n s i t i o n k e y w o r d s ：s t o c h a s t i cp r o c e s sa l g e b r a s ( s p a ) ，b i s i m u l a t i o ne q u i v a l e n c e ，s i r e u l a t i o ne q u i v a l e n c e ，a l g o r i t h m s 原创性声明 本人郑重声明：本人所呈交的学位论文，是在导师的指导下独立进行 研究所取得的成果。学位论文中凡引用他人已经发表或未发表的成果、 数据、观点等，均已明确注明出处。除文中已经注明引用的内容外，不 包含任何其他个人或集体已经发表或撰写过的科研成果。对本文的研究成 果做m 重要贡献的个人和集体，均己在文中以明确方式标明。 本声明的法律责任由本人承担。 论文作者签名：乏至塾筵 日 期：坦12 ：! ! 关于学位论文使用授权的声明 本人在导师指导下所完成的论文及相关的职务作品，知识产权归属兰 州大学。本人完全了解兰州大学有关保存、使用学位论文的规定，同意学 校保存或向国家有关部门或机构送交论文的纸质版和电子版，允许论文被 查阅和借阅；本人授权兰州大学可以将本学位论文的全部或部分内容编入 有关数据库进行检索，可以采用任何复制手段保存和汇编本学位论文。本 人离校后发表、使用学位论文或与该论文直接相关的学术论文或成果时， 第一署名单位仍然为兰州大学。 保密论文在解密后应遵守此规定。 论文作者签名：蝰塾量。导师签名： 第一章引言 1 1 研究背景 并发性( c o n c u r r e n c y ) 是现实生活中普遍存在的现象，它包括并行 性( p a r a l l e l ) 和分布性( d i s t r i b u t i o n ) 。事实上，现实中的绝大多数系统在 本质上都具有并行性和分布性，纯顺序的系统很少，我们称这样的系统为并发 系统( c o n c u r r e n ts y s t e m s ) 。例如并行计算机系统，计算机网络系统，移动通信 系统，通信协议，集成电路系统等等。研究并发系统的行为是最近二十多年理 论计算机科学中一个很重要的课题。由于并发系统的复杂性，对它的研究人们 通常采用的都是形式化方法( f o r m a lm e t h o d s ) 。形式化方法是基于严格的数学 框架的一种对系统进行刻画、分析和推理的方法。它通过对系统进行严格的语 法和语义的定义，使得系统的分析和推理能够精确化、数学化，从而保证系统 刻画和分析的正确性。 目前，在并发系统的理论研究领域，普遍采用的一种形式化方法是进程代 数( p r o c e s sa l g e b r a ) 方法。进程代数是一种抽象描述语言，它提供了一种用于 并发系统建模的严格的数学框架。在进程代数方法中，系统的行为用进程来描 述，进程由一个系统所能执行的动作所组成。这里，动作是一个抽象的概念， 它的含义不需要具体解释，用来表示一个抽象的活动或行为。例如，发送一条 消息，接收一条消息等等。因此，以进程代数为框架的并发系统分析都是建立 在动作这个基本概念上的。以动作为基础，进程代数用算子的形式定义了进程 问的各种相互作用。例如，前缀操作( ) 、顺序操作( ：) 、选择操作( + ) 、并发 操作( 0 ) 等，这样，进程代数就能以一种组合化的方式来描述复杂并发系统的 行为。这种组合化的系统描述方式将一个大系统看作很多小的子系统组合而 成，所以特别适合于描述大规模复杂并发系统，进程代数也因此成为了当今复 杂并发系统形式化刻画与分析的主要工具。比较著名的进程代数有r m i l n e r 提 出的c c s ( c a l c u l u so fc o m m u m c a t i o ns y s t e m s ) 1 ，2 1 ，c a r h o a r e 提出的 c s p ( c o m m u n i c a t i n gs e q u e n t i a lp r o c e s s e s ) 3 ，4 1 ，以及其后在这两种进程代 数的基础上由国际标准化组织( i s o ) 给出的标准化的l o t o s ( l a n g u a g eo f t e m p o r a lo r d e r i n gs p e c i f i c a t i o n s ) 【5 】。 2 随机进程代数的等价性判定计算 并发系统的研究可以从很多不同的角度进行，但所有的研究都集中在两方 面，一方面是研究如何对系统的功能特征进行刻画分析，另一方面是研究如何 对系统的性能特征进行刻画分析。 1 1 1 并发系统的功能分析 形式化方法的一个重要应用就是对并发系统功能方面的特性进行刻画、设 计和分析。所谓的功能特征主要指的是系统”能做什么“和”怎么做“，例如，一 个网络协议主要完成两个通信主体之间的信息交换，对它的功能特征进行分析 时，所关心的就是这个协议主要执行的动作以及这些动作之间的相互联系和作 用。这是最初并发系统的研究所主要关心的问题。这方面的研究导致了最早的 一批进程代数如c c s ，c s p 的产生。 进程代数作为并发系统的一种描述语言。其语义问题是它的核心内容。语 义研究的目的是建立一个精确的、无歧义的框架，来对并发系统进行推理。在 各种进程代数的语义研究中，我们可以将其划分为两大类：一类是所谓的交 织( i n t e r l e a v i n g ) 语义，一类是所谓的非交织( n o n i n t e r l e a v i n g ) 或真并发( t r u e c o n c u r r e n c y ) 语义。这两类语义划分的主要依据是对进程代数中并发算子的不 同解释。在交织语义下，两个进程并发执行的含义是两个进程的动作任意交叉 执行，从而一个系统的执行动作总是形成一个全序( t o t a l - o r d e r ) ，在进程代数 语言中，这种语义使得并发算子可以用顺序算子和选择算子来表示，如： aj ib = o ；b + 6 ；a 这种形式的转换在进程代数理论中称为展开律( e x p a n s i o nl a w ) ，它在某些 情况下可以使得我们对进程行为的推理更加方便。相反，真并发语义对并发 算子不是以两个进程的动作任意交叉执行来解释，而是保留了并发的真正含 义，即两个并发执行的动作可以是同时的，它们之间没有先后顺序关系，从 而在一个系统的执行中，其执行动作之间不存在一个全序关系，而是一个偏 序( p a r t i a l - o r d e r ) 关系。因此，这种语义又叫做偏序语义，在这种语言框架下， 进程代数语言中没有展开律。 1 1 2 并发系统的性能分析 并发系统性能分析( p e r f o r m a n c ea n a l y s i s ) 所关注的是并发系统性能上的特 征，例如时间特征、概率特征、随机特钲等。在传统的性能评价领域，人们已经 第一章引言3 建立了不少成熟的性能评价模型，如排队模型，马尔可夫模型等。通常这些性 能模型并不关心系统功能方面的特性，而仅仅是从性能方面来刻画系统，由此 就产生了将系统的功能分析与性能分析完全分割开来的两个不同的领域，两个 领域的研究者分别采用各自的模型和方法来研究各自领域的问题，导致了大量 相互无关的模型与分析技术的产生。 然而，随着现代系统复杂性的增加，尤其是并发系统的大量存在，现代复杂 系统的功能特性与性能特性之间的界限已经越来越模糊。很多系统性能方面的 特征与系统功能特征是密切相关的，因此单纯的功能模型和性能模型都无法有 效的对这样的复杂系统进行刻画和分析，这就促使人们将系统的功能分析与性 能分析结合在一起的研究工作，随机进程代数就是为解决这一问题而提出来的 形式化研究工具，它能够精确的模拟和评价系统功能和性能特性，对随机进程 代数的研究形成了最近十年来并发系统研究领域的另一个重点内容，很多集功 能和性能分析于一体的随机化模型被提了出来，成为研究这一交叉领域的有力 工具。 随机进程代数由经典的进程代数发展而来，其主要研究内容是语义模型的 定义，和等价概念的定义与判定，以及反映这些等价关系的方程公理系统的建 立，为了能够刻画系统的性能特征，在随机进程中增加了随机变化的时间信息。 增加时间信息后的随机进程模型既能描述系统的行为，又能反映某些特定的数 量上的性能特征，还能组合现有的性质以刻画更复杂的并发系统的行为特征。 并发系统的随机进程代数模型是进行系统性能评价的基础，但是随机进程 代数的刻画能力和附加进系统的随机变量的随机分布类型密切相关。科学研究 者做了一些尝试，企图将一般化的随机分布变量放入经典的进程代数中，但是 一般的随机变量放入进程代数后，都会面l 临相同的问题：会引导出难于处理的 随机进程，使得对系统的有效性能分析几乎成为不可能。然而，当我们将引入 到经典进程中的时间随机变量的分布类型限制为指数分布时，这样的情况就会 完全消失。 具有指数分布特性的随机进程模型是当代并发系统性能分析的基本模 型。它们能够对现实生活中很多现象，特别是对资源共享的并发系统能够进 行精确的描述。因为通过这样的模型可以较容易的得到一个连续时间马尔可 夫链( c t m c ) 模型，因此c t m c 上各种有效的数值计算方法能够用于并发 系统的性能分析中，这方面的研究代表有h e r z o g 6 1 的带时间的进程和性能评 4 随机进程代数的等价性判定计算 价( t i p p ) ，h i l l s t o n 7 ，8 】的性能评价进程代数( p e p a ) ，b u c l l i l o l z 【9 】的扩展的马 尔可夫进程代数( e m p a ) ，h e 咖m a l l s 【6 】的交互式马尔可夫链( i m c ) 等。 1 1 3 并发系统上的行为等价关系 用进程代数研究并发系统的另一个研究重点是进程的各种行为等 价( b e h a v i o u re q u i v a l e n c e ) 关系和前序( p r e o r d e r ) 关系。通常，等价和前 序关系是状态空间上的二元关系，但是这些二元关系可以用于两个进程间的行 为比较，因此，给出了一个进程能否正确的执行另一个进程的形式化描述方式。 直觉上，等价关系可以被看作是进程间的相等关系，即，等价的进程具有相同 的“行为”。前序关系是“单向”关系，它描述的是“行为和某进程相同”的概念。很 多的前序关系5 可以解释为：如果进程p 15p 2 当且仅当任何b 的行为，都是 岛可执行的行为。因此，p 2 所具有的安全性性质( 某些不好的行为不会出现) ， b 同样会具有前序关系曼的核= 三l l ! - 1 是一个等价关系，该等价关系将 所有满足相同安全性性质的进程视为“相等”进程。而且核等价关系是粗于互 模拟等价的，因此具有十分重要的研究价值。 如果等价关系关于进程代数中定义的算子具有同余性质，则该等价关系支 持并发系统结构设计的逐步细化方式。例如，在一个并行合成的系统设计模型 p 一l i q 中，我们可以用低层次的系统说明q 替代和它等价的高层次的 系统说明q ，得到的细化系统设计p ，一1 | q ”和p 等价，p 和p ，满足相 同的性质。因此用这种方法，可以将一个复杂的系统设计逐步的从高层次的说 明细化成具有相同功能且可以被实现的低层次描述。同样的，由于等价关系关 于抽象算子的同余性，在系统的性能分析中，可以用简化的状态空间s 替代 原来的状态空间，从而简化系统的分析过程。 作为自动化的系统行为和功能验证的基础，检查两个进程问是否存在某个 等价关系或前序关系的计算算法，或建立等价关系的商空间就显得特别重要。 对各种模型中等价关系的计算方法，人们已经做了很多的研究并且获得了判定 等价性问题的不少计算算法1 0 ，1 1 ，1 2 ，1 3 ，1 4 ，1 5 ，1 6 1 。 1 2 研究内容 本文系统的研究了马尔可夫随机进程代数上最重要的等价性概念一一互模 拟等价和模拟前序的定义，以及它们的判定算法，主要研究对象是交互式马尔 第一章引言 5 可夫链( i m c ) 和经典动作与时间延迟动作共存的随机进程代数，它们是既能用 于并发系统的功能刻画，同时又能用于并发系统的性能分析的模型，主要的研 究内容包括在交织语义下模拟和互模拟关系的定义，以及判断进程间这些关系 存在的计算算法。 1 2 1i m c 模型上模拟关系 等价关系在并发理论研究当中具有很重要的地位，它在不同的系统行为之 间建立了比较的依据。是很多其他研究工作的基础，例如状态空间的化简，同余 性问题等。在经典的并发系统理论当中，各种等价关系的概念都已经被建立起 来，这些等价关系可以从根本上划分为两类，一类是所谓的线性时间等价关系， 如迹等价。另一类是所谓的分支时间等价关系，如互模拟等价。对于传统的并 发系统的功能模型，这些等价关系主要用于比较两个不同的系统行为，并建立 各种代数系统的相等公理。随着现代系统复杂性的增加，系统的可靠性等性能 特征变得越来越重要，人们就把这些等价关系的概念引入到性能模型当中，建 立了概率系统模型、随机系统模型上的等价关系，如离散时间马尔可夫链和连 续时间马尔可夫链上的互模拟等价关系都被建立了起来，在这些性能模型上建 立的等价关系是进行系统状态空阃化简的一个重要手段。 本文在已有工作的基础上，将分支时间的模拟关系概念平移到i m c 模型上， 系统的研究了i m c 模型上的各种分支时间等价关系，主要研究了互模拟等价和 模拟关系概念的定义和它们的判定算法。由于i m c 模型具有行为分析和性能评 价两种功能，这些等价关系的定义和判定使得我们即可以对i m c 模型的特征进 行比较，还能简化性能分析模型的状态空间，即我们定义的等价关系综合了已 有的等价关系的功能，是现有的功能分析领域和性能评价领域分支时间等价关 系的推广，而给出的算法也是在现有的经典代数和马尔可夫链代数的( 互) 模 拟判定算法的基础上改进得到的。 1 2 2 随机进程代数上的等价性计算 本论文考虑的随机进程代数是既有经典动作转移，又有指数延迟时问的 动作转移的进程代数，并且假定在我们的随机进程代数中两个进程的同步马 尔可夫延迟率是两个同步动作的延迟率的乘积。它是i m c 模型的推广，我们 将i m c 模型上建立起来的( 互) 模拟等价概念推广到随机进程上，通过改进现 6 随机进程代数的等价性判定计算 有的判定模拟等价和模拟前序的算法，给出了s p a 上的互模拟和模拟的判定算 法。 1 2 3 相关工作 并发系统的等价关系是以进程代数为框架的并发理论研究中的一个核心问 题，它一方面是对并发系统的行为进行比较的一个准则，另一方面又是进程代 数中各种代数公理系统建立的基础。经典的并发系统的等价关系概念由m i l n e r 在他提出的c c s 中进行研究【1 ，2 】，随后r o bj v a ng l a b b e e k 将并发系统中的等 价概念进一步细化，得到了一个从线性时间到分支时间的等价关系谱1 7 ，1 8 1 a 由于分支时间等价关系，尤其是互模拟等价关系具有良好的性质，因此在各个 领域中都得到了广泛的研究。【1 9 ，2 0 最先将分支时间等价关系中的( 互) 模 拟等价概念引入到概率模型上，此后，各种概率并发模型和随机并发模型上 的互模拟概念都被提了出来【2 1 ，2 2 ，2 3 ，2 4 ，2 5 ，2 6 ，2 7 ，7 1 ，2 9 ，3 0 ，3 1 1 ，| 3 2 1 则 在这些工作的基础上将概率和随机模型上的各种分支时间关系统一起来，研 究了它们之间的相互联系及逻辑特征，得到了一个离散时间与连续时间马尔 可夫链上的分支时间等价关系谱。各种模型上的等价关系的判定算法也被给 出【l o ，1 1 ，1 2 ，1 3 ，1 4 ，1 5 ，1 6 ，2 3 ，2 2 1 。这些工作形成了本文进行随机进程代数上 分支时间等价关系研究的基础和动机。 1 3 本文组织 本文主要分为五部分，下面对每一部分内容做一简要说明：第一章：引言 本章对本论文的研究背景、意义、相关工作、主要研究内容等基本概念做了介 绍。 第二章：进程代数本章对本文涉及的经典进程代数中的基本概念做一简要 介绍，主要内容包括经典进程代数的语法定义，语义模型一一标记转移系统，互 模拟等价。重点介绍了互模拟判定的计算算法，这些算法是我们后续工作的基 础。 第三章：马尔可夫链代数本章介绍的是随机进程代数中最基本的概念。包 括概率，随机变量，分布函数及随机过程，其中重点介绍了马尔可夫链。作为广 泛应用的一个数学模型，马尔可夫链的理论已经比较丰富和成熟，交互式马尔 第一章引言 7 可夫链的性能分析基础就是基于马尔可夫链模型的，因此本章对马尔可夫链的 相关性质和等价计算算法做了重点介绍。 第四章：交互式马尔可夫进程代数本章介绍本论文的主要研究对象一一交 互式马尔可夫链，详细说明了该模拟的优点和我们进行研究的动机，交互式马 尔可夫链是传统的标记转移与连续时间马尔可夫链相结合的一个并发系统模 型，其中标记转移系统是经典进程代数的语义模型，而连续时间马尔可夫链则 是应用最为广泛的性能评价模型，在结合这两种模型的时候，i m c 采取了正交 结合的方式，最大程度的保持了原有两个模型的优点，尤其是它的同步组合操 作非常的简单和自然。使得i m c 成为一个优秀的可以组合化的性能评价模型。 本章对i m c 模型进行了形式刻画，定义了它的( 互) 模拟关系，并给出了判定 算法。这些工作是后续工作的基础。 第五章：随机进程代数本章在前面工作的基础上给出了s p a 上互模拟等 价和模拟前序关系。其中包括强( 互) 模拟和弱( 互) 模拟关系，我们将i m c 上 的这些分支时间等价关系的概念推广到s p a 上，分别定义了s p a 上的强( 互) 模拟和弱( 互) 模拟等价关系，并且给出了这些等价关系的计算判定算法。 第二章进程代数 并发理论是指计算机科学中并行和分布式系统理论，进程代数( p a ) 是并 发理论中的一个研究领域。进程代数的研究最早要追溯述到二十世纪七十年 代早期，主要目的是描述时间 3 3 1 。“进程代数( p r o c e s sa l g e b r a ) ”一词首先是 在1 9 8 2 年由b e r g s t r a 和k l o p 3 4 发明的。进程代数是范代数中的一种结构，它 满足特殊的公理集。首先，考虑“进程( p r o c e s s ) ”，它指系统的行为。系统是展 示行为的系统，特别是一个软件系统的执行、一个机器的动作，甚至一个任意 的动作。行为是一个软件系统执行的动作或事件的总和。这些动作或事件的执 行可能是定时的或随机的。通常，为了研究需要，我们只考虑“真实”行为的一 种抽象，而不考虑其它方面，而且，我们常常只注意行为被观察得到的结果，动 作则称为观察的单位。因此，动作被考虑为离散的，即，一个动作在某一时刻出 现，并且不同的动作在时间上被分离。所以，一个进程有时被称为一个离散事 件系统。“代数( a l g e b r a ) ”指用代数的或公理的方法讨论行为。所以，我们可以 说，进程代数是用代数的方法研究系统的行为的一门学科。 目前，进程代数是一种形式化的描述复杂系统的建模工具，是一种高层的 描述语言，是支持并发分布系统的组合描述和其性质的形式化证明的代数语言。 它以代数形式来描述模型，并为模型化系统定义了一套完整的语法和语义。 2 1 进程代数与标记转移系统 本节我们先简要介绍一下基本的进程代数理论，然后引入标记转移系统。 进程代数是一种抽象描述语言，它通过一种组合化方式来描述一个并发系统， 即，它将一个大的系统看作是由很多小的子系统构成的，每个子系统又可以由 更小的系统组合而成，通过进程代数提供的各种操作，我们可以将一个大系统 分解为更小的系统来刻画，大大降低系统的复杂度。因此，这种组合化的思想是 目前人们解决复杂系统问题的一个主要思路。例如，面向对象的程序设计思想， 基于组件的软件设计技术等等都是这一思想的具体体现。如第一章的引言中所 述，进程代数有很多具体的系统( 如c c s 、c s p 、l o t o s 等) ，我们在这里采 用的是一个简化的l o t o s 进程代数模型，它是作为开放系统互连模型( o s l ) 1 0 随机进程代数的等价性判定计算 的形式刻画语言由国际标准化组织( i s 0 ) 提出来的，本文我们只涉及l o t o s 的 基本语言部分，有关l o t o s 的完整介绍读者可以参考 5 ，3 5 】。 在进程代数框架下，并发系统是建立在动作这个基本概念上的，一个系 统( 通常被称为一个进程) 由它所能执行的动作组成，因此，在本文中我们 假设存在一个由所有可以观察的动作构成的集合d 6 8 。其中的动作我们用 a ，b ，c ，等小写字母来表示( 可能带上下标) ，另外还有一个外部不可见的动 作t r g o b s ，用于表示系统内部执行的动作。令a = o b s u 7 表示所有动作 的全集。 定义2 1 设a a ，a a ，v a r 表示一个进程变量的集合，o v a r 。一个基 本进程代数b p a 由以下语法产生 p ：= 0a pip 1 ；p 2p l + 恳f 且忆岛fp aizl 肛p 上面定义给出的实际上是进程代数作为一种形式刻画语言的语法构成，它 可以看成是由一个进程的集合及定义在其上的一些操作算子构成的一个代数系 统。我们先给出这些操作算子的直观含义如下： 0 代表中止进程，即不能执行任何动作的进程。 n p 是动作前缀，表示系统先执行动作a ，然后执行进程p 。 p 1 ；岛是顺序操作，表示系统先执行进程只的动作，p 1 成功结束后系统 接着执行进程p 2 。 县+ 恳是选择操作，其含义是系统要么执行进程只，要么执行进程p 2 ， 两者之间的选择是非确定的，即选择p l 或者易都是可能，具体执行起来 是依赖系统运行的环境的。这种选择的非确定性是并发系统的一个重要特 征，也是与传统顺序系统相比的一个重要区别特征。 p 1 忆p 2 是并发操作，也是进程代数中最重要的一个操作，它代表两个进 程只和恳的并发执行，其中集合a 中的动作是两个进程需要同时执行 的动作，即需要同步的动作。如果a = o ，则p 1 和岛不需要同步任何动 作，此时我们称p 1 与p 2 是异步并发执行的，并将f i 口简记为。另外，为 了书写方便，对于只有一个元素的集合a ，我们将省略掉花括号而直接用 该元素来表示该集合 第二章进程代数 p a 是隐藏操作，或者叫抽象操作，进程p a 的行为与p 类似。唯一的 不同是进程p a 中那些在集合a 中的动作都被看成内部动作( 通过改名 为7 - 1 ，即外部将不再可以观察到。 z 和肛p 是为了支持递归操作而引入的操作符，其中z 表示一个进程变 量，肛p 是递归表达式，其中变量z 可能在进程p 中出现形成一个递归 函数。我们称被递归算子p 限制的变量( 如肛p 中的z ) 为约束( b o u n d ) 变量，没有被递归算子限制的变量称为自由( f r e e ) 变量。自由变量可以 通过替换来实例化( i n s t a n t i a t e d ) 而约束变量则不受变量替换的影响，因 此约束变量的名字可以被认为是无关紧要的。一个进程表达式中的某项如 果没有自由变量，则我们称该项为闭项( c o s e d ) ，反之称为开项( o p e n ) 。 对于递归表达式，我们要求递归项是w e l l - g u a r d e d 的【3 6 1 ，这一条保证了 递归项的语义模型与它的指称函数的不动点相对应并且是唯一的。递归表 达式的引入使得进程代数的表达能力更加的强大，更适合描述一些特定的 系统。 我们假定，这些进程代数的操作算子如果没有用括号来表示优先级，则默 认按照以下的顺序结合( 优先级由高到低排列) ：，；，+ ，0 ，。 例2 1 以下是合法的进程代数表达式： ( 1 ) p 1 = a b 0 + b a 0 ( 2 ) 恳= o ( 6 0 + c o ) ( 3 ) 马= p l0 。岛 进程代数作为一种严格的形式化方法，除了要有严格的语法结构外，还需 要有严格定义的语义模型。进程代数的形式语义通常用一种称为结构化操作语 义( s t r u c t u r a lo p e r a t i o n a ls e m a n t i c s ，s o s ) 【3 7 】的方式给出，之所以这么叫是 因为它递归的在每个语法结构上定义了一个行为表达式的操作解释。s o s 采用 下面的表达方式： 前提1 a 前提2 a 燮呈( 条件) 结论 1 2 随机进程代数的等价性判定计算 表2 1 ：b p a 的结构化操作语义 称为一条规则，可以读做：如果条件成立的话，该规则可以应用，并且当 前提1 到前提n 都满足的时候，结论成立。其中，规则中的前提与结论都具有形 式p p ，表示进程p 可以执行动作a ，同时演变成进程p ，。表2 1 给出 了b p a 的结构化操作语义。其中p q x 表示将进程p 中所有进程变量茁的 出现都替换成进程0 得到的进程。 对于并发系统的行为刻而，标记转移系统( l a b e l e dt r a n s i t i o ns y s t e m s ，l t s ) 是 一种传统的广为人们接受的基于抽象状态机的状态转移方法。标记转移 系统首先分别由k e l l e | 3 8 1 和l i e nf 3 9 1 两人独立提出来的，但现在很多人认为 是p l o t k i n 首先提出的4 0 1 ，这可能是因为k e l l e r 和l i e n 当时提出的转移系统由状 第二章进程代数1 3 态和转移两个元组构成，而p l o t k i n 贝t 认为转移系统是由状态、转移和标记( 动 作) 三个元组构成，这更接近我们现在普遍采用的“标记转移系统”或“状态转 移系统”。目前转移系统已经向多方面扩展，对其名字有多种不同的称谓，但本 质上都是基于上述三位作者的思想。 由b p a 的操作语义我们很自然的可以得到一个标记转移系统，其中每个转 移都形如与，即上面带有一个动作标记，所以，i t s 是经典进程代数的操作 语义模型，它是在通常的状态转移图中