| It has become a very important issue that how to improve the efficiency of software development, as the computer software progresses rapidly. Formulation technology has the benefits of reducing errors in early stage of software design, and shortening the duration of development. It also helps to improve the reliability of software and build a communication environment for developers. One of the most well-known formulation methods is Petri nets.Petri nets are crucial tools for formulation software and graphical representation, with advantages of intuitiveness, understandability and usability which make them suitable for the use of modeling and verifying discrete event systems with concurrent, asynchronous, parallel, uncertainness and randomness. The information of model structure and dynamic behavior can be given by verification and it can be used to promote system.This dissertation aims to present Petri nets abilities of modeling, verification, and application in routing algorithm and to tackle the limitations in the latest development. The main results of this research are as follows:First, based on the functional classifications of ordinary invisible tasks, the a# algorithm was proposed, which made use of several reasoning methods for the detection of invisible tasks and broke the blind section in mining techniques. To evaluate the proposed algorithm, a number of experiments were implemented based on artificial logs and real-life logs from corporations. A mining plug-in is integrated in open-source process mining framework named ProM. This dissertation also focuses on the modeling language. We defined a transformation between BPMN and YAWL which could clarify the ambiguous syntaxes of BPMN. At the same time, BPMN models can be analyzed by YAWL verification tools via mapping. The transformation benefits the improvement of BPMN specification.Second, by studying the various existing Petri nets reduction methods, a new logic algebra reduction algorithm based on logic circuit was proposed. The reduction operation unit was extended from element object to acyclic subnet. The major advantage of this algorithm lied in greater efficiency and broader reduction scope. Furthermore, structural and behavioral prosperities of Petri nets were investigated, especially on liveness (including structural liveness). A polynomial algorithm about minimal marking of structural live Petri nets was presented. In an empty marking net, it was verified that the reproducibility can be held under operations. These results can be used in process mining.Third, we presented a novel CDN infrastructure based on P2P. In combination with Petri nets and ant colonies algorithm, the optimized path routing algorithm was proposed. The experimental results demonstrated that the net was a general structure overlay network with high stability and robustness. |