Computation of K-reachable paths in Petri nets

The enumeration of legal transition paths leading to a target state (or set of states) is of paramount importance in the control of discrete event systems, but is hindered by the state explosion problem. A method is proposed in this paper, in the context of Petri nets, to calculate and enumerate firing count vectors for which there exists at least an admissible transition sequence leading to a given target marking. The method is based on the concept of singular complementary transition invariants proposed by Kostin and combines an integer linear programming formulation that finds the shortest minimal solution and a branching procedure that effects a partition of the solution set. The enumeration can be restricted to minimal solutions or extended to non-minimal ones. Some analytical examples are discussed in detail to show the effectiveness of the proposed approach.