论文研究-着色Petri网的结构展开方法.pdf

所需积分/C币:15 2019-09-20 16:26:09 735KB .PDF
收藏 收藏
举报

论文研究-着色Petri网的结构展开方法.pdf,  为提升着色Petri网的设计分析与模型检验能力,讨论了着色Petri网的结构化展开技术.以着色Petri网的令牌单元和绑定单元为基元,通过对着色Petri网展开为普通Petri网的等价性证明,提出了基于着色Petri网关联矩阵和标准元语言的展开规则和规范化步骤.研究结果为着色Petri网到普通Petri网的自动转换过程和着色Petri网验
第2期 宋阿妮,等:着色 Petri网的结构展开方法 317 不同的库所区分不同的令牌,所以CPNs的令牌展开到OPNs后,失去了颜色,但占据了各自的库所.T从 CPNs中变迁的绑定单元展开而来,由CPNs中约束的不同触发条件和相应变迁组成CPNs中的每个变迁, 结合其绑定单元,展开为OPNs中的一个或多个变迁 OPNs中变迁的输入弧连接着其前集库所,输出弧连接后集库所.T的输入弧由CPNs中的令牌单元与 绑定单元的关系来确定.如果F(,t)<b>(c)≠0,意为CPNs中由b约束的变迁t触发,至少从p移走 一个令牌则在OPNs的P×T之间必有一条输入弧.同样由E(t.p)<b>(c)≠0来确定T的输出弧 OPNs的输入弧和输出弧的权重(N+),即弧权重W由CPNs中弧表达式颜色令牌数目来确定. 可以证明,这样定义的等价性满足自反、对称和传递等条件.CPNs和OPNs的标识、使能、触发序列 等是Pet网行为特性的重要体现.关于展开后二者的行为等价一致性,有如下定理山 定理1一个CPN展开得到等价的OPN记为OPN,有如下特性 ①触发序列一致性,Y-Y; ②触发序列下的可达标识一致生,M1,M2∈M,Y∈Y:M1Y>CPNM2M1Y>OPNM2 证明特性@:从基本概念和定义中知道,触发序列Y包含BEMS中所有的非空有限多重集,Y包含 TMs中所有的非空有限多重集.口定义4②给出的T与BE映射关系,所以Y=Y成立 特性②:Ptri网中M1Y> CPN M22可以表示为矩阵形式:M2=M1+ IM,Y,M1Y>OPNM2 表示为M2=M1+ IMCPN. Y.由关联矩阵定义有 IMCPN=E(T,P)-E(P,T),IMPN=W(7,P) W(P,⑦).而根据定义4③④给出的CPNs弧函数与OPNs弧权重映射关系,W(P,m分E(P,t)<b>(c) 而E(P,T)=E(P,c),(t,b),所以IMCP分 IM,从而M1Y>CPNM2台M1Y>oPNM2 3CPNs的展开规则 CPNs中丰富的颜色集类型、数据信息以及函数运算、操作等由标准化元语言10( meta language,ML 描述,是构成CPN的基本要素. CPN ML是一类强类型( strongly typed)的函数型编程语言( functional programming language),其中类型参数是构成CPNs库所、变迁和弧的颜色集、弧表达式、警卫函数的主体, 也是欧洲学者研究参数化网络和统Peti网( unified petri nets)理论的重要实例 根据ML语义,以“类”为核心概念,把库所的颜色属性即令牌单元,变迁绑定单元以及输入/输出弧函 数作为对象,从CPNs的关联矩阵出发获得完全一致的OPNs关联矩阵.关联矩阵的行对应为 Petri网的库 所节点,列对应为变迁节点,矩阵中的元素反映库所与变迁间的输入/输出弧约束关系.记CPNs的关联矩阵 为IMO,展开得到OPNs关联矩阵为IM°,每一个元素IM展开到OPNs里对应MO的一个分块矩阵 ⅠMQ 31CPNs展开规则 考虑CPNs建模中典型的变迁绑定单元及弧表达式情形,分类讨论CPNs的展开规则.为叙述方便,约 定CPNs的弧上除变量外其它表达式均写为函数形式,并记所讨论的CPNs的变迁在关联矩阵ⅠMC中的 列为i,记为T Case1ⅠM℃中变迁T对应列,其非零元素均为变量 规则1.若T2只有一个绑定单元,则展开为OPNs的一个同名变迁,构成分块矩阵IM的列 规则2.若变迁T的前、后集库所的颜色集均为一个基本形式颜色集,如int,real, string,unit,即前 后集库所的令牌单元只有一个,则展开到OPNs中为一个同名库所.若是复合颜色集,如 product, rccord, union,则展开到OPNs为多个库所,分别对应CPNs的每个令牌单元CPNs的库所令牌单元构成OPNs分 块矩阵ⅠMO的行 规则3.MC中变量IM9对应的分块矩阵IM9的元素值为弧(×P或P×T)的权重 示例:如图1,变迁起到传递变量的作用.图中h是颜色集 Height的变量,s是颜色集 Speed的变量, t是颜色集Time的变量.m1,m2为正整数,表示弧上传递的变量数目.库所按规则1,2展开.展开得到的 OPNs变迁T不变,弧上权重为相应的正整数 Case2IMC中变迁T对应列的元素,有定义为结构语句的函数,形如 if(A)then(13B) else if (C) then(n4D) 318 系统工程理论与实践 第31卷 P Meature colse product corset INT corset INT corset corset P n 图1Case1示例 else if(E)then(n5 F) *n73,m14,m5为正整数,表示输出变量个数,默认为1*/ 记该弧函数在IMC中的行是k,即库所Pk为T的前集或后集库所 规则4.i语句的条件A、C、E等确定T的绑定单元,构成分块短阵ⅠM的列 规则5.then的结果B、D、F等确定库所P的令牌单元,构成分块矩阵ⅠM的行 规则6.分块矩阵IM中列为A,行是B的元素值为73或-m3(值的正负与IM一致,由变迁的输 入/输出弧确定),即OPNs里,A对应的变迁和B对应的库所间有一条权重为m3的弧连接.同理,列为C行 是D的元素值为n4或-m4、列为E行是F的元素值为m5或-m5.分块矩阵IM中其它元素值为0,表 示相应的变迁与库所间没有任何关系,尤弧连接.特别地,当某条件下输出为“ empty',在CPNs中表示空, 则此条件所表示的情况不用展开 规则7.若弧函数调用的变量对应为库所P,其令牌单元为(P,1),(P,m2),…,(P,am),当7的绑定 单元涵盖了a1,2,…,am,则分块矩阵IM中该列元素都为m或-m(值的正负与IMC一致),当T的绑 定单元只涵盖部分变量,则分块矩阵IM该列中,只有行是这部分变量的元素值为或-m,其它为0. 示例:如图2.图中变迁T2的输出弧函数为FUNa,b),是一个i语句.CPN中f语句的条件 般来源于变迁的输入弧变量,构成相应的判断条件,从而决定了相应的绑定单元.then是相应条件下的输 出,它在ⅠMO中决定了弧连接的库所分块矩阵的值.根据规则4可知,变迁T2有3个绑定单元,分别为 (T2,a>b),(2,a<b,(T2,a=b).展开右边的OPNs为相应的3个变迁,CPNs中的函数关系通过OPN 中的不同变迁和输出库所来体现 fun se if then 4 else empty; colse 图2Case2示例 Case3MC中变迁T对应列的元素,有定义为cae语句的函数,形如: pat1→m6exp1 pat2→m7exp2 patn→m2expm *76,n7,m为正整数,表示输出变量个数,默认为1* 记该弧函数在IMC中的行是m,即库所Pn为T的前集或后集库所 第2期 宋阿妮,等:着色 Petri网的结构展开方法 319 规则8.case语句的条件patl,pat2,…patm确定变迁的绑定单元,构成分块矩阵IMOn的列 规则9.相应条件下的输出exp1,exp2,…, expn确定库所令牌单元,构成分块矩阵IM的行. 规则10.分块矩阵ⅠM9,中列为pat1,行是expl的元素值为n6或-m6,即OPNs里pat1对应的变 迁和cxp1对应的库所间有一条权重为n6的弧.同理,列为pat2行是cxp2的元素为m7或-n7,…,列为 pat行是 expn的元素等的值为n或-m.其它元素值为0,表示相应的变迁与库所间没有任何关系,无弧 连接 另外,;对应刎的元素为case函数调用的变量,其展廾规则与规则7相同. 示例:如图3.变迁⑦3的输出弧函数FUN(p)是case型函数,按照规则7,8,9,10,73有3个绑定单元 分别为(3,p=mam).(13,p=w0mm),(T3,p= child),因而展井到OPNs为3个变迁,case条件卜的输 出对应到相应的令牌单元 cosset =with >2 STRING( 图3Case3示例 Gase4IMC中变迁T对应列的元素,有运算函数、递归函数 规则11.T展开到OPNs中为一个同名变迁,表示运算过程 1;列的变量元素按规则7展开 示例:如图4.左边CPNs图中变迁T4的输出弧函数ged(a,b)定义为对两个整数a,b求最大公约数,运 算结果存放在库所P8中.CPNs中对数据的操作和运算能力非常强大,而OPNs不能做任何计算,且CPNs MIL里没有for或 while循环语句,而是用递归函数实现.因此,当CPNs中涉及到数值或递归运算时,展开 到OPNs中只是对数值运算的逻辑表达.图中右边OPNs中变迁T4表示求最大公约数运算,库所P8RES 表示计算结果,但没有真正的后台运算,只是一种逻辑表示 coSet =product* AB colse =INT corset =INT corset INT fun if =o then RES 图4Case4示例 常见的弧函数,包括布尔型的警卫函数( guard function),都可以由上述Case2-4表示.以上各种情形的 详细展开规则囊括了CPNs建模中典型的令牌单元、绑定单元以及弧函数约束情况.当变迁的前集或后集 库所有多个,即IMC中变迁所在的列元素有多个变量或多个函数,其处理方法与以上规则相同 32CPNs展开算法 基于CPNs展开规则,归纳CPNs展开到OPNs的算法步骤如下 320 系统工程理论与实践 第31卷 Step1构造CPNs的关联矩阵 IMC矩阵的行对应库所集合P,列对应变迁集合T,其中m Pl,m=·矩阵中的元素IMC=E(t1,p)-E(P,t),1≤≤m,1≤j≤m; Step2库所令牌单元展开.根据 Casel-4中的规则2,5,9,依次把每个库所按令牌单元等价展开为 OPNs的一个或多个库所,令”=C(m) for(i=1:t≤m;z+-) for(a=1;a≤;a++) ;a=(P2,Ca) /*其中,p∈P,ca∈C(p2)*/ Step3变迁绑定单元展开.根据 Case14中的规则1,4,8,11,依次把每个变迁按绑定单元展开为 OPNs的一个或多个变迁,令t=|B(t)| for(=1:;j≤m;++) for(x=1;x≤w;++) ;x=(t,ba)} /*其中,t∈T,bn∈B(t;)*/ step4构造一个新的矩阵IM.矩阵的行对应为库所集合P={1-1,…,1-n,D2_1,…,7,n,…,7m_1, nm2},列为变迁集合T={1-1,…,71_m,72-1,…,72,…,Zn-1,…,Znn}.以IMO每个库所和变迁下 标“”左边的数为准分块,构成一个分块矩阵,把每块看作IMO的一个元素,则IMO是m×n维矩阵, 它的每一块分别对应IMC的一个矩阵元素; Step5IM℃中元素展开.根据Case1-4中的规则3,6,7,10.将IMC中的元素,即库所与变迁间连 接弧上的变量或函数,展到MO的分块矩阵中:记IM的每一个分块矩阵为IM9,DM9=E(t,p)< )-E(p,t+)<b Step6根据I作出OPNs图 算法结束 4CPNs的结构展开实例 哲学家用餐问题叫是 Petri网理论分析与研究的典型案例,本节以其为例说明着色 Petri网的结构展 开方法的应用哲学家用餐的CPNs模型如图5(a)所示.为分析方便,这里考虑3位哲学家.图中库所 Think,Eat分别表示哲学家处于想、吃的状态,其颜色集为PH.UnCS表示没有用的筷子,颜色集为CS. 变迁 akers和 PutDowncs分别表示哲学家拿起和放下筷子 coset colset index with 1..3 PHallo var: i else if tnen 1 else if then 1 else empty; (a)哲学家用CPNs模型 (b)哲学家用餐CPNs模型关联矩阵 图5 根据第3节所给的展开规则和算法,对哲学家用餐的CPNs模型结构化展开: 1)由(PNs模型得到其关联矩阵如图5(b) 2)根据 Casel-4中的规则2,5,9,库所 Think和Eat的颜色集类型为PH,则其令牌单元为( Think/Eat, ph(1),( Think/Fot,mh(2),( Think/Fnt,mh(3),同理可得到库所UmCS的令牌单元 3)由 Case1-4中的规则1,4,8,1,是颜色集PH的变量,因此,变迁 Takes和 Put Downes的绑定 单元分别是:( akers/ Put Downes,p=mh(1),( Takes/ Put Ounce,p=ph(2),(akCS/ Put Downes, 第2期 宋阿妮,等:着色 Petri网的结构展开方法 321 p=ph(3) 4)以变迁绑定单元为列,库所令牌单元为行,构造新的矩阵IMO 5)对于ⅠMO的分块矩阵元素值,根据 Case14中的规则3,6,7,10,关联矩阵中元素IM2,IM2是函 数 chopsticks(),当函数的输入变量是ph(1),即相应的变迁绑定单元为( Takes/ Put Downes,p=ph(1) 则函数输出为cs(1)和cs(2),即库所UnC里的令牌单元为1cs(1)++1cs(2).所以,当|IM8和|IM4 为1时,相应地,M|、|M|和IM、IM9为1.同理,根据CPNs中关联矩阵里各元素对应的弧变 量或弧函数关系,得到OPNs关联矩阵的各个元素如图6 图6哲学家用餐OPNs模型关联矩阵 6)由这个关联矩阵我们就可以方便地得到哲学家用餐模型的OPN模型,如图7 图7哲学家用餐OPNs模型 为验证结构化展开得到的晢学家用餐OPNs模型与它的CPNs模型逻辑行为是一致的,给定初始标识 3个哲学家都处于“ Think”即“想”的状态,3只筷子都没有用(UnCS).对CPNs模型进行基于状态空间 的出现图( occurrence graph)叫分析,得到哲学家用餐CPNs模型的出现图如图8(a)所示.而对展开得到 的OPNs模型进行可达性( reachability graph)分析,得到可达图如图8(b)所示观察二者的状态转移情 况,以及引起状态变化的相应事件,它们是完全一致的结构化展开得到的哲学家用餐OPNs模型保持与原 CPNs模型完全一致的逻辑行为 由这个完全一致的哲学家用餐OPNs模型,就可以快捷地得出许多逻辑结构性质,如:S不变量、T不 变量、陷阱(Trap)与虹吸( Siphon)结构、冲突结构等,以及活性、家性、结构有界性等行为性质判定,为系 统进一步的逻辑行为分析和仿真评价提供方便和支持 322 系统工程理论与实践 第31卷 Think: Iph(1) Takecs_ph(3) Think_ph(1), Think__ph(2), ++1ph(2) ++1ph(3) 4Think: Iph(1)++I ph(2) Eat_ph(3) UnCS:Ics(1) 1:1Ea;ph(3 Put DounCs ph( 3) UnCs_cs(2) ++1Cs(2) UnCS: I cs(2) Think_ph(l) ++Ics(3) Take C8:p-pi(3)) Take Cs p/i2 Think ph(3 Think phl, Think ph(3), 3 Think: 1 ph(1)++lph(3) Eat ph(2) 3:3 1:1Far:1)ph(2) UnCS cs(). Put_ph(2) UnCs cs(2) UnCs_cs(1) UnCS:Ics(1) Pur DownS.R=ph(1) UnCs_cs(3) +PulDownCS ph(1) 27ink:1ph(2)++1ph(3) Takecs-ph d) Think_ph(2), Think_ph(3) 1:1 Eat: Iph(l) Eat_ph(1), UnCS: Ics(3) UnCs cs(3 (a)哲学家用餐CPNs模型出现图 (b)哲学家用餐OPNs模型可达图 图8 5结论 基于CPNs和OPNs的“折叠”与“展开”互逆恒等操作,面向工程应用,提出了完全一致和等价的 CPNs→OPNs展开规则,算法和步骤.获得的研究结果容易推广到更一般的 Petri网,如非纯网.本文提出 的展开算法清晰,步骤具体,可操作性强.通过该算法易于获得CPNs相应的OPNs关联矩阵,准确反映出 原CPNs仝局结构.方便地通过OPNs相关算法快速确定CPNs的结构性质和逻辑行为特征 类”是折叠与展开操作的核心概念.依据不同的分类标准,同一被折叠的OPNs,可能会有多个不同基 础网结构的CPNs.换句话说,CPNs的展开是非常复杂的,本文仅讨论了常见的实用CPNs展开规则.因此, 为了充分应用OPNs已有的分析理论与方法来充实和提高CPNs的结构化分析功能,推进CPNs技术的广 泛应用,还需要进一步研究、规范和提炼公认的“好”的展开规则和算法,为CPNs-OPNs展开的自动化程序 实现提供有效支持 参考文献 1 Jensen K Colored Petri Nets Basic Concepts, Analysis Methods and Practical Use Volume 1: Basic Concepts[M 2nd ed. Berlin: Springer, 1992. 2 Smith E. Principles of high-level net theory [J]. Lectures on Petri Nets I Basic Models, Lecture Notes in Computer Science,1998.1491:174210 B]郝克刚,葛玮.论高级 Petri网系统的等价谱系J计算机学报,1993,16(7):553558 Hao K G, Ge W. A spectrum of equivalent HL-Net systems J. Chinese J Computers, 1993, 16(7):553-558 4 Kordon F, Linard A, Paviot-Adet F Opt imized colored nets unfolding[C// International Conference on Formal Methods for Networked and Distributed Systems(FORTE'06). Paris: Springer, 2006: 339-355 5 Bashirov R, Kordon F, Lort H. Exploiting colored Petri nets to decide on permutation admissibility[J]. Acta Informatica. 2009. 46: 43-55 6 McMillan K l. Using unfolding to avoid the state explosion problem in the verification of asynchronous circuitsJ Lecture Notes in Computer Science, 1992, 663: 164-174 7 Kozura V E. Unfolding of coloured Petri nets[J]. Technical Report 80, A P Ershov Institute of Informatics ystems,2000:268278 8 Khomenko V, Koutny M. Branching processes of high-level Petri nets[J. Technical Report CS-TR-763, Depart- Inlent of Conputing Science, University of Newcastle, 2002: 458-472 9Januzaj V CPNunf: A tool for McMillan's unfolding of coloured Petri Nets[Cl//Eighth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the cPn Tools. Denmark: DAIMi PB 2007: 117--165 10 Paulson L c,ML程序设计教程M.柯韦,译.2版.北京:机械工业出版社,2005 Paulson L C. ML for the Working Programmer M. 2nd ed. Beijing: Chinese Machine Press, 2005 11 Jensen K, Christensen S, Kristensen L M. CPN Tools State Space ManualM. 2006

...展开详情
试读 8P 论文研究-着色Petri网的结构展开方法.pdf
立即下载 低至0.43元/次 身份认证VIP会员低至7折
抢沙发
一个资源只可评论一次,评论内容不能少于5个字
weixin_38744207 你的留言是对我莫大的支持
2019-09-20
  • 至尊王者

    成功上传501个资源即可获取
关注 私信 TA的资源
上传资源赚积分,得勋章
最新推荐
论文研究-着色Petri网的结构展开方法.pdf 15积分/C币 立即下载
1/8
论文研究-着色Petri网的结构展开方法.pdf第1页
论文研究-着色Petri网的结构展开方法.pdf第2页

试读结束, 可继续读1页

15积分/C币 立即下载 >