Model repair for Markov decision processes

ISCAS OpenIR

	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
页码	85-92
会议日期	July 1, 2013 - July 3, 2013
会议地点	Birmingham, United kingdom
收录类别	EI
出版地	IEEE Computer Society, 2001 L Street N.W., Suite 700, Washington, DC 20036-4928, United States
ISBN	9780768550534
部门归属	(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
摘要	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.
语种	英语
内容类型	会议论文
URI标识	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]. IEEE Computer Society, 2001 L Street N.W., Suite 700, Washington, DC 20036-4928, United States,2013:85-92.