A Novel Method for Reachability Determination in Petri Nets

Reachability is one of the most important behavioral properties of Petri nets and the past four decades have witnessed great efforts in developing various implementable methodologies in determining reachability of Petri nets. We propose in this paper a novel method for solving the fundamental equation in the reachability analysis, which has been known to be NP-complete. More specifically, by adopting a revised version of the cell enumeration method for an arrangement of hyperplanes in discrete geometry, we develop an efficient solution scheme to identify firing count vector solution(s) to the fundamental equation on a bounded integer set, with a complexity bound of O((nω)n–m), where n is the number of transitions, m is the number of places and ω is the upper bound of the number of firings for every transition.