Font Size: a A A

The Simulation And Verify Of Petri Nets

Posted on:2007-04-20Degree:MasterType:Thesis
Country:ChinaCandidate:J H YeFull Text:PDF
GTID:2178360182487068Subject:Computer software and theory
Abstract/Summary:
Petri Nets is widely applied in simulation and analysis discrete event systems because of it owns simple, intuitionistic, and the strong power of simulation. It has main characteristics, such as, parallel, nondetermination, asynchronism and the power of distributing and analysis. Liveness, boundness (always call N-safeness), home-state, justice are some basis properties of Petri Nets. From the beginning of the Petri Nets, the research about these properties is always activity. The researcher use some methods to analysis it, such as, coverability graphs, simple and abstract, invariants, synchronization and structural theory and so on. The algorithms about boundness Nets is always NP problems (always call The explosive in state space). The researches of our country and abroad are always pay more attention to the sub-classes on Petre Nets. They have given some well results, however, the results is short of application because of the particularity of sub-classes on Petri Nets. Our main works are basis on the general Nets.Starting from two aspects, simulation and verify by the structural analyse theory, simple and invariant technology are used in our works. And our research is in-depth and detailed to the simulation capability and the main properties of Petri Nets. We have had some new results include as follows:(1) The dining philosophers can be regarded as a representationalproblem in sharing resource cooperation, which perform the occurrence application program. It is a testing standard in evaluate synchronization methodological. Firstly, in the paper, it simulates the dining philosophers based on C/E systems, which has very well practicality background, because of conditions and events sets in C/E systems can achieved by switch or door circuit. Through the simulation of dining philosophers, there have a perfdct model which can be optional controlled by exterior conditions.(2) Recent ten years, more and more expert pay attention to the method based on S-invariant. The classical S-invariant always is used to explain and decide the properties of system, or analyse some concrete properties through determine the nature or quantitative analysis. The paper shows how to decide the structural liveness to the general Nets with the incidence matrix.(3) liveness is one of basic properties of Petri nets. A polynomial algorithm about minimal marking of structural live Petri nets is presented, it is based on incidence matrix and analysis the structure of transitions sequence.(4) Cyber nets are self-modifying nets. It is applied in concurrent program specification, the math modeling and industrial control. The nonlinear nature of the S-invariants and T-invariants of such nets keeps them away from application of known methods. The analysis mostly concerns on concrete systems. However, there have few literature on discussing its linear nature. Our approach extends the scopes of the invariants in cyber-nets and proposes a theorem.
Keywords/Search Tags:Petri Nets, Simulation, Verify, S-invariants, Structural theory
Related items