Analysis of Unbounded Petri Net With Lean Reachability Trees

At present, no efficient method is proposed for the liveness analysis of general unbounded Petri nets (UPNs) except some of their subclasses. Our previous work presents a non-Karp-Miller finite reachability tree, i.e., lean reachability tree (LRT) to represent their markings. It faithfully expresses and folds the reachability set of an unbounded net. It can totally avoid the efforts made by the ex...