A slicing-based approach to enhance Petri net reachability analysis

W. J. Lee, H. N. Kim, Sungdeok Cha, Y. R. Kwon

Research output: Contribution to journalArticle

12 Citations (Scopus)

Abstract

Reachability graph analysis is one of the most widely used techniques to verify the behaviour of asynchronous and concurrent systems modeled in Petri nets. Unfortunately, a state explosion problem is often the bottleneck when applying Petri net modeling and analysis to large and complex industrial systems. This paper proposes an approach in which Petri net slices are computed based on structural concurrency inherent in the P/T net and compositional reachability graph analysis is performed. Petri net slices are proven to provide behavioural equivalence to P/T nets. This approach may enable verification of properties such as boundedness and liveness which may fail on unsliced P/T nets due to a state explosion problem. Effectiveness and scalability of our approach is demonstrated using both dining philosophers and feature interaction problems found in telecommunication software. Copyright

Original languageEnglish
Pages (from-to)131-143
Number of pages13
JournalJournal of Research and Practice in Information Technology
Volume32
Issue number2
Publication statusPublished - 2000 Dec 1
Externally publishedYes

Fingerprint

Petri nets
Explosions
Telecommunication
Scalability
Explosion
Graph

Keywords

  • Compositional analysis
  • Petri net Slice
  • Petri nets
  • Place/Transition nets
  • Reachability analysis
  • Structural concurrency

ASJC Scopus subject areas

  • Information Systems
  • Computer Graphics and Computer-Aided Design
  • Software

Cite this

A slicing-based approach to enhance Petri net reachability analysis. / Lee, W. J.; Kim, H. N.; Cha, Sungdeok; Kwon, Y. R.

In: Journal of Research and Practice in Information Technology, Vol. 32, No. 2, 01.12.2000, p. 131-143.

Research output: Contribution to journalArticle

@article{510b83407f30462bb978258fc6a5c28a,
title = "A slicing-based approach to enhance Petri net reachability analysis",
abstract = "Reachability graph analysis is one of the most widely used techniques to verify the behaviour of asynchronous and concurrent systems modeled in Petri nets. Unfortunately, a state explosion problem is often the bottleneck when applying Petri net modeling and analysis to large and complex industrial systems. This paper proposes an approach in which Petri net slices are computed based on structural concurrency inherent in the P/T net and compositional reachability graph analysis is performed. Petri net slices are proven to provide behavioural equivalence to P/T nets. This approach may enable verification of properties such as boundedness and liveness which may fail on unsliced P/T nets due to a state explosion problem. Effectiveness and scalability of our approach is demonstrated using both dining philosophers and feature interaction problems found in telecommunication software. Copyright",
keywords = "Compositional analysis, Petri net Slice, Petri nets, Place/Transition nets, Reachability analysis, Structural concurrency",
author = "Lee, {W. J.} and Kim, {H. N.} and Sungdeok Cha and Kwon, {Y. R.}",
year = "2000",
month = "12",
day = "1",
language = "English",
volume = "32",
pages = "131--143",
journal = "Journal of Research and Practice in Information Technology",
issn = "1443-458X",
publisher = "Australian Computer Society",
number = "2",

}

TY - JOUR

T1 - A slicing-based approach to enhance Petri net reachability analysis

AU - Lee, W. J.

AU - Kim, H. N.

AU - Cha, Sungdeok

AU - Kwon, Y. R.

PY - 2000/12/1

Y1 - 2000/12/1

N2 - Reachability graph analysis is one of the most widely used techniques to verify the behaviour of asynchronous and concurrent systems modeled in Petri nets. Unfortunately, a state explosion problem is often the bottleneck when applying Petri net modeling and analysis to large and complex industrial systems. This paper proposes an approach in which Petri net slices are computed based on structural concurrency inherent in the P/T net and compositional reachability graph analysis is performed. Petri net slices are proven to provide behavioural equivalence to P/T nets. This approach may enable verification of properties such as boundedness and liveness which may fail on unsliced P/T nets due to a state explosion problem. Effectiveness and scalability of our approach is demonstrated using both dining philosophers and feature interaction problems found in telecommunication software. Copyright

AB - Reachability graph analysis is one of the most widely used techniques to verify the behaviour of asynchronous and concurrent systems modeled in Petri nets. Unfortunately, a state explosion problem is often the bottleneck when applying Petri net modeling and analysis to large and complex industrial systems. This paper proposes an approach in which Petri net slices are computed based on structural concurrency inherent in the P/T net and compositional reachability graph analysis is performed. Petri net slices are proven to provide behavioural equivalence to P/T nets. This approach may enable verification of properties such as boundedness and liveness which may fail on unsliced P/T nets due to a state explosion problem. Effectiveness and scalability of our approach is demonstrated using both dining philosophers and feature interaction problems found in telecommunication software. Copyright

KW - Compositional analysis

KW - Petri net Slice

KW - Petri nets

KW - Place/Transition nets

KW - Reachability analysis

KW - Structural concurrency

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

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

M3 - Article

VL - 32

SP - 131

EP - 143

JO - Journal of Research and Practice in Information Technology

JF - Journal of Research and Practice in Information Technology

SN - 1443-458X

IS - 2

ER -