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 条

[1] MathMC: A mathematica-based tool for CSL model checking of Deterministic and Stochastic Petri Nets
Martinez, Jose M.
Haverkort, Boudewijn R.
[J]. QEST 2006: THIRD INTERNATIONAL CONFERENCE ON THE QUANTITATIVE EVALUATION OF SYSTEMS, 2006, : 133 - +
[2] CSL model checking for generalized Stochastic Petri Nets
Cerotti, Davide
Donatelli, Susanna
Horvath, Andras
Sproston, Jeremy
[J]. QEST 2006: THIRD INTERNATIONAL CONFERENCE ON THE QUANTITATIVE EVALUATION OF SYSTEMS, 2006, : 199 - +
[3] Model Checking Timed and Stochastic Properties with CSLTA
Donatelli, Susanna
Haddad, Serge
Sproston, Jeremy
[J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2009, 35 (02) : 224 - 240
[4] Efficient model checking of the stochastic logic CSLTA
Amparore, E. G.
Donatelli, S.
[J]. PERFORMANCE EVALUATION, 2018, 123 : 1 - 34
[5] Design and Identification of Stochastic and Deterministic Stochastic Petri Nets
El Mehdi, Souleiman Ould
Bekrar, Rebiha
Messai, Nadhir
Leclercq, Edouard
Lefebvre, Dimitri
Riera, Bernard
[J]. IEEE TRANSACTIONS ON SYSTEMS MAN AND CYBERNETICS PART A-SYSTEMS AND HUMANS, 2012, 42 (04): : 931 - 946
[6] Model checking Petri nets with MSVL
Shi, Ya
Tian, Cong
Duan, Zhenhua
Zhou, Mengchu
[J]. INFORMATION SCIENCES, 2016, 363 : 274 - 291
[7] MODEL CHECKING OF PERSISTENT PETRI NETS
BEST, E
ESPARZA, J
[J]. LECTURE NOTES IN COMPUTER SCIENCE, 1992, 626 : 35 - 52
[8] ON SYMBOLIC MODEL CHECKING IN PETRI NETS
HIRAISHI, K
NAKANO, M
[J]. IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, 1995, E78A (11) : 1479 - 1486
[9] Transient analysis of deterministic and stochastic Petri nets with concurrent deterministic transitions
Lindemann, C
Thümmler, A
[J]. PERFORMANCE EVALUATION, 1999, 36-7 : 35 - 54
[10] Numerical analysis of deterministic and stochastic Petri nets with concurrent deterministic transitions
Lindemann, C
Shedler, GS
[J]. PERFORMANCE EVALUATION, 1996, 27-8 : 565 - 582

← 1 2 3 4 5 →