Research On Deadlock Detection-oriented Unfolding Of Unbounded Petri Nets

With the development of information technology,more and more distributed concurrent systems exhibit characteristics such as synchronism,concurrency,resource sharing and conflict.Deadlock has become a common phenomenon the above systems must face.Petri nets have an intuitive graphical representation and a solid mathematical analysis foundation,and thus are widely used in the modeling and analysis of distributed concurrent systems,especially in deadlock detection field.However,the state-space explosion has been obstructing the application of Petri nets.Net unfolding techniques can effectively solve the state explosion problem caused by concurrency.Existing unfolding techniques are only applicable to bounded Petri nets,and the unfolding-based deadlock detection method for bounded Petri nets is relatively mature.For unbounded Petri nets,existing unfolding methods can only determine boundedness and coverability property of net systems.Deadlock detection of unbounded Petri nets based on unfolding is still an open problem.To address the problem,this paper proposes a deadlock detection-oriented method for unbounded Petri nets.The main research contents are as follows:(1)A deadlock detection-oriented unfolding method toward unbounded Petri nets(D2U)is proposed..D2U has the following advantages over traditional ones in solving deadlock detection problems:Firstly,each configuration-corresponding cyclic or acyclic transition sequence in D2U is firable from the initial marking;Secondly,D2U can completely decide the existence of deadlocks when there is no ?--condition in D2U;Finally,D2U contains no spurious dead markings unlike traditional unfolding techniques of unbounded Petri nets.(2)D2U-based deadlock detection method is presented for unbounded Petri nets.Specifically,two deadlock detection methods are proposed:the first method can detect all deadlocks in D2U,but the efficiency is low.The second one can only determine the existence of deadlock in D2U and if there are deadlocks in D2U,it can only give one deadlock,but the efficiency is higher than the former.(3)AD2U software tool for unbounded Petri nets is designed and developed.We design and implement a D2U tool for unbounded Petri nets.When the input Petri net is bounded,the tool can output the finite complete prefix of the net system.When unbounded,the tool can output its D2U.In addition,combining with some specific examples,this work compares D2U,reachability trees and structural deadlock analysis methods of unbounded Petri nets.Their respective advantages and disadvantages are discussed.