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 条
  • [1] Temporal coercion of Petri nets
    Lime D.
    Martinez C.
    Roux O.H.
    Journal Europeen des Systemes Automatises, 2011, 45 (1-3): : 13 - 28
  • [2] Distributed Monitoring of Temporal System Properties using Petri Nets
    Baldellon, Olivier
    Fabre, Jean-Charles
    Roy, Matthieu
    2012 31ST INTERNATIONAL SYMPOSIUM ON RELIABLE DISTRIBUTED SYSTEMS (SRDS 2012), 2012, : 398 - 399
  • [3] Decidability of a temporal logic problem for Petri nets
    Jancar, Petr, 1600, (74):
  • [4] Propositional dynamic logic for Petri nets
    Lopes, Bruno
    Benevides, Mario
    Haeusler, Edward Hermann
    LOGIC JOURNAL OF THE IGPL, 2014, 22 (05) : 721 - 736
  • [5] Structural properties of a class of Petri nets
    Amer-Yahia, C
    Zerhouni, N
    El Moudni, A
    Ferney, M
    MANAGEMENT AND CONTROL OF PRODUCTION AND LOGISTICS, VOL 1 AND 2, 1998, : 215 - 220
  • [6] Event-Based Runtime Verification of Temporal Properties Using Time Basic Petri Nets
    Camilli, Matteo
    Gargantini, Angelo
    Scandurra, Patrizia
    Bellettini, Carlo
    NASA FORMAL METHODS (NFM 2017), 2017, 10227 : 115 - 130
  • [7] On the analysis of some structural properties of Petri nets
    Bouyekhf, R
    El Moudni, A
    IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART A-SYSTEMS AND HUMANS, 2005, 35 (06): : 784 - 794
  • [8] Properties of Plain, Pure, and Safe Petri Nets
    Barylska, Kamila
    Best, Eike
    Schlachter, Uli
    Spreckels, Valentin
    TRANSACTIONS ON PETRI NETS AND OTHER MODELS OF CONCURRENCY XII, 2017, 10470 : 1 - 18
  • [9] Verification of Reachability Properties for Time Petri Nets
    Klai, Kais
    Aber, Naim
    Petrucci, Laure
    REACHABILITY PROBLEMS, 2013, 8169 : 159 - 170
  • [10] Properties and applications of synchronized choice Petri nets
    Chao, DY
    Niedao, JA
    2001 IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN, AND CYBERNETICS, VOLS 1-5: E-SYSTEMS AND E-MAN FOR CYBERNETICS IN CYBERSPACE, 2002, : 2742 - 2747
12345