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