SML语义检验的着色Petri网展开算法
2018-06-30廖晶静
廖晶静
以逻辑事件结构为主体架构的大型集成系统广泛采用Petri网对系统进行建模分析,主要是因为Petri网理论在静态分析和动态分析方面均有其他大多工具无法比拟的特色:系统逻辑结构分析和系统动态行为分析方法.特别是因为由Petri网理论的结构化分析方法获得的系统逻辑事件性能分析结果和系统的初始状态无关,对认识和解析大型复杂工程系统的全局结构化行为特性具有重要的指导意义.
普通Petri网在大型工程系统应用受限是由于其规模呈指数增长带来的模型规模爆炸的问题.为解决这一问题,1981年K.Jensen教授在其博士论文中首次提出着色Petri网(Colored Petri Nets,CPN)[1].着色Petri网以采用标准元语言(SML)、数据类和层次建模技术为特征,精确而简洁的系统描述,较普通Petri网工程应用性更强,更适用于大型工程系统的建模,成为目前被广泛应用于工程系统结构设计的主要的可视化建模仿真分析工具[2−4].
但是,由于CPN建模引用了SML语言,由此造成基于CPN关联矩阵的系统结构分析成为着色Petri网工程系统应用中至今难以逾越的难题.为了使着色Petri网具备与普通Petri网一样功效的结构分析能力,首先需要解决的问题是着色Petri网的恒等展开(Unfolding).
1992年,K.Jensen就给出了CPN与普通Petri网(OPN)等价性证明,但是这样的证明只停留在概念层面上,无法实际执行.同样,文献[5]研究了高级Petri网与普通Petri网的联系,应用商(Quotient)网的概念,也只是在理论上说明了普通Petri网的不变量和可达性树分析在着色网中的等价实现.而文献[6]提出的CPN展开技术只能在某一类所谓结构“好”(Well Formed)的颜色集中应用.文献[7]则从工程系统应用出发,提出了CPN到OPN模型的部分等价展开规则和展开算法.还有更多的CPN展开(Unfolding)论文[8],都是针对解决CPN展开的状态空间爆炸问题开展的研究,很少涉及基于CPN关联矩阵的展开问题.
综观以上研究,我们领会到确实解决CPN到OPN等价展开问题的核心问题是如何有效准确地解释CPN中采用的SML语言.随之将会遇到的另一个问题是如何解决结构化SML语义解析中所存在歧义性问题.为此,本文在总结上述研究结果的基础上,通过综合应用Petri网本身具备的语义校验功能,研究基于SML语义检验和CPN关联矩阵的等价展开,提出获得OPN模型的CPN展开算法和步骤,并且给出能确实应用于工程系统着色Petri网模型展开的算法程序实现.
1 基本概念与定义
1.1 基本定义
普通Petri网由五元组OPN=(P,T,F,W,M0)构成,其中P={p1,p2,···,pm}是库所的有限集合,T={t1,t2,···,tn}是变迁的有限集合,F⊆ (P×T)∪(T×P)是弧的集合,W:F→ {1,2,3,···}是弧函数,M0:P→ {0,1,2,3,···}是初始标识,P∩T=∅andP∪T,∅.
着色Petri网由九元组组成[1]:
其中,P为有限非空“类”集合,称之为颜色集;P为有限非空库所元素集合;T为有限非空变迁元素集合;A为弧集合,有P∩T=P∩A=T∩A=∅;N为节点,有N:A→P×T∪T×P;C是库所的颜色函数,C:P→ P;G是变迁的警卫函数,G:T→ expr(expr即表达式),有∀t∈T:[Type(G(t))=B∧Type(Var(G(T)))⊆P],
其中B为布尔型函数,Var(·)为变量,Type(·)为类型(type);E为弧表达式函数,E:A→ expr,有∀a∈A:[Type(E(a))=C(P)MS∧Type(Var(E(a)))⊆P],其中P是N(a)的库所集元素,下标MS为多重集函数;I是初始标识.
1.2 SML折叠规则的OPN检验
文献[9]详细叙述了基于Petri网的规则集的校验方法,给出了规则集的Petri网的产生式语义表示.SML中多采用产生式语句表示.每条产生式规则语句由前提和结论组成.前提和结论可以是谓词(或命题)的析取和合取,还可以受全称量词∀和存在量词∃的限制,所有产生式规则a→b构成CPN模型的一类组成.
Horn句型能描述所有能用逻辑刻画的问题[5].规则p1∧p2∧···∧pn→q转化为如图1所示的OPN模型,用一个变迁表示规则的推理过程,变迁的n个输入库所代表命题p1,p2,···,pn,变迁的输出库所代表命题q.
1.3 SML表示的歧义性问题
在采用SML语言完成CPN弧函数表达式中可能存在产生冗余、不一致和死循环等问题.[10−11]简单说明如下.
不一致.规则集的不一致是指在相同的前提下,推导出相互矛盾的结论.当两条规则r1和r2前提等价,而结论矛盾时,称这两条规则矛盾.例如p→q与p→¬q矛盾.当两条规则链集在相同的条件下得出的结论互相矛盾,则称这两条规则链集矛盾,如:规则链p→q,q→f与规则链p→s,s→t,t→¬f矛盾.
同一.当两条规则r1和r2在前提相同,结论也相同时,称这两条规则同一.如规则p∧q→r与q∧p→r同一.
循环推理.在规则表示中,通过一系列的逻辑推理,由一个前提出发又回到该前提,反复而不能正常结束.循环规则链是指一组规则形成的循环链.例如图2中(其中库所r1,r2,r3表示相应的命题)r1→r2,r2→r3,r3→r1就是一条循环规则链.
冗余.系统中存在冗余是指一个规则系统中可以从同一给定的事实或前提推出相同的结论.如图3所示,表示展开的OPN网出现了两个重复的命题.
有向图的邻接矩阵.矩阵的行和列都为图的顶点,若图中
有向图的可达性矩阵.如果从顶点Vi可到达顶点Vj,那么可达性矩阵的对应元素aij为1,否则为0.从可达性矩阵入手,解决规则集存在的某些歧义性问题.
规则节点集.对于一个产生式规则集M,集合W={x|∀x→y∈M}∪{y|∀x→y∈M},为产生式规则集的规则节点集,是指M中的所有规则的所有前提和结论组成的集合.
规则有向图.对于产生式规则集M,构造一个简单有向图D=(V,E),其中节点集V为产生式集M,边集合E={(x→y,y→z)|x,y,z∈W,x→y,y→z∈M},则该有向图D称为产生式集M的“规则有向图”.
1.4 SML语言的形式化定义
标准元语言 (Standard ML)[12−13]的引入使得CPN能够对各种数据操作进行建模,并且使得模型得以参数化和更加紧凑,结合实际工程建模实践,给出建模中用的SML的子集ML0的形式化定义.
类型声明:
变量声明:
vara,b,c:Type;
表达式:
S为表达式,B为布尔表达式
2 CPN展开规则
在标准化元语言(Standard Meta Language,SML)的基础之上扩展的CPN-ML,用来描述CPN库所、变迁和弧的颜色集、弧表达式、警卫函数的主体.在工程应用中,根据CPN的逻辑表示,将其关联矩阵展开为普通Petri网的关联矩阵,关联矩阵中的元素反映反映库所与变迁间的输入/输出约束关系.
为描述的一致性和简便性,假定CPN的弧表达式为变量或函数形式.
如图4所示为CPN的一个子网,库所Pre1、Pre2、Pos1、Pos2的颜色集类型分别为t1、t2、t3、t4,它与变迁T连接的弧上的弧表达式分别为变量n10x、n20f2(x)和函数n30f3(x)、n40f4(x).弧表达式是SML表达式,根据SML类型系统它们都有对应的类型.对于一个SML表达式e,Type[e]表示e的类型.
在Petri网中,每个变迁触发代表事件序列的推进,基于每个变迁的触发来描述展开步骤:
步骤1.结合ML0的类型定义,考虑展开变迁的输入和输出库所:
1)如果弧表达式为变量
CPN中每个库所都有相应的颜色集,此颜色集是基于SML语言表达的.将复杂颜色集展开为若干基本颜色集,每个基本颜色集可以展开为普通Petri网中的一个库所.也就是说,这种情况下,可以将PN中的单个库所展开为普通Petri网中的一个或多个库所.具体展开过程如图5所示.
2)如果弧表达式为IF...THEN
CPN中IF...THEN语句是表达在相应变迁的输弧变量构成的判断条件相应的输出.这种情况下,除将输入库所和输出库所展开为若干基本颜色集后,还应将对应变迁和相应的输入弧展开为输入弧变量的不同判断条件,输出弧展开为不同的输出条件,与相应的输出库所相连.具体展开过程如图6所示.
步骤2.在将单个规则展开后,要进行规则模型的校验,在展开的过程中进行规则模型的不一致、冗余和等价问题的校验.对于某个特定的变迁,将其展开得到了一个新产生的规则的集合M0,将其与产生的规则集合M进行比较.其中规则集合构成了规则有向图,M中的每一条规则都可以写成IF...THEN的形式,方便进行ML语义分析.
冗余.如果2条规则的结论相同或2条规则的前提集合为包含关系,那么就可能产生冗余.
冲突.如果2条规则的结论相互冲突、2条规则的前提集合不冲突、任意结论不为对方的前提,那么2条规则冲突.
等价.如果2条规则的结论相同,那么这2条规则是等价的.
如果出现上述3种情形,将程序的错误结果报告给专家进行处理.
将CPN按上述步骤展开后,即可得到OPN关联矩阵,再进行循环规则的检查:
设产生式集M中的规则有向图是D(D的节点表示规则),构造图D的邻接矩阵A,由A出发求有向图D的可达性矩阵P.如果P的对角元素为1,则说明从该节点出发有一条循环规则链.
在找到循环规则链后,系统可以将它提交给领域专家进行人工处理,以消除规则链的循环.
3 算法实现
使用CPN Tools这一工具软件来进行CPN的编辑和仿真,该软件产生的CPN文件以XML格式存储.首先解析XML文件,得到CPN网的基本信息,包括库所,变迁和弧函数的信息和网中各个节点的连接关系.
然后需要构造CPN ML子集的虚拟机[14−15],虚拟机的系统结构如图7所示.
在基于此语法和组件的基础上,用标准C实现了解释系统(虚拟机)和运行支持平台.然后在此平台的基础上,实现了上一小节所述的CPN展开算法.
示例.以哲学家CPN模型的展开变换为例.3位中国哲学家同时用餐的CPN模型如图8所示,图中库所Think,Eat分别表示哲学家处于思考和就餐的状态,其颜色集为PH.UnCS表示尚未使用的筷子,颜色集为CS.变迁TakeCS和PutDownCS分别表示哲学家拿起和放下筷子的动作.
图9是根据上述步骤展开得到相应的OPN模型.哲学家pi(i=0,1,2)围圆桌而坐,pi和pi+1共享餐叉fi.pi共有两种可能的状态:就餐态ei和思考态ki.按照上述的展开算法,将复合颜色集CS和PH展开,对应3个哲学家和筷子.根据弧函数上的规则和逻辑得到如下的OPN的关联矩阵.运行程序,得到OPN的关联矩阵如图10所示.
4 总结与展望
本文在讨论CPN-ML语义逻辑检验的基础上,提出了面向工程系统应用的CPN关联矩阵到OPN关联矩阵的展开规则、算法和实现步骤,并给出了基于CPN-OPN展开操作算法的计算机实现.应用本文提出的算法步骤而开发的CPN展开支持软件,容易获得复杂工程系统CPN模型的恒等OPN关联矩阵,由此能方便地通过OPN的相关结构化分析算法,实现CPN模型的结构性质和逻辑行为特性分析.
本文完成的CPN-ML语义解释和检验没有包含SML语句的全部表达形式.对那些还不能够应用Horn句型准确化解的CPN-ML表达式的语义解析、展开和检验还需要做进一步的深入研究.
1 JENSEN K.Colored Petri nets basic concepts,analysis methods and practical use volume 1:basic concepts.second edition[M].Berlin:Springer,1992:1−87.
2 WAGENHALS L W,SHIN I,KIM D,et al.Synthesizing executable models of object oriented architectures[J].Systems Engineering,2003,6(4):266−300.
3 MURATA T.Petri nets:properties,analysis and applications[J].Proceeding of IEEE,1989,77(4):541−580.
4 HUANG H J,CHEUNG T,MAK W M.Structure and behavior preservation by Petri-net-based refinement in system design[J].Theoretical Computer Science,2004,328(3):245−269.
5 SMITH E.Principles of high-level net theory[J].Lectures on Petri Nets I.Basic models,Lecture Notes in Computer Science,1998,1491(1):174−210.
6 KORDON F,LINARD A,PAVIOT-ADET E.Optimized colored nets unfolding[C]//International Conference on Formal Methods for Networked and Distributed Systems(FORTE’06).Paris:Springer,2006:339−355
7宋阿妮,王明哲,郭法滨,等.着色Petri网的结构展开方法[J].系统工程理论与实践,2011,31(2):315−322.
8 MCMILLAN K L.Using unfolding to avoidthestateexplosionproblem in the verificatio of asynchronous circuits[J].Lecture Notes in Compuuter Science,1992,663(2):164−174.
9 ZAIDI A K,LEVIS A H.Validation and verificatio of decision making rules[J].Automatica,1997,33(4):155−169.
10 LOONEY C G,LIANG L R.Inference via fuzzy belief Petri nets[C]//Sacramento:Proceedings of the 15th IEEE International Conference on Tools with Artificia Intelligence.IEEE Computer Society,2003
11陈朝东,黄国兴.图论在产生式系统知识库维护中的应用[J].微型电脑应用,2000,16(4):35−37.
12 PAULSON L C.ML for the working Programmer.Second edition[M].Beijing:China Machine Press,2005:51−239.
13 PAULSON L C.ML程序设计教程[M].柯韦,译,2版.北京:机械工业出版社,2005.
14 AHO A V,LAM M S,SETHI R,et al.Compilers:principles,techniques and tools,second edition[M].Beijing:China Machine Press,2009:33−89.
15 NIELSON H R,NIELSON F.Semantics with applications:an appetizer[M].London:Springer-Verlag,2007:26−212.
