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 条

[1] TCTL Model Checking of Time Petri Nets
Boucheneb, Hanifa
Gardey, Guillaume
Roux, Olivier H.
[J]. JOURNAL OF LOGIC AND COMPUTATION, 2009, 19 (06) : 1509 - 1540
[2] CTL* model checking for time Petri nets
Boucheneb, H
Hadjidj, R
[J]. THEORETICAL COMPUTER SCIENCE, 2006, 353 (1-3) : 208 - 227
[3] Covering Steps Graphs of Time Petri Nets
Boucheneb, Hanifa
Barkaoui, Kamel
[J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 239 : 155 - 165
[4] Consistency's checking of chronicles' set Using Time Petri Nets
Saddem, Ramla
Toguyeni, Armand
Tagina, Moncef
[J]. 18TH MEDITERRANEAN CONFERENCE ON CONTROL AND AUTOMATION, 2010, : 1520 - 1525
[5] CTL model checking of time Petri nets using geometric regions
Yoneda, T
Ryuba, H
[J]. IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 1998, E81D (03) : 297 - 306
[6] Bounded model checking of Time Petri Nets using SAT solver
Yokogawa, Tomoyuki
Kondo, Masafumi
Miyazaki, Hisashi
Amasaki, Sousuke
Sato, Yoichiro
Arimoto, Kazutami
[J]. IEICE ELECTRONICS EXPRESS, 2015, 12 (02):
[7] Towards TCTLhΔ model checking of Time Petri Nets
Chtourou, Ameni
Sbai, Zohra
[J]. 2016 INTERNATIONAL CONFERENCE ON CONTROL, DECISION AND INFORMATION TECHNOLOGIES (CODIT), 2016, : 563 - 568
[8] Model checking Bounded Prioritized Time Petri Nets
Berthomieu, Bernard
Peres, Florent
Vernadat, Francois
[J]. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2007, 4762 : 523 - +
[9] 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
[10] Model checking time-dependent system specifications using Time Stream Petri Nets and UPPAAL
Cicirelli, Franco
Furfaro, Angelo
Nigro, Libero
[J]. APPLIED MATHEMATICS AND COMPUTATION, 2012, 218 (16) : 8160 - 8186

← 1 2 3 4 5 →