Model checking of time Petri nets based on partial order semantics

被引:0
|
作者
Bieber, B [1 ]
Fleischhack, H [1 ]
机构
[1] Univ Oldenburg, Fachbereich Informat, D-26111 Oldenburg, Germany
来源
关键词
D O I
暂无
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
Model checking of place/transition-nets based on partial order semantics has been applied successfully to the analysis of causal behaviour of distributed systems. Here, this approach is extended to the causal behaviour of time Petri nets. Expansion of a time Petri net to an equivalent P/T-net is defined, and it is shown that tan abstraction of the McMillan unfolding of the expanded net is sufficient for model checking w.r.t. formulae of a simple branching time temporal logic L.
引用
收藏
页码:210 / 225
页数:16
相关论文
共 50 条
  • [41] SMT-Based Reachability Checking for Bounded Time Petri Nets
    Polrola, Agata
    Cybula, Piotr
    Meski, Artur
    [J]. FUNDAMENTA INFORMATICAE, 2014, 135 (04) : 467 - 482
  • [42] Implementing model checking and equivalence checking for time petri nets by the RT-MEC tool
    Bystrov, AV
    Virbitskaite, IB
    [J]. PARALLEL COMPUTING TECHNOLOGIES, 1999, 1662 : 194 - 199
  • [43] ON THE SEMANTICS OF PETRI NETS
    MESEGUER, J
    MONTANARI, U
    SASSONE, V
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1992, 630 : 286 - 301
  • [44] Improving state class constructions for CTL* model checking of time Petri nets
    Hadjidj R.
    Boucheneb H.
    [J]. International Journal on Software Tools for Technology Transfer, 2008, 10 (2) : 167 - 184
  • [45] Specification and model checking of temporal properties in time Petri nets and timed automata
    Penczek, W
    Pólrola, A
    [J]. APPLICATIONS AND THEORY OF PETRI NETS 2004, PROCEEDINGS, 2004, 3099 : 37 - 76
  • [46] Assessing Time Behaviour in Disaster Management by Using Petri Nets and Model Checking
    Cicirelli, Franco
    Nigro, Libero
    [J]. 2023 INTERNATIONAL CONFERENCE ON INFORMATION AND COMMUNICATION TECHNOLOGIES FOR DISASTER MANAGEMENT, ICT-DM, 2023, : 181 - 186
  • [47] Model checking of time Petri nets using the state class timed automaton
    Lime, Didier
    Roux, Olivier H.
    [J]. DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS, 2006, 16 (02): : 179 - 205
  • [48] Model Checking of Time Petri Nets Using the State Class Timed Automaton
    Didier Lime
    Olivier H. Roux
    [J]. Discrete Event Dynamic Systems, 2006, 16 : 179 - 205
  • [49] A partial order semantics for FIFO-nets
    Bernardeschi, C
    De Francesco, N
    Vaglini, G
    [J]. IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 1998, E81D (08) : 773 - 782
  • [50] Reactive Semantics for Component Based Petri Nets
    Hammal, Youcef
    [J]. 2012 2ND IEEE INTERNATIONAL CONFERENCE ON PARALLEL, DISTRIBUTED AND GRID COMPUTING (PDGC), 2012, : 795 - 805