Model Checking CSLTA with Deterministic and Stochastic Petri Nets

被引：0

作者：

Amparore, Elvio Gilberto ^{[1
]}

Donatelli, Susanna ^{[1
]}

机构：

[1] Univ Turin, Dipartimento Informat, I-10124 Turin, Italy

来源：

2010 IEEE-IFIP INTERNATIONAL CONFERENCE ON DEPENDABLE SYSTEMS AND NETWORKS DSN | 2010年

关键词：

Stochastic Model Checking; DSPN; MARKOV-CHAINS;

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

CSLTA is a stochastic temporal logic for continuous-time Markov chains (CTMC), that can verify the probability of following paths specified by a Deterministic Timed Automaton (DTA). A DTA expresses both logic and time constraints over a CTMC path, yielding to a very flexible way of describing performance and dependability properties. This paper explores a model checking algorithm for CSLTA based on the translation into a Deterministic and Stochastic Petri Net (DSPN). The algorithm has been implemented in a simple Model Checker prototype, that relies on existing DSPN solvers to do the actual numerical computations.

引用

页码：605 / 614

页数：10

共 50 条

[41] Interval diagram techniques for symbolic model checking of Petri nets
Strehl, K
Thiele, L
[J]. DESIGN, AUTOMATION AND TEST IN EUROPE CONFERENCE AND EXHIBITION 1999, PROCEEDINGS, 1999, : 756 - 757
[42] Improvements in model checking for Object-Oriented Petri Nets
Hasa, L
Ceska, M
[J]. ISAS/CITSA 2004: INTERNATIONAL CONFERENCE ON CYBERNETICS AND INFORMATION TECHNOLOGIES, SYSTEMS AND APPLICATIONS AND 10TH INTERNATIONAL CONFERENCE ON INFORMATION SYSTEMS ANALYSIS AND SYNTHESIS, VOL 3, PROCEEDINGS, 2004, : 269 - 274
[43] On-the-fly TCTL model checking for time Petri nets
Hadjidj, Rachid
Boucheneb, Hanifa
[J]. THEORETICAL COMPUTER SCIENCE, 2009, 410 (42) : 4241 - 4261
[44] Model checking of reconfigurable FPGA modules specified by Petri nets
Grobelna, Iwona
[J]. JOURNAL OF SYSTEMS ARCHITECTURE, 2018, 89 : 1 - 9
[45] Interpolation Based Unbounded Model Checking for Time Petri Nets
Igawa, Nao
Yokogawa, Tomoyuki
Amasaki, Sousuke
Komoku, Kiyotaka
Sato, Yoichiro
Arimoto, Kazutami
[J]. 2018 IEEE 7TH GLOBAL CONFERENCE ON CONSUMER ELECTRONICS (GCCE 2018), 2018, : 619 - 623
[46] Model Checking of Variable Petri Nets by Using the Kripke Structure
Yang, Ru
Ding, Zhijun
Guo, Tong
Pan, Meiqin
Jiang, Changjun
[J]. IEEE TRANSACTIONS ON SYSTEMS MAN CYBERNETICS-SYSTEMS, 2022, 52 (12): : 7774 - 7786
[47] Model Checking Control Flow Petri Nets Using PAT
Ho, Dung T.
Bui, Thang H.
Quan, Tho T.
[J]. PROCEEDINGS OF THE 2013 13TH INTERNATIONAL CONFERENCE ON COMPUTATIONAL SCIENCE AND ITS APPLICATIONS (ICCSA 2013), 2013, : 124 - 129
[48] Analysis of the performance of inventory management systems using the SCOR model and Batch Deterministic and Stochastic Petri Nets
Fattah, Jamal
Ezzine, Latifa
El Moussami, Haj
Lachhab, Abdeslam
[J]. INTERNATIONAL JOURNAL OF ENGINEERING BUSINESS MANAGEMENT, 2016, 8 : 1 - 11
[49] Faulty Model identification in deterministic labeled Time Petri nets
Basile, Francesco
Chiacchio, Pasquale
Coppola, Jolanda
[J]. 2016 13TH INTERNATIONAL WORKSHOP ON DISCRETE EVENT SYSTEMS (WODES), 2016, : 486 - 492
[50] Modeling of DRAM power control policies using deterministic and stochastic Petri nets
Fan, XB
Ellis, CS
Lebeck, AR
[J]. POWER-AWARE COMPUTER SYSTEMS, 2003, 2325 : 130 - 140

← 1 2 3 4 5 →