| Legal firing sequence (LFS for short) is a sub-problem of reachability of Petri Nets. It is in fact a process of verificating the executability of a n-vector of non-negative integer X. An algorithm is presented to solve LFS of bounded Petri Nets in the thesis.The precondition of algorithm presented in this paper is theory of transition sequence decomposition. It is given in chapter three and four. The feasibility of decomposition of transition firing sequence, the application of them in the detecting LFS and the reverse course of decomposition-synthesis are discussed. They provide theoretic basis for our algorithm in the field of Petri Net.Supported by the above, two main part is included in the algorithm:At first, X is transacted according to the following method in order to get a set of Xb named as basic vector of X which is the firing count vector of a directed path without circle if Md is reached from M0 in the RG(M0). The max value among all sums of each non-zero entry of Xb is noted down preparing for using as of the terminal condition of the second part. At the same time, problem of detecting LFS of X is changed into problem of detecting of Xb.In the second part of algorithm, a partial reachability tree RT (∑1) of bounded Petri Net ∑1 = (S,T;F,M0) and a partial reverse reachability tree RT'(∑2)of bounded Petri Net ∑2 =(S,T;F,Md)are constructed. Common marking M' appearing in RT'(∑1) and RT(∑2) is searched simultaneously. If marking satisfying the requirement is found, the algorithm finishes in a success result. Otherwise, the algorithm ended with conclusion of no LFS.
|
PDF Full Text Request