Liveness and deadlock-freeness verification and enforcement in bounded Petri nets using basis reachability graphs

被引：0
|
作者：
Gu, Chao [1 ]
Ma, Ziyue [1 ]
Li, Zhiwu [1 ,2 ]
机构：
[1] Xidian Univ, Sch Electromech Engn, Xian, Peoples R China
[2] Macau Univ Sci & Technol, Inst Syst Engn, Taipa, Macao, Peoples R China
来源：
AUTOMATICA | 2024年 / 164卷
基金：
中国国家自然科学基金; 国家重点研发计划;
关键词：
Petri net; Deadlock-freeness; Liveness; Basis reachability graph; FLEXIBLE MANUFACTURING SYSTEMS; FEEDBACK-CONTROL LOGIC; PREVENTION POLICY; ENFORCING SUPERVISORS;
D O I：
10.1016/j.automatica.2024.111625
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
This paper studies the verification and enforcement of deadlock -freeness and liveness in partially controllable Petri nets. First, we introduce a particular type of basis reachability graphs called conflict -free -control -explicit basis reachability graphs (CFCE-BRGs), in which the firings of all structurally conflicting transitions and all controllable ones are explicitly encoded. We propose two sufficient and necessary conditions for verifying deadlock -freeness and liveness of a Petri net; both can be verified by inspecting a CFCE-BRG using graph theory. Moreover, we develop two maximally permissive deadlockfreeness and liveness enforcing supervisors based on the trimming of CFCE-BRGs. The developed approaches are applicable to arbitrary bounded Petri nets, without an exhaustive reachability space enumeration. (c) 2024 Published by Elsevier Ltd.
引用
收藏
页数：13
相关论文
共 33 条
  • [1] On the equivalence between liveness and deadlock-freeness in Petri nets
    Barkaoui, K
    Couvreur, JM
    Klai, K
    [J]. APPLICATIONS AND THEORY OF PETRI NETS 2005, PROCEEDINGS, 2005, 3536 : 90 - 107
  • [2] On the Reachability Space and Deadlock-Freeness in Flexible Nets
    Julvez, Jorge
    [J]. 2023 62ND IEEE CONFERENCE ON DECISION AND CONTROL, CDC, 2023, : 6936 - 6941
  • [3] Non-Blockingness Verification of Bounded Petri Nets Using Basis Reachability Graphs
    Gu, Chao
    Ma, Ziyue
    Li, Zhiwu
    Giua, Alessandro
    [J]. IEEE CONTROL SYSTEMS LETTERS, 2022, 6 : 1220 - 1225
  • [4] Preservation of liveness and deadlock-freeness in synchronous synthesis of petri net systems
    Pu, Fei
    Lu, Wei-Ming
    [J]. Ruan Jian Xue Bao/Journal of Software, 2003, 14 (12): : 1977 - 1988
  • [5] Verification of Nonblockingness in Bounded Petri Nets With Min-Max Basis Reachability Graphs
    Gu, Chao
    Ma, Ziyue
    Li, Zhiwu
    Giua, Alessandro
    [J]. IEEE TRANSACTIONS ON SYSTEMS MAN CYBERNETICS-SYSTEMS, 2022, 52 (10): : 6162 - 6173
  • [6] Deadlock-freeness analysis of continuous mono-T-semiflow Petri nets
    Julvez, Jorge
    Recalde, Laura
    Silva, Manuel
    [J]. IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2006, 51 (09) : 1472 - 1481
  • [7] Deadlock-Freeness Verification of Business Process Configuration Using SOG
    Boubaker, Souha
    Klai, Kais
    Schmitz, Katia
    Graiet, Mohamed
    Gaaloul, Walid
    [J]. SERVICE-ORIENTED COMPUTING, ICSOC 2017, 2017, 10601 : 96 - 112
  • [8] Noninterference Analysis of Bounded Petri Nets Using Basis Reachability Graph
    Ran, Ning
    Nie, Jingyao
    Meng, Aiwen
    Seatzu, Carla
    [J]. IEEE Transactions on Automatic Control, 2024, 69 (10) : 7159 - 7165
  • [9] Marking Estimation in Petri Nets Using Hierarchical Basis Reachability Graphs
    Ma, Ziyue
    Zhu, Guanghui
    Li, Zhiwu
    [J]. IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2021, 66 (02) : 810 - 817
  • [10] Codiagnosability Verification of Bounded Petri Nets Using Basis Markings
    Ran, Ning
    Su, Hongye
    Giua, Alessandro
    Seatzu, Carla
    [J]. 2016 IEEE 55TH CONFERENCE ON DECISION AND CONTROL (CDC), 2016, : 3948 - 3953
1234