Towards Reachability Trees for High-level Petri Nets

High-level Petri nets have been introduced as a powerful net type, by which it is possible to handle rather complex systems in a succinct and manageable way. The success of high-level Petri nets is undebatable when we speak about description, but there is still much work to be done to establish the necessary analysis methods. It has already been shown how to generalize the concept of place-invariants and transition-invariants, from place-transition-nets to high-level Petri nets. Our present paper constitutes the first steps towards a generalization of reachability trees, which is one of the other important analysis methods known for PT-nets. The central idea in our paper is the observation, that HL-nets often possess classes of equivalent markings. As an example an HL-net describing the five dining philo\-sophers has an equivalence-class consisting of those five markings in which exactly one philosopher is eating. These five markings are interchangeable, in the sense that their subtrees represent equivalent behaviours, where the only difference is the identity of the involved philosophers and forks. If we analyze one of these subtrees, we also understand the behaviour of the others. We describe an algorithm which constructs the HL-tree. The algorithm can easily be automated and we will soon start the work on an implementation. The constructed HL-trees turn out to be considerably smaller than the corresponding PT-trees (reachability trees for the equivalent PT-nets).