Synthesis for PCTL in Parametric Markov Decision Processes

Ernst Moritz  Hahn; Tingting Han; Lijun Zhang

doi:10.1007/978-3-642-20398-5_12

Synthesis for PCTL in Parametric Markov Decision Processes

Ernst Moritz Hahn, Tingting Han, Lijun Zhang

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

48 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 language	English
Title of host publication	NASA Formal Methods
Subtitle of host publication	Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings
Place of Publication	Berlin, Heidelberg
Publisher	Springer
Pages	146-161
ISBN (Electronic)	978-3-642-20398-5
ISBN (Print)	978-3-642-20397-8
DOIs	https://doi.org/10.1007/978-3-642-20398-5_12
Publication status	Published - 2011
Externally published	Yes
Event	3rd International Symposium on NASA Formal Methods, NFM 2011 - Pasadena, United States Duration: 18 Apr 2011 → 20 Apr 2011 Conference number: 3

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	6617
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	3rd International Symposium on NASA Formal Methods, NFM 2011
Abbreviated title	NFM
Country	United States
City	Pasadena
Period	18/04/11 → 20/04/11

Access to Document

10.1007/978-3-642-20398-5_12

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

Cite this

@inproceedings{e79cd938f14041fc8a6666cfbed94da2,

title = "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.",

author = "Hahn, {Ernst Moritz} and Tingting Han and Lijun Zhang",

year = "2011",

doi = "10.1007/978-3-642-20398-5_12",

language = "English",

isbn = "978-3-642-20397-8",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "146--161",

booktitle = "NASA Formal Methods",

note = "3rd International Symposium on NASA Formal Methods, NFM 2011, NFM ; Conference date: 18-04-2011 Through 20-04-2011",

}

Hahn, EM, Han, T & Zhang, L 2011, Synthesis for PCTL in Parametric Markov Decision Processes. in NASA Formal Methods: Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings. Lecture Notes in Computer Science, vol. 6617, Springer, Berlin, Heidelberg, pp. 146-161, 3rd International Symposium on NASA Formal Methods, NFM 2011, Pasadena, United States, 18/04/11. https://doi.org/10.1007/978-3-642-20398-5_12

Synthesis for PCTL in Parametric Markov Decision Processes. / Hahn, Ernst Moritz ; Han, Tingting; Zhang, Lijun.

NASA Formal Methods: Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings. Berlin, Heidelberg : Springer, 2011. p. 146-161 (Lecture Notes in Computer Science; Vol. 6617).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Synthesis for PCTL in Parametric Markov Decision Processes

AU - Hahn, Ernst Moritz

AU - Han, Tingting

AU - Zhang, Lijun

N1 - Conference code: 3

PY - 2011

Y1 - 2011

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-642-20398-5_12

DO - 10.1007/978-3-642-20398-5_12

M3 - Conference contribution

SN - 978-3-642-20397-8

T3 - Lecture Notes in Computer Science

SP - 146

EP - 161

BT - NASA Formal Methods

PB - Springer

CY - Berlin, Heidelberg

T2 - 3rd International Symposium on NASA Formal Methods, NFM 2011

Y2 - 18 April 2011 through 20 April 2011

ER -