Reachability analysis and simulation tools for high-level nets spend a significant amount of the computing time in performing
enabling tests, determining the assignments under which transitions are enabled. Unlike the majority of earlier work on computing
enabled transition bindings, the techniques presented in this paper are highly independent of the algebraic operations supported
by the high-level net formalism.
Performing enabling tests is viewed as a unification problem. A unification algorithm is presented and modifications to it
are suggested. One variant of the algorithm constructs finite unfoldings for nets with unbounded domains. Some heuristics
for optimising the enabling tests are discussed and their usefulness is evaluated based on experiments. The algorithms have
been implemented in the reachability analyser Maria.
Keywords high-level Petri nets - reachability analysis - unification - unfolding