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)

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.
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
PublisherSpringer
Pages146-161
ISBN (Electronic)978-3-642-20398-5
ISBN (Print)978-3-642-20397-8
DOIs
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
PublisherSpringer
Volume6617
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference3rd International Symposium on NASA Formal Methods, NFM 2011
Abbreviated titleNFM
CountryUnited States
CityPasadena
Period18/04/1120/04/11

Fingerprint

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

Cite this