Synthesis for PCTL in Parametric Markov Decision Processes

Ernst Moritz Hahn, Tingting Han, Lijun Zhang

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

52 Citations (Scopus)


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.
Original languageEnglish
Title of host publicationNASA Formal Methods
Subtitle of host publicationThird International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings
Place of PublicationBerlin, Heidelberg
ISBN (Electronic)978-3-642-20398-5
ISBN (Print)978-3-642-20397-8
Publication statusPublished - 2011
Externally publishedYes
Event3rd International Symposium on NASA Formal Methods, NFM 2011 - Pasadena, United States
Duration: 18 Apr 201120 Apr 2011
Conference number: 3

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference3rd International Symposium on NASA Formal Methods, NFM 2011
Abbreviated titleNFM
CountryUnited States


Dive into the research topics of 'Synthesis for PCTL in Parametric Markov Decision Processes'. Together they form a unique fingerprint.

Cite this