（计算机软件与理论专业论文）petri网的模拟与验证.pdf

西华大学硕士学位论文 p e t r i 网的模拟与验证 计算机软件与理论专业 研究生叶剑虹指导教师柬文 p c t r i 网以其简捷、直观、潜在模拟能力强等特点被广泛用于离 散事件系统的模拟和分析中p e 耐网的主要特点包括t 并行、不确 定性、异步和分布描述能力和分析能力。活性( 1 j v c n e 哟、有界性 ( b o u n d e d a c s s ，又称为n - 安全性( n - s a 劬c s s ) 1 、家态( h 洲t a t e ) 、公 平性等性质是p c t r i 网的系统分析中最重要的几个性质。自p e 啊网的 概念形成以来，有关这些性质的研究就非常活跃。网人( 研究p e t d 网的人员自己使用这个称呼) 使用了许多分析方法：覆盖图技术、化 简和抽象、不变( i n v a i j 8 鹏) 技术、同步论以及结构分析技术等。对于 一般的有界p e t r i 网，只要一涉及网的性质，常常得到的算法都是n p 难的( 又称作状态空间爆炸) 。对于这些n p 问题，目前国内、国外的 理论研究基本停留在一般子类上的研究，尽管得到了许多好的结果， 但是由于子类的特殊性，使得所得结果缺乏很好的应用性。本人的工 作是基于一般网的一些性质的研究。 本人的研究是从模拟与验证两方面展开的。利用结构性分析理 论、化简技术、不变技术，对p c t r 网的模拟能力以及主要行为特征 进行了较为深入细致的研究，得到了一些新的结果。主要贡献包括： ( 1 ) 哲学家就餐问题可以看作当应用程序中包含并发线程的执 行时，处理共享资源合作的一个有代表性的问题，该问题是评价同步 方法的一个测试标准。本文利用p e 廿i 网下的c 疆系统来模拟和完善 哲学缘就餐问题井给出一个可以允许外部条件来加以有选择控制的 挫毗t c e 系统f 的条件事件集的发生可以在硬件中很容易的用 j 。关或者门电路来实现故此模拟具有很好的实际应用背景。 ( 2 ) 近十几年来，基于s 不变探讨p c 廿j 网系统结构的方法越来 西华大学硕士学位论文 越受到人们的关注，经典的s 不变的方法往往只用来对系统性质的 一种解释和判定，或者是对一些具体的范例的性质的一种定性、定量 分析，本文通过网的关联矩阵( i n c i d e n c em a t r i x ) 用s - 不变方法，讨论 了在般网系统下如何判定系统的结构活性。 ( 3 ) 从网的关联矩阵以及所定义的变迁发生序列的结构入手，对 结构活的网添加托肯o b k c n ) ，求解那些既能保证系统的启动，又使 得所需托肯资源嚣少的标识集( 我 门定义为最小标识集) 。并最终得到 了一个多项式时间内求解最小标识集的算法。 ( 4 ) 自控网是一种自修正系统，主要用于并发系统中的程序规范 以及工业控制中的数学建模等领域。由于自控网的s 不变、不变的 非线性，使得它无法直接套用p c t r i 网中一些已有的分析方法。有关 不变的讨论一般在具体系统中作具体分析，从而给出具体的解释。对 于一般网中s 不变呈现的特性在自控网上是否有条件的成立却鲜有 文献涉及，本文给出了一个自控网的s 不变呈现的线性特性相应的 定理。 关键词：p e t r i 网；模拟；验证；s 不变技术；结构技术 西华大学硕士学位论文 t h es i m u l a t i o na n d v e r i f y o fp e t r in e t s y e j i a n - h o n g ( c o m p u t e rs o f t w a r et h e o r e t i c s ) d i r e c t e db yp r o f s o n gw e n a b s t r a c t p e t r in e t si sw i d e l ya p p l i e di ns i m u l a t i o na n da n a l y s i sd i s c r e t ee v e n t s y s t e m sb e c a u s eo f i to w n ss i m p l e ，i n t u i t i o n i s t i c ，a n dt h es t r o n gp o w e ro f s i m u l a t i o n i th a sm a i n c h a r a c t e r i s t i c s , s u c h a s ，p a r a l l e l ， n o n d e t e r m i n a t i o n ，a s y n c h r o n i s ma n dt h ep o w e ro fd i s t r i b u t i n g a n d a n a l y s i s l i v e n e s s ，b o u n d n e s s ( a l w a y s c a l l n - s a f e n e s s ) ，h o m e - s t a t e ， j u s t i c ea r es o m eb a s i sp r o p e r t i e so fp e t r in e t s f r o mt h eb e g i n n i n go ft h e p e t r in e t s ，t h er e s e a r c ha b o u tt h e s ep r o p e r t i e si sa l w a y sa c t i v i t y t h e r e s e a r c h e ru s es o m em e t h o d st oa n a l y s i si t ，s u c ha s ，c o v e r a b f l i t yg r a p h s ， s i m p l ea n da b s t r a c t ，i n v a r i a n t s ，s y n c h r o n i z a t i o na n ds t r u c t u r a lt h e o r ya n d s oo i lt h ea l g o r i t h m sa b o u tb o u n d n e s sn e t si s a l w a y sn pp r o b l e m s ( a l w a y sc a l lt h ee x p l o s i v ei ns t a t es p a c e ) t h er e s e a r c h e so fo u rc o u n t y a n da b r o a da r ea l w a y sp a ym o r ea t t e n t i o nt ot h es u b - c l a s s e so np e t en e t s t h e yh a v eg i v e ns o m ew e l lr e s u l t s ，h o w e v e r ，t h er e s u l t s i ss h o r to f a p p l i c a t i o nb e c a u s eo ft h ep a r t i c u l a r i t yo fs u b c l a s s e so np e t r in e t s o u r m a i nw o r k sa r eb a s i so nt h eg e n e r a ln e t s s t a r t i n gf r o mt w oa s p e c t s ，s i m u l a t i o na n dv e r i f yb yt h es t r u c t u r a l a n a l y s et h e o r y , s i m p l ea n di n v a r i a n tt e c h n o l o g ya t eu s e di no n rw o r k s a n do u rr e s e a r c hi si n d e p t ha n dd e t a i l e dt ot h es i m u l a t i o nc a p a b i l i t ya n d t h em a i np r o p e r t i e so fp e t r in e t s w eh a v eh a ds o m en e wr e s u l t si n c l u d e a s f o l l o w s ： ( 1 ) t h ed i n i n gp h i l o s o p h e r sc a nb er e g a r d e da s ar e p r e s e n t a t i o n a l 西华大学硕士学位论文 p r o b l e mi ns h a r i n gr e s o u r c ec o o p e r a t i o n ，w h i c hp e r f o r mt h e 咖e n c g a p p l i c a t i o np r o g r a m i ti sat e s t i n gs t a n d a r di ne v a l u a t es y n c h r o n i z a t i o n m e t h o d o l o g i c a l f i r s t l y , i nt h ep a p e r , i ts i m u l a t e st h ed i n i n gp h i l o s o p h e r s b a s e do nc es y s t e m s ，w h i c hh a sv e r yw e l lp r a c t i c a l i t yb a c k g r o u n d ， b e c a u s eo fc o n d i t i o n sa n de v e n t ss e t si n c es y s t e m sc a na c h i e v e db y s w i t c ho rd o o rc i r c u i t t h r o u l g ht h es i m u l a t i o no fd i n i n gp h i l o s o p h e r s ， t h e r eh a v eap e r f e c tm o d e lw h i c hc a nb eo p t i o n a lc o n t r o l l e db ye x t e r i o r c o n d i t i o n s ( 2 ) r e c e n tt e ny e a r s ，m o r ea n dm o r ee x p e r tp a ya u e n t i o nt ot h e m e t h o db a s e do ns - i n v a r i a n t t h ec l a s s i c a ls - i n v a r i a n ta l w a y si su s e dt o e x p l a i na n dd e c i d et h ep r o p e r t i e so fs y s t e m ，o ra n a l y s es o m ec o n c r e t e p r o p e r t i e st h r o u g hd e t e r m i n et h en a t u r eo rq u a n t i t a t i v ea n a l y s i s t h ep a p e r s h o w sh o wt od e c i d et h es t r u c t u r a ll i v e n e s st ot h eg e n e r a ln e t sw i t ht h e i n c i d e n c em a t r i x ( 3 ) l i v e n e s si so n eo fb a s i cp r o p e r t i e so fp e t r in e t s ap o l y n o m i a l a l g o r i t h ma b o u tm i n i m a lm a r k i n go fs t r u c t u r a ll i v ep e t r in e t si sp r e s e n t e d , i ti sb a s e do ni n c i d e n c em a t r i xa n da n a l y s i st h es t r u c t u r eo ft r a n s i t i o n s s e q u e n c e ， ( 4 ) c y b e rn e t sa r es e l f - m o d i e y i n gn e t s i ti sa p p l i e di nc o n c u r r e n t p r o g r a ms p e c i f i c a t i o n ，t h em a t hm o d e l i n ga n di n d u s t r i a lc o n t r 0 1 t h e n o n l i n e a rn a t u r eo ft h es - i n v a r i a n t sa n dt - i n v a r i a n t so fs u c hn e t sk e e p s t h e ma w a yf r o ma p p l i c a t i o no fk n o w nm e t h o d s t h ea n a l y s i sm o s t l y c o d c e f i i so nc o n c r e t es y s t e m s h o w e v e r t h e r eh a v ef e wl i t e r a t u r eo n d i s c u s s i n g i t sl i n e a rn a t u r e o u ra p p r o a c he x t e n d st h es c o p e so ft h e i n v a r i a n t si nc y b e v n e t sa n dp r o p o s e sat h e o r e m k e yw o r d s ：p e t r in e t s ；s i m u l a t i o n ；v e r i f y ；s - i n v a r i a n t s ；s t m c t u r a lt h e o r y 西华大学硕士学位论文 第一章综述 1 1p e t r i 网理论的发展与应用 1 9 6 2 年由德国的c a r la d a mp e t r i 在他的博士论文 “k o m m u n i k a t i o n m i t a u t o m a t e n ”f 自动机通讯) 1 1 】中提出了p e t r i 网 的概念。p e t r i 阐述了一台计算机中的两个异步分支间的通讯理论 基础。并特别注意到事件之间因果关系的描述。他的论文是p e t r i 网理论研究发展的奠基石。 p e t f i 的论述引起了a d r ( 应用数据研究) 和麻省理工学院 ( m i 的m a c 理论研究小组的注意，并做了相关的研究工作，这 些研究主要展示了如何用p e t r i 网来模拟和分析具有并行分支的系 统，时至今日，p e t r i 网的应用和研究大大地扩展了，并形成了一 个专致于p e t r i 网的学术团体。其理论研究工作已经沿着两个方向 发展：其纵向发展为：条件事件( c 但) 网【”，位置变迁( p 门) 网1 3 j ， 高级网( h l n ，包括谓词变迁网1 4 1 ，有色网【5 , 6 】等1 。横向发展为： 无参数网到时间p e t r i 网【7 】，随机p e t r i 网【8 】 自然数标记个数到概 率标记个数等1 9 , 1 0 1 。 p e t r i 网是一种可用图形表示的组合模型，具有直观、易懂的 优点，对描述和分析并发现象有独到之处。它是一种适用于多种系 统的图形化、数学化建模工具，为描述和研究具有并行、异步、分 布式和随机性等特征的信息加工系统提供了强有力的手段。作为一 种图形化工具，可以把p e t r i 网看作与数据流图相似的通讯辅助方 法；作为一种数学化工具，它可以建立状态方程、代数方程和其他 描述系统行为的数学模型。经过4 0 多年的发展，它己成为描述物 理世界的异步并发现象并揭示其可计算规律的重要理论和成熟模 型。网人己证明了带抑制弧的p e t f i 网的模拟能力与图灵机( t u r i n g 西华大学硕士学位论文 m a c h i n e ) 等价。 p e t r i 网模拟以及数学分析方式已广泛应用于网络协议、人工 智能、形式语义、操作系统、并行编译、数据管理等计算机学科的 各个领域，2 1 世纪是一个网络化的时代。软件开发常常面对的是 信息处理系统的日益庞大和复杂化，越来越需要采用形式化的方法 进行软件开发，p e t r i 网是目前人们公认最有效的形式化软件开发 方法。对于网络环境，需要描述冲撞，冲突，并发，同步等基本特 征。以t u r i n g 机为模型，可以很好的描述冯诺依曼的机器，但是， 用t u r i n g 机描述网络环境就显得勉为其难了。p e t r i 网以它简洁， 直观，潜在的模拟能力强等特点被广泛地应用于离散事件系统的模 拟和分析中，p e t r i 网是动态系统的静态描述，它的主要特征包括： 并发、不确定性、异步和分步描述能力和分析能力。它在多处理器 计算机系统，计算机网络，交通控制系统，柔性制造等方面都有深 入、广泛的应用。发展p e t r i 网计算机是p e t r i 网模型的必然要求和 最终目标1 1 1 - 1 6 1 。 p e t r i 网的主要功能是为各种与并行系统有关的特性和问题提 供分析方法。利用p e t r i 网模型可以研究两类特性：依赖于初始状 态和独立于初始状态的特性1 1 7 。2 0 l 。前者是指状态行为特性，后者是 指状态结构特性。p e t r i 网可以分析的状态行为特征有可达性、有 界性、活性、活性单调性、家态( 可逆性) 、包容性和持续性等1 2 1 。矧。 一般情况下，p e t f i 网中变迁发生条件满足局部化公理，不用表示 系统中数据值或属性的具体变化或运算。在大型和复杂的系统模型 应用中，p e t r i 网的模型状态空间的规模将随着实际系统规模的扩 大而呈指数增长。因此，在实际应用中，常常不仅需要根据特定的 应用环境对网模型加以限制、修改或扩充，而且需要对p e t r i 网模 型进 j 二化简处理或结构分析等+ ”j 。 2 西华大学硕士学位论文 1 2 国内外关于p e t r i 网的模拟与性质的研究背景及成果 p e t r i 网不仅具有可视化的描述特点，同时还提供完善的分析 工具【3 7 4 1 】。高级p e t r i 网能够进一步提供简洁的系统描述，能够对 数据腔制流，触发条件动作，多样化的系统资源进行建模，其模 拟能力已经广泛用于形如工作流的模拟1 4 “、模糊p e t r i 网( f u z z y p e t r in e t s ) 1 4 ”、o b j e c tp e t r in e t 4 4 4 5 】等。但是随着p e t r i 网模型的描 述能力越强，性质分析就越困难。动态系统行为的复杂性导致p c t r i 网分析的高度复杂，这也影响了p e t f i 网在实际中的应用。为此， 国内外的网人一方面不断充实和发展p e t r i 网的抽象能力和描述能 力，从c e 网，经过p 厂r 网直到p 以网及有色网。另一方面，对 于复杂的系统，从基于p e t r i 网的结构分析理论入手【3 0 l ，研究网的 合成与分解理论。 从p c t r i 网问世以来，有关p e t r i 网的性质的研究就一直非常的 活跃。现已被广泛研究的p e t r i 网的性质包括活性、活性单调性、 有界性、s i p h o n 、陷阱( t r a p ) 、s - i n v a r i a n t 、t - i n v a r i a n t 等1 4 “。其 中活性和活性有界性是p e t r i 网分析中的重要行为特征，活性反映 了被描述系统的无死锁性，有界性保证了系统的无溢出。对于一般 的p e t r i 网系统，有关这些性质的判定非常困难，此类算法的复杂 度往往是指数级的，对于大一点的系统往往不实用。如何去寻找对 网的性质的判定的多项式时间的算法的各种研究一直非常活跃，其 探索过程也相当的艰苦。现已得到的对一些有限定的某些网类已经 证实其相应系统的活性和有界性的多项式判定算法确实存在。这些 算法涉及到p e t r i 网系统的活性与该网的不变特性密切相连，有几 个概念在基于结构分析技术的研究过程中一直扮演着重要的角色， s i p h o n 、陷阱( t r a p ) 和不变( 1 n v a r i a n t s ) 。s i p h o n 是这样一些库所集 合，它们一旦不被标识就一直不被标识，而陷阱一旦被标识将永远 标识，当一些库所集合既是s i p h o n 也是陷阱即是s 不变1 5 。 在研究p e t r i 网的性质过程中，探索的脚步首先从标识图 西华大学硕士学位论文 ( m a r k e dg r a p h ，简称m g ) 和状态机( s t a t em a c h i n e ，简称s m ) l s l l 开 始，并得到了比较理想的结果：s m 是活的当且仅当它是强联通且 被标识的【5 2 5 3 】；m g 是活的当且仅当其每个有向回路中至少有一 个被初始标识标识【5 4 1 。但m g 与s m 所代表的系统范围及其有限。 1 9 7 2 年，h a c k 在他的硕士论文中定义了自由选择网( f r e ec h o i c e n e t s ，简称f c 网1 ，f c 是包含m g 和s m 的子类。并给出了f c 网 活的充分必要条件：一个f c 网是活的当且仅当它的每个( 极小) 非 空s i p h o n 含有个被标识的陷阱l ”1 ( 在p e t r i 网的结构分析技术中， 称作为s t o 条件1 。一个f c 网是有界的当且仅当网被强连通的s 分支覆盖且每个s 分支的标识有限1 5 。一个活的且有界的f c 网满 足活性单调性1 5 7 1 。一个活的且安全的f c 网具有家态f 删。当网人把 f c 网的性质扩展到更大的子类：非对称选择网( a s y m m e t r i c c h o i c e n e t s ，简称a c 网1 ，在f c 网上成立的很多充分必要性质在a c 网 上不存在了。于是，至上世纪9 0 年代初期到目前，以a c 网为轴 心的的研究是结构分析技术的主要内容，其最新的研究成果参见文 【5 5 ，5 6 ，5 7 1 。 在这些研究过程中，活性，单调性等描述的是网的动态行为， 而结构活，同步距离岱y n c h r o n i cd i s t a n c e ) 4 2 蛐述的是网的静态结 构，其中联系动态行为和静态结构的桥梁是什么? 在研究过程中发 现，由于不变可以描述系统的动态行为；不变的求解可以通过网的 关联矩阵( i n c i d e n c em a t r i x ) 5 1 】，即，通过网的静态结构来实现。是 否不变即是我们所追求的桥梁? 在此猜想的激励下，我们对不变作 了一些较深入的研究。我们想知道，当仅知道网的静态结构，是否 可以判定网的结构活性；在结构活的基础上，如何去寻找那些初始 标识使得网所对应的系统是活的。同时，在探索过程中，有一类网 引起了我们极大的兴趣：自控n ( c y b e r - n e t s ) 。自控网是一种自修正 系统，主要用于并发系统中的程序规范以及工业控制中的数学建模 等领域。而p e t r i 网本身并不具有自修正性。要反映对象的这些特 征，常常需要加以许多的外部控制，导致整个网的模型显的更为复 4 西华大学硕士学位论文 杂。这正是自控网的长处所在。但是由于自控网的非线性，使得它 无法直接套用p c t r i 网中一些已有的分析方法。文 4 2 1 对自控网作 了深入的研究工作。但对于s 一不变的更一般的特性在自控网上如 何体现? 对自控网的性质判定又有何益处? 我们得到了较一般的 结论。 1 3 本文的主要内容 第二章主要介绍p e t r i 网的基本概念、符号和一些简单的性质； 在第三章，我们首先详细叙述了有关哲学家就餐问题在操作系统中 的意义以及如何利用c 但系统对哲学家就餐问题进行模拟，并进 一步解决共享资源的冲突问题及全局死锁问题，在此基础上进步 讨论如何解决共享资源的动态管理。另外，我们还将改用p r 厂r 系 统对哲学家就餐问题进行简单的模拟，同时比较两种系统进行模拟 的优劣。第四章讨论如何利用s 不变判定系统的结构活性，并给 出了相应的证明。更进一步的，在一个已判定活的网上如何去添加 托肯形成最小标识，以保证让一个系统活只需占用最少的托肯资 源。第五章对自控网的s 不变作了一些研究，并给出了一个在一 般网中s 不变呈现的线性特性在自控网上是否成立相应的定理。 西华大学硕士学位论文 第二章基本概念和术语 本章，我们将对以后各章节所需要用到的p e t r i 网的一些基本 概念和术语作简单的介绍，为了方便读者理解，我们还会给出一些 图例，详见 4 2 ，5 0 ，5 1 。 2 1p e t r i 网理论的基本概念 定义2 1 1 三元组n ；( p ，r ；f ) 是一个p e t r i 网( 简称网) ，当且 仅当p = 且，p 2 ，p 。) 是一个有限库所集( p l a c es e t ) ； t = “，t 2 ，t 。) 是一个有限变迁集( t r a n s i t i o ns e t ) ， 尸n7 1 = 妒，p u t * ；f 是n 上的流关系( f l o wr e l a t i o n ) ，其元素叫 孤。，( p 丁) u ( 丁p ) d o m ( f ) uc o d ( f ) = p u t ， d d 以f ) ；缸1 3 y ：( y ) ，) ，c o d ( f ) = 仁j 3 y ：( y ，x f ) ) 定义2 1 2 令是网，x ；p u t ，对于v x x 称 x ； y i ( y ，工) ，) 为x i ( p r e s o t ) ；z = yj ( 工，y ) e f 为x 的后置集( p o s t s e t ) x 酬y f i g 1 a ne x a m p l e f o re x p l a i n i n g y ) f n ( p x t ) 图1 伍y ) f n f p x t ) 图形表示 x 口_ o y f i g 2a ne x a m p l ef o re x p l a i n i n g ( x ，y ) efn ( t p ) 图2 ( x , y ) f n ( t p ) 图形表示 在p e t r i 网的图形表示中，库所用圆来表示，而变迁则用短的 线段或小方块来表示，库所和变迁之间是通过有向弧来连接的。 西华大学硕士学位论文 定义2 1 3 标j , 其( m a r k i n g ) 是函数m ：p m 。，ho = 0 ，1 ， 2 ，) ；三= ( n ，m o ) 被称作一个p e t r i 网系统，m o 称作网的初始标 识。 定义2 1 4 n 是一个p c t r i 网，k ：p m ，m = 1 ，2 ，) ， 称为网的容量函数( c a p a c i t yf u n c t i o n ) ；阿：f n 称为网上的 权函数。 定义2 1 5 n 是一个p e t r i 网，变迁t 在m 下使0 k ( e n a b l e d 又称 f i r a b l e ) 的条件是：白r ：m ( 力m f ) v p 日：m 佃) + 脚，力s j r 0 ) 一个在m 下使能的变迁t 发生，产生一个新的标识m ，m 由下 式给出v 口p ： 朋( p ) = 掰( p ) + ( f ，p )，f 一f m ( p ) 一w ( p ，f ) p e 1 一t m ( p ) 一w ( p ，f ) + w ( t ，p ) p tn f m ( p ) o t h e r w i s e 记作m t m ，称m 为肘的后继标$ 只( s u c c e s s o r ) 。 定义2 1 6 令是一个p e t r i 网， ( ，m 。) 的可达标识集记为 m 。，是满足下列两个条件的最小集：( 1 ) m 。e m 。，； ( 2 ) v m 【m o ，如果j f e t ，s t a l t m ，则m e m o 定义2 1 7 令是网，x = 尸u 丁，若v x x ：x n 工= 驴，则 为单纯l 网( p u r en e t ) 。若v x ，y x ：x = 了a z = y z = y ，则为 简单网( s i m p l en e t ) 。 定义2 1 8 冲突关系( c o n f l i c 0 若m 【f 1 肘b 2 ，但，m 【 f ，f 2 ) ，则f l 和t 2 在m 互相冲突， 冲突有的时候又称为选择( c h o i c e ) 和不确定( n o n d e t e r m i n i s m ) ，因为 它可以作为允许外部环境加以选择决策( d e c i s i o n ) 之处。 西华大学硕士学位论文 f i 9 3a nn e tw i t hc o n f l i c ti nt la n dt 2 图3 t l 和t 2 处存在冲突关系 定义2 1 9 冲撞关系( c o n t a c t ) 若有p e p ，m e m o 和f r 使得t m ，而且，m a t + 则 说在标识m 下p 处有冲撞。通过添加互补库所( c o m p l e m e n t a r y ) 往 往可以消除冲撞。 f i 9 4a nn e tw i t hc o n t a c ti n p 图4 p 处存在冲突关系 定义2 1 1 0 ( 1 ) 以库所集p 为序标集的列向量y ：p z 叫作 网n 的p 一向量，其中z 是整数集；( 2 ) 以变迁集丁为序标集的列 向量u ：t z 叫作网n 的r 一向量：( 3 ) 以p t 为序标集的n 阶矩阵c ：p x t z 叫作网n 的关联矩阵( i n c i d e n c e m a t r i x ) ，其矩 阵元素g ，t j ) = 暇t j ，月) 一h 协，0 ) 2 2p e t r i 网系统以及几个特殊的子类 定义2 2 1 条件事件系统( c o n d i t j o n 但v e ns y s t e m ) 简称c e 系 统，是通用网论，特别是同步论和网逻辑的基础。一个四元组 ( 尸，t ；f ，k ，w ，m ) 能构成c e 一系统的要求是：( 1 ) ( p ，t ；f ，k ，w ) 为简单有向网，称为的基网；( 2 ) v t t - d m x ，鸭m s t 3 ，i t ，m 2 ； 西华大学硕士学位论文 ( 3 )v p 丹m 1 ，m 2 l m s j p m 1 p q e m 2i gm l i t m 2 ( 4 ) v p e p ，v t 丁：x ( p ) ；1 , w ( t ，p ) ；1v w ( p ，f ) = 1 定义2 2 2 库所变迁系统( p 1 a c e m a s i t i o ns y s t e m ) 简称p 厂r 系 统，p 厂r 系统是c e 系统在库容量函数以及权值函数上的扩展。其 定义与c 厄系统类似，不同之处是： ( 1 ) v p g p , v t g t ：k ( p ) 苫i , w ( t , 力 l v w ( p , t ) ：- 1 ； ( 2 ) c e 系统的事件容许反向发生。 定义2 2 3 谓词变迁系统( p r e d i c a t e t r a n s i t i o ns y s t e m ) 简称p r t 系统。p r f r 系统区分托肯个体，给每个个体起个名字，以谓词描述 个体状态；故称之为谓词变迁系统。 = ( 尸，t ；f ，d ，v ，a p ，a r ，a f ，m 。) 称为谓词变迁系统的条件是： ( 1 ) ( p ，t ；f ) 为有向网，称为三的基网；( 2 ) d 为非空有限集，称为 的个体集；d 上有给定的运算符集q ：( 3 ) 矿是d 上的变量集： ( 4 ) a e ：p 一玎，其中9 g 是d 上的可变谓词集。对p p ，若4 p ) 为n 元谓词，就说p 是忍元谓词；( 5 ) a r ：t 一，d ，其中厂d 是d 的 公式集，对t e t ，a r ( f ) 只能含静态谓词和q 中的运算符；( 6 ) a ，：f 一九，其中丘是d 的符号和集。对n 元谓词p e p ，若 ( p ，f ) fv ( t ，p ) f ，则4 ( f ，p ) v a r ( p ，t ) 为n 元符号和。对于 t e t ，公式4 0 ) 中的自由变量必须是以t 为一端的有向弧上的自 由变量；( 7 ) m 。：p 一九，对n 元谓词p p ，m 。( p ) 是h 元符号和。 定义2 2 4 标识网( m a r k e dn e t s 、 令n = ( p ，丁；f ) 是一个p e t r i 网，称 ，为标识网，当且仅当 坳e p ，吖( p ) l = fn ：k ( p ) = * ；v p ，w ( p ) = 1 定义2 2 5 状态机( s t a t em a c h i n e ) ，标识图( m a r k e dg r a p h ) 令n = ( p ，丁；，) 是一个p e t r i 网。( 1 ) j v 称为状态机( 简称s m ) ， 当且仅当r ：卜h t + i = 1 ：( 2 ) n 称为标识图( 简称m g ) ，当且 仅当v p 尸：i 。p = i p i = l 。 9 西华大学硕士学位论文 铂羚 f i g sa ne x a m p l ef o re x p l a i n i n gs m o e f c ) a n dm g ( r i g h t ) 图5s m ( 左) 和m g ( 右) 的范例 定义2 2 6 自由选择网( f r e ec h o i c en e t ，简称f c 网) 令；( p ，r ；，) 是一个p e t r i 网称为自由选择网，当且仅 当对砌，p ：p ，如果p ：n p ；一庐，那么l p ：| - 正l = 1 ( 等价的定 义还有：v t 。，t ：，r ，n 。t 2 庐，那么f t ，jn l t 2f = 1 ) 定义2 2 7 非对称选择网( a s y m m e t r i cc h o i c en e t ，简称a c 网) 令；，r ；f ) 是个p e t r i 网，称为非对称选择网，当且 仅当对坳，p ：e p ，如果p in p i 庐，那么p ：p ；，或者p ；p i a f j 酯a ne x a m p l ef o re x p l a i n i n gf c ( 1 c f l ) a n da c ( r i g h t ) 图6f c ( 左) 和a c ( 右) 的范例 2 3p e t r i 网的结构和行为特征 p e t r i 网有许多的结构和行为的特征，在此，我们仅介绍与后 面章节所相关的那些结构和行为特征。 定义2 3 1 s i p h o n 和陷阱( t r a p ) 令= ( 尸，死f ) 是一个p e t f i 网，( 1 ) d p 是的一个 s i p h o n ( 陷阱) 当且仅当d d 。( d 。d ) ：( 2 ) d c p 是的一个极 1 0 西华大学硕士学位论文 小s i p h o n ( 陷阱) 当且仅当d 的任何非空子集都不是的s i p h o n ( 辂 阱1 。 性质2 3 1 【2 1 】令= ( 尸，f ；，) 是一个p e t r i 网，m 为其一个标识， d 是v 的一个s i p h o l l ，s 是的一个陷阱，则：( 1 ) 如果d 不被m 标识，那么v m 【m ，d 也不被m 标识：( 2 ) 如果s 被m 标 识，那么v m e l m ，s 也被m 标识；( 3 ) s i p h o n ( 陷阱) 的并仍然 是s i p h o n ( 陷阱1 。 定义2 3 2 活性( l i v e n e s s ) ，有界性( b o u n d e d n e s s ) = ( p ，t ；f ) 是一个p e t r i 网，= ( ，m 。) 是一个网系统。( 1 ) 变迁t t在 下是活的当且仅 当对 【坻，埘e mt s 埘p ) ；( 2 ) 是活的当且仅当r 中所有 的t 在中都是活的；( 3 ) 中库所p 是有界的，当且仅当存在一 个正整数k ，对v m e m o ，有肘( 功e 七；( 4 ) 是有界的，当且仅当 中所有库所都是有界的；( 5 ) 标识m 是的活标识，当且仅当 ( ，肘) 是活的；( 6 ) 是弱活的( d e a d l o c k - f r e e ) 当且仅当 v m e m o ，玉r ，s s m t ；( 7 ) z 是死的( d e a d l o c k ) 当且仅当 j m m 0 ，v f r ，s t ，m 【f 定义2 - 3 3 结构活( s t r u c t u r a ll i v e n e s s ) ，结构有界( s t r u c t u r a l b o u n d e d n e s s ) 设= ( p ，t ；f ) 是一个p e t r i 网。( 1 ) | v 是结构活的当且仅当存 在一个标识ms j ( ，m ) 是活的：( 2 ) n 是结构有界的当且仅当对 任意的标识吖，( n ，m ) 是有界的。 定义2 3 4 强连通( s t r o n g l yc o n n e c t e d 、 一个p e t r i 网n = ( 尸，t ；f ) 是强连通的当且仅当对 比，y 尸u t ，存在由z 到y 的有向路径。 定义2 3 5 家态( h o m es t a t e ) 令n ；( 尸，t ；f ) 是一个p e t r i 网，= ( ，m 。) 是一个网系统。 如果v m e i m 。，3 m o e m ，那么称m 。是该网系统的一个家态。 定义2 j 6s 不变( s i n v a r i a n t ) 、t - 不变( t - i n v a r i a n t ) 1 2 1 】 西华大学硕士学位论文 是一个p e t r i 网，c 是网的关联矩阵，j 是一个p 向量， ，是的一个s 不变当且仅当：c 7 ，- 0 ：j 是一个t 向量， 是的一个t 不变当且仅当：c - j ：0 ： 若i 0 ，i 是正的s 不变：n 被s 不变覆盖当且仅当任意的p 存在着，使得，( p ) 0 ； p e t f i 网的s 不变的线性组台仍然是s 不变。t - 不变的线性组 合仍然是t _ 不变。 西华大学硕士学位论文 第三章哲学家就餐问题的模拟与验证 p e t r i 网广泛应用于复杂系统的设计和分析中，如计算机系统、 分布式并行处理系统等。用p e t r i 网来表示并发、互斥、同步显得 直接、自然、精确。文 4 2 1 给出了哲学家就餐问题( 简称就餐问题) 在c e 系统下的模型：如何解决共享资源的冲突以及全局死锁。 文【4 2 】还进一步对模型作了化简，从活性定理来简单论证了所给出 的模型是有效的。 在讨论就餐问题的大多数文献中，就共享资源冲突及全局死锁 问题，都只给出些关于如何去解决死锁的方法( 包括死锁的预防、 避免以及检测和恢复) 【5 8 ，59 1 。利用p e t r i 网这个数学建模工具，我们 可以给出关于哲学家就餐问题的完善的模型。文 6 0 】给出了关于 p e t r i 网的合成化简，并对合成后的网的活性进行了讨论，这给我 们对所做模型的活性的验证提供良好的理论依据。 文【4 2 】给出了一个关于哲学家就餐问题的模型，但此模型无法 允许外部环境对系统资源的动态管理，在此模型的基础上，我们进 一步做了些工作，建立了一个允许外部环境动态参与就餐问题的模 型。利用改进后的模型，我们能够很好地模拟操作系统中的三种状 态：就绪状态、执行状态、等待状态。 3 1 本章相应的概念 定义