PROVING TEMPORAL PROPERTIES OF PETRI NETS

被引：0
|
作者：
BRADFIELD, JC
机构：
来源：
LECTURE NOTES IN COMPUTER SCIENCE | 1991年 / 524卷
关键词：
PETRI NETS; TEMPORAL LOGIC; TABLEAU SYSTEMS; MODEL-CHECKING;
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We present a sound and complete tableau system for proving temporal properties of Petri nets, expressed in a propositional modal mucalculus which subsumes many other temporal logics. The system separates the checking of fix-points from the rest of the logic, which allows the use of powerful reasoning, perhaps specific to a class of nets or an individual net, to prove liveness and fairness properties. Examples are given to illustrate the use of the system. The proofs of soundness and completeness are given in detail.
引用
收藏
页码：29 / 47
页数：19
相关论文
共 50 条
  • [21] Modeling Hybrid Systems with Petri Nets
    Bera, Debjyoti
    van Hee, Kees
    Nijmeijer, Henk
    SIMULATION AND MODELING METHODOLOGIES, TECHNOLOGIES AND APPLICATIONS, SIMULTECH 2014, 2015, 402 : 17 - 42
  • [22] Verifying CTL with Unfoldings of Petri Nets
    Dong, Lanlan
    Liu, Guanjun
    Xiang, Dongming
    ALGORITHMS AND ARCHITECTURES FOR PARALLEL PROCESSING, ICA3PP 2018, PT IV, 2018, 11337 : 47 - 61
  • [23] Model checking Petri nets with MSVL
    Shi, Ya
    Tian, Cong
    Duan, Zhenhua
    Zhou, Mengchu
    INFORMATION SCIENCES, 2016, 363 : 274 - 291
  • [24] Properties research of Petri nets-safety place substitution based on workflow nets
    Dong L.-D.
    Cheng X.-H.
    Zheng H.
    Zhejiang Daxue Xuebao (Gongxue Ban)/Journal of Zhejiang University (Engineering Science), 2010, 44 (09): : 1711 - 1718
  • [25] Modeling by Petri Nets
    Kubatova, H.
    ACTA POLYTECHNICA, 2005, 45 (02) : 5 - 13
  • [26] Quotient Petri nets
    Ramirez-Trevino, A.
    Vazquez, C. R.
    Paniagua, I
    Vazquez, G.
    IFAC PAPERSONLINE, 2022, 55 (28): : 315 - 321
  • [27] Negotiations and Petri Nets
    Desel, Joerg
    Esparza, Javier
    TRANSACTIONS ON PETRI NETS AND OTHER MODELS OF CONCURRENCY XI, 2016, 9930 : 203 - 225
  • [28] Transformations of Petri Nets
    Ehrig, H.
    Hoffmann, K.
    Padberg, J.
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 148 (01) : 151 - 172
  • [29] Petri Nets With Persistence
    Crazzolara, Federico
    Winskel, Glynn
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 121 : 143 - 155
  • [30] A Congruence for Petri Nets
    Sassone, Vladimiro
    Sobocinski, Pawel
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 127 (02) : 107 - 120
12345