Rate Reduction for State-labelled Markov Chains with Upper Time-bounded CSL Requirements

被引：3

作者：

Tati, Bharath Siva Kumar ^{[1
]}

Siegle, Markus ^{[1
]}

机构：

[1] Univ Bundeswehr Munchen, Neubiberg, Germany

来源：

ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE | 2016年 / 220期

关键词：

D O I：

10.4204/EPTCS.220.7

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

This paper presents algorithms for identifying and reducing a dedicated set of controllable transition rates of a state-labelled continuous-time Markov chain model. The purpose of the reduction is to make states to satisfy a given requirement, specified as a CSL upper time-bounded Until formula. We distinguish two different cases, depending on the type of probability bound. A natural partitioning of the state space allows us to develop possible solutions, leading to simple algorithms for both cases.

引用

页码：77 / 89

页数：13

共 12 条

[1] Model-checking algorithms for continuous-time Markov chains
Baier, C
Haverkort, B
Hermanns, H
Katoen, JP
[J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2003, 29 (06) : 524 - 541
[2] Bartocci E, 2011, LECT NOTES COMPUT SC, V6605, P326, DOI 10.1007/978-3-642-19835-9_30
[3] Ceska M, 2014, LECT NOTES COMPUT SC, V8859, P86, DOI 10.1007/978-3-319-12982-2_7
[4] Model Repair for Markov Decision Processes
Chen, Taolue
Hahn, Ernst Moritz
Han, Tingting
Kwiatkowska, Marta
Qu, Hongyang
Zhang, Lijun
[J]. 2013 INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE), 2013, : 85 - 92
[5] Daws C, 2005, LECT NOTES COMPUT SC, V3407, P280
[6] Probabilistic reachability for parametric markov models
Hahn E.M.
Hermanns H.
Zhang L.
[J]. International Journal on Software Tools for Technology Transfer, 2011, 13 (1) : 3 - 19
[7] Hahn EM, 2010, LECT NOTES COMPUT SC, V6174, P660, DOI 10.1007/978-3-642-14295-6_56
[8] Approximate Parameter Synthesis for Probabilistic Time-Bounded Reachability
Han, Tingting
Katoen, Joost-Pieter
Mereacre, Alexandru
[J]. RTSS: 2008 REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS, 2008, : 173 - 182
[9] The ins and outs of the probabilistic model checker MRMC
Katoen, Joost-Pieter
Zapreev, Ivan S.
Hahn, Ernst Moritz
Hermanns, Holger
Jansen, David N.
[J]. PERFORMANCE EVALUATION, 2011, 68 (02) : 90 - 104
[10] Kwiatkowska Marta, 2011, Computer Aided Verification. Proceedings 23rd International Conference, CAV 2011, P585, DOI 10.1007/978-3-642-22110-1_47

← 1 2 →