PROVING TEMPORAL PROPERTIES OF PETRI NETS

被引:0
|
作者
BRADFIELD, JC
机构
关键词
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] PETRI NETS
    ROZENBLYUM, LY
    ENGINEERING CYBERNETICS, 1983, 21 (05): : 19 - 43
  • [42] Petri nets
    Advances in Industrial Control, 2009, (9781848822436): : 17 - 43
  • [43] Petri nets
    Petrinetze
    Informatik-Spektrum, 1600, Springer Verlag (37): : 165 - 167
  • [44] BDD-based Bounded Model Checking for Temporal Properties of 1-Safe Petri Nets
    Meski, Artur
    Penczek, Wojciech
    Polrola, Agata
    FUNDAMENTA INFORMATICAE, 2011, 109 (03) : 305 - 321
  • [45] Using colored Petri nets to simulate object Petri nets
    Corchado, FFR
    Gallegos, FZ
    Jiménez, AA
    Dávila, HIP
    International Conference on Computing, Communications and Control Technologies, Vol 5, Proceedings, 2004, : 27 - 31
  • [46] Petri Nets with Time Windows: A Comparison to Classical Petri Nets
    Wegener, Jan-Thierry
    Popova-Zeugmann, Louchka
    FUNDAMENTA INFORMATICAE, 2009, 93 (1-3) : 337 - 352
  • [47] Schedulability Analysis of Petri Nets Based on Structural Properties
    Liu, Cong
    Kondratyev, Alex
    Watanabe, Yosinori
    Desel, Joerg
    Sangiovanni-Vincentelli, Alberto
    FUNDAMENTA INFORMATICAE, 2008, 86 (03) : 325 - 341
  • [48] Validation of biological models with temporal logic and timed hybrid Petri nets
    Troncale, Sylvie
    Comet, Jean-Paul
    Bernot, Gilles
    2007 ANNUAL INTERNATIONAL CONFERENCE OF THE IEEE ENGINEERING IN MEDICINE AND BIOLOGY SOCIETY, VOLS 1-16, 2007, : 4603 - 4608
  • [49] Concurrent temporal planning using timed Petri nets - Policy evaluation
    Liew, Melissa
    White, Langford B.
    AI 2007: ADVANCES IN ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2007, 4830 : 727 - 731
  • [50] Managing feature interactions in telecommunications systems by temporal colored Petri nets
    Lu, YQ
    Wei, G
    Cheung, TY
    SEVENTH IEEE INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS, PROCEEDINGS, 2001, : 260 - 269