Lower and upper bounds of shortest paths in reachability graphs

Abstract

We prove the following property for safe marked graphs, safe conflict-free Petri nets, and live and safe extended free-choice Petri nets. We prove the following three results. If the Petri net is a marked graph, then the length of the shortest path is at most (|T|−1)⋅|T|/2. If the Petri net is conflict free, then the length of the shortest path is at most (|T|+1)⋅|T|/2. If the petrinet is live and extended free choice, then the length of the shortest path is at most |T|⋅|T+1|⋅|T+2|/6, where T is the set of transitions of the net.