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 条

[21] Word level bitwidth reduction for unbounded hardware model checking
Bjesse, Per
FORMAL METHODS IN SYSTEM DESIGN, 2009, 35 (01) : 56 - 72
[22] Improvements in model checking for Object-Oriented Petri Nets
Hasa, L
Ceska, M
ISAS/CITSA 2004: INTERNATIONAL CONFERENCE ON CYBERNETICS AND INFORMATION TECHNOLOGIES, SYSTEMS AND APPLICATIONS AND 10TH INTERNATIONAL CONFERENCE ON INFORMATION SYSTEMS ANALYSIS AND SYNTHESIS, VOL 3, PROCEEDINGS, 2004, : 269 - 274
[23] Model Checking of Variable Petri Nets by Using the Kripke Structure
Yang, Ru
Ding, Zhijun
Guo, Tong
Pan, Meiqin
Jiang, Changjun
IEEE TRANSACTIONS ON SYSTEMS MAN CYBERNETICS-SYSTEMS, 2022, 52 (12): : 7774 - 7786
[24] Model Checking Control Flow Petri Nets Using PAT
Ho, Dung T.
Bui, Thang H.
Quan, Tho T.
PROCEEDINGS OF THE 2013 13TH INTERNATIONAL CONFERENCE ON COMPUTATIONAL SCIENCE AND ITS APPLICATIONS (ICCSA 2013), 2013, : 124 - 129
[25] Verifying multi-agent systems via unbounded model checking
Kacprzak, M
Lomuscio, A
Lasica, T
Penczek, W
Szreter, M
FORMAL APPROACHES TO AGENT-BASED SYSTEMS, 2005, 3228 : 189 - 212
[26] Model Checking of Concurrency in Cyber-Physical Systems Specified with Interpreted Petri Nets
Grobelna, Iwona
2024 23RD INTERNATIONAL SYMPOSIUM INFOTEH-JAHORINA, INFOTEH, 2024,
[27] Method and case study of model checking concurrent systems that use unbounded timestamps
Nakano, Shinya
Tsuchiya, Tatsuhiro
2017 IEEE 22ND PACIFIC RIM INTERNATIONAL SYMPOSIUM ON DEPENDABLE COMPUTING (PRDC 2017), 2017, : 261 - 266
[28] Symbolic Representation of Time Petri Nets for Efficient Bounded Model Checking
Igawa, Nao
Yokogawa, Tomoyuki
Amasaki, Sousuke
Kondo, Masafumi
Sato, Yoichiro
Arimoto, Kazutami
IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 2020, E103D (03) : 702 - 705
[29] How to use Model Checking for Diagnosing Fault Patterns in Petri nets
Bakalara, Johanne
Pencole, Yannick
Subias, Audine
IFAC PAPERSONLINE, 2020, 53 (04): : 269 - 274
[30] Performance evaluation and model checking in systems modeled as Hybrid Petri nets
Renganathan, K.
Bhaskar, Vidhyacharan
APPLIED MATHEMATICAL MODELLING, 2012, 36 (08) : 3941 - 3947

← 1 2 3 4 5 →