形式化开发方法Petri网

单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,-,*,-,软件工程形式化方法,1,第5章 形式化开发方法,(1),2,内容安排,软件开发的形式化方法,形式化开发方法,(1),Petri,网,形式化开发方法,(2), 时态逻辑,形式化开发方法,(3),Z,方法,3,软件开发的形式化方法,软件开发的形式化方法定义,软件开发的形式化方法（,formal methods,）是建立在严格数学基础上，具有精确数学语义的开发方法,简单地说，凡在系统研究中，应用了数学的方法，都是形式化方法,本章所介绍的形式化开发方法是指软件规格说明数学建模、数学验证和数学程序求精,4,形式化方法与结构化和OO方法区别,结构化和,OO,方法,使用了大量的自然语言。自然语言的二义性、不完整和抽象层次的混杂等问题的解决，必然使开发系统的质量不高、成本增加和进度拖长；尤其对安全性或其他质量因素要求极高的软件，任何微小的错误都可能带来灾难性的后果,形式化的方法,可以帮助软件开发人员开发出更为无二义性、完整的和准确的需求规格说明，进而通过严格的验证发现问题，以达到对软件质量、开发成本和开发进度的有效控制,5,形式化开发方法发展历史,20世纪60年代末,形式化方法与非形式化大致同步,都是为解决当时出现的“软件危机”提出,一般认为是,Floyd、Hoare和Manna,等在程序正确性证明方面的研究。但由于这些方法受程序规模的限制而未能应用,20世纪80年代末,在硬件设计领域形式化方法的工业应用结果，又掀起了软件形式化开发方法的学术研究和工业应用的热潮，建立了一些较为成熟的方法和语言,如,Petri网、statecharts,、通信顺序过程、通信系统演算、程序正确性证明、时态逻辑、模型验证、,Z语言、 VDM及Larch等,6,目前流行的形式化开发方法,形式化规格说明建模,形式化验证,形式化程序求精,7,形式化规格说明建模,操作类,基于状态和转移,Petri,网、有限状态机和状态图,描述类,基于数学公理和概念,基于逻辑的描述方法：命题线性时态逻辑,（PLTL）、一阶线性时态逻辑（FOLTL）、计算树逻辑（CTL）,基于代数的描述方法：Z语言、VDM和Larch,双重类,兼有操作类和描述类两者的特点,扩展状态机（ESM）、实时时态逻辑（RTTL）,8,形式化验证,模型验证和定理证明,模型验证是对规格说明所建立起来的模型状态空间进行搜索，以确认该系统模型是否具有所期望的某些性质,定理证明是以逻辑公式作为系统及其性能的规格说明，其中逻辑由一个具有公理和推理规则的形式化系统给出。进行定理证明的过程就是应用这些公理或推理规则来证明系统是否具有所期望的性质,9,形式化程序求精,形式化程序求精就是将自动推理与形式化规格说明相结合而形成的一门技术,研究如何从形式化的规格说明推演出具体的面向计算机的程序代码的全过程,基本思想就是用一个抽象程度低和过程性强的程序，去代替一个抽象程度高和过程性弱的程序，并保证它们的功能和性质完全一致,形式化程序求精与形式化规格说明和形式化验证三者是紧密联系和相辅相成,10,形式化开发方法主要问题,对软件开发人员（包括管理人员和用户）的数学素质有较高的要求,主要是离散数学中的集合、代数结构、数理逻辑等基础内容在软件工程中的具体应用,对于原来一些数学背景较差的工程人员要花许多时间去学习和掌握。有的甚至还要克服对数学的畏惧心理,在选择和应用形式化开发方法时应注意的问题,Bowan和Hinchley,提出了“形式化法方法的十条戒律”,11,形式化开发方法(1),Petri网,12,什么是,Petri网,Petri网是一种网状结构,的系统的描述和分析工具,对于具有并发、异步、分布、并行、不确定性或随机性的信息系统，都可以利用这种工具构造出要开发的Petri网模型。然后对其进行分析，即可得到有关系统结构和动态行为方面的信息。根据这些信息就可以对要开发的系统进行评价和改进,Petri网的提出,由德国C.A. Petri在他的62年博士论文“Communication with automata”中提出,当时引起一些欧美科学家的重视。他们在引用这种网状结,构模拟和分析并行系统中称它为“Petri Nets”。从此以后大家都称它为Petri,网,13,Petri网介绍的内容,示例-四季系统,Petri网的定义,Petri网的基本原理-静态结构,Petri网的基本原理-动态特征,建模实例,特性分析,Petri网的特性分析方法,改进Petri网及其应用,时间网和随机网,从Petri网到程序结构的转换,14,示例：四季系统,一年有四季，四季气候的变化,该,系统可以由图形表示,15,系统,的Petri网图形表示,16,系统,的Petri网数学表示,=,（P，T；F，M,0,）,P=p1, p2, p3, p4,T=t1, t2, t3, t4,F=（p1, t1）, （t1, p2）, （p2, t2）, （t2, p3）, （p3, t3）, （t3, p4）, （p4, t4）, （t4, p1） ,M,0,=（0, 0, 0, 1）,17,Petri网描述系统,的特点,从四季系统,中，可以看出这种利用事物的因果关系对系统进行网状结构的描述，有以下特点,自然,没有任何不必要的人为控制，完全反映了现实世界的真实情况,局部确定原理,因为事件或转移的发生和结果都由局部状态决定,既有系统静态结构，又有动态行为方面的信息,既有图形工具，又有数学工具,图形工具和数学工具完全等价,图形工具直观、形象、易懂、易学；数学工具严谨，既便于计算，又便于验证,18,Petri网的基本原理：静态结构,任何系统都有两类元素组成：表示状态的元素和表示状态变化的元素,Petri网,位置（place）：状态,转移（transition,）：改变状态,两者之间的依赖关系用弧（箭头）表示,19,Petri,网的基本成分（1）,20,Petri,网的基本成分（2）,其中：,P=（p,1,p,2, ,p,m,）,是,N,的有穷位置集合,T=（t,1,t,2,t,n,）,是,N,的有穷转移集合,F,是由,N,中一个,P,元素和一个,T,元素组成的有序偶的集合，,F,称为流关系。,（PT）,和,（TP）,中的“,”为笛卡尔乘积。,DOM（,F,）=,x,y,：,（,x,y,）,F,，COD（,F,）=,x,y,：（,y，x,F,分别为F所含的有偶序偶的第一个元素组成的集合和第二个元素组成的集合。,21,Petri,网的基本成分（3）,由上可以说明,N=,（,P,T；F,）是位置集合,P,和转移集合,T,构造Petri网的两个基本成分,P,与,T,两者间的流关系,F,是从它们构造出来的。所以在,P、T,之后的F用分号“；”隔开来,P,T,说明网中至少要有一个,元素,P,T=,说明P和T为两类不同的元素,两者不能有交,F,（,PT,）,（,TP,）说明一个,P,元素代表一个资源,其流动由,F,关系规定。所以,转移T只能与位置有直接的流关系,不是从,PT,就是从,T P,。而不参与任何转移的资源为孤立的,P,不引起资源流动的转移为孤立的,T,。所以,DOM（,F,）,COD（,F,）=,P,T,说明网中不能有孤立的元素,P,或,T,22,前集、后集、子网,设 ，令,*x=,y|,（,y, x,）,F, x*=,y|,（,x, y,）,F,*x,被称为x的前集或输入集。,x*,被称为x的后集或输出集。,在,N,1,=,（,P,1,T,1,;F,1,）和,N,2,=,（,P,2,T,2,;F,2,）,中，,如果 , , 且 ,则称,N,1,是,N,2,的子网。,23,纯网,在,N=,（,P,T；F,）中,如果对似有,x,P,T,都有,*x,x*=,则称,N,为纯网（pure net）,纯网中无公共前后集（环）,24,简单网,如果对所有,x,y,P,T,都有（,*x= *y,） （,x*=y*,）,x=y,则称,N,为简单网（simple net）,简单网中无相同的前后集,25,Petri,网的基本原理：动态特征（1）,Petri网作为系统的建模工具,除具有上述描述的静态结构外,还应包括位置的容量和转移发生对位置容量的影响信息。有限容量可用大于零的整数表示,转移发生对位置中标记数的影响用孤上的整数表示。于是,具有动态特征的Petri网可表示为六元组：,26,Petri,网的基本原理：动态特征（2）,Petri网的六元组：,其中：,（,P,T；F,）含义同前,K：PN,是位置上的容量函数,N,= 0,1,2,3, ,若,K,（,p,）,=,表示位置中的容量为无穷,W：F N,是孤集合上的孤函数,M：P N,0,是Petri网的标识（marking）。,M,0,为初始标识,N,0,=,0,1,2,3, ,p,P,必须满足,M,（,p,）,K,（,p,）,在Petri网的图形表示中,M,（,p,）不是用数字,而是用实圆点表示。每个实圆点为一个标记,同一个位置中的诸多标记代表同一类完全等价的个体。弧（,x,y,）上的,W,值标注在孤（,x,y,）上,27,转移发生规则（1）,Petri网的动态行为是通过转移发生引起标识改变来体现的,转移可发生的条件和发生规则,转移,t,可发生的条件,若在标识,M,下,p,1, p,1,*t,M,（,p,1,）,（,p,1,t,）,且,p,2, p,2,t*,M,（,p,2,）,+W,（,t, p,2,）,K,（,p,2,）,+W,（,t, p,2,） ,K,（,p,2,）,此时称,t,在,M,下可发生,记为,M,t ,转移,t,发生的结果,若,t,在,M,下可发生, 就可以发生, 发生后将,M,变成新标识,M,出视方出记为,M,tM,或,M M,并称,M,为,M,的后继标识,对,p,P, M,（,p,）,=M,（,p,）,W,（,p,t,）,当,p,* t t *,=M,（,p,）,W（t,p,）,当,p,t * * t,=M,（,p） W,（,p,t,）,W,（,t,p,）,当,p,* t,t *,=M,（,p,）,当,p,t *,* t,28,转移发生规则（2）,注意,一个没有任何输入位置的转移叫源转移,一个源转移的可发生是无条件的。一个源转移的发生只会产生标记,而不消耗任何标记,一个没有任何输出位置的转移叫潭转移,一个潭转移的发生将消耗标记,而不产生任何标记,29,示例：转移发生规则,以本例来说明网论中的转移发生规则，以及网论中的冲突（conflict）、并发（concurrent）和碰撞（contact）现象,有时，一个Petri网中同时存在并发和冲突，而且并发的发生会引起冲突的消失或出现。网论中称这种现象为混惑（confusion）,30,并发和冲突概念的完整描述,并发,设,M,为Petri网,的一个标识，若存在,t,1,和,t,2,使得,M,t,1,和,M,t,2,，并满足 ，且则称,t,1,和,t,2,在,M,下并发,冲突,设,M,为Petri网,的一个标识，若存在,t,1,和,t,2,使得,M,t,1,和,M,t,2,，并满足 ，且则称,t,1,和,t,2,在,M,下冲突,31,网系统分类,根据,Petri,网系统中容量函数,K,和权函数,W,的不同可分为三种情况,K,1，,W,1,为基本网（,elementary net,EN）系统,这种网系统位置,p,中，只有有标记和无标记两种状态。习惯上把这种网称为条件/ 转移网系统,K,，,W,1 为,P,/,T,（place/transition）网,K,和,W,为任意函效 为,P,/,T,系统,P/T,网和,P/T,系统中都是物质资源，它们与EN系统有本质的不同。所以，EN系统又叫做条件/事件网系统。,P/T,网和,P/T,系统也有区别。,K,（,p,）（位置容量）是其能容纳此类资源的能力，也称空间资源。而,W,（,p,t,）和,W,（,t,p,）分别是转移,t,发生时释放和占用此类空间资源的数量。,P,/,T,网的位置,p,容量足够大，所以不会发生碰撞。而,P,/,T,系统，如果位置,p,容量有限，且不进行技术处理，则有可能发生碰撞,32,Petri,网转移发生规则的简化,对Petri网简化的原因是为了对Petri网进行理论上研究的方便,通过上面讨论可以看出，对于简单的Petri网，由于,K,和,W,已无任何限制作用。所以，一般把这种Petri网系统记为：=（,N,M,）=（,P,T;F,M,）。这种Petri网系统的转移发生规则，可以简化为：,若M,t,，当且仅当,p,p，,M,（,p,） 1，,t,发生后，,M,t,M,M,（,p,）=,M,（,p,） 1 当,p,*,t t,*,=M,（,p,） 1 当,p,t * * t,=M,（,p,） 其它,网论可以证明，经过适当加技术处理，都可以把,K、W,任意的,P/T,网或,P/T,系统改造为,K,W,1的Petri网,M（p）=M（p） 1 当p * t t *,=,M（p） 1 当p ,t * * t,=,M（p） 其它,33,建模实例：有限状态机,34,建模实例：并行活动,35,建模实例：数据流计算,36,建模实例：通信协议,37,建模实例：同步控制,38,建模实例：生产者/消费者系统（1）,39,建模实例：生产者/消费者系统（2）,抑制弧,40,建模实例：形式语言,41,建模实例：机械加工（1）,42,建模实例：机械加工（2）,43,建模实例：机械加工（3）,44,建模实例：机械加工（4）,45,建模实例：机械加工（5）,46,特性分析,Pretri网的特性主要包括,可达性（Reachability）,有界性（Boundedness）,活性（Liveness）,可逆性（Reversibility）,可覆盖性（Coverability）,持久性（Persistence）,同步距离（Synchronic Distance）,公平性（Fairness）,47,特性分析-可达性,对Petri网（,N，M,0,），如果存在一个从,M,0,到,M,n,的发生序列，则称标识,M,n,是从,M,0,可达的。发生序列表示为,=,M,0,t,1,M,1,t,2,M,2,t,3,M,3,t,n,M,n,，或简化为,=t,1,t,2,t,n,。,可用,M,0,M,n,表示三者间的关系。在Petri网（,N,M,）中所有从标识,M,0,可达的标识集合，可表示为,R（N，M,0,）或个简化为,R,（,M,0,）。从,M,0,出发的所有可能发生序列的集合，可表示为,L,（,N,M,0,）或简化为,L,（,M,0,）。,这样,Petri网的可达性问题就转换为对于Petri网（,N,M,）和给定标识,M,0,寻找是存在,M,0,R,（,M,0,）,可达性是研究任何系统动态特性而与基础,48,特性分析-有界性,对Petri网（,N,M,），若存在一个非负整数K，使得,M,0,的任何一个可达标识的每个位置中的标记数都不超过,K,，即对每个标识,M,R,（,M,0,）和每个位置,p,M,（,p,） ,K,均成立，则称Petri网（,N,M,0,）为,K,有界，或简称有界,若Petri网（,N,M,0,）为1有界，则称此Petri网为安全的。这种网的每一个位置要么有一个标记，要么没有标记,通常用Petri网中的位置表示实际系统中存储数据的缓冲区和寄存器。通过分析网的有界性或安全性，就可以考察实际系统中缓冲区或寄存器是否会溢出,49,特性分析-活性,一个Petri网（,N,M,）被称为活的或称,M,0,是网,N,的一个活标识，仅当从,M,0,可达的任一标识出发都可以通过执行某一转移序列而最终发生任一转移。这意味着，无论选择什么样的发生序列，一个活的Petri网都可以保证无死锁操作。活性是许多系统的理想特性。但这是不现实现的，也是不必要的,对于Petri网（,N，M,0,）中的一个转移,t,，实际上可能属于以下情况：,L0级活（死的）：仅当,t,在,L,（,M,0,）中任何发生序列中都无法发生,L1级活（可能能发生）：仅当,t,在,L,（,M,0,）中的一些发生序列中至少可发生一次,L2级活：已知任一正整数,k,，仅当,t,在,L,（,M,0,）中的一些发生序列至少可发生,k,次,L3级活：仅当,t,在,L,（,M,0,）中的一些发生序列中可以无限制的发生,L4级活（活的）：仅当,t,在,R,（,M,0,）中的每个标识是L1活的,50,特性分析-可逆性,一个Petri网（,N,M,0,）称为可逆的，仅当对,R,（,M,0,）中每个标识,M,M,0,都是从,M,可达的。因此，一个可逆网可以返回到初始标识或初始状态。在很多名小应用中只要求系统回到某个特定状态而无需回到初始状声在态我们称这个特定状态为主（home）状态即对于,R,（,M,0,）的每个标识,M,主状态,M,都是可达的,有界性、活性和可逆性是三种相互独立的特性,51,特性分析-可覆盖性,一个Petri网（,N,M,0,）中一个标识M称做可覆盖的，仅当在,R,（,M,0,）中存在一个标识,M,，使得对网中的每个位置,M,（,p,） ,M,（,p,）成立,可覆盖性与L1活（潜在的可发生性）紧密相关。设,M,是转移,t,发生所必需的最小标识。那么，当且仅当,M,是不可覆盖的，,t,是死的（非L1活）。也就是说，,t,是L1活，当且仅当,M,是可覆盖的,52,特性分析-持久性,一个Petri网（,N,M,0,）称为持久的，仅当对于任意两个可发生转移，其中一个转移的发生不会使另一个转移不发生。就是说，持久网中的一个转移一旦可发生，将保持这种可发生性直至它发生为止,所有位置都只有一条输入孤和一条输出弧的Petri网（标识图）具有持久性,53,特性分析-同步距离,同步距离是条件/事件系统中两个,事件间相互独立程度紧密相关的,一种量度。我们用,来定义Petri网（,N,M,0,）中两个转移,t,1,和,t,2,间的同步距离。其中,是起始于,R,（,M,0,） 中的任何标识,M,的一个发生序列，（,t,i,）是转移,t,i,（,I,= 1,2, ）在 中发生的次数。,右图们仍所示Petri网中,d,12,=1,d,34,=1,d,13,=,同步有不同的形式（见例1例5）,54,同步形式（1）,它们共同执行一个任务，只有,p,1,、,p,2,中的标记同时到达时才能同步,55,同步形式（2）,这是一个顺序系统，,t,1,t,2,为同步。但它们交替发生，,t,1,与,t,2,的关系为11,56,同步形式（3）,这是一个并发系统，,t,1,、t,2,发生的关系也为11。但它们不是交替发生，而可同时发生，也可一先一后发生,57,同步形式（4）,本例中，,t,2,不能先发生，只有,t,1,可以发生。这也就是说，只有,t,1,发生后，,t,2,才能发生。这时，仍只有,t,1,能够发生。即,t,1,第二次发生后，,t,2,才能发生。由此可见,t,1,与,t,2,也为顺序关系，但它们的关系为21,58,同步形式（5）,本例中，,t,1,与,t,2,的关系为1或1，这就等于无同步可言,59,同步距离刻画事件间的同步关系,d,12,=,两组事件不同步，即异步,d,12,M,（,p,） 的每个位置,p,，用,重置,M,（p）,d. 引入,M,作为树的一个结点，从,M,向,M,画用,t,标注的弧，并对,M,加上,“新的”标志。,76,从,Petri,网获得可覆盖性树,77,使用可覆盖性树可研究,Petri,网的特性（1）,对于一个,Petri,网（,N, M,0,），且因此,R,（,M,0,）,是通过使用可覆盖性树可以研究以下特性,一个网,（,N, M,0,）,是有界的，,且因此,R,（,M,0,）,是有限的，,当且仅当,不会出现在可覆盖性树中的任一结点标注中,一个网（,N, M,0,）,是安全的，当且仅当只有“0”和“1”出现在可覆盖性树的结点标注中,一个转移,t,是死的，当且仅当,t,不出现在可覆盖性树的任一弧的标注中,如果,M,从,M,0,可达，则存在一个标注,M,的结点，使得,M,M,78,使用可覆盖性树可研究,Petri,网的特性（2）,对于一个有界的,Petri,网，其可覆盖性树被称为可达性树。这是因为它包括所有可能到达的标识。在这种情况下，前面计讨论的所有行为特性的分析问题都可以通过可达性树来解决，这是一种穷举法,但在通常情况下，由于使用符号,会使一些信息丢失，所以可达性和活性问题不可能单单利用可覆盖性树方法来解决。我们可看下页所示的两个不同的,Petri,网，它们有相同的可覆盖性树。但其中一个是活的,Petri,网，而另一个不是活的，因为该网在发生,t,1,、,t,2,和,t,3,以后再也没有可发生的转移,79,使用可覆盖性树可研究,Petri,网的特性（3）,两个不同的,Petri,网,一个活的,Petri,网 一个不活的,Petri,网,80,使用可覆盖性树可研究,Petri,网的特性（4）,相同的可覆盖性树,81,使用可覆盖性树可研究,Petri,网的特性（5）,不同的可达状态,一个活的,Petri网 一个不活的Petri,网,82,不变量、关联矩阵和状态方程,这一部分介绍的是完全用代数计算来对网系统进行分析。,前边介绍的可达集都是从网的整体行为来刻画的。这里讲不变量，整体中有许多不变量，这是局部行为。,不变量用关联矩阵定义，它给出了系统的结构。,根据关联矩阵与网存在的一一对应关系推出状态方程。,最后就可用关联矩阵和状态方程计算出网的不变量和网的各种特性。,83,不变量,（invariant）,网系统中有,S,-,不变量和,T,-,不变量,如果网系统中有一些位置，其中包含的资源（标记）的总和在任何可达标识情况下均为常数，即系统不论发生什么事件，这些位置中的标记总数不变，则这些位置就是系统的一个,S,-,不变量。也就是说，,S,-,不变量代表着网系统中若干个资源的流动范围,如果网系统中有一些转移，它们的发生会使它们的标识恢复到它们的开始状态，则这些转移就是系统的一个,T,-,不变量,84,不变量-示例1,S,-,不变量和,T,-,不变量一般采用向量表示，即以位置元素为序标的列向量表示,S,-,不变量，以转移元素为序标的列向量表示,T,-,不变量,本网系统的不变量为：,S,-,不变量,T,-,不变量,85,不变量-示例2,本网系统的不变量：,86,不变量-示例3,本网系统的不变量：,87,关联矩阵,（Incidence Matrix）（ 1）,正如网系统的标识可以表示为一个向量一样，网结构也可以用一个矩阵来表示。,设,=（,N,M,0,）,其中,N,=（,P,T,;,F,）,是一个纯网，其中,P,=,p,1,p,2,p,m,，,T,=,t,1,t,2,t,n,用,S,-,元素作为序标的列向量,V,：,P,Z,称为,的,S,-,向量，,Z,为正负数集合。其中，,Z=2, 1,0,1,2, ,为正负数集合,用,T,-,元素作为序标的列向量,U,：,T,Z,称为,的,T,-,向量,用,P,T,作为序标的矩阵,C,：,P,T,Z,称为,的关联矩阵,其关联矩阵元素,C,（,p,i,t,j,）=,W,（,t,j,p,i,） ,W,（,p,i,t,j,）,88,关联矩阵（2）,C,（,p,i,t,j,）=,W,（,t,j,p,i,） ,W,（,p,i,t,j,）,也可写成：,C,ij,mn,=,C,ij,mn, ,C,ij,mn,其中,C,ij,就是从转移j到它的输出位置I的弧的权，,C,ij,是抗持转移的输入伍卜位置I到转移j的弧的权。从转移规则很容易看出，,C,ij,、,C,ij,和,C,ij,分别表示当转移j一旦发生，位置i中标记取走、增加和改变的数量。,当（t,j, p,i,）F,其他,当（p,i, t,j,）F,其他,89,关联矩阵（3）,关联矩阵一般表示形式,其中,C,ij,表一下示取走、增加后产生的变化数。此关联矩阵给出了系统的结构,90,状态方程,如果,N,=（,P,T,;,F,）,是纯网，则,C,与,N,存在一一对应关系。在此，我们用,m,维列向量来表示标识,M,，即,M,=,M,（,p,1,）,M,（,p,2,）, ,M,（,p,m,）,T,。这样，,M,t,j,的充分必要条件为：,i,1,2, m：,C,ij,M,（,i,）,或写成：,C,*j,M,其中,C,*j,表示矩阵,C,ij,的第j列。,如果,M,1,t,j,M,2,，则有,M,2,=,M,1,+,C,*j,。,若,M,0, ,M,，就可以推出状态方程为：,M,=,M,0,+,CU,其中,CU,是矩阵乘法，是的转移序列，,U,是,的,T,-,向量表示，它以,t,j,为序标的分量值为,t,j,在,中出现的次数，即,U,（,t,j,）=#（,t,j,/ ），,M,0,是,的初始标识的,S,-,向量表示，由导出的可达标识,M,也表示为,S,-,向量形式。,91,用关联矩阵和状态方程求不变量,设,I,是的,S,-不变量，,M,M,0,，则,I,T,M,=,I,T,M,0,设是从,M,0,到,M,的转移序列：,M,0, ,M,，,于是,M,0,+,C,T,U,=,M,，,其中,U,是对应于的,T,-向量，对所有,t,j,T,，,U,（,t,j,）是,t,j,在 中出现的次数。两边同时乘以,I,T,，则得,I,T,M,0一,+,I,T,C,T,U,=,I,T,M,92,状态方程在可达性分析中的应用（1）,状态方程,M,=,M,0,+,C,T,U,为部分解决可达性问题提供了一个依据。若,M,d,从,M,0,可达则方程,C,T,U,=,M,d,M,0,=,M,必然存在一个非负整数解,U,x,，该解即为发生的计数向量。若无这样的解，,M,d,就不继从,M,0,到达。,示例1,93,状态方程在可达性分析中的应用（2）,示例1（续）,在所示的Petri网中：,在状态,M,0下转移,t,3是可发生的。设,M,1是发生,t,3所得的标识，则有,94,状态方程在可达性分析中的应用（3）,示例1（续）,发生序列,=,t,3,t,2,t,3,t,2,t,1,表示成发生计数向量（1,2,2），发生后产生的新标识为,95,状态方程在可达性分析中的应用（4）,示例1（续）,考察标识 ，它可以从标识,M,0,到达方程为,有一个解,U,=（0,4,5），它对应于发生序列,=,t,3,t,2,t,3,t,2,t,3,t,2,t,3,t,2,t,3,96,状态方程在可达性分析中的应用（5）,再考察后标识 ，因方程,无解，所以标识 为不可达标识,97,状态方程在可达性分析中的应用（6）,注意，状态方程有解只是可达性的必要条件，而不是充分条件。这是由于缺少,M,初始标识信息导致的,示例2,考察所示的Petri网,98,状态方程在可达性分析中的应用（7）,示例2（续）,在所示的,Petri网中,方程,99,状态方程在可达性分析中的应用（8）,示例2（续）,有一个解,U,= 。这个解对应的两个可能发生序列为,t,1,t,2,或,t,2,t,1,，然而这两个序列都不是可发生序列。因为在,M,0,下，,t,1,、,t,2,都不可能发生。这里,若取初始标识为,则为可达的，且对应于发生计数向量 的发生序列为,t,1,t,2,100,关联矩阵和状态方程在其他特性方面的应用（1）,结构有界性,N,=（,P,T,；,F,）称为结构有界，是指对任何初始标识,M,0,，（,N,M,0,）都是有界的。可以证明，网,N,结构有界的充分必要条件是存在,m,维正整数向量,V,，使得,C,T,V,0,守恒性,如果存在,P,上的一个正整数函数,V,，使得对任何初始标识,M,0,和任何,M,R,（,M,0,），,M,（,i,）,V,（,i,）为一固定值，则称,N,为守恒的。可以证明，网,N,守恒的充分必要条件是存在,m,维正整数向量,V,，使得,C,T,V,=0,可重复性,如果在存在初始标识,M,0,，在（,N,M,0,）中存在无限转移序列,，使得,M,0,，,而且每个转移,t,j,都在,中出现无限多次，则称网,N,为可重复的。可以证明，网N可充分必要条件是存在,n,维正整数向量,U,，使得,C U,0,101,关联矩阵和状态方程在其他特性方面的应用（2）,相容性,如果存在初始标识,M,0,，在（,N,M,0,）中存在无限转移序列，使得,M,0,M,0，,而且,t,j,T,，# （,t,j,/） 1，则称网,N,为可相容的。可以证明，网,N,为相容的充分必要条件是存在,n,维正整数向量,U,，使得,C U =,0,结构公平性,如果对任何初始标识,M,0，,在（,N,M,0,）中都是公平网，则称网N为公平网。,可以证明，网,N,为公平网的充分必要条件是对任意,n,维非负整数向量,U,：,C U,0,i,1,2, ,m,：,U,（i） 0，而且若有,U,1,和,U,2,满足,C U,1,0 和,C U,2,0 ，则,U,1,和,U,2,线性相关,102,关联矩阵和状态方程在其他特性方面的应用（3）,示例,本例所示的网（,N,M,0,），它的位置集,S,和转移集,T,各有4个元素，流关系如图所示，初始标识,M,0,=1,0,0,0。对这样的网（,N,M,0,），可以写出它的关联矩阵和状态方程,103,关联矩阵和状态方程在其他特性方面的应用（4）,由于,M,0,C,*2,，所以t2可以发生。设,M,0,t,2,M,1,，则,如没=,t,2,t,1,t,2,t,1,t,2,t,4,在,M,0,可以发生，记,M,0,M,2,，则可计算出,M,2,为,104,关联矩阵和状态方程在其他特性方面的应用（5）,本例容易证明，存在,U,1,= 使得,CU,1,=0。所以网,N,是相容的，也是可重复,的。但不存在四维正整数向量,V,，使得,C,T,V,0。所以网,N,不是结构有界的,对于任意非负整数,kV,=,k,都满足,C,T,V,=0。何所以,k,是,N,的一个,S-,不,变量，从而,S,1,S,2,S,4,是,N,的,S,-不变量的支集。,同理，,N,的,T,-不变量额广都有,k,的形式，也即转移集,T,本身是,N,的,T,-不变量的支集,由于存在,U,2,= ，使得,CU,2,= ，而,U,2,中含有零分量。所以,N,不是,公平,105,改进,Petri,网及其应用,什么是改进,Petri,网,改进,Petri,网指的是谓词/转移网和着色网。它们由基本网改进而来，故称它们为改进,Petri,网。有的称它们为变形网，还有的称它们为高级网,既然有了上面讨论的基本网，为什么还要高级网,这是因为在实际应用中，一个稍复杂的网系统就会使用大量的位置和转移，由此引起状态组合爆炸问题，使,Petri,网难以理解和分析。有人甚至认为在状态（可达集）组合爆炸这一基本问题未获解决或有可能避免之前，,Petri,网建模不可能出现实质性的成功或突破。所以还要介绍高级网。,高级网系统如何构造,高级网系统如何构造，一般都从应用的问题的,P/T,网系统模型着手，经折叠而成。所以，我们就应该先弄清什么是,P/T,网系统的折叠，然后介绍折叠的高级网系统的定义,什么是折叠,折叠就是采用抽象的方法，把具有同类逻辑功能制的位置和转移进行合并，这样就可以大大减少位置和转移的数量，将结点多的,P/T,网系统转换为结点较少的高级网系统,106,谓词/转移网,谓词/转移网（,Predicate/Transition nets, Pr/T网）,Pr/T,网的转移发生条件和引起的标识变化是通过刻画标记性质的谓词来解释的,示例：一个机械制造车间零件加工的简化,Pr/T,网系统模型,107,一个机械制造车间零件加工的简化,Pr/T,网系统模型（1）,1,问题描述,有一名工人分别在机床甲和机床乙上加工零件。先加工完的机床要等待另一台机床加工完后，零件经装配才能卸下。然后，机床转入空闲，再进入就绪。以上加工过程重复进行,为简化问题，这里只考虑工人和机床的关系。其他如原材料来源、成品的去处，以及辅助工具（刀、量等）等一概不考虑,108,一个机械制造车间零件加工的简化Pr/T网系统模型（2）,2,P/T,网系统模型,109,一个机械制造车间零件加工的简化,Pr/T,网系统模型（3）,3,先分析位置,从上可知：本系统中有3 个个体：工人、机床甲作和机床乙，用,w、a、b,来表示,这3 个个体可能处于4 种状态：就绪（,ready,）、工作（,working,）、等待（,waiting,）和休息（,resting,）,工作必须是,w,和,a,或,w,和,b,的结合，为了强调结合用,joint,（结合）表示,working,如果用,P,-,元素表示4个状态，用,w、a、b,三个个体名代替没有个性的标记。就可把逻辑功能相同的位置（状态）折叠在一起,这样位置由10个减少为4个,110,一个机械制造车间零件加工的简化,Pr/T,网系统模型（4）,逻辑功能相同的位置折叠在一起的图形表示,111,一个机械制造车间零件加工的简化,Pr/T,网系统模型（5）,在位置折叠的图中可见,它保留了,P/T,网系统中的全部有向孤和所有转移。有向张上旅弧上标注了孤上流动的个体或由个体结合而成的偶如,w,a,或,w,b,P,-,元素（位置）已不是原,P/T,网系统中的位置，而是其中个体当前的状态，即谓词。谓词中的标识也不是非负整数，而是由个体组成的集合。如,P,1,中初始标识有3个个体，表明,w、a、b,都处于就绪状态。,P,2,、,P,3,和,P,4,在初始标识下，均无个体，为空集。由此可见，引进谓词后，减少了,P,（位置）的个数,112,一个机械制造车间零件加工的简化,Pr/T,网系统模型（4）,4,再分析转移,很明显，由上图可见：转移也可分为4类：结合（,joint,）（开始工作）=,t,1,t,2,、完成（,finish,）（工作完成）=,t,3,t,4,、装配（,assemble,）=,t,5,和准备（,to-ready,）=,t,6,t,7,t,8,由上图还可见：同类转移有相同的前集和后集，,t,1,与,t,2,、,t,3,与,t,4,，以及,t,6,、,t,7,和,t,8,之间的区别在于参与转移的个体不同。如果我们用变量,x,来代替个体名，则可把同类转移也合并为一个。这就可以得到合并转移后的网系统,113,一个机械制造车间零件加工的简化,Pr/T,网系统模型（5）,合并转移后得到的网系统,114,一个机械制造车间零件加工的简化,Pr/T,网系统模型（6）,在转移折叠的图中可见,把,P、T,两个元素间的多条有向弧合并为一条，弧上标注也用“+”号连在一起。如,P,1,与,t,1,、t,2,之间的两条弧合并为一条后，弧上记为,w,+,x,，,x,表示,P,1,中的任何一个个体。为统一符号，,w,a,和,w,b,可改写为,w,x,。用尖括号及“+”号连在一起的表达式为符号和,必须指出，,w,+,x,是两个独立的个体，,w,x,是两个结合在一起的个体,新转移,joint、finish、assemble,和,to-ready,分别代表系统中的同一类转移,当从,P,1,到,joint,的弧上标注,w,+,x,中的变量,x,取个体,a,为值时，转移,joint,发生就是原系统中,t,1,的发生。当,x,以,b,为值时，,joint,发生不是,t,1,，而是,t,2,。但,x,不能以,w,为值,图中只使用了一个变量名,x,，但,x,并非表示同一个变量。事实上，只有同一个转移的所有,I/O,弧上的变量才是同一个变量，它必须取同一个个体为值。由此可见，引进变量后减少了,T,-元素的个数,115,一个机械制造车间零件加工的简化,Pr/T,网系统模型（7）,5,Pr/T,网系统的转移规则,Pr/T,网系统的标识为系统中每个谓词指明了其外延。在转移的折叠图中,P,1,的外延为,|,a,，,b,，,w,|,，写成符号和为,+,。而,P,2,、,P,3,和,P,4,的外延均为空集合。转移,joint,前后的变量,x,可以分别以,a,和,b,值发生，发生的两次转移分别记为,joint（,x,a,）,和,joint（,x,a,）,，而,x,a,和,x,b,称为转移j,oint,的可行替换，即以,a,替换,x,和以,b,替换,x,。这肘转移才有发生权和发生权的后继。对,joint,而言，,x,w,不是可行替换，,joint（,x,w,）,在初始标下没有发生权。所以,Pr/T,网系统不能离开变量替换来讨论,joint,（,x,a,）,发生伪一的后果是化从,P,1,中拿走个体,a,和,w,，在,P,2,中加上,a,和,w,的结合，这些都是由,joint,的,I/O,弧上的标注和替换,x,a,计算出来的。,joint （,x,a,）,发生后的后继,M,1,为,M,1,（,P,1,）,=，,M,1,（,P,2,）,=,|,，,M,1,（P3）=,M,1,（,P,4,）=null,，即空符号和,按上述规则，可以给出转移折叠图的,Pr/T,网系统中一些可能替换及相应的谓词外延的变化如下页列表所示,116,一个机械制造车间零件加工的简化,Pr/T,网系统模型（8）,Pr/T,网系统的转移规则（续）,谓词外延的变化,表中谓词外延以集合形式给出以便比较集合的形式与符号和的对,应关系,117,一个机械制造车间零件加工的简化,Pr/T,网系统模型（9）,6,Pr/T,网系统的定义,=（,P,T；F,D,V,A,M,0,）,其中,（,P,T；F,）为有向网，即,的基网,D,为非空有限集，即,的个体集（标记的分类）,V,为,D,上的变量集,A,为有向集,F,上的可变谓词集（这些谓词是以,V,的元素为变元的逻辑式或代数式）,M,0,为,状态的初始标识,说明,定义中没有明确给出的两点要求是：,M,0,必须是,D,在谓词集,P,上的一个分布，而每个转移,t,T,必须是个体守恒的。转移,t,的个体字恒表现在，即出现在它的输入弧上的个体必须也出现在它的输出弧上。反之亦然。出现的形式可以不同,118,一个机械制造车间零件加工的简化,Pr/T,网系统模型（10）,7,Pr/T,网系统的行为,与,P/T,网系统相同点,谓词/转移网和着色网实质上都是,P/T,网系统为与折叠和扩充行为上自然类似顺序并发和冲突等基本现象都可以得到严格的描述。所以，分析,P/T,网系统行为的方法都可以用来分析,Pr/T,网系统和着色网系统,与,P/T,网系统不同点,因为,Pr/T,网