As a powerful analysis tool of Petri nets, reachability trees are fundamental for systematically investigating many characteristics such as boundedness, liveness and reversibility.This work proposes a method to genera...As a powerful analysis tool of Petri nets, reachability trees are fundamental for systematically investigating many characteristics such as boundedness, liveness and reversibility.This work proposes a method to generate a reachability tree,called ω RT for short, for a class of unbounded generalized nets called ω-independent nets based on new modified reachability trees(NMRTs). ω RT can effectively decrease the number of nodes by removing duplicate and ω-duplicate nodes in the tree, and verify properties such as reachability, liveness and deadlocks.Two examples are provided to show its superiority over NMRTs in terms of tree size.展开更多
基金supported by National Natural Science Foundation of China(61374148,61472361,61374005)Natural Science Foundation of Zhejiang Province(LY15F030003,LY15F030002,LR14F020001)+3 种基金the National Science Foundation of USA(CMMI-1162482)the Opening Project of State Key Laboratory for Manufacturing Systems Engineering(sklms2014011)Zhejiang NNST Key Laboratory(2015C31064)the State Scholarship Fund of China
文摘As a powerful analysis tool of Petri nets, reachability trees are fundamental for systematically investigating many characteristics such as boundedness, liveness and reversibility.This work proposes a method to generate a reachability tree,called ω RT for short, for a class of unbounded generalized nets called ω-independent nets based on new modified reachability trees(NMRTs). ω RT can effectively decrease the number of nodes by removing duplicate and ω-duplicate nodes in the tree, and verify properties such as reachability, liveness and deadlocks.Two examples are provided to show its superiority over NMRTs in terms of tree size.
