The Algebric Method For Reachability Analysis Of Petri Nets

Reachability is one of the most basic and important dynamic properties of Petri nets and its decision problem plays an important role in Petri net theory. This paper majors in reachability analysis with algebraic method and the content is mainly composed of the following aspects:(1)Proposes the definition of nonreachability identification vectors of a marking and provide the computation method of two special kinds of nonreachability identification vectors.The first kind of identification vectors belongs to the S-invariants. In order to find it, several new algorithm to compute S-invariants is provided. In detail, STRK algorithm can find some minimal-support S-invariants in polynomial time complexity even though it cannot play its role sometimes. SRK algorithm can always find one minimal-support S-invariants at least provided that S-invariants exist, and the time complexity of which is polynomial on average. Except for the above two algorithms, ERK algorithm can find all the minimal-support S-invariants, and EERK algorithm can find all the minimal S-invariants.The second kind of identification vectors comes from Modular-S-invariants. As a foundation, the definition of elementary integral transformation and the method to factorize an integral matrix with elementary integral transformation is proposed firstly. After that, the problem how to find identification vectors in Modular-S-invariants is solved.(2) Introduces a method to decide whether or not the real solutions, the rational solutions, the integral solution and the nonnegative integral solution of state equation exist. After that, classify the nonreachable markings into several subclasses according to the relation among the state equation, S-invariants, Modular-S-invarants, siphons and traps when they are used to decide the nonreachability. Furthermore designs a new kind of algorithm to solve state equation.(3)Defines several new subclasses of Petri nets, including MTC Nets, TSIC Nets, MTSITC nets, MSC Nets, TSOC Nets and MTSOSC nets. And proves that reachability is equivalent to state equation satisfiability for the first four Petri net subclasses when there is no token-free circuit in the initial marking. As well for the other four subclasses when there is no token-free circuit in the destination marking.(4)Completes the proof of the equivalence between reachability and the satisfiability of reachability equation. And designs a new algorithm which can judge whether or not a given nonnegative integral vector corresponds to a friable trasition sequence. Then the algorithm is used to analyze the reachability of net system which has unique reachable vector or has no T-invariants.