Reference

[HahnHZ11] Hahn, E. M.; Han, T. and Zhang, L. Synthesis for PCTL in Parametric Markov Decision Processes. In NFM, Springer, LNCS , 2011.
Downloads: pdf, bibAbstract. 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 Phi in PCTL, we synthesise the parameter valuations under which Phi is true. First, we divide the possible parameter space into hyper-rectangles. We use existing decision procedures to check whether Phi 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.