Institutional Repository
| 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 | |
| Conference Name | 2013 International Symposium on Theoretical Aspects of Software Engineering, TASE 2013 |
| Pages | 85-92 |
| Conference Date | July 1, 2013 - July 3, 2013 |
| Conference Place | Birmingham, United kingdom |
| Indexed Type | EI |
| Publish Place | IEEE Computer Society, 2001 L Street N.W., Suite 700, Washington, DC 20036-4928, United States |
| ISBN | 9780768550534 |
| Department | (1) Department of Computer Science, University of Oxford, United Kingdom; (2) Department of Automatic Control and Systems Engineering, University of Sheffield, United Kingdom; (3) State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, China |
| English Abstract | 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. |
| Language | 英语 |
| Content Type | 会议论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/16661 |
| Collection | 中国科学院软件研究所 |
| Recommended Citation GB/T 7714 | Chen, Taolue ,Hahn, Ernst Moritz ,Han, Tingting ,et al. Model repair for Markov decision processes[C]. IEEE Computer Society, 2001 L Street N.W., Suite 700, Washington, DC 20036-4928, United States,2013:85-92. |
| Files in This Item: | There are no files associated with this item. | |||||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment