Affiliations: [a] Department of Computing Science, University of Oldenburg, Oldenburg, Germany. wuerdemann@informatik.uni-oldenburg.de
| [b] Université Paris-Saclay, INRIA and LMF, CNRS and ENS Paris-Saclay, Gif-sur-Yvette, France. thomas.chatain@inria.fr
| [c] Université Paris-Saclay, INRIA and LMF, CNRS and ENS Paris-Saclay, Gif-sur-Yvette, France. stefan.haar@inria.fr
| [d] Department of Computing Science, University of Oldenburg, Oldenburg, Germany. lukas.panneke@informatik.uni-oldenburg.de
Correspondence:
[*]
Address for correspondence: Department of Computing Science, University of Oldenburg, Oldenburg, Germany
Note: [*] This is a revised and extended version of the article [1] that is published in the Proceedings of PETRI NETS 2023.
Abstract: 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.
Keywords: Petri Nets, High-level Petri Nets, Unfoldings, Concurrency Theory
