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 条
  • [31] Symbolic computation tree logic model checking of time Petri nets
    Okawa, Y
    Yoneda, T
    ELECTRONICS AND COMMUNICATIONS IN JAPAN PART III-FUNDAMENTAL ELECTRONIC SCIENCE, 1997, 80 (04): : 11 - 20
  • [32] UML behavioral consistency checking using instantiable Petri nets
    Thierry-Mieg, Yann
    Hillah, Lom-Messan
    INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING, 2008, 4 (03) : 293 - 300
  • [33] UML behavioral consistency checking using instantiable Petri nets
    Yann Thierry-Mieg
    Lom-Messan Hillah
    Innovations in Systems and Software Engineering, 2008, 4 (3) : 293 - 300
  • [34] Petri nets behavioral equivalence checking in SMV
    Drozdov, Dmitrii
    Dubinin, Victor
    Kulagin, Vladimir
    2016 INTERNATIONAL SIBERIAN CONFERENCE ON CONTROL AND COMMUNICATIONS (SIBCON), 2016,
  • [35] Model checking time-dependent system specifications using Time Stream Petri Nets and UPPAAL
    Cicirelli, Franco
    Furfaro, Angelo
    Nigro, Libero
    APPLIED MATHEMATICS AND COMPUTATION, 2012, 218 (16) : 8160 - 8186
  • [36] Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking
    Cabodi, G.
    Camurati, P. E.
    Palena, M.
    Pasini, P.
    FORMAL METHODS IN SYSTEM DESIGN, 2022, 60 (02) : 117 - 146
  • [37] Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking
    G. Cabodi
    P. E. Camurati
    M. Palena
    P. Pasini
    Formal Methods in System Design, 2022, 60 : 117 - 146
  • [38] Bounded Model Checking High Level Petri Nets in PIPE plus Verifier
    Liu, Su
    Zeng, Reng
    Sun, Zhuo
    He, Xudong
    FORMAL METHODS AND SOFTWARE ENGINEERING, ICFEM 2014, 2014, 8829 : 348 - 363
  • [39] Model Checking of Time Petri Nets Using the State Class Timed Automaton
    Didier Lime
    Olivier H. Roux
    Discrete Event Dynamic Systems, 2006, 16 : 179 - 205
  • [40] Model checking multi-agent systems with logic based Petri nets
    Tristan M. Behrens
    Jürgen Dix
    Annals of Mathematics and Artificial Intelligence, 2007, 51 : 81 - 121
12345