第二部分Petr网的动态质

上传人:痛*** 文档编号:148812738 上传时间:2022-09-05 格式:PPT 页数:23 大小:1.03MB
收藏 版权申诉 举报 下载
第二部分Petr网的动态质_第1页
第1页 / 共23页
第二部分Petr网的动态质_第2页
第2页 / 共23页
第二部分Petr网的动态质_第3页
第3页 / 共23页
资源描述:

《第二部分Petr网的动态质》由会员分享,可在线阅读,更多相关《第二部分Petr网的动态质(23页珍藏版)》请在装配图网上搜索。

1、第二部分 Petri网的动态性质提纲n网系统网系统(以原型以原型Petri网为模型网为模型)运行过程中的一些运行过程中的一些性质统称为动态性质性质统称为动态性质(dynamic properties)或行为性质或行为性质(behavioral properties)n这些性质同这些性质同Petri网所模拟的实际系统运行过程中网所模拟的实际系统运行过程中的某些方面的性质有密切的联系的某些方面的性质有密切的联系提纲n可达性可达性n有界性和安全性有界性和安全性n活性活性n公平性公平性n持续性持续性可达性n可达性是可达性是Petri网的最基本的动态性质,其余各种性质都要通过可达网的最基本的动态性质,其

2、余各种性质都要通过可达性来定义性来定义n定义定义2.1.设设PN=(P,T;F,M)为一个为一个Petri网。网。如果存在如果存在t T,使,使MtM,则称,则称M为从为从M直接可达的直接可达的如果存在变迁序列如果存在变迁序列t1,t2,t3,tk和标识序列和标识序列M1,M2,M3,Mk使得使得 Mt1M1t2M2,Mk-1 tkMk (2.1)则称则称Mk为从为从M可达的可达的从从M可达的一切标识的集合记为可达的一切标识的集合记为R(M),约定,约定M R(M)如果记变迁序列如果记变迁序列t1,t2,t3,tk为为,则,则(2.1)式也可记为式也可记为M Mk 可达性n设初始标识设初始标识

3、M0表示系统的初始状态,表示系统的初始状态,R(M0)给给出系统运行过程中可能出现的全部状态的集合。出系统运行过程中可能出现的全部状态的集合。n定义定义2.2.设设PN=(P,T;F,M0)为一个为一个Petri网网,M0为初始标识。为初始标识。PN的的可达标识集可达标识集R(M0)定义为定义为满足下面两条件的最小集合:满足下面两条件的最小集合:(1)M0 R(M0);(2)若)若M R(M0),且存在,且存在t T,使得,使得MtM,则则M R(M0)可达性n定理定理2.1.设设PN=(P,T;F,M0)为一个为一个Petri网,网,M0为初始标识。则:为初始标识。则:(1)对任意对任意M

4、R(M0),都有,都有R(M)R(M0);(2)对任意对任意M1,M2 R(M0),R(M1)=R(M2)当且当且仅当仅当M1 R(M2)且且M2 R(M1)。证:证:(1)由于由于M R(M0),所以,所以 M R(M):M R(M0),从而,从而R(M)R(M0)。同理可证同理可证(2)。可达性n定义定义2.3.设设PN=(P,T;F,M0)为一个为一个Petri网,网,M R(M0)。如果。如果 M R(M0),都有,都有M R(M),则,则称称M为为PN的一个的一个可返回标识可返回标识或一个或一个家态家态(home state)。)。n定义定义2.4.设设PN=(P,T;F,M0)为一

5、个为一个Petri网网。如果。如果M0是一个家态,则称是一个家态,则称PN为为可逆网系统可逆网系统(reversible net system),或称可回复系统。),或称可回复系统。网系统家态的存在是一个良好性质,在评测系统性能或在系统模拟过程中网系统家态的存在是一个良好性质,在评测系统性能或在系统模拟过程中具有非常关键的作用。具有非常关键的作用。可达性n推论推论2.1.设设PN=(P,T;F,M0)为一个为一个Petri网,网,M1,M2是是PN的家态,则的家态,则 R(M1)=R(M2)。证明:证明:因为因为M1,M2是是PN的家态,的家态,所以首先有所以首先有M1 R(M0),M2 R(

6、M0),进而进而M1 R(M2),M2 R(M1)。根据定理根据定理2.1(2),则有,则有R(M1)=R(M2)。有界性和安全性n定义定义2.4.设设PN=(P,T;F,M0)为一个为一个Petri网网,p P。若存在正整数。若存在正整数B,使得使得 M R(M0):M(p)B,则称库所则称库所p为为有界的有界的(bounded)。并称满足此条件的最小正整数并称满足此条件的最小正整数B为库所为库所p的界,记为的界,记为B(p)。即。即B(p)=minB|M R(M0):M(p)B 当当B(p)=1时,称库所时,称库所p为为安全的安全的(safe)。)。n定义定义2.5.设设PN=(P,T;F

7、,M0)为一个为一个Petri网网。如果每个。如果每个p P都是都是有界的,则称有界的,则称PN为为有界有界Petri网网。称。称 B(PN)=maxB(p)|p P为为PN的界。当的界。当B(PN)=1时,称时,称PN为为安全的安全的。有界性和安全性p1p2t1t2p4p6p5t3t4p3p0t0t5p1p2t1t2p4t3t4p3PetriPetri网的有界性(网的有界性(boundednessboundedness)反映)反映被模拟系统运行过程中对有关资源的容量要求被模拟系统运行过程中对有关资源的容量要求库所库所p p3 3无界无界其它库所的界为其它库所的界为1 1B(p1)=B(p2)

