Publications-Periodical Articles

Article View/Open

Publication Export

Google ScholarTM

NCCU Library

Citation Infomation

Related Publications in TAIR

題名 Proof by model: a new knowledge-based reachability analysis methodology for Petri net
作者 趙玉;季延平;游宗憲;游禮志;李耀中
貢獻者 資管博五
關鍵詞 control systems, discrete event systems, flexible manufacturing systems, petri nets
日期 2016-07
上傳時間 29-Jun-2017 10:05:36 (UTC+8)
摘要 To solve the state explosion problem in the reachability analysis of Petri nets, Chao recently broke the NP(nondeterministic polynomial time)-complete barrier by developing the first closed-form solution of the number of Control Related States for the kk th-order system. In this paper, we propose a new proof methodology known as proof by model, which is based on the validated information of the reverse net, to simplify and accelerate the construction of the closed-form solution for Petri nets. Here, we apply this methodology to the proof procedure of Top-Right systems with one non-sharing resource placed in the top position of the right-side process. The core theoretical and data basis are that any forbidden (resp. live) state in a Petri net is non-reachable (resp. live) in its reverse net; and the validated information of the Bottom-Right system, the reverse net of Top-Right.
關聯 IMA Journal of Mathematical Control and Information, 32, 1-22
資料類型 article
DOI http://dx.doi.org/10.1093/imamci/dnw025
dc.contributor 資管博五
dc.creator (作者) 趙玉;季延平;游宗憲;游禮志;李耀中zh_TW
dc.date (日期) 2016-07
dc.date.accessioned 29-Jun-2017 10:05:36 (UTC+8)-
dc.date.available 29-Jun-2017 10:05:36 (UTC+8)-
dc.date.issued (上傳時間) 29-Jun-2017 10:05:36 (UTC+8)-
dc.identifier.uri (URI) http://nccur.lib.nccu.edu.tw/handle/140.119/110593-
dc.description.abstract (摘要) To solve the state explosion problem in the reachability analysis of Petri nets, Chao recently broke the NP(nondeterministic polynomial time)-complete barrier by developing the first closed-form solution of the number of Control Related States for the kk th-order system. In this paper, we propose a new proof methodology known as proof by model, which is based on the validated information of the reverse net, to simplify and accelerate the construction of the closed-form solution for Petri nets. Here, we apply this methodology to the proof procedure of Top-Right systems with one non-sharing resource placed in the top position of the right-side process. The core theoretical and data basis are that any forbidden (resp. live) state in a Petri net is non-reachable (resp. live) in its reverse net; and the validated information of the Bottom-Right system, the reverse net of Top-Right.
dc.format.extent 796523 bytes-
dc.format.mimetype application/pdf-
dc.relation (關聯) IMA Journal of Mathematical Control and Information, 32, 1-22
dc.subject (關鍵詞) control systems, discrete event systems, flexible manufacturing systems, petri nets
dc.title (題名) Proof by model: a new knowledge-based reachability analysis methodology for Petri net
dc.type (資料類型) article
dc.identifier.doi (DOI) 10.1093/imamci/dnw025
dc.doi.uri (DOI) http://dx.doi.org/10.1093/imamci/dnw025