Constructing Complete Finite Prefixes of Symbolic Unfoldings for Safe High-level Petri Nets

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.