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] Constrained properties, semilinear systems, and Petri nets
    Bouajjani, Ahmed
    Habermehl, Peter
    Lecture Notes in Computer Science, 1119
  • [22] 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
  • [23] CLOSURE-PROPERTIES OF DETERMINISTIC PETRI NETS
    PELZ, E
    LECTURE NOTES IN COMPUTER SCIENCE, 1987, 247 : 371 - 382
  • [24] PROVING PRECEDENCE PROPERTIES - THE TEMPORAL WAY
    MANNA, Z
    PNUELI, A
    LECTURE NOTES IN COMPUTER SCIENCE, 1983, 154 : 491 - 512
  • [25] 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
  • [26] Verification of Reachability Properties for Time Petri Nets
    Klai, Kais
    Aber, Naim
    Petrucci, Laure
    REACHABILITY PROBLEMS, 2013, 8169 : 159 - 170
  • [27] STOCHASTIC PETRI NETS - PROPERTIES, APPLICATIONS AND TOOLS
    FLORIN, G
    FRAIZE, C
    NATKIN, S
    MICROELECTRONICS AND RELIABILITY, 1991, 31 (04): : 669 - 697
  • [28] TIMED PETRI NETS DEFINITIONS, PROPERTIES, AND APPLICATIONS
    ZUBEREK, WM
    MICROELECTRONICS AND RELIABILITY, 1991, 31 (04): : 627 - 644
  • [29] Jumping Petri Nets. Specific properties
    Laurentiu, Tiplea, Ferucio
    Makinen, Erkki
    Fundamenta Informaticae, 1997, 32 (3-4): : 373 - 392
  • [30] 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