@inproceedings{e324b525721242f3bf019e353f53bd6c,
title = "Lean reachability tree for Petri net analysis",
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.",
keywords = "Deadlock, Petri nets, Reachability tree, Unboundedness",
author = "Jun Li and Xiaolong Yu and Mengchu Zhou",
note = "Funding Information: The authors wish to thank the Ministry of Agriculture, Fisheries and Food for funding this work, and would like to acknowledge Dr. Pauline Jas for her contribution to the work. Publisher Copyright: {\textcopyright} 2016 IEEE.; 13th IEEE International Conference on Networking, Sensing and Control, ICNSC 2016 ; Conference date: 28-04-2016 Through 30-04-2016",
year = "2016",
month = may,
day = "25",
doi = "10.1109/ICNSC.2016.7478977",
language = "English (US)",
series = "ICNSC 2016 - 13th IEEE International Conference on Networking, Sensing and Control",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
booktitle = "ICNSC 2016 - 13th IEEE International Conference on Networking, Sensing and Control",
address = "United States",
}