（计算机软件与理论专业论文）广反应系统中的行为同余问题研究.pdf

摘要 现在很多计算机系统是并发系统。并发系统固有的复杂性以及对并发性的本质 没有全面正确的认识使开发出的这类系统的可靠性与正确性无法得到保证。 为了解释并发性的本质并在此基础上提出开发并发系统的正确方法，r m i l n e r 于2 0 0 1 年提出t x 2 图反应系统( b i g r a p h i c a lr e a c t i v es y s t e m ，b r s ) 理论。在该模型中， 用双图表示系统状态，用反应规则表示系统的动态变化。b r s 是广反应系统( w i d e r e a c t i v es y s t e m 。w r s ) 的特例。为了在系统开发中能使用逐步精化方法及在分析系统行 为时能使用合成方法，希望由反应规则所导出的行为关系是同余的。r m i l n e r 证明 了有足够的r p o 的w r s 中双相似是同余的，进而证明了具体b r s 中双相似是同余的。 本文对三种常用的行为关系( 迹预序、弱双相似和失败预序) 在w r s 和其支持 商中以及具体b r s 中是否是同余的问题进行了研究。在j j l e i f e r 和r m i l n e r 提出 的理论基础上，证明了在有足够相对推出( r e l a t i v ep u s h o u t ，r p o ) 的w r s 及其支持 商中迹预序是同余，弱双相似和失败预序在其反应上下文子s 范畴中是同余：进而 得出在任何b r s 中迹预序是例余，弱双相似和失败预序在其反应上下文子s 范畴中 是同余的结论。 得到这些结果的证明过程为：证明w r s 的支持商是反应系统，从而得到函子反 应系统。在轨迹函子概念基础上证明了w r s 有足够的r p o 等价于由它生成的函子反 应系统有足够的r p o 。由于w r s 的标记变迁与函子反应系统中的不同，本文在j j l e i f e r 的同余性证明基础上，针对w r s 的标记变迁得到了w r s 的支持商中这些关系 的同余性结果。在证明w r s 的支持商与w r s 中的这些关系的对应性基础上，得到 w r s 中这些关系的同余性结果。再进一步得到了具体b r s 中这些关系的同余性结果。 硕士研究生鞠文广( 计算机软件与理论) 指导教师许日滨教授 关键词：并发理论双图反应系统同余双相似预序 b e h a v i o r a lc o n g r u e n c e sf o rw i d er e a c t i v es y s t e m s a b s t r a c t t h e r ea r em a n yc o n c u r r e n to n e sa m o n gc o m p u t e rs y s t e m sn o w a d a y s b e c a u s eo f t h ei n t r i n s i cc o m p l e x i t yo f c o n c u r r e n ts y s t e m s ，w eh a v en o ts t i l lk n o w nt h ee s s e n c eo f c o n c u r r e n c y s ot h er e l i a b i l i t ya n dc o r r e c t n e s so fs u c hs y s t e m sc a n n o tb ee n s u r e d i no r d e rt oa c c o u n tf o rt h ee s s e n c eo f c o n c u r r e n c ya n dt oa c h i e v et h em e t h o d o l o g y o f d e v e l o p i n gc o n c u r r e n ts y s t e m sc o r r e c t l y , r m i l n e ri n t r o d u c e dt h et h e o r yo fb i g r a p h i c a l r e a c t i v es y s t e m s ( b r s ) i n 2 0 0 1 i n t l l i s m o d e l f o rc o n c u r r e n c y ，as t a t e o f as y s t e m i sr e p r e s e n t e da sa b i g r a p h ，a n dat r a n s i t i o nb e t w e e ns t a t e si sr e p r e s e n t e da sar e a c t i o n r u l ef o rb i g r a p h s b r s sa r ei n s t a n c e so fw i d er e a c t i v es y s t e m s ( w r s ) i no r d e rt ou s e s t e p w i s er e f i n e m e n t si ns y s t e md e v e l o p m e n t sa n dc o m p o s i t i o n a la p p r o a c h e sw h e na n a l y - - z i n gs y s t e mb e h a v i o r , b e h a v i o r a lr e l a t i o n sa r er e q u i r e dt ob ec o n g r u e n c e s r m i l n e rh a s p r o v e dt h a tb i s i m i l a r i t yi na w r sw h i c hh a ss u f f i c i e n tr e l a t i v ep u s h o u t s ( r p o ) i sac o n g r u e n c e ，a n dh a sp r o v e df u r t h e rt h a ti ti na c o n c r e t eb r si sac o n g r u e n c e o nt h ef o u n d a t i o n so f j j l e i f e r sa n dr m i l n e r st h e o r y , a n du s i n gb a s i cm e t h o d s i nc a t e g o r yt h e o r y , t h i st h e s i sa n s w e r st h ef o l l o w i n gq u e s t i o n s ：w h e t h e rt h r e eu s u a l b e h a - v i o r a lr e l a t i o n s t r a c ep r e o r d e r ，w e a kb i s i m i l a r i t ya n df a i l u r ep r e o r d e r i naw r s ，i t s s u p p o r tq u o t i e n t , a n dac o n c r e t eb r s a r er e s p e c t i v e l yc o n g r u e n c e s t h et h e s i sf i r s tp r o v e st h a t ，i nt h es u p p o r tq u o t i e n to f aw r sw h i c hh a ss u f f i c i e n t r e l a t i v ep u s h o u t s ( r p o ) ，t r a c ep r e o r d e ri sac o n g r u e n c e ，a n dw e a kb i s i m i l a r i t ya n df a i l u r e p r e o r d e ra r eb o t hc o n g r u e n c e si ni t sr e a c t i v ec o n t e x ts u b - - s - c a t e g o r y a n do nt h ef o u n d a t i o no f t h e s ec o n c l u s i o n s ，t h et h e s i st h e np r o v e st h a t ，i naw r sw h i c hh a ss u f f i c i e n tr e l a - f i v ep u s h o u t s ( r p o ) ，t r a c ep r e o r d e ri sac o n g r u e n c e ，a n dw e a kb i s i m i l a r i t ya n df a i l u r e p r e o r d e ra r eb o t hc o n g r u e n c e si ni t sr e a c t i v ec o n t e x ts u b s c a t e g o r y a n df u r t h e r , i na n y b r s ，t r a c ep r e o r d e ri sp r o v e dt ob eac o n g r u e n c e ，a n dw e a kb i s i m i l a r i t ya n df a i l u r ep r e o r d e ra r eb o t hp r o v e dt ob ec o n g r u e n c e si ni t sr e a c t i v ec o n t e x ts u b s - - c a t e g o r y p o s t g r a d u a t es t u d e n t ：w e n - g u a n gj u ( c o m p u t e rs o f t w a r ea n dt h e o r y ) d i r e c t e db yp r o f y u e - b i nx u k e y w o r d s 。c o n c u r r e n c yt h e o r y ；b i g r a p h i e a lr e a c t i v es y s t e m ；c o n g r u e n c e ； b i s i m f l a r i t y ；p r e o r d e r 青岛大学硕士学位论文 学位论文独创性声明 本人声明，所呈交的学位论文系本人在导师指导下独立完成的研究成果。文中 依法引用他人的成果，均己做出明确标注或得到许可。论文内容未包含法律意义上 已属于他人的任何形式的研究成果，也不包含本人已用于其他学位申请的论文或成 果。 本人如违反上述声明，愿意承担由此引发的一切责任和后果。 论文作者签名：相研日期：婶广月柙 学位论文知识产权权属声明 本人在导师指导下所完成的学位论文及相关的职务作品，知识产权归属学校。 学校享有以任何方式发表、复制、公开阅览、借阅以及申请专利等权利。本人离校 后发表或使用学位论文或与该论文直接相关的学术论文或成果时，署名单位仍然为 青岛大学。 本学位论文属于： 保密口，在年解密后适用于本声明。 不保密囱。 ( 请在以上方框内打“4 ”) 日期： 碲5 月陴日 日期：硒7 年缃拍 ( 本声明的版权归青岛大学所有，未经许可，任何单位及任何个人不得擅自使用) 厂谚鬈 炙“ 帽 名 氰 、7 签 、 誊 名 作 登 文 鏖 论 导 青岛大学硕士学位论文 第1 章绪论 我们现在所使用的很多软件都是并发系统，比如现代操作系统u n i x 、w m d o w s 等都是并发系统。并发系统( c o n c u r r e n ts y s t e m s ) 是指由同时活动的相互作用的多个计 算主体( c o m p u t i n g a g e n t s ) 所构成的计算机系统，其中每个计算主体称为进程。并发 系统包括很多种系统体系结构，从紧耦合、大部分是同步的并行系统，到松耦合的、 存在大量异步的分布式系统。实现并发系统的计算机程序称为并发程序( c o n c u r r e n t p r o g r a m s ) 。并发性( c o n c 嘲c y ) 是指并发系统的基础特征【l j 在很多情况下顺序程序( s e q u e n t i f lp r o g r a m s ) 不能满足人们的需要，需使用并发 系统，例如需要并发操作系统。在开发并发系统的过程中，人们遇到了在开发顺序 程序时不曾遇到的各种问题，例如：进程间相互干扰( i n t e r f e r e n c e ) 、系统死锁、活锁 ( l i v e l o c k ) 、竞争条件( r a c ec o n d i t i o n s ) 等。这些问题使得在没有正确开发方法的情况 下很难保证所开发系统的可靠性，无法保证系统的正确性。导致这些问题的直接原 因是进程间经常有微妙的、预料不到的相互作用。此外，实际需要的很多并发系统 不应当终止( t 蛐t i o n ) ，例如操作系统、分布式数据库、w e b 服务器和控制系统等。 这与传统的顺序程序是不同的，这就使得正确性的传统观念不再适用，因为传统的 正确性观念依赖于把输入与程序终止时期望的输出相联系。像操作系统这样不应当 终止，并且通过与环境进行一系列交互的方式工作的并发系统被称为反应系统 ( r e a c t i v es y s t e m s ) 。 针对实践中出现的这些问题，人们就开展这方面的研究，这就逐渐形成了并发 理论( c o n c u r r e n c yt h e o r y ) 这个相对独立的研究领域。要解决这些问题，最主要的就是 要开发出能正确并且容易地解释这些现象的数学框架即并发模型与逻辑。并发理论 包括并发模型与逻辑，以及怎样应用这些并发模型或逻辑来正确地规约( s p e c i f y ) 、 验证( v e r i f y ) 与实现并发系统。这方面的研究可追溯到2 0 世纪6 0 年代1 2 , 3 】。并发理论 对开发出正确的复杂并发系统来说是一个必要条件。而现在需要开发的系统大多是 并发系统。而且，新一代计算范型是交互和网络化的，因此并发理论所起的作用会 遣来越大。 1 1 并发模型 为了刻画并发系统的基础特征，在过去四十年中研究者们提出了很多种并发性 的数学理论，例如p e t r i 网，进程代数( p r o c e s sa l g e b r a ) 、事件结构( e v e n ts t a t u r e s ) 、 时序逻辑( t e m p o r a il o g i c ) 等。在这些不同的研究流派中，有一点是一致的：反应性 的本质和不确定性特点决定了并发系统的模型不能是从输入到输出的映射。事实上， 这类系统与别的系统进行一系列的交互，因此表现出随时间变化的刺激反应关系模 式。所以并发模型不使用输入到输出的映射概念，而一般都是基于变化的原子性单 第1 章绪论 元的，例如变迁( t r a n s t i o n s ) 、动作( a c t i o n s ) 、事件( e v e n t s ) 等。它们是不可分的。再 由这些原子性单元来组成计算步，而整个计算就是由这些计算步组成的【4 1 。 对并发模型可按三个维度来分类： ( 1 ) 内涵( i n t e n s i o n a l i t y ) 与外延( e x t e n s i o n a l i t y ) 内涵模型着重于描述系统“做什么”，它可以显式地表示系统的状态。而外延模 型是基于外部观察者所看到的，它把状态信息抽象掉了。 内涵模型从状态和状态间变迁的角度来对系统建模。在标记变迁系统( l a b e l e d t r a n s i t i o ns y s t e m s ，l t s ) 【5 】中，每个标记变迁( l a b e l e dt r a n s i t i o n ) 都由变迁发生前后的两 个状态及表示与环境交互的原子动作( a t o m i ca c t i o n s ) 构成，原子动作在这里称为 标记( l a b e l ) 。进程代数，例如a c p ( a l g e b r af o rc o m m u n i c a t i n gp r o c e s s e s ) 嘲，c c s ( c f l c d u so f c o m m u n i c a t i n gs y s t e m s ) i t j 和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 e o c e s s e s ) 1 卅 等，就是从这个角度来对系统建模的。p e t r i 网 9 1 中状态可在不同位置间分布，这样 就扩展了这种状态变迁范型。 外延模型则先定义观察的概念，然后从观察的角度来表示系统。系统的行为就 用时间轴上动作( 或事件) 出现( 或发生) 的模式来描述。对系统最基本的一个观 察就是迹( t r a c e ) ，即系统所执行的原子动作序列【引。失败集( f a i l u es e t s ) t l o 】是对迹的 发展，它在迹信息的基础上加上了在系统执行了一个动作序列后它可以响应什么刺 激的信息。同步树( s y n c h r o n i z a t i o nt r e e ) i l l 把系统行为表示为一棵有向树，动作用边 来表示。事件结构【1 2 】用原子事件集上的偏序来表示并发性信息，用冲突关系( c o n f l i c t r e l a t i o n ) 来表示执行期间做出选择( c h o i c e ) 的信息。 ( 2 ) 交叉( i n t e r l e a v i n g ) 与真并发( t r u ec o n c u r r e n c y ) 交叉模型把并发性归结为不确定性，它把动作的并行执行理解为在它们的所有 串行化( s e q u e m i 目a i z a t i o n ) 间做出选择。这种观点可称为并发性的“单处理器”方法。 各种进程代数都使用了这种交叉语义。基于迹的模型和同步树模型也用这种交叉语 义来建模并发系统。 真并发模型把并发性作为本原概念，从事件间的因果关系这个角度来表示系统 的行为。p e t r i 网与事件结构就是以这种方式来表示并发性的。 ( 3 ) 分支时间( b r a n c h i n gt i m e ) 与线性时间( l i n e a rt i m e ) 线性时间模型从系统的可能运行集合这个角度来描述并发系统，而分支时间模 型则记下了不同的执行相互分离的选择点。迹是线性时间模型，而同步树与事件结 构是分支时间模型。 不同的模型用于不同的目的。外延模型对解释系统行为很有用，而内涵模型便 于自动分析，因为它们可产生( 有限) 状态机。分支时间语义对系统将来的行为建 模很有用，而线性时间语义可用来描述执行历史。 2 青岛大学硕士学位论文 传统的并发理论关注如何对选择与并发性进行建模，近年来的工作着重于在传 统理论基础上加上系统行为的其他方面的刻画，包括实时性、概率与安全性。 目前，并发理论有了一些比较成熟的模型与逻辑，例如进程代数、p e t r i 网和时 序逻辑等，并发系统的规约，设计与验证方法和工具在活跃地发展，许多有相当复 杂度的应用取得了成功。 尽管并发理论研究取得了很多成就，但现有的并发模型都有自身无法克服的缺 陷，还无法正确全面地解释并发性的本质，因此还没有适用于开发复杂的并发系统 的正确完善的方法。 1 2 行为等价与预序 在并发系统规约与验证方面，目前有两个研究流派：一个着重于并发逻辑( l o g i c f o rc o n c u r r e n c y ) 方法，强调使用逻辑公式来表示和验证所关心的性质；另一个则着 重于行为关系( b e h a v i o r a lr e l a t i o n s ) 的方法，使用高层系统作为低层系统的规约，通 过证明低层系统与高层系统之间是行为等价( f _ x l u v i l a n c e ) 或预序( p r e o r d e r ) 关系来说 明低层系统正确实现了规约。 基于行为关系的方法使用行为等价或预序把系统的规约与实现联系起来。等价 是指具有自反性、对称性和传递性的关系；预序是指具有自反性和传递性的关系。 等价是对称的预序，是预序的特例。 这种方法首先由m i l n 一1 在研究c c s 时提出，后来被各种进程代数【6 8 】普遍采 用。在这种方法中，系统用进程表示。规约与实现都用同一种进程描述语言表示为 进程，规约描述所期望的高层行为，而实现则描述表明高层行为是如何实现的低层 细节。在基于等价的方法中，证明实现是正确的就是要证明它的行为和规约的行为 完全相同，即证明这两个进程是等价的。在基于预序的方法中，要证明实现具有规 约所描述的行为，而且实现可以有规约所没有的“好”行为。 在基于行为关系的方法中，我们希望所使用的关系基于进程的可观察行为，因 为我们所关心的是并发系统的交互行为，而不是它内部的计算过程，只要系统能正 确地进行所有的交互而且不会做出不希望的交互，那么就认为系统是正确的。基于 系统行为的哪些方面是可观察的，人们提出很多种等价和预序。例如双模拟 ( b i s i m u l a t i o n ) 等价、观察( o b s e r v a t i o n ) 等价、迹预序和失败( f a i l u r e ) 预序。r j v a i l g l a b b o e k 【t 3 对各种行为等价及它们之间的关系进行了分析。 我们希望所使用的行为关系是同余( c o n g r u e n c e ) 的。直观上，关系是同余的就是 指它所在的形式体系中的所有语法构造都保持这种关系。这样证明两个大进程具有 某种关系就归结为证明它们的组件分别具有这种关系。因此同余是关系的一个很有 用的性质。 基于行为关系的方法要求对所期望的可观察行为给出完整的规约，预序比等价 第1 章绪论 的要求要宽松一些。系统验证中所使用的关系至少应是预序关系【1 4 1 。因为只有同余 的预序关系才支持对系统的逐步精化( s t e p - w i s er e f i n e m e n t ) 和分析系统行为的合成 方法。 早期的进程代数都以标记变迁的方式来刻画系统的状态变化，标记就是表示与 环境交互的原子动作，因此它就是对系统行为的一种观察。对各种行为预序和等价 关系是同余的证明，都是在标记变迁系统的基础上进行的。近年来的并发模型普遍 使用反应规则来定义系统的动态机制。反应规则就是无标记变迁，它仅刻画系统内 部的状态变化，反应的发生不需要与周围环境的交互。反应规则表达力很强并且很 简洁，但有局限性：它们不能像标记变迁那样自然地导出同余的行为等价和预序关 系。因此我们就希望由反应规则导出恰当的l t s ，再由l t s 导出同余的行为等价和预 序。为此，l e i f e r t l 5 1 提出相对推出( i k l a l i v ep u s h o u t , r e o ) 的范畴论概念，在此基础上 由反应规贝u ( r e a c t i o nr u l e ) 导出l t s ，并确保在有足够的r p o 存在的前提下由导出的 l t s 得到的几个行为关系( 强双模拟、弱双模拟、迹预序和失败预序) 是同余，这就 为得到有用的行为同余关系提供了统一的方法。 1 3 双图反应系统模型 为了解释并发性的本质，进而得出适用于开发复杂并发系统的正确完善的方法， m i l n e r 1 6 】在2 0 0 1 年提出双图反应系统( b i g r a p h i c a lr e a c t i v es y s t e m s ，b r s ) 模型。 它是一个可对移动计算建模的图形模型，既强调位置性，又强调连接性。双图( b i g r a p h ) 由两个正交的结构组成：描述计算节点的层次化位置关系的位置图( p l a c eg r a p h ) 和表 示节点问相互联系情况的链接图( l m kg r a p h ) 。双图的动态变化用双图反应规则表示 【1 7 1 8 , 1 9 。 为了提出b r s 模型，m i i n e r i l 7 】先提出广反应系统( w i d er e a c t i v es y s t e m s 。w i s ) 理论， 而b r s 是w r s 的特例。由于符合一定条件的两个双图可以合成，这样就可由小的双 图来形成大的双图。因此，如果b r s 模型中的行为关系是同余的，它就能支持对系 统的逐步精化和分析系统行为的合成方法，而这对于开发复杂并发系统是很重要的。 所以，他在i p o 与r p o 的基础上提出广反应系统中的标记变迁概念，进而证明了 在有所有反应前件r p o 的w r s 中双相似是同余；又在b r s 中为任意可交换方形构造 出r p o ，从而证明了在b r s 中双相似是同余。 为了表示疗演算的输入前缀( 它绑定了名字) ，o j e n s e n 与1 l m i l i l c r 【1 s 提出了绑 定双图( b i n d i n gb i g r a p h ) 这个概念。在绑定双图中，用位置来定义约束链接的范围 即约束链接局限于某一位置范围内。这样位置性与连接性就不是相互独立的。 k m i l n e 产0 】提出双图结构的公理体系，并证明它是完备的，这使得双图可以用 代数式来表示。t c d a m g a a r d 和l b i r k e d a l t 2 1 】在此基础上提出绑定双图的公理体系， 并证明该体系是完备的，这样我们就可以用代数式来表示任意一个双图。 4 青岛大学硕士学位论文 很多并发模型，比如p e t r i 网、c c s 、疗演算和移动环境演算( m o b i l e a m b i e n t ) 等，都可以用b r s 表示。1 l m i l n e r 瞄 用b r s 表示了条件事件p c t r i 网( c o n d i t i o n - o v e n t n e t s ) ，为其提供了行为语义，并根据点火规则用双图中的统一技术导出双相似等价 并确保它是同余，而且这个双相似等价与p e t r i 网的实验这个自然观念相一致。 1 l m i l n e r 谰b r s 表示了有限纯c c s ，并导出标记变迁系统和双相似同余，所得到 的标记变迁系统和双相似与c c s 中原来的理论符合得很好。o j e n s e n 与r m i l n e r t 哺，l 川 用b r s 表示了异步带演算，并表明所生成的标记与异步，r 演算中的标准标记相符合， 所导出的双相似也与标准双相似一致。m b u n d g a a r d 与v s a s s o n e 2 习用b r s 来表示了 类型多价石演算( t y p e dp o l y a d i c ，fc a l c u l u s ) ，并用r p o 理论导出该演算的标记变 迁系统，由这个标记变迁系统得出该演算的行为同余。因此b r s 可以认为是一个很 有希望的并发性元模型。 1 4 本文的工作 r m i l n e r l l _ 7 】证明了在有所有反应前件r p o 的w 塔中双相似是同余；还证明了在 任意b r s 中双相似都是同余。但关于经常使用的其他行为同余，例如弱双相似、迹 预序与失败预序等，还没有研究结果。 本文针对广反应系统和双图反应系统，研究了以下问题： ( 1 ) 在广反应系统中弱双相似、迹预序与失败预序是否是同余? ( 2 ) 在支持商广反应系统中这些关系是否是同余? ( 3 ) 在具体双图反应系统中这些关系是否是同余? 在j j l e i f e r 和r g i l n e r 提出的理论基础上，证明了在有足够r i o 的w r s 及 其支持商中迹预序是同余，弱双相似和失败预序在其反应上下文子s 范畴中是同余； 进而得出在任何b r s 中迹预序是同余，弱双相似和失败预序在其反应上下文子s 范 畴中是同余的结论。 得到这些结果的证明过程为：证明了w r s 的支持商是反应系统，从而得到函子 反应系统。在轨迹函子概念基础上证明了w r s 有足够的r p o 等价于由它生成的函子 反应系统有足够的r p o 。提出w r s 中的弱双相似、迹预序和失败预序的概念。由于 w r s 的标记变迁与函子反应系统中的不同，本文在l e i f e r 的同余证明基础上，针对 w r s 的标记变迁得到了w r s 的支持商中这些关系的同余性结果在证明w r s 的支持 商与w r s 中的这些关系的对应性基础上，得到w r s 中这些关系的同余性结果。再进 一步得到了具体b r s 中这些关系的同余性结果。 5 青岛大学硕士学位论文 第2 章预备知识 2 1 双图反应系统模型中的双图示例 为了对b r s 模型有一个直观认识，我们先来看一些双图示例。 例1 图2 1 用双图g 来表示楼宇环境内主体及计算机之间进行通信，比如说进行电 话会议。双图是b r s 中s 范畴的箭。图中用粗实线图形表示节点( n o d e ) ，用细实线表 示节点间的链接( l i n k ) ，最外边的大方形表示区域( r c g i o n ) ；a 、b 、c 、r 等大写字 母标明了节点的控制( c o n t r 0 1 ) ，也就是节点的种类；y , z 等小写字母表示名字 ( n a m e ) ，名字包括内部名和外部名。具体来说，这里b 表示楼房；r 表示房间； a 表示主体，比如可以是配备设备的人；c 表示计算机。图中用链接来表示主体及 计算机之间的通信；y 和z 是外部名，这种链接可以由别的双图使用。图中有两个 区域，它们可以离得任意远。双图的点( p o i n t ) 包括内部名与节点上的端口( p o r t ) ， 链接都是把点连起来，可以有分叉，链接分为边( e d g e ) 与外部名( o u t e r n a m e ) 两类。该双图可以有很多种变化，例如主体可以进入或离开房间，这些变化用双图 反应规则来表示。 r 。，* ，。_ 4 ，4 - ，+ ，。t _ - 。- 。，j ，_ 图2 1 表示楼字环境内通信的双图g 每个双图都有内部接n ( i n n e r f a c e ) 和外部接m ( o u t e r f a c e ) ，每个接1 3 ( i n t e r f a c e ) 都由两部分组成：区域( 地点) 数和外部( 内部) 名字集。其中，地点( s i t e ) 是指 双图中的空缺，如图2 2 中灰色方形所示，地点中可以放入其他双图中序号相同的 区域。图2 1 中的双图g 可表示为g 。 接口这个概念很重要，因为双图的合成运算要求参与合成的两个双图中一个的 内接口要与另一个的外接口相同，并且它们的支持不相交，即没有公共节点和公共 边。双图之间还有一种称为张量积固的运算。它要求参加运算的两个双图的支持不 相交，并且它们的内部名不相交，外部名也不相交。o 运算的实质就是把这两个双 图并列放置在一起从而形成新的双图。 f 口 ， j 图2 2 可“放入”其他双图的上下文双图f 图2 3f 与g 合成所得到的双图f o g 倒3 图2 4 用双图反应规则来表示c c s 中的一条反应规n - ( 工，+ 埘) i q + ) 一p i q ，其x p 表示卫式输出，x q 表示卫式输入。这条规则 表示通道x 上的通信。用双图五表示反应前件，用双图r 表示反应后件。双图反应 规则表示为( r ，r 。 图2 4 中使用了三个控制：s e n d 表示输出，g e t 表示输入，a l t 表示选择。这些 7 青岛大学硕士学位论文 控制都是被动控制，即它们内部不能发生反应。这条双图反应规则的含义是：在一 个大的双图中，反应前件r 能用反应后件丑来替换。图中有四个地点，也就是反应 规则的参数，分别用o 3 表示。并行算子i 在双图r 中直接用节点间的并列表 示，而选择算子+ 则是通过把各选择项并列放在控制为a l t 的节点中来实现，前 缀算子的表示方式为：把动作前缀后面的进程作为一个节点或地点放进该动作前缀 的节点中。 图2 4 用来表示c c s 的一条反应规则的双图反应规则 例4 图2 5 2 7 表示把双图g ( 如图2 5 ) 分解为它的两个成分：位置图( 如图2 6 ) 和链接图( 如图2 7 ) 。图中没有标出节点的控制。位置图是由有向树组成的森林， 每个区域内的节点组成了一棵树，根节点为区域。位置图去掉了双图中节点间的链 接信息，只表示节点间的位置层次关系。而链接图只表示节点和内部名之间的链接 信息，而不表示位置信息。 图2 5 一个双图g 由于双图是预范畴、良支持预范畴、s 范畴、广s 范畴，双图反应系统是广反应 系统【m ，因此上面这些例子有助于理解本文后面的相关内容。 8 第2 章预备知识 r l 厂y 8 00 l8 2 图2 6g 的位置图 y o暂l啦 x 0重l 图2 7g 的链接图 本章以下定义及未加证明的命题和定理均直接引鼽1 5 ，1 7 ，1 8 ，2 4 ，2 5 ，2 6 ，2 7 。 2 2 基本的范畴概念 定义2 1 范畴c 由 ( 1 ) 一族对象o b j c ， ( 2 ) 任意一对对象a ，曰对应一个集合c ( 4 ，b ) ，其元素称为箭或态射，使得当a 一彳 或b b 时，c ( a ，口) n c ：曰- d 。 组成，满足： ( 1 ) 复合运算律：若爿，b ，c o b j c ，c o ，b ) ，g c p ，c ) ，则存在唯一的 矿e c ( a ，c ) ，称为，与g 的复合。 ( 2 ) 结合律：若爿，b ，c ，d e o b j c ，f c ( a ，b ) ，g c ( b ，c ) ，h c ( c ，d ) ，则有 ( 盯) - ( h g ) f ( 3 ) 单位箭：每一个对象a ，存在一个箭i d 。c ，爿) 使得对任意的厂c ，功及 g c ( c ，4 ) 有f i d a - f ，吐g - g 范畴c 的箭的全体记做m o r e f c ( a ，b ) 记为，：一一曰，称a 是，的域，口为，的余域，记为d o m ，- a ， 彤- b 定义2 2 设a ，b 是范畴c 中的两个对象，：彳一口。若存在箭g ：口一彳使得 矿- i d 。，f g - i d 8 ，则称箭厂是同构。如果存在同构，：爿一曰则称对象彳与口是 同构的。 定义2 3 设c 和d 是范畴。函子f ：c d 由两个映射组成： o b j c o b j d ：彳i - - - f 似) ， ff t n m o r e - m o r d ：4 _ 彳一f ) _ ，o 9 青岛大学硕士学位论文 并且满足：f ( i d ) - i d ，“) ；若d o i n g - c o d 则f ( ) - f ( g ) f ( ，) 。 定义2 4 若函子f ：c d 是含入函数，则称c 是d 的子范畴。 命题2 1 函子保持同构。 2 3 基本的预范畴概念 定义2 5 预范畴c 与范畴的不同点在于：箭的合成不总有定义。具体来说，预范畴 c 由 ( 1 ) 一族对象o b j c ， ( 2 ) 任意一对对象a ，b 对应一个集合c ( a ，b ) ，其元素称为箭或态射，使得当a a 或b _ b 时，c b ) n c ( a ：曰一g 。 组成，满足下面条件： ( 1 ) 复合运算律：设a ，b ，c o b j c ，厂c ，b ) ，g e c ( a ，c ) 。若存在c o ，c ) ， 则盯是唯一的：g f 称为，与g 的复合。 ( 2 ) 结合律：若坛和盯有定义，则或者( h g ) f 和i l ( ) 都无定义，或者都有定义且 相等。 ( 3 ) 单位箭：每一个对象a ，存在一个箭i d a c ( a ，a ) 使得对任意的，c o ，b ) 及 g c ( c ，彳) 有f l d 一，i d a g g 。 明显地，范畴都是预范畴。 定义2 6 良支持预范畴c 是预范畴且满足下列属性： ( 1 ) c 有支持函数i i ，它把c 中的箭映射到一个集合，使有定义当且仅当 i g l n i f i i gf l d o m g c o d 。满足：若盯有定义，则i g f i - 4 9 i + i ，l a ( 2 ) 对任意箭，c ( i ，) 和任意入射p ，其中d o m p 习，i ，存在箭p ，c ( i ，- ，) ， 称为，通过p 的支持翻译，p 满足： p ( 矿) 一( p g x p ，) ， i d u l f 一， ( n 岛) ，p l ( p o ，) ， p ，。( p f i f l ) ，i p ，i p ( 1 厂i ) 注：用“+ ”表示集合的不交并，如i 盯i - i g i + i ，i 中的“+ ”。 命题2 2 在良支持预范畴，c 中，l i d ，i - 力。 i 正h ) l - 由定义2 5 ，i d ，。i d 有定义又由定义2 6 ，g i i d ，i n i i d ，h i d ，i 。- 命题2 3 在良支持预范畴- c 中，对任意入射p 都有p i d ，- l d ，。 定义2 7 严对称幺半群预范畴是在对象和箭上有部分张量积 的预范畴。o 有单位 对象s ，称为原点，使对所有对象，都有l 固e - - - - ，= ，。对，0 ，和j o ，有对称 同构r ，：， ，一， ，。张量和对称满足下列等式( 若等式两边都有定义) ： 第2 章预备知识 ( 1 ) ，o ( g 圆_ 1 1 ) 一( ， 暑) 固| l ， ( 2 ) ( 五。舅x 矗 g 。) 一五兀0 9 撂。， ( 3 ) n 。= i d ， ( 4 ) y s r ，- ，i d ，。， ( 5 ) ，j ( ， g ) 一 o ，) h j ， 对，：日一，和g ：，一k ( 6 ) ，m 口玉一( r l 五o i d s x i d f y s a r ) 命题2 4 在严对称幺半群预范畴中，j d ， ，- ，。 定义2 8s 范畴c 是严对称幺半群预范畴和良支持预范畴，并且满足下列属性： 对，：日一门铂g ：，一尺，若h o j 和i 固k 有定义且i ，l n l g l t 乃，则张量积 ， g ：日 ，一i k 有定义，而且l ， g l 掌| ，i + l g l ，p ( ， 占) 一p ， p g 2 4r p 0 与i p o 定义2 9 若对箭五：何一厶和五：日一，l ( 域都是h ) ，箭岛：厶一譬和g l ：，l 一置( 余 域都是k ) ，有g 。厶- 毋 ，就说( 岛，9 1 ) 是( 矗，1 ) 的约束。若( ，o ，正) 有约束，就说 它是相容的 定义2 1 0 设( 岛：，0 一足，最：- - - k ) 是( a ：日一，o ，五：日一) 的约束( ， ) 相对 ( g o ，9 1 ) 的约束( ，啊，1 1 ) 是指( ，啊) 是( 矗，五) 的约束且帆一g 。，帆- g l ，简称该三 元组为相对约束，如图2 8 。 ( ，o ，五) 相x q ( g 。，9 1 ) 的相对推出( r e l a t i v ep u s h o u t , r p o ) 是一个相对约束 魄，啊，h ) ，使对任何其他相对约束瓴，毛，七) 都有唯一的箭，使殖。- k o ，矾- 毛和 筋- h ，如图2 9 。 图2 8 相对约束图2 9 相对推出( r p o ) 定义2 1 1 若三元组魄：，o 一- ，h l ：i 一，i d j ) 是( 厶：日一，o ，五：日一) 相对于 魄， ) 的r 1 0 ，则称魄，啊) 是( 厶，五) 的幂等出( i d e m p u s h o u t , i p o ) 。 j j k i f c r 【2 】在范畴配置下证明了r p o 的性质，r m i i n c r 【1 】证明了在预范畴配置 1 1 青岛大学硕士学位论文 f 这些性质也成立。 命题2 5 ( 1 ) 在预范畴。c 中，若( 兀， ) 相对于皓。，9 1 ) 的r f o 存在，则在同构