Abstract
This work presents a non-Karp-Miller tree called a lean reachability tree (LRT). It does not try to equivalently represent but faithfully express in a finite manner the reachability set of an unbounded Petri net. First, we derive a sufficient and necessary condition of unbounded places and some incremental reachability properties to characterize unbounded nets. Then, we present a sufficiently enabling condition (SEC) and an LRT generation algorithm. No fake marking is produced and no legal marking is lost during the tree generation. We prove that LRT can represent faithfully the reachability set of an unbounded net in a finite manner. Also, we examine its properties and prove a sufficient condition for deadlock checking based on it. Our examples show that LRT outperforms the latest modified Karp-Miller trees in terms of size, expressiveness, and applicability.