Lean Reachability Tree for Unbounded Petri Nets
针对无界Petri网，提出一种非Karp-Miller树的精简可达树生成算法，避免虚假标记并保留所有合法标记，在规模、表达力和适用性上优于现有改进树。
Elaborate efforts have been made to eliminate fake markings and refine ω-markings in the existing modified or improved Karp-Miller trees for various classes of unbounded Petri nets since the late 1980s. The main issues fundamentally are incurred due to the generation manners of the trees that prematurely introduce some potentially unbounded markings with ω symbols and keep their growth into new ones. Aiming at addressing them, this work presents a non-Karp-Miller tree called a lean reachability tree (LRT). First, a sufficient and necessary condition of the unbounded places and some reachability properties are established to reveal the features of unbounded nets. Then, we present an LRT generation algorithm with a sufficiently enabling condition (SEC). When generating a tree, SEC requires that the components of a covering node are not replaced by ω symbols, but continue to grow until any transition on an output path of an unbounded place has been branch-enabled at least once. In return, no fake marking is produced and no legal marking is lost during the tree generation. We prove that LRT can faithfully express by folding, instead of equivalently representing, the reachability set of an unbounded net. Also, some properties of LRT are examined and a sufficient condition of deadlock existence based on it is given. The case studies show that LRT outperforms the latest modified Karp-Miller trees in terms of size, expressiveness, and applicability. It can be applied to the analysis of the emerging discrete event systems with infinite states.