Nick Würdemann ; Thomas Chatain ; Stefan Haar ; Lukas Panneke - Taking Complete Finite Prefixes To High Level, Symbolically

fi:12578 - Fundamenta Informaticae, November 10, 2024, Volume 192, Issues 3-4: Petri Nets 2023
Taking Complete Finite Prefixes To High Level, SymbolicallyArticle

Authors: Nick Würdemann ; Thomas Chatain ; Stefan Haar ; Lukas Panneke

    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.


    Volume: Volume 192, Issues 3-4: Petri Nets 2023
    Published on: November 10, 2024
    Accepted on: August 19, 2024
    Submitted on: November 21, 2023
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Formal Languages and Automata Theory,F.m

    Consultation statistics

    This page has been seen 6 times.
    This article's PDF has been downloaded 4 times.