Using Integer Time Steps for Checking Branching Time Properties of Time Petri Nets

被引：0
|
作者：
Janowska, Agata [1 ]
Penczek, Wojciech [2 ]
Polrola, Agata [3 ]
Zbrzezny, Andrzej [4 ]
机构：
[1] Univ Warsaw, Inst Informat, PL-00325 Warsaw, Poland
[2] Inst Comp Sci PAS & UPH Siedlce, Siedlce, Poland
[3] Univ Lodz, FMCS, PL-90131 Lodz, Poland
[4] Jan Dlugosz Univ, IMCS, Czestochowa, Poland
来源：
TRANSACTIONS ON PETRI NETS AND OTHER MODELS OF CONCURRENCY VIII | 2013年 / 8100卷
关键词：
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Verification of timed systems is an important subject of research, and one of its crucial aspects is the efficiency of the methods developed. Extending the result of Popova which states that integer time steps are sufficient to test reachability properties of time Petri nets [8,11], in our work we prove that the discrete-time semantics is also sufficient to verify properties of the existential and the universal version of CTL* of TPNs with the dense semantics. To show that considering this semantics instead of the dense one is profitable, we compare the results for SAT-based bounded model checking of the universal version of CTL-X properties and the class of distributed time Petri nets.
引用
收藏
页码：89 / 105
页数：17
相关论文
共 50 条
  • [31] Shrinking of Time Petri nets
    Lime, Didier
    Martinez, Claude
    Roux, Olivier H.
    [J]. DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS, 2013, 23 (04): : 419 - 438
  • [32] Time Recursive Petri Nets
    Dahmani, Djaouida
    Ilie, Jean-Michel
    Boukala, Malika
    [J]. TRANSACTIONS ON PETRI NETS AND OTHER MODELS OF CONCURRENCY I, 2008, 5100 : 104 - +
  • [33] Probabilistic Time Petri Nets
    Emzivat, Yrvann
    Delahaye, Benoit
    Lime, Didier
    Roux, Olivier H.
    [J]. APPLICATION AND THEORY OF PETRI NETS AND CONCURRENCY, PETRI NETS 2016, 2016, 9698 : 261 - 280
  • [34] Shrinking of Time Petri nets
    Didier Lime
    Claude Martinez
    Olivier H. Roux
    [J]. Discrete Event Dynamic Systems, 2013, 23 : 419 - 438
  • [35] On the composition of time Petri nets
    Florent Peres
    Bernard Berthomieu
    François Vernadat
    [J]. Discrete Event Dynamic Systems, 2011, 21 : 395 - 424
  • [36] Petri nets and time modelling
    Latif Salum
    [J]. The International Journal of Advanced Manufacturing Technology, 2008, 38 : 377 - 382
  • [37] Embedding Time Petri nets
    Comlan, Maurice
    Delfieu, David
    Sogbohossou, Medesu
    Vianou, Antoine
    [J]. 2017 4TH INTERNATIONAL CONFERENCE ON CONTROL, DECISION AND INFORMATION TECHNOLOGIES (CODIT), 2017, : 404 - 409
  • [38] On Persistency in Time Petri Nets
    Barkaoui, Kamel
    Bouchene, Hanifa
    [J]. FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, FORMATS 2018, 2018, 11022 : 108 - 124
  • [39] Time-independent Liveness in Time Petri Nets
    Bachmann, Joerg Peter
    Popova-Zeugmann, Louchka
    [J]. FUNDAMENTA INFORMATICAE, 2010, 102 (01) : 1 - 17
  • [40] 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
12345