Research On The State Space Explosion Problems Of Petri Nets Based On The Partial Order Reduction Methods

Nowadays,concurrent systems such as resource allocation systems,robot systems,network communication systems,and traffic control systems widely exist in all walks of life.Petri nets,as a formalized modeling tool,can effectively describe and analyze concurrent systems.By using Petri nets to verify the performance of concurrent systems,the state space exploration(or reachability analysis)method is usually adopted,which has great practical value in analyzing various properties of Petri nets,such as liveness,safeness and boundedness.Unfortunately,there is a main obstacle for the application of this method,which is the state space explosion problem.This problem arises since the number of reachable states(or markings)grows exponentially with the increase of the size of Petri nets,which greatly limits the application of Petri nets in large and complex systems.The partial order reduction techniques have been proven to be the most successful strategies for alleviating the state space explosion problem in practice.Unfortunately,the existing partial order reduction techniques are not mature enough and the size of state space of concurrent systems still needs further reduction.Meanwhile,little progress has been made so far on properties analysis of systems based on reduced state graphs.Thus,on the basis of the partial order reduction methods,we study how to further mitigate the state space explosion and how to utilize reduced state graphs to verify the liveness of Petri nets.The major contributions of this work are listed as follows:1.A new definition of sound steps is proposed,which provides a strong theoretical support for the further reduction of state space;2.We propose a sufficient condition about how to find the set of sound steps at each state,which is of practical significance;3.Combining the persistent sets with sound steps,a new definition of good steps is introduced.Based on the concept of good steps,an algorithm for constructing a maximal goodstep graph is established.Compared with the existing partial order reduction techniques,the firing of a good step at each marking enables to extremely reduce the state space;4.We propose a new method about utilizing the proposed maximal good step graphs to analyze the liveness of Petri nets,it has been proven that the liveness of Petri nets can still be verified via the reduced state graphs rather than the whole reachability graphs.This method avoids the state space explosion problem,and the calculation efficiency is also improved compared with other methods of liveness analysis based on reachability graphs.Finally,conclusions and future work on alleviating the state space explosion problem and analyzing the liveness of Petri nets are illustrated.