Shortest Paths in Reachability Graphs

摘要

We prove the following property for safe marked graphs, safe conflict-free Petri nets, and live and safe extended free-choice Petri nets: Given two markings M1, M2 of the reachability graph, if some path leads from M1 to M2, then some path of polynomial length in the number of transitions of the net leads from M1 to M2.