{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T14:28:31Z","timestamp":1777645711517,"version":"3.51.4"},"reference-count":0,"publisher":"SAGE Publications","issue":"3-4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["FI"],"published-print":{"date-parts":[[2024,9,20]]},"abstract":"<jats:p>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\u2019s 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.<\/jats:p>","DOI":"10.3233\/fi-242196","type":"journal-article","created":{"date-parts":[[2024,9,20]],"date-time":"2024-09-20T10:33:01Z","timestamp":1726828381000},"page":"313-361","source":"Crossref","is-referenced-by-count":0,"title":["Taking Complete Finite Prefixes To High Level, Symbolically*"],"prefix":"10.1177","volume":"192","author":[{"given":"Nick","family":"W\u00fcrdemann","sequence":"first","affiliation":[{"name":"Department of Computing Science, University of Oldenburg, Oldenburg, Germany. wuerdemann@informatik.uni-oldenburg.de"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Chatain","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Saclay, INRIA and LMF, CNRS and ENS Paris-Saclay, Gif-sur-Yvette, France. thomas.chatain@inria.fr"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Haar","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Saclay, INRIA and LMF, CNRS and ENS Paris-Saclay, Gif-sur-Yvette, France. stefan.haar@inria.fr"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lukas","family":"Panneke","sequence":"additional","affiliation":[{"name":"Department of Computing Science, University of Oldenburg, Oldenburg, Germany. lukas.panneke@informatik.uni-oldenburg.de"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","container-title":["Fundamenta Informaticae"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/FI-242196","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T06:33:03Z","timestamp":1777444383000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/FI-242196"}},"subtitle":[],"editor":[{"given":"Robert","family":"Lorenz","sequence":"additional","affiliation":[],"role":[{"role":"editor","vocabulary":"crossref"}]},{"given":"S\u0142awomir","family":"Lasota","sequence":"additional","affiliation":[],"role":[{"role":"editor","vocabulary":"crossref"}]}],"short-title":[],"issued":{"date-parts":[[2024,9,20]]},"references-count":0,"journal-issue":{"issue":"3-4"},"URL":"https:\/\/doi.org\/10.3233\/fi-242196","relation":{},"ISSN":["0169-2968","1875-8681"],"issn-type":[{"value":"0169-2968","type":"print"},{"value":"1875-8681","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,20]]}}}