Basis Marking Representation of Petri Net Reachability Spaces and Its Application to the Reachability Problem

In this paper, a compact representation of the reachability graph of a Petri net is proposed. The transition set of a Petri net is partitioned into the subsets of explicit and implicit transitions in such a way that the subnet induced by implicit transitions does not contain directed cycles. The firing of implicit transitions can be abstracted so that the reachability set of the net can be completely characterized by a subset of reachable markings called basis makings. We show that to determine a max-cardinality-TI basis partition is an NP-hard problem, but a max-set-TI basis partition can be determined in polynomial time. The generalized version of the marking reachability problem in a Petri net can be solved by a practically efficient algorithm based on the basis reachability graph. Finally, this approach is further extended to unbounded nets.