Optimizing Algebraic Petri Net Model Checking by Slicing

Yasir Imtiaz Khan, Matteo Risoldi

Research output: Contribution to conferencePaper

1 Citation (Scopus)

Abstract

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
Pages275
Publication statusPublished - 2013
EventInternational Workshop on Modeling and Business Environments ModBE'13 - Milano, Italy
Duration: 24 Jun 201325 Jun 2013

Conference

ConferenceInternational Workshop on Modeling and Business Environments ModBE'13
Abbreviated titleModBE'13
CountryItaly
CityMilano
Period24/06/1325/06/13

Keywords

  • High-level Petri nets
  • Model checking
  • Slicing

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

  • Cite this

    Khan, Y. I., & Risoldi, M. (2013). Optimizing Algebraic Petri Net Model Checking by Slicing. 275. Paper presented at International Workshop on Modeling and Business Environments ModBE'13, Milano, Italy.