Unfoldings are a well known partial-order semantics of P/T Petri nets that can be applied to various model checking or verification problems. For high-level Petri nets, the so-called symbolic unfolding generalizes this notion. A complete finite prefix of a P/T Petri net's unfolding contains all information to verify, e.g., reachability of markings. We unite these two concepts and define complete finite prefixes of the symbolic unfolding of high-level Petri nets. For a class of safe high-level Petri nets, we generalize the well-known algorithm by Esparza et al. for constructing small such prefixes. We evaluate this extended algorithm through a prototype implementation on four novel benchmark families. Additionally, we identify a more general class of nets with infinitely many reachable markings, for which an approach with an adapted cut-off criterion extends the complete prefix methodology, in the sense that the original algorithm cannot be applied to the P/T net represented by a high-level net.

翻译：展开是一种著名的P/T Petri网的偏序语义，可应用于各类模型检验或验证问题。对于高层次Petri网，所谓的符号化展开推广了这一概念。P/T Petri网展开的完整有限前缀包含验证标记可达性等所需的所有信息。我们将这两个概念统一起来，定义了高层次Petri网符号化展开的完整有限前缀。针对一类安全的高层次Petri网，我们推广了Esparza等人提出的经典算法，用于构造此类小型前缀。我们通过原型实现，在四个新型基准测试族上评估了这一扩展算法。此外，我们识别出具有无穷多个可达标记的更广泛网类，对于该类网，采用自适应截断准则的方法扩展了完整前缀方法学——从原始算法无法应用于高层次网所表示的P/T Petri网这一意义上而言。