专业课课件操作系统第2章petri网

闻立杰清华大学软件学院2013年/秋Lecture2Petrinets2PetriandPetriNetCarlAdamPetri (1962,PhDthesis)InsixtiesandseventiesfocusmainlyontheorySinceeightiesalsofocusontoolsandapplications(cf.CPNworkbyKurtJensen)3PetriNetandItsNotationsA(Petri)NetisatripleN=(S,T,F)S

T

andST=F(ST)(TS)dom(F)ran(F)=S

T

4TheMarkingofaPetriNetwemarkthestatesofa(Petri)NetbyTokens，

S1,S2,S3,S4,S5,S6,S7,S8(1,1,1,0,0,0,0,0)摆棋子t8t1t2t4t7t3t7t5s0s1s2s4s3s9s5s8s6s7MarkingVector:5PetriNetand(Petri)NetSystem

s1s2s3s4s5NetSystem=Net+InitialMarkingDefaultAssumptionsatmostonetokeperS-elementonlyonetokeconsumed/producedperflowrelation6PureNet&SimpleNetPurenet(纯网/单纯网)对于网N(S,T;F), xX;xx=，其中X=STSimplenet(简单网）对于网N(S,T;F),

若x,yX,x=yx=y则x=y，其中X=ST7FreeChoicePetrinetGivenaPetrinet(P,T;F)Iffforeverytwotransitionst1andt2,•t1

•t2implies•t1=•t2t1andt2areenabledatthesametimeFiringt1orFiringt2aredeterminedbytheenvironment8pre-set&post-set N=(S,T,F),xXN,YXN

x的前集，pre-set(x) ·x={yXN:(y,x)F} x的后集，post-set(x)

x·={yXN:(x,y)F}

·Y=

·x Y·=

x·

x

Y

x

Yt8t1t2t4t7t3t7t5s0s1s2s4s3s9s5s8s6s79Question1:EnabledQ:Whencanatransitiont

fireatamarkingM?A:tcanfireatM

allpre-setsholdatM(t

M)and nopost-setsholdatM(t

M=

)记作，

M[t>NEnabled

可实施的/有发生权的/受权的/使能的发生条件10ExampleofQ1s1s2s3s4s5t1t2t3t4哪一个变迁可以发生？11Question2:FiringQ:Whatistheresultofatransitiont

firingatamarkingM?A:WhentoccursatMthepre-setoftceasetoholdandthepost-setoftbegintohold;theremainingpartofthecaseremainsunaffected.(HencetheresultingcaseM’is(M

t)t)记作，M[t>NM’Firing

实施/发生/触发/点火发生结果12Extension(外延)ofTransitionN=(S,T,F),M,M’P(S),tTM[t>NM’iff

M-M’=t&M’-M=t

t=t

tistheextensionoft，

即变迁的域局部确定性

13ExampleofQ2s1s2s3s4s5t1t2t3t4变迁实施效果？t1和t2能同时发生吗？14The

Temporal

StepAbasicTime-StepE(anEvent)

consistsofasetofTransitions,whichchangethatmarkingMintoamarkingM’

inawaydescribedbyRule2:

ResolveConflicts!Thisslide’scopyrightisreservedbyPetri15Thisslide’scopyrightisreservedbyPetri16TheBehaviorofPetriNet ATokenGame

Sequence17TheBehaviorofPetriNet ATokenGame

ParallelTheTemporalStep18TheBehaviorofPetriNet ATokenGame Conflict19TheBehaviorofPetriNet ATokenGame

Termination20SequentialMarkingGraphLetNbeaNetSystemTheSequentialMarkingGraphofN,SMG(N),isthe

initializededge-labeledgraph((V,Y),Vin)suchthatV=MN,Vin=inm(N),and Y={(m1,{e},m2):m1,m2MN,eTNandm1[{e}>Nm2}21DrawaSMGoftheNSs1s2s3s4s5s6s7s8s9s10s11s12s13s14s15s17s16s1822PetriNet编辑与分析工具:

PIPE23Petri网标记语言：PNMLPetriNetMarkLanguage24结构、标识和行为Petri网的行为由结构和标识共同决定举个例子：串行还是并行？25DeadlockinPetrinets26LiveLockinPetrinets27思考题如何判定一个Petrinet是连通的给定一个Petrinet系统如何判定其中存在的并发变迁集合？所有的，最大的，…给定一个Petrinet系统如何判定两个变迁是否能顺序、并发出现异或冲突？……28关于Petrinet合理性的文献[Ko95]KovalyovA.Analgorithmtoverifylivenessandboundednessinextendedfreechoicenets.In:Proc.the10thIEEEInternationalSymposiumonIntelligentControl,Monterey,California,USA,1995:591-601[Ke92]KemperP,Bausef.Anefficientpolynomial-timetodecidelivenessandboundednessoffree-choicenets.LectureNotesinComputerScience616,Springer,1992:263-278[Ji04]L.Jiao,T.Cheung,andW.Lu.OnLivenessandBoundednessofAsymmetricChoiceNets.InTheoreticalComputerScience,2004.[Mu89]MurataT.Petrinets:Properties,analysisandapplications.ProcoftheIEEE,1989,77(4):541-580[Aa00]W.vanderAalst.WorkflowVerification:FindingControl-FlowErrorsUsingPetri-Net-BasedTechniques.BusinessProcessManagements:Models,Techniques,andEmpiricalStudies2000.29ANetExamplet8t1t2t4t7t3t7t5s0s1s2s4s3s9s5s8s6s7N=(S,T,F)S={s0,…,s9}T={t1,…,t8}F={(s1,t1),(s0,t1),(s0,t2),(s2,t2),……(t5,s1),(t8,s0),(t7,s2)}棋盘,还需要说明什么?30MatrixRepresentationofaNetbeginsend_mailwrite_resttype_ma