[HahnHZ11a] Synthesis for PCTL in Parametric Markov Decision Processes Hahn, E. M.; Han, T. and Zhang, L. In NASA Formal Methods - Third International Symposium (NFM), pages 146-161, Springer, Lecture Notes in Computer Science 6617, 2011.
Downloads: pdf, bibURL: http://dx.doi.org/10.1007/978-3-642-20398-5_12 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.