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