Hierarchical high-level Petri nets have been proposed in recent years as a powerful formal method for modeling large concurrent and distributed systems, but they are even more difficult to analyze than fiat high-level Petri nets, which are also lacking effective analysis methods themselves. In this paper, a method for analyzing properties of hierarchical predicate transition Petri nets is proposed. The method employs two temporal induction techniques, one for safety properties and the other for liveness properties, without using temporal logic formalism. Within each induction technique, a hybrid reasoning technique combining net structural and behavioral reasoning, and ordinary first-order logic reasoning is used.
