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