Synthesis for PCTL in Parametric Markov Decision Processes
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.