Petri net is an important tool to model and analyze concurrent systems,but Petri net models are frequently large and complex,and difficult to understand and modify.Slicing is a technique to remove unnecessary parts wi...Petri net is an important tool to model and analyze concurrent systems,but Petri net models are frequently large and complex,and difficult to understand and modify.Slicing is a technique to remove unnecessary parts with respect to a criterion for analyzing programs,and has been widely used in specification level for model reduction,but researches on slicing of Petri nets are still limited.According to the idea of program slicing,this paper extends slicing technologies of Petri nets to four kinds of slices,including backward static slice,backward dynamic slice,forward static slice and forward dynamic slice.Based on the structure properties,the algorithms of obtaining two kinds of static slice are constructed.Then,a new method of slicing backward dynamic slice is proposed based on local reachability graph which can locally reflect the dynamic properties of Petri nets.At last,forward dynamic slice can be obtained through the reachability marking graph under a special marking.The algorithms can be used to reduce the size of Petri net,which can provide the basic technical support for simplifying the complexity of formal verification and analysis.展开更多
基金Supported by the National Natural Science Foundation of China(No.90818023)the National Basic Research Program of China(No.2010CB328101)+2 种基金Shanghai Science&Technology Research Plan(No.09JC1414200,09510701300)"Dawn"Program of Shanghai Education Commission,Program for Changjiang Scholars and Innovative Research Team in University(PCSIRT),National Major Projects of Scienceand Technology(No.2009ZX01036-001-002:part 5)Natural Science Foundation of Educational Government of Anhui Province(No.KJ2011A086)
文摘Petri net is an important tool to model and analyze concurrent systems,but Petri net models are frequently large and complex,and difficult to understand and modify.Slicing is a technique to remove unnecessary parts with respect to a criterion for analyzing programs,and has been widely used in specification level for model reduction,but researches on slicing of Petri nets are still limited.According to the idea of program slicing,this paper extends slicing technologies of Petri nets to four kinds of slices,including backward static slice,backward dynamic slice,forward static slice and forward dynamic slice.Based on the structure properties,the algorithms of obtaining two kinds of static slice are constructed.Then,a new method of slicing backward dynamic slice is proposed based on local reachability graph which can locally reflect the dynamic properties of Petri nets.At last,forward dynamic slice can be obtained through the reachability marking graph under a special marking.The algorithms can be used to reduce the size of Petri net,which can provide the basic technical support for simplifying the complexity of formal verification and analysis.
