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] Properties of object Petri nets
    Köhler, M
    Rölke, H
    APPLICATIONS AND THEORY OF PETRI NETS 2004, PROCEEDINGS, 2004, 3099 : 278 - 297
  • [4] Observability properties of Petri nets
    Giua, A
    Seatzu, C
    PROCEEDINGS OF THE 39TH IEEE CONFERENCE ON DECISION AND CONTROL, VOLS 1-5, 2000, : 2676 - 2681
  • [5] Specification and model checking of temporal properties in time Petri nets and timed automata
    Penczek, W
    Pólrola, A
    APPLICATIONS AND THEORY OF PETRI NETS 2004, PROCEEDINGS, 2004, 3099 : 37 - 76
  • [6] Decidability of a temporal logic problem for Petri nets
    Jancar, Petr, 1600, (74):
  • [7] Timed Petri nets and temporal linear logic
    Tanabe, M
    APPLICATION AND THEORY OF PETRI NETS 1997, 1997, 1248 : 156 - 174
  • [8] On temporal logic programming using Petri nets
    Zaidi, AK
    IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART A-SYSTEMS AND HUMANS, 1999, 29 (03): : 245 - 254
  • [9] DECIDABILITY OF A TEMPORAL LOGIC PROBLEM FOR PETRI NETS
    JANCAR, P
    THEORETICAL COMPUTER SCIENCE, 1990, 74 (01) : 71 - 93
  • [10] Temporal Petri nets model of concurrent systems
    Ding, ZJ
    Jiang, CJ
    COMPUTER SYSTEMS SCIENCE AND ENGINEERING, 2002, 17 (06): : 353 - 358
12345