Model repair for Markov decision processes
文献类型：会议论文
| 作者 | Chen, Taolue (1) ; Hahn, Ernst Moritz (1) ; Han, Tingting (1) ; Kwiatkowska, Marta (1) ; Qu, Hongyang (2) ; Zhang, Lijun (3) |
| 出版日期 | 2013 |
| 会议名称 | 2013 International Symposium on Theoretical Aspects of Software Engineering, TASE 2013 |
| 会议日期 | July 1, 2013 - July 3, 2013 |
| 会议地点 | Birmingham, United kingdom |
| 页码 | 85-92 |
| 中文摘要 | Markov decision processes (MDPs) are often used for modelling distributed systems with probabilistic failure or randomisation. We consider the problem of model repair for MDPs defined as follows: if the MDP fails to satisfy a property, we aim to find new values for the transition probabilities so that the property is guaranteed to hold, while at the same time the cost of repair is minimised. Because solving the MDP repair problem exactly is infeasible, in this paper we focus on approximate solution methods. We first formulate a region-based approach, which yields an interval in which the minimal repair cost is contained. As an alternative, we also consider sampling based approaches, which are faster but unable to provide lower bounds on the repair cost. We have integrated both methods into the probabilistic model checker PRISM and demonstrated their usefulness in practice using a computer virus case study. © 2013 IEEE. |
| 英文摘要 | Markov decision processes (MDPs) are often used for modelling distributed systems with probabilistic failure or randomisation. We consider the problem of model repair for MDPs defined as follows: if the MDP fails to satisfy a property, we aim to find new values for the transition probabilities so that the property is guaranteed to hold, while at the same time the cost of repair is minimised. Because solving the MDP repair problem exactly is infeasible, in this paper we focus on approximate solution methods. We first formulate a region-based approach, which yields an interval in which the minimal repair cost is contained. As an alternative, we also consider sampling based approaches, which are faster but unable to provide lower bounds on the repair cost. We have integrated both methods into the probabilistic model checker PRISM and demonstrated their usefulness in practice using a computer virus case study. © 2013 IEEE. |
| 收录类别 | EI |
| 会议录出版地 | IEEE Computer Society, 2001 L Street N.W., Suite 700, Washington, DC 20036-4928, United States |
| 语种 | 英语 |
| ISBN号 | 9780768550534 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/16661]  |
| 专题 | 软件研究所_软件所图书馆_会议论文 |
| 推荐引用方式 GB/T 7714 | Chen, Taolue ,Hahn, Ernst Moritz ,Han, Tingting ,et al. Model repair for Markov decision processes[C]. 见:2013 International Symposium on Theoretical Aspects of Software Engineering, TASE 2013. Birmingham, United kingdom. July 1, 2013 - July 3, 2013. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。