Using Transition Invariants for Reachability Analysis of Petri Nets

A new approach to reachability analysis in general Petri nets is proposed, formally described, and illustrated by examples tested with a prototype program. For a given original Petri net, the reachability analysis is reduced to the computation and investigation of T-invariants of the complemented Petri net consisting of the original Petri net and an additional, complementary transition with input and output arcs depending on the given initial and target markings. It is shown that, without the loss of reachability information, one can carry out reachability analysis using only a finite number of T-invariants. We did not address, in this chapter, complexity aspects of the proposed approach to reachability analysis. Complexity of some problems of Petri nets, including the reachability problem, was investigated elsewhere (Jones et al., 1977). Most of the running time in the proposed reachability analysis scheme will be spent in computing minimal-support Tinvariants and their linear combinations, solving ILP problems, and trying to find legal firing sequences for the computed T-invariants. This can be done with the use of existing methods (Watanabe, 2000; Yamauchi & Watanabe, 1998; Huang & Murata, 1998).