Coming Home for Blocking Transitions Fast
摘要
Gaujal, Haar, and Mairesse proved in 2003 that every cluster in a live, bounded, free-choice Petri net system (i.e., transitions that share the same set of input places) has a blocking marking, i.e., a marking which enables only the transitions of the cluster. Moreover, for each cluster, this blocking marking is unique and reachable from every state of the system. In this paper, we study live, bounded, free-choice systems that, in addition, possess a home cluster, i.e., a cluster whose blocking marking only marks the places of the cluster. Prototypical examples are sound free-choice workflow nets, a commonly used subset of the standard model class in process mining. Our main result shows that in such systems, shortest firing sequences to blocking markings have linear length. Moreover, we obtain a quadratic upper bound on the length of shortest firing sequences between arbitrary markings once a home cluster is present. Both results strongly improve known bounds, as the best currently known bound is the cubic one of Desel and Esparza for general live, bounded, free-choice systems. Furthermore, we show that each transition can be enabled via an elementary firing sequence, i.e., a firing sequence which contains at most one transition per cluster. These insights might be of independent interest for future research on free-choice systems.