Lower and upper bounds of shortest paths in reachability graphs (Q1777827)

Summary: 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)\cdot|T|/{2}\). If the Petri net is conflict free, then the length of the shortest path is at most \((|T|+1)\cdot|T|/{2}\). If the petrinet is live and extended free choice, then the length of the shortest path is at most \(|T|\cdot|T+1|\cdot|T+2|/{6}\), where \(T\) is the set of transitions of the net.