A survey of petri nets slicing

Research output: Contribution to journalArticle

19 Downloads (Pure)

Abstract

Petri nets slicing is a technique that aims to improve the verification of systems modeled in Petri nets. Petri nets slicing was first developed to facilitate debugging, but then was used for the alleviation of the state space explosion problem for the model checking of Petri nets. In this article, different slicing techniques are studied along with their algorithms introducing: (i) a classification of Petri nets slicing algorithms based on their construction methodology and objective (such as improving state space analysis or testing); (ii) a qualitative and quantitative discussion and comparison of major differences such as accuracy and efficiency: (iii) a syntactic unification of slicing algorithms that improve state space analysis for easy and clear understanding; and (iv) applications of slicing for multiple perspectives. Furthermore, some recent improvements to slicing algorithms are presented, which can certainly reduce the slice size even for strongly connected nets. A noteworthy use of this survey is for the selection and improvement of slicing techniques for optimizing the verification of state event models.

Original languageEnglish
Article number109
Number of pages26
JournalACM Computing Surveys (CSUR)
Volume51
Issue number5
DOIs
Publication statusPublished - 23 Jan 2019

Fingerprint

Slicing
Petri nets
Petri Nets
State Space
Model checking
Syntactics
Explosions
Debugging
Unification
Slice
Explosion
Model Checking
Testing
Methodology

Bibliographical note

© ACM, 2018. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ACM Computing Surveys (CSUR), [VOL 51, ISS 5], (December 2018) http://doi.acm.org/10.1145/3241736

Copyright © and Moral Rights are retained by the author(s) and/ or other copyright owners. A copy can be downloaded for personal non-commercial research or study, without prior permission or charge. This item cannot be reproduced or quoted extensively from without first obtaining permission in writing from the copyright holder(s). The content must not be changed in any way or sold commercially in any format or medium without the formal permission of the copyright holders.

Keywords

  • Model checking
  • Petri nets
  • Slicing
  • Testing

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

A survey of petri nets slicing. / Khan, Yasir Imtiaz; Konios, Alexandros; Guelfi, Nicolas.

In: ACM Computing Surveys (CSUR), Vol. 51, No. 5, 109, 23.01.2019.

Research output: Contribution to journalArticle

@article{d758b0c3f1d841b1b9ec1d8984c4e5ba,
title = "A survey of petri nets slicing",
abstract = "Petri nets slicing is a technique that aims to improve the verification of systems modeled in Petri nets. Petri nets slicing was first developed to facilitate debugging, but then was used for the alleviation of the state space explosion problem for the model checking of Petri nets. In this article, different slicing techniques are studied along with their algorithms introducing: (i) a classification of Petri nets slicing algorithms based on their construction methodology and objective (such as improving state space analysis or testing); (ii) a qualitative and quantitative discussion and comparison of major differences such as accuracy and efficiency: (iii) a syntactic unification of slicing algorithms that improve state space analysis for easy and clear understanding; and (iv) applications of slicing for multiple perspectives. Furthermore, some recent improvements to slicing algorithms are presented, which can certainly reduce the slice size even for strongly connected nets. A noteworthy use of this survey is for the selection and improvement of slicing techniques for optimizing the verification of state event models.",
keywords = "Model checking, Petri nets, Slicing, Testing",
author = "Khan, {Yasir Imtiaz} and Alexandros Konios and Nicolas Guelfi",
note = "{\circledC} ACM, 2018. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ACM Computing Surveys (CSUR), [VOL 51, ISS 5], (December 2018) http://doi.acm.org/10.1145/3241736 Copyright {\circledC} and Moral Rights are retained by the author(s) and/ or other copyright owners. A copy can be downloaded for personal non-commercial research or study, without prior permission or charge. This item cannot be reproduced or quoted extensively from without first obtaining permission in writing from the copyright holder(s). The content must not be changed in any way or sold commercially in any format or medium without the formal permission of the copyright holders.",
year = "2019",
month = "1",
day = "23",
doi = "10.1145/3241736",
language = "English",
volume = "51",
journal = "ACM Computing Surveys",
issn = "0360-0300",
publisher = "ACM",
number = "5",

}

TY - JOUR

T1 - A survey of petri nets slicing

AU - Khan, Yasir Imtiaz

AU - Konios, Alexandros

AU - Guelfi, Nicolas

N1 - © ACM, 2018. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ACM Computing Surveys (CSUR), [VOL 51, ISS 5], (December 2018) http://doi.acm.org/10.1145/3241736 Copyright © and Moral Rights are retained by the author(s) and/ or other copyright owners. A copy can be downloaded for personal non-commercial research or study, without prior permission or charge. This item cannot be reproduced or quoted extensively from without first obtaining permission in writing from the copyright holder(s). The content must not be changed in any way or sold commercially in any format or medium without the formal permission of the copyright holders.

PY - 2019/1/23

Y1 - 2019/1/23

N2 - Petri nets slicing is a technique that aims to improve the verification of systems modeled in Petri nets. Petri nets slicing was first developed to facilitate debugging, but then was used for the alleviation of the state space explosion problem for the model checking of Petri nets. In this article, different slicing techniques are studied along with their algorithms introducing: (i) a classification of Petri nets slicing algorithms based on their construction methodology and objective (such as improving state space analysis or testing); (ii) a qualitative and quantitative discussion and comparison of major differences such as accuracy and efficiency: (iii) a syntactic unification of slicing algorithms that improve state space analysis for easy and clear understanding; and (iv) applications of slicing for multiple perspectives. Furthermore, some recent improvements to slicing algorithms are presented, which can certainly reduce the slice size even for strongly connected nets. A noteworthy use of this survey is for the selection and improvement of slicing techniques for optimizing the verification of state event models.

AB - Petri nets slicing is a technique that aims to improve the verification of systems modeled in Petri nets. Petri nets slicing was first developed to facilitate debugging, but then was used for the alleviation of the state space explosion problem for the model checking of Petri nets. In this article, different slicing techniques are studied along with their algorithms introducing: (i) a classification of Petri nets slicing algorithms based on their construction methodology and objective (such as improving state space analysis or testing); (ii) a qualitative and quantitative discussion and comparison of major differences such as accuracy and efficiency: (iii) a syntactic unification of slicing algorithms that improve state space analysis for easy and clear understanding; and (iv) applications of slicing for multiple perspectives. Furthermore, some recent improvements to slicing algorithms are presented, which can certainly reduce the slice size even for strongly connected nets. A noteworthy use of this survey is for the selection and improvement of slicing techniques for optimizing the verification of state event models.

KW - Model checking

KW - Petri nets

KW - Slicing

KW - Testing

UR - http://www.scopus.com/inward/record.url?scp=85061455838&partnerID=8YFLogxK

U2 - 10.1145/3241736

DO - 10.1145/3241736

M3 - Article

VL - 51

JO - ACM Computing Surveys

JF - ACM Computing Surveys

SN - 0360-0300

IS - 5

M1 - 109

ER -