Core Concepts
The authors generalize the concept of complete finite prefixes and the ERV-algorithm from low-level Petri nets to the symbolic unfoldings of a class of safe high-level Petri nets, where the guards are expressed in a decidable theory and the nets have finitely many reachable markings.
Abstract
The paper starts by recalling the definitions and formalism for high-level Petri nets and symbolic unfoldings from prior work. It then defines the class of safe high-level Petri nets, called NF, for which the authors generalize the construction of complete finite prefixes.
The key contributions are:
Lifting the concepts of completeness, adequate orders, and cut-off events to the level of symbolic unfoldings of high-level Petri nets. The authors show that for P/T nets interpreted as high-level nets, the generalized concepts coincide with their low-level counterparts.
Generalizing the ERV-algorithm to construct small complete finite prefixes of the symbolic unfoldings of high-level Petri nets in NF.
Identifying a more general class of "symbolically compact" high-level Petri nets, where the number of steps needed to reach all reachable markings is bounded, but the number of reachable markings may be infinite. The authors adapt the generalized ERV-algorithm to handle this class.
Presenting a prototype implementation of the generalized ERV-algorithm and evaluating it on four new benchmark families of high-level Petri nets.