Model Checking of ω-Independent Unbounded Petri Nets for an Unbounded System

被引：0

作者：

Wang, Shuo ^{[1
,2
]}

Yang, Ru ^{[3
]}

Yu, Wangyang ^{[4
,5
,6
]}

Ding, Zhijun ^{[1
,2
,7
]}

Jiang, Changjun ^{[1
,2
,7
]}

机构：

[1] Tongji Univ, Minist Educ, Key Lab Embedded Syst & Serv Comp, Shanghai 201804, Peoples R China

[2] Tongji Univ, Dept Comp Sci & Technol, Shanghai 201804, Peoples R China

[3] Shanghai Normal Univ, Dept Comp Sci & Technol, Shanghai 200234, Peoples R China

[4] Shaanxi Normal Univ, Minist Educ, Key Lab Modern Teaching Technol, Xian 710062, Peoples R China

[5] Shaanxi Normal Univ, Sch Comp Sci, Xian 710119, Peoples R China

[6] Anhui Univ Sci & Technol, Anhui Prov Engn Lab Big Data Anal & Early Warning, Huainan 232001, Anhui, Peoples R China

[7] Shanghai Artificial Intelligence Lab, Shanghai 200232, Peoples R China

来源：

IEEE TRANSACTIONS ON COMPUTATIONAL SOCIAL SYSTEMS | 2024年

基金：

中国国家自然科学基金;

关键词：

Formal verification; model checking; omega-independent petri nets; unbounded system;

D O I：

10.1109/TCSS.2024.3462455

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

This work on model checking of unbounded Petri nets either not really concern the omega-component or only focus on the omega symbols, which may lead to incorrect judgments. This article proposes a model checking approach of omega-independent unbounded Petri nets. First, this approach can ensure the complete state space required for model checking by analyzing the enabled/unenabled marking set of conditionally enabled transition. Second, a comprehensive model checking process of omega-independent unbounded PN is presented, including the generation of extended new modified reachability graph. Third, two theorems are presented to prove that extended new modified reachability graph includes complete reachable markings and sequences of transitions. Finally, the proposed new approach is illustrated through a practical example.

引用

页数：12

共 50 条

[41] ON-THE-FLY DIAGNOSABILITY ANALYSIS OF BOUNDED AND UNBOUNDED LABELED PETRI NETS USING VERIFIER NETS
Li, Ben
Khlif-Bouassida, Manel
Toguyeni, Armand
INTERNATIONAL JOURNAL OF APPLIED MATHEMATICS AND COMPUTER SCIENCE, 2018, 28 (02) : 269 - 281
[42] New reachability trees for analyzing unbounded Petri nets with semilinear reachability sets
Shouguang WANG
Dan YOU
Mengchu ZHOU
Science China(Information Sciences), 2018, 61 (12) : 193 - 195
[43] An Efficient Algorithm for K-Diagnosability Analysis of Bounded and Unbounded Petri Nets
Chouchane, A.
Ghazel, M.
IFAC PAPERSONLINE, 2024, 58 (01): : 162 - 167
[44] PERFORMANCE EVALUATION OF PARALLEL SYSTEMS BY USING UNBOUNDED GENERALIZED STOCHASTIC PETRI NETS
GRANDA, M
DRAKE, JM
GREGORIO, JA
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1992, 18 (01) : 55 - 71
[45] Augmented reachability trees for 1-place-unbounded generalized Petri nets
Jeng, MD
Peng, MY
IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART A-SYSTEMS AND HUMANS, 1999, 29 (02): : 173 - 183
[46] The Probabilistic Liveness Decision Method of Unbounded Petri Nets Based on Machine Learning
Qi, Hongda
Wang, Junli
Yan, Chungang
Jiang, Changjun
IEEE TRANSACTIONS ON SYSTEMS MAN CYBERNETICS-SYSTEMS, 2024, 54 (02): : 1070 - 1081
[47] Correction to “Synchronizing sequences on a class of unbounded systems using synchronized Petri nets”
Changshun Wu
Isabel Demongodin
Alessandro Giua
Discrete Event Dynamic Systems, 2019, 29 : 521 - 526
[48] A New Modified Reachability Tree Approach and Its Applications to Unbounded Petri Nets
Wang, ShouGuang
Zhou, MengChu
Li, ZhiWu
Wang, ChengYing
IEEE TRANSACTIONS ON SYSTEMS MAN CYBERNETICS-SYSTEMS, 2013, 43 (04): : 932 - 940
[49] LTL model checking for modular Petri nets
Latvala, T
Mäkelä, M
APPLICATIONS AND THEORY OF PETRI NETS 2004, PROCEEDINGS, 2004, 3099 : 298 - 311
[50] Petri nets, traces, and local model checking
Cheng, A
THEORETICAL COMPUTER SCIENCE, 1997, 183 (02) : 229 - 251

← 1 2 3 4 5 →