HomeNewsCase StudiesPeoplePublications
[HHZ11] E. M. Hahn, T. Han and L. Zhang. Synthesis for PCTL in Parametric Markov Decision Processes. In Mihaela Gheorghiu Bobaru and Klaus Havelund and Gerard J. Holzmann and Rajeev Joshi (editors), Proc. 3rd NASA Formal Methods Symposium (NFM'11), volume 6617 of Lecture Notes in Computer Science, pages 146-161, Springer. April 2011. [pdf] [bib]
Downloads:  pdf pdf (229 KB)  bib bib
Notes: The original publication is available at www.springerlink.com.
Abstract. In parametric Markov Decision Processes (PMDPs), transition probabilities are not fixed, but are given as functions over a set of parameters. A PMDP denotes a family of concrete MDPs. This paper studies the synthesis problem for PCTL in PMDPs: Given a specification Φ in PCTL, we synthesise the parameter valuations under which Φ is true. First, we divide the possible parameter space into hyper-rectangles. We use existing decision procedures to check whether Φ holds on each of the Markov processes represented by the hyper-rectangle. As it is normally impossible to cover the whole parameter space by hyper-rectangles, we allow a limited area to remain undecided. We also consider an extension of PCTL with reachability rewards. To demonstrate the applicability of the approach, we apply our technique on a case study, using a preliminary implementation.