Lean Reachability Tree for Unbounded Petri Nets

Jun Li, Xiaolong Yu, Meng Chu Zhou, Xianzhong Dai

Research output: Contribution to journalArticlepeer-review

9 Scopus citations

Abstract

Elaborate efforts have been made to eliminate fake markings and refine ω -markings in the existing modified or improved Karp-Miller trees for various classes of unbounded Petri nets since the late 1980s. The main issues fundamentally are incurred due to the generation manners of the trees that prematurely introduce some potentially unbounded markings with ω symbols and keep their growth into new ones. Aiming at addressing them, this work presents a non-Karp-Miller tree called a lean reachability tree (LRT). First, a sufficient and necessary condition of the unbounded places and some reachability properties are established to reveal the features of unbounded nets. Then, we present an LRT generation algorithm with a sufficiently enabling condition (SEC). When generating a tree, SEC requires that the components of a covering node are not replaced by ω symbols, but continue to grow until any transition on an output path of an unbounded place has been branch-enabled at least once. In return, no fake marking is produced and no legal marking is lost during the tree generation. We prove that LRT can faithfully express by folding, instead of equivalently representing, the reachability set of an unbounded net. Also, some properties of LRT are examined and a sufficient condition of deadlock existence based on it is given. The case studies show that LRT outperforms the latest modified Karp-Miller trees in terms of size, expressiveness, and applicability. It can be applied to the analysis of the emerging discrete event systems with infinite states.

Original languageEnglish (US)
Article number7513384
Pages (from-to)299-308
Number of pages10
JournalIEEE Transactions on Systems, Man, and Cybernetics: Systems
Volume48
Issue number2
DOIs
StatePublished - Feb 2018

All Science Journal Classification (ASJC) codes

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

Keywords

  • Complex systems
  • Petri nets (PNs)
  • complexity
  • deadlock
  • discrete event systems
  • liveness
  • modeling and analysis
  • reachability tree
  • unboundedness

Fingerprint

Dive into the research topics of 'Lean Reachability Tree for Unbounded Petri Nets'. Together they form a unique fingerprint.

Cite this