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 条
  • [31] Exploiting temporal uncertainty in the distributed simulation of time Petri nets
    Cicirelli, F
    Furfaro, A
    Nigro, L
    38th Annual Simulation Symposium, Proceedings, 2005, : 233 - 240
  • [32] Checking linear temporal formulas on sequential recursive Petri nets
    Haddad, S
    Poitrenaud, D
    EIGHTH INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING, PROCEEDINGS, 2001, : 198 - 205
  • [33] A new technique for behavior and temporal analysis of timed Petri nets
    Hwang, CP
    Ho, CS
    JOURNAL OF THE CHINESE INSTITUTE OF ENGINEERS, 1997, 20 (05) : 481 - 492
  • [34] FORMAL ANALYSIS OF THE ALTERNATING BIT PROTOCOL BY TEMPORAL PETRI NETS
    SUZUKI, I
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1990, 16 (11) : 1273 - 1281
  • [35] Reachability and temporal conflicts in t-time Petri nets
    Riviere, N
    Pradin-Chezalviel, B
    Valette, R
    9TH INTERNATIONAL WORKSHOP ON PETRI NETS AND PERFORMANCE MODELS, PROCEEDINGS, 2001, : 229 - 238
  • [36] A NEW STRUCTURAL INDUCTION THEOREM FOR RINGS OF TEMPORAL PETRI NETS
    LI, J
    SUZUKI, I
    YAMASHITA, M
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1994, 20 (02) : 115 - 126
  • [37] From Coloured Petri Nets to Object Petri Nets
    Lakos, C
    APPLICATION AND THEORY OF PETRI NETS 1995, 1995, 935 : 278 - 297
  • [38] Proving correctness of distributed algorithms using high-level Petri nets - A case study
    Desel, J
    Kindler, E
    1998 INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN, PROCEEDINGS, 1998, : 177 - 186
  • [39] PETRI NETS
    PETERSON, JL
    COMPUTING SURVEYS, 1977, 9 (03) : 223 - 252
  • [40] PETRIREVE - PROVING PETRI NET PROPERTIES WITH REWRITING-SYSTEMS
    CHOPPY, C
    JOHNEN, C
    LECTURE NOTES IN COMPUTER SCIENCE, 1985, 202 : 271 - 286
12345