Sciweavers

NFM
2011

Synthesis for PCTL in Parametric Markov Decision Processes

12 years 10 months ago
Synthesis for PCTL in Parametric Markov Decision Processes
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.
Ernst Moritz Hahn, Tingting Han, Lijun Zhang
Added 14 May 2011
Updated 14 May 2011
Type Journal
Year 2011
Where NFM
Authors Ernst Moritz Hahn, Tingting Han, Lijun Zhang
Comments (0)