Optimizing Algebraic Petri Net Model Checking by Slicing

Yasir Imtiaz Khan, Matteo Risoldi

    Research output: Contribution to conferencePaperpeer-review


    High-level Petri nets make models more concise and readable
    as compared to low-level Petri nets. However, usual verification
    techniques such as state space analysis remain an open challenge for
    both because of state space explosion. The contribution of this paper is
    to propose an approach for property based reduction of the state space
    of Algebraic Petri nets (a variant of high-level Petri nets). To achieve
    the objective, we propose a slicing algorithm for Algebraic Petri nets
    (APNSlicing). The proposed algorithm can alleviate state space even for
    certain strongly connected nets and is proved not to increase the state
    space. We exemplify our technique through the running case study of car
    crash management system.
    Original languageEnglish
    Publication statusPublished - 2013
    EventInternational Workshop on Modeling and Business Environments ModBE'13 - Milano, Italy
    Duration: 24 Jun 201325 Jun 2013


    ConferenceInternational Workshop on Modeling and Business Environments ModBE'13
    Abbreviated titleModBE'13


    • High-level Petri nets
    • Model checking
    • Slicing


    Dive into the research topics of 'Optimizing Algebraic Petri Net Model Checking by Slicing'. Together they form a unique fingerprint.

    Cite this