A reachability algorithm for general Petri nets based on transition invariants

Abstract

A new reachability algorithm for general Petri nets is proposed. Given a Petri net with an initial and a target markings, a so called complemented Petri net is created first that consists of the given Petri net and an additional, complementary transition. Thereby, the reachability task is reduced to calculation and investigation of transition invariants (T-invariants) of the complemented Petri net. The algorithm finds all minimal-support T-invariants of the complemented Petri net and then calculates a finite set of linear combinations of minimal-support T-invariants, in which the complementary transition fires only once. Finally, for each T-invariant with a single firing of the complementary transition, the algorithm tries to create a reachability path from initial to target marking or determines that there is no such path.