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

Fingerprint

Model checking
Petri nets
Explosions

Keywords

  • High-level Petri nets
  • Model checking
  • Slicing

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.

Optimizing Algebraic Petri Net Model Checking by Slicing. / Khan, Yasir Imtiaz; Risoldi, Matteo.

2013. 275 Paper presented at International Workshop on Modeling and Business Environments ModBE'13, Milano, Italy.

Research output: Contribution to conferencePaper

Khan, YI & Risoldi, M 2013, 'Optimizing Algebraic Petri Net Model Checking by Slicing' Paper presented at International Workshop on Modeling and Business Environments ModBE'13, Milano, Italy, 24/06/13 - 25/06/13, pp. 275.
Khan YI, Risoldi M. Optimizing Algebraic Petri Net Model Checking by Slicing. 2013. Paper presented at International Workshop on Modeling and Business Environments ModBE'13, Milano, Italy.
Khan, Yasir Imtiaz ; Risoldi, Matteo. / Optimizing Algebraic Petri Net Model Checking by Slicing. Paper presented at International Workshop on Modeling and Business Environments ModBE'13, Milano, Italy.
@conference{bb6f25dd0a674b69963ad7f9d8733d14,
title = "Optimizing Algebraic Petri Net Model Checking by Slicing",
abstract = "High-level Petri nets make models more concise and readableas compared to low-level Petri nets. However, usual verificationtechniques such as state space analysis remain an open challenge forboth because of state space explosion. The contribution of this paper isto propose an approach for property based reduction of the state spaceof Algebraic Petri nets (a variant of high-level Petri nets). To achievethe objective, we propose a slicing algorithm for Algebraic Petri nets(APNSlicing). The proposed algorithm can alleviate state space even forcertain strongly connected nets and is proved not to increase the statespace. We exemplify our technique through the running case study of carcrash management system.",
keywords = "High-level Petri nets, Model checking, Slicing",
author = "Khan, {Yasir Imtiaz} and Matteo Risoldi",
year = "2013",
language = "English",
pages = "275",
note = "International Workshop on Modeling and Business Environments ModBE'13, ModBE'13 ; Conference date: 24-06-2013 Through 25-06-2013",

}

TY - CONF

T1 - Optimizing Algebraic Petri Net Model Checking by Slicing

AU - Khan, Yasir Imtiaz

AU - Risoldi, Matteo

PY - 2013

Y1 - 2013

N2 - High-level Petri nets make models more concise and readableas compared to low-level Petri nets. However, usual verificationtechniques such as state space analysis remain an open challenge forboth because of state space explosion. The contribution of this paper isto propose an approach for property based reduction of the state spaceof Algebraic Petri nets (a variant of high-level Petri nets). To achievethe objective, we propose a slicing algorithm for Algebraic Petri nets(APNSlicing). The proposed algorithm can alleviate state space even forcertain strongly connected nets and is proved not to increase the statespace. We exemplify our technique through the running case study of carcrash management system.

AB - High-level Petri nets make models more concise and readableas compared to low-level Petri nets. However, usual verificationtechniques such as state space analysis remain an open challenge forboth because of state space explosion. The contribution of this paper isto propose an approach for property based reduction of the state spaceof Algebraic Petri nets (a variant of high-level Petri nets). To achievethe objective, we propose a slicing algorithm for Algebraic Petri nets(APNSlicing). The proposed algorithm can alleviate state space even forcertain strongly connected nets and is proved not to increase the statespace. We exemplify our technique through the running case study of carcrash management system.

KW - High-level Petri nets

KW - Model checking

KW - Slicing

M3 - Paper

SP - 275

ER -