Reachability trees for high-level Petri nets

Reviewer: Daniel P. Bovet

High-level Petri nets (HL-nets) have been introduced to handle rather complex systems in a succinct and manageable way, although there is still much work to be done in order to establish the necessary analysis methods. A method is proposed to derive finite reachability trees for HL-nets: the reduction is obtained by means of covering markings (introducing &ohgr;-symbols) and duplicate markings (cutting away subtrees). Once the tree has been derived in a proper way, several properties of the system (bounded net, no dead reachable marking, etc.) can be shown by making use of four proof rules for HL-trees. The proposed method relies heavily on the notion of equivalent &ohgr;-markings; this concept, in turn, implies a symmetry among sets of markings. Although the authors show how to derive such symmetry on a few simple examples, neither a general algorithm nor any upper bound on the execution time of such an algorithm is given.