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 条
  • [41] An extremum timed extended reachability graph for temporal analysis of time Petri nets
    Zhou, Jiazhong
    Lefebvre, Dimitri
    Li, Zhiwu
    DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS, 2024, 34 (03): : 403 - 427
  • [42] Qualitative simulation of temporal concurrent processes using Time Interval Petri Nets
    Bulitko, V
    Wilkins, DC
    ARTIFICIAL INTELLIGENCE, 2003, 144 (1-2) : 95 - 124
  • [43] EXPLORING THE PROPERTIES OF MSC DOCUMENTS BY TRANSLATING THEM INTO PETRI NETS
    Kryvyi, S. L.
    Chugayenko, O. V.
    Matveeva, L. E.
    CYBERNETICS AND SYSTEMS ANALYSIS, 2009, 45 (06) : 997 - 1003
  • [44] Token Trail Semantics - Modeling Behavior of Petri Nets with Labeled Petri Nets
    Bergenthum, Robin
    Folz-Weinstein, Sabine
    Kovar, Jakub
    APPLICATION AND THEORY OF PETRI NETS AND CONCURRENCY, PETRI NETS 2023, 2023, 13929 : 286 - 306
  • [45] Divergence Properties of Labeled Petri Nets and Their Relevance for Diagnosability Analysis
    Giua, Alessandro
    Lafortune, Stephane
    Seatzu, Carla
    IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2020, 65 (07) : 3092 - 3097
  • [46] Token Variation Vector and Analysis of some Properties of Petri Nets
    Costa, E. M. M.
    Medeiros, J. B.
    Pozzebon, E.
    Perez, A. F. L.
    Filho, J. V. S.
    IEEE LATIN AMERICA TRANSACTIONS, 2010, 8 (05) : 499 - 504
  • [47] Proving guarantee and recurrence temporal properties by abstract interpretation
    1600, Springer Verlag (8931):
  • [48] Petri nets behavioral equivalence checking in SMV
    Drozdov, Dmitrii
    Dubinin, Victor
    Kulagin, Vladimir
    2016 INTERNATIONAL SIBERIAN CONFERENCE ON CONTROL AND COMMUNICATIONS (SIBCON), 2016,
  • [49] Property Directed Reachability for Generalized Petri Nets
    Amat, Nicolas
    Dal Zilio, Silvano
    Hujsa, Thomas
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2022, PT I, 2022, 13243 : 505 - 523
  • [50] Model checking of Signal Interpreted Petri Nets
    Weng, XY
    Litz, L
    2001 IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN, AND CYBERNETICS, VOLS 1-5: E-SYSTEMS AND E-MAN FOR CYBERNETICS IN CYBERSPACE, 2002, : 2748 - 2752
12345