Research On Refinement And Semantic Equivalence Of Process Net

Process Net is a novel petri net model with a combination of process algebra and petri net theory. We use process net system model in practical applications, when the system is too complicated, node explosion problem will be encountered, at this moment, it is necessary to introduce process net with hierarchy. This paper presents a process net with hierarchical structure, gives the hierarchical model and modeling algorithm. It solves large, complex systems modeling, settles space explosion problems. It can clearly reflect the level of model, so as to facilitate the process net refinement to obtain the accurate model, also easily use stepwise refinement, top-down approach to complete modeling of the simulate system, it can help users to achieve a variety of size simulation services.Using Process Net to model, the initial model is rough. In order to establish an accurate abstract modeling of system, reduce the complexity of large systems modeling and analysis, refinement of Process Net is proposed. Refinement of Process Net is forming more detailed subnets by replacing some of the single components (such Transition) at a higher level of abstraction. This paper defines five refinement rules based on Process Net:subnet refinement, synchronization refinement, selection refinement, loop refinement, communication refinement rules. It implements hierarchical refinement based on hierarchical Process Net. Experimental results show that the refinement of Process Net reflects hierarchies of modeling. It provides an effective method for complex system simulation. Refinement is helpful to analyze system abstract model, solve the state space explosion problem and improve the descriptive ability of Process Net modeling.We study the verification methods of Process Net semantic equivalence. It was divided into semantic equivalence and semantic equivalence preservation. According to the definition of soundness and sufficient and necessary condition of soundness. We verify the Soundness of refinement rules. Analyzing the reachability graph of refinement rules to illustrate some properties preserving of process net. Depending on the definition of bisimulation to verify the rules on weak bisimulation and strong bisimulation. Finally, we build the model of booking system. Experimental results show that the hierarchical selecting and refinement of process network can be achieved. It also reflects the process net’s hierarchy clearly.