www.prismmodelchecker.org
[HHZ11] Ernst Moritz Hahn and Tingting Han and Lijun Zhang. Synthesis for PCTL in Parametric Markov Decision Processes. In Proc. 3rd NASA Formal Methods Symposium (NFM'11). April 2011. [pdf] [bib]
Downloads:  pdf pdf (229 KB)  bib bib
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.

Publications