Model repair for Markov decision processes

Taolue Chen, Ernst Moritz Hahn, Tingting Han, Marta Kwiatkowska, Hongyang Qu, Lijun Zhang

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

47 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationProceedings - 2013 International Symposium on Theoretical Aspects of Software Engineering, TASE 2013
Pages85-92
Number of pages8
DOIs
Publication statusPublished - 2013
Externally publishedYes
Event7th International Symposium on Theoretical Aspects of Software Engineering, TASE 2013 - Birmingham, United Kingdom
Duration: 1 Jul 20133 Jul 2013
Conference number: 7

Conference

Conference7th International Symposium on Theoretical Aspects of Software Engineering, TASE 2013
Abbreviated titleTASE 2013
CountryUnited Kingdom
CityBirmingham
Period1/07/133/07/13

Fingerprint Dive into the research topics of 'Model repair for Markov decision processes'. Together they form a unique fingerprint.

Cite this