Reachabillity analysis in T-invariant-less Petri nets

Abstract

An algorithm for reachability analysis in place/transition Petri nets having no transition invariants (T-invariants) is proposed. Given a Petri net with initial and 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 computation and investigation of those minimal-support and linearly combined T-invariants of the complemented Petri net, in which the complementary transition fires only once. Then, for each T-invariant with a single firing of the complementary transition, the algorithm will try to create a reachability path from the given initial marking to the target marking.