Lean reachability tree for Petri net analysis

Jun Li, Xiaolong Yu, Mengchu Zhou

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

Abstract

This work presents a non-Karp-Miller tree called a lean reachability tree (LRT). It does not try to equivalently represent but faithfully express in a finite manner the reachability set of an unbounded Petri net. First, we derive a sufficient and necessary condition of unbounded places and some incremental reachability properties to characterize unbounded nets. Then, we present a sufficiently enabling condition (SEC) and an LRT generation algorithm. No fake marking is produced and no legal marking is lost during the tree generation. We prove that LRT can represent faithfully the reachability set of an unbounded net in a finite manner. Also, we examine its properties and prove a sufficient condition for deadlock checking based on it. Our examples show that LRT outperforms the latest modified Karp-Miller trees in terms of size, expressiveness, and applicability.

Original languageEnglish (US)
Title of host publicationICNSC 2016 - 13th IEEE International Conference on Networking, Sensing and Control
PublisherInstitute of Electrical and Electronics Engineers Inc.
ISBN (Electronic)9781467399753
DOIs
StatePublished - May 25 2016
Event13th IEEE International Conference on Networking, Sensing and Control, ICNSC 2016 - Mexico City, Mexico
Duration: Apr 28 2016Apr 30 2016

Other

Other13th IEEE International Conference on Networking, Sensing and Control, ICNSC 2016
CountryMexico
CityMexico City
Period4/28/164/30/16

All Science Journal Classification (ASJC) codes

  • Artificial Intelligence
  • Computer Networks and Communications
  • Control and Systems Engineering
  • Modeling and Simulation

Fingerprint Dive into the research topics of 'Lean reachability tree for Petri net analysis'. Together they form a unique fingerprint.

Cite this