Efficient methods for verification and performance evaluation of concurrent systems by Petri nets

Petri nets are an efficient and powerful formal tool for modeling, analysis and synthesis of asynchronous, distributed systems with concurrency. Petri nets combine convenient modular graphical representation with mathematical formalism and possess such qualities as generality, simplicity and formality. They have a developed theory of analysis and synthesis.; Here we consider verification of concurrent system correctness. Correctness qualities can be classified into two groups: semantical and syntactical. Semantical qualities rely on specifics of the particular application field. Syntactical qualities are more generic. They can be defined without knowing the specific purpose of the system. Here correctness is considered as a syntactical quality. The correctness of the system can be expressed in terms of the behavioral properties of a Petri net modeling the system. Two major behavioral properties are commonly used for the definition of correctness of concurrent systems. They are liveness (the absence of partial and global deadlocks) and boundedness (the absence of overflows in finite stores). The developed universal methods for analyzing these properties face the state explosion problem. Actually, the main weakness of Petri nets is the complexity problem. The objectives of the thesis are the creation of efficient methods and algorithms for verification of concurrent systems.; We develop a set of simple local reduction rules for Extended Free Choice Petri nets. We give a complete reduction method for regular Petri nets and estimate its complexity as O(|S| × |T|).; We develop an O(|S| × | T|)-algorithm to decide if a given Extended Free Choice Petri net is live and bounded, which is a reduction by one order of magnitude, compared to the previous algorithm (O(|S| 2 × |T|)). We present an O(| S| × |T|)-algorithm to decide if a given Petri net is regular.; We prove several Rank Theorems for Extended Free Choice and general class of Petri nets and show that they can be used as an alternative technique for the verification of workflow procedures.; We propose a cubic algorithm for the computation of the concurrency relation of Live and Bounded Extended Free-Choice Petri nets. Prior to this work the problem was shown to be polynomial only for live Marked Graphs and 1-bounded Conflict-Free Petri nets. We generalize the previous algorithm for Free-Choice Petri nets, to regular Petri nets. The time complexity of the algorithm is O(n4), where n is the number of nodes in the net.; In [46] we propose polynomial algorithms for performance evaluation of communication networks using stochastic Petri nets. We used theoretical results and polynomial algorithms from [13, 19, 20, 57] for quantitative analysis of stochastic Petri nets.