Tools for state space exploration, or reachability analysers, work by incrementally constructing a set of reachable states. The applicability of these tools is limited by the vast state space of real systems. One way to attack this problem are different reduction methods - another approach is to come up with techniques for representing the set of reachable states in a compact way.
The state - or marking - of a high-level Petri net can be viewed as a sequence of finite multi-sets. A method for encoding markings containing structured values is described, and a comparison to an earlier implementation is presented.