Liveness Analysis of ω -Independent Petri Nets Based on New Modified Reachability Trees

Ru Yang, Zhijun Ding, Meiqin Pan, Changjun Jiang, Mengchu Zhou

Research output: Contribution to journalArticlepeer-review

7 Scopus citations

Abstract

Liveness of Petri nets means all activities in a modeled system can potentially take place and thus implies deadlock freedom. The research on liveness analysis approaches is inadequate. This paper proposes a liveness judgment reachability graph (LJRG) approach to analyze the liveness of ω -independent Petri nets. Such nets can be loosely explained as a class of unbounded Petri nets in which the changes of tokens in unbounded places are not related to each other. This paper proposes several algorithms to transform a new modified reachability tree to a new modified reachability graph and then transform it to an LJRG. It then develops the application of LJRG into the liveness analysis of ω -independent unbounded Petri nets. The proposed method provides a new theoretical method and important tool for the liveness analysis of unbounded Petri nets. It is illustrated via some examples.

Original languageEnglish (US)
Article number7457700
Pages (from-to)2601-2612
Number of pages12
JournalIEEE Transactions on Systems, Man, and Cybernetics: Systems
Volume47
Issue number9
DOIs
StatePublished - Sep 2017

All Science Journal Classification (ASJC) codes

  • Software
  • Control and Systems Engineering
  • Human-Computer Interaction
  • Computer Science Applications
  • Electrical and Electronic Engineering

Keywords

  • Discrete event systems
  • liveness
  • reachability graph (RG)
  • unbounded Petri net
  • ω-independent Petri net

Fingerprint

Dive into the research topics of 'Liveness Analysis of ω -Independent Petri Nets Based on New Modified Reachability Trees'. Together they form a unique fingerprint.

Cite this