Structural model abstraction is a powerful technique for reducing the
complexity of a state based enumeration analysis.We present in this paper accurate
reductions for high-level Petri nets based on new ordinary Petri nets reductions.
These reductions involve only structural and algebraical conditions. They preserve
the liveness of the net and any LTL formula that does not observe the reduced
transitions of the net. The mixed use of structural and algebraical conditions
signi cantly enlarges their application area. Furthermore the speci cation of the
transformation is parametric with respect to the cardinalities of coloured domains.
