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] Model checking multi-agent systems with logic based Petri nets
Behrens, Tristan M.
Dix, Juergen
ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE, 2007, 51 (2-4) : 81 - 121
[42] Assessing Time Behaviour in Disaster Management by Using Petri Nets and Model Checking
Cicirelli, Franco
Nigro, Libero
2023 INTERNATIONAL CONFERENCE ON INFORMATION AND COMMUNICATION TECHNOLOGIES FOR DISASTER MANAGEMENT, ICT-DM, 2023, : 181 - 186
[43] Improving state class constructions for CTL* model checking of time Petri nets
Hadjidj R.
Boucheneb H.
International Journal on Software Tools for Technology Transfer, 2008, 10 (2) : 167 - 184
[44] Model checking of time Petri nets using the state class timed automaton
Lime, Didier
Roux, Olivier H.
DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS, 2006, 16 (02): : 179 - 205
[45] LTL model checking probabilistic Petri net system
Liu, Yang
Miao, Huaikou
International Journal of Advancements in Computing Technology, 2012, 4 (01) : 172 - 178
[46] A General Model Checking Method of Electronic Transaction Protocols Using Colored Petri Nets
Xu, Meng
Su, Guiping
Wei, Jin
HIS 2009: 2009 NINTH INTERNATIONAL CONFERENCE ON HYBRID INTELLIGENT SYSTEMS, VOL 2, PROCEEDINGS, 2009, : 298 - 303
[47] Model checking Petri nets with names using data-centric dynamic systems
Montali, Marco
Rivkin, Andrey
FORMAL ASPECTS OF COMPUTING, 2016, 28 (04) : 615 - 641
[48] Model Checking ARAN Ad Hoc Secure Routing Protocol with Algebraic Petri Nets
Pura, Mihai Lica
Buchs, Didier
2014 10TH INTERNATIONAL CONFERENCE ON COMMUNICATIONS (COMM), 2014,
[49] Unbounded Protocol Compliance Verification Using Interval Property Checking With Invariants
Nguyen, Minh D.
Thalmaier, Max
Wedler, Markus
Bormann, Joerg
Stoffel, Dominik
Kunz, Wolfgang
IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2008, 27 (11) : 2068 - 2082
[50] Model Checking Autonomous Components within Electric Power Systems Specified by Interpreted Petri Nets
Grobelna, Iwona
Szczesniak, Pawel
SENSORS, 2022, 22 (18)

← 1 2 3 4 5 →