8、=B(p3)=2 其它库所界为其它库所界为1 1有界性和安全性n定理定理2.2.设设PN=(P,T;F,M0)为一个为一个Petri网网。R(M0)为有限集当且仅当为有限集当且仅当PN是有界的。是有界的。证:证:活性nPetri网活性(网活性(Liveness)概念的提出源于对实际系统运行中是否会出现死锁的探索)概念的提出源于对实际系统运行中是否会出现死锁的探索的需要。的需要。n定义定义2.6.设设PN=(P,T;F,M0)为一个为一个Petri网,网,M0为初始标识,为初始标识,t T。如果对任意。如果对任意M R(M0),都存在,都存在M R(M),使得,使得Mt,则称变迁,则称变迁t为为

9、活的活的。如果每个如果每个t T 都是活的,则称都是活的,则称PN为活的为活的Petri网。网。p1p2t1t2t3p1p2t1t2p4t3t4p32t1 1和和t t2 2是活的,是活的,t3是不活的是不活的不活的不活的活的活的活性n与实际系统中的无死锁概念更为接近的定义。与实际系统中的无死锁概念更为接近的定义。n定义定义2.7.设设PN=(P,T;F,M0)为一个为一个Petri网,网,如果对如果对M R(M0),使得使得 t T:Mt,则称,则称M为为PN的一个的一个死标识死标识(dead marking)。如果)。如果PN中不存在死标识,则称中不存在死标识,则称PN为为弱弱活的活的(w

10、eak live)或者)或者不死的不死的(non-dead)。)。n定理定理2.3.设设PN=(P,T;F,M0)为一个为一个Petri网。若网。若PN中有一个中有一个变迁是活的,则变迁是活的,则PN是弱活的。是弱活的。证:证:用反证法。假设用反证法。假设PN不是弱活的,则必存在一个死标识不是弱活的,则必存在一个死标识M R(M0),即即 t T:Mt。从而不存在。从而不存在M R(M),使得,使得Mt。即任一个变迁都不是活的,这同假设矛盾。即任一个变迁都不是活的,这同假设矛盾。活性p1p5t1t2p4t5t4p3t3p2t6PN是弱活的是弱活的,但不是活的,但不是活的(1,0,0,0,0)(

11、0,0,0,1,0)(0,0,1,0,0)(0,0,0,0,1)(0,1,0,0,0)t4t5t3t2t1t6活性n定义定义2.8.设设PN=(P,T;F,M0)为一个为一个Petri网,网,t T。若若 M R(M0):Mt,则称变迁,则称变迁t为为死的死的。如果一个如果一个PetriPetri网中没有死变迁,网中没有死变迁,那么它是活的吗?是弱活的吗?那么它是活的吗?是弱活的吗?p1p2t1t2t3t3是死变迁是死变迁公平性n在在Petri网中引入公平性(网中引入公平性(fairness)概念,旨在讨论网系统中两个变迁的)概念,旨在讨论网系统中两个变迁的发生之间的相互关系。这种关系反映被模

12、拟系统的各个部分在资源竞争中的发生之间的相互关系。这种关系反映被模拟系统的各个部分在资源竞争中的无饥饿性问题。无饥饿性问题。n定义定义2.9.设设PN=(P,T;F,M0)为一个为一个Petri网,网,M0为初始标识,为初始标识,t1,t2 T。如果存在正整数如果存在正整数k,使得,使得 M R(M0),T*:M都有都有#(,ti)=0#(,t3-i)k,i=1,2 则称变迁则称变迁t1和和t2处于处于公平关系公平关系。如果如果PN中任意两个变迁都处于公平关中任意两个变迁都处于公平关系,则称系,则称PN为为公平公平Petri网网。其中。其中#(,ti)表示在序列表示在序列中中ti的出现次数。的

13、出现次数。n如果如果PN中不存在可发生的无限变迁序列,则网系统总是公平的。中不存在可发生的无限变迁序列,则网系统总是公平的。公平性n定义定义2.10.设设PN=(P,T;F,M0)为一个为一个Petri网,网,M0为初始标识,为初始标识,t1,t2 T。如果。如果 M R(M0),都,都存在正整数存在正整数k,使得,使得 T*:M都有都有#(,ti)=0#(,t3-i)k,i=1,2 则称变迁则称变迁t1和和t2处于处于弱公平关系弱公平关系。如果如果PN中任意两个变迁都处于弱公平关系,则中任意两个变迁都处于弱公平关系,则称称PN为为弱公平弱公平Petri网网。p1t1t2p4t4p3p2t3t

14、2和和 t3是公平关是公平关系,也是弱公平系,也是弱公平关系关系t2和和 t3是弱公平是弱公平关系,但不是公关系,但不是公平关系平关系公平性n定理定理2.4.Petri网中变迁之间的公平关系是一种等价关系网中变迁之间的公平关系是一种等价关系 证:证:公平关系的自反性和对称性是显然的。下面证明其传递性。公平关系的自反性和对称性是显然的。下面证明其传递性。设设t1和和t2处于公平关系,即存在处于公平关系,即存在k1,使得,使得 M R(M0),T*:M都有都有#(,t1)=0#(,t2)k1#(,t2)=0#(,t1)k1 把把写成写成=0 t2 1 t2 2 t2 3 j-1 t2 j,j k1

15、.显然显然#(i,t2)=0 设设t2和和t3处于公平关系,即存在处于公平关系,即存在k2,使得,使得 M R(M0),T*:M都有都有#(,t2)=0#(,t3)k2#(,t3)=0#(,t2)k2 则由则由t2和和t3的公平关系可知的公平关系可知#(i,t3)k2,#(,t3)k2(j+1)k2(k1+1)k.其中其中k=maxk2(k1+1),k1(k2+1)即即#(,t1)=0#(,t3)k 同理可证同理可证#(,t3)=0#(,t1)k 所以,所以,t1和和t3处于公平关系。处于公平关系。持续性n定义定义2.11.设设PN=(P,T;F,M0)为一个为一个Petri网。如果对网。如果

16、对任意任意 M R(M0)和任意和任意t1,t2 T(t1 t2),有,有 (Mt1 Mt2M)Mt1 则称则称PN为为持续网系统持续网系统。n定理定理2.5.设设PN=(P,T;F,M0)为一个持续网系统。对于为一个持续网系统。对于任意任意 M R(M0),如果,如果 Mt1 且且M,#(,t1)=0,则,则有有Mt1 且且Mt1。证明:对证明:对的长度进行数学归纳。的长度进行数学归纳。持续性n定理定理2.6.设设N=(P,T;F)为一个纯网,那为一个纯网,那么么PN=(N,M0)是持续网系统的充要条件是持续网系统的充要条件 M R(M0),t1,t2 T(t1 t2),t1和和t2 在在M

17、不存在冲突。不存在冲突。持续性n定理定理2.7.若若N=(P,T;F)为一个为一个T-图,则对图,则对N的的任意初始标识任意初始标识M0,PN=(N,M0)都是持续网系都是持续网系统统。证明:已知证明:已知 M R(M0)和任意和任意t1,t2 T(t1 t2),有,有(Mt1 Mt2M)。并且并且 t1t2=,t1t2=证明证明Mt1。公平性实例n变迁序列:变迁序列:(1)(t1t2t3t4)*k=1(2)弱公平弱公平非公平,因为若选定某个非公平,因为若选定某个k,则只要让则只要让p1中中存储存储k+1个个token,就无法满足条件就无法满足条件定理2.5n(1)|sigma|=1,Mt1 且且 Mt2,则根据持续网的定义,则根据持续网的定义,Mt1t2且且Mt2t1(2)假设假设|sigma|且且Mt2,所以所以Mt2Msigma t3且且Mt2Mt1,根据归根据归纳假设,纳假设,M sigma t3t1,所以所以Mt1t2sigma t3同时,同时,Mt2sigma Mt3,而根据归纳假设,而根据归纳假设,Mt2sigma t1,所以所以Mt1,

展开阅读全文
温馨提示:
1: 本站所有资源如无特殊说明,都需要本地电脑安装OFFICE2007和PDF阅读器。图纸软件为CAD,CAXA,PROE,UG,SolidWorks等.压缩文件请下载最新的WinRAR软件解压。
2: 本站的文档不包含任何第三方提供的附件图纸等,如果需要附件,请联系上传者。文件的所有权益归上传用户所有。
3.本站RAR压缩包中若带图纸,网页内容里面会有图纸预览,若没有图纸预览就没有图纸。
4. 未经权益所有人同意不得将文件中的内容挪作商业或盈利用途。
5. 装配图网仅提供信息存储空间,仅对用户上传内容的表现方式做保护处理,对用户上传分享的文档内容本身不做任何修改或编辑,并不能对任何下载内容负责。
6. 下载文件中如有侵权或不适当内容,请与我们联系,我们立即纠正。
7. 本站不保证下载资源的准确性、安全性和完整性, 同时也不承担用户因使用这些下载资源对自己和他人造成任何形式的伤害或损失。
关于我们 - 网站声明 - 网站地图 - 资源地图 - 友情链接 - 网站客服 - 联系我们

copyright@ 2023-2025  zhuangpeitu.com 装配图网版权所有   联系电话:18123376007

备案号:ICP2024067431-1 川公网安备51140202000466号


本站为文档C2C交易模式,即用户上传的文档直接被用户下载,本站只是中间服务平台,本站所有文档下载所得的收益归上传人(含作者)所有。装配图网仅提供信息存储空间,仅对用户上传内容的表现方式做保护处理,对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私,请立即通知装配图网,我们立即给予删除!