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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Aspnes, J., Herlihy, M.: Fast randomized consensus using shared memory. Journal of Algorithms 11(3), 441–461 (1990)
Baier, C.: On algorithmic verification methods for probabilistic systems. Mannheim University, Habilitationsschrift (1998)
Baier, C., Hermanns, H.: Weak bisimulation for fully probabilistic processes. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 119–130. Springer, Heidelberg (1997)
Baier, C., Katoen, J.P.: Principles of Model Checking (Representation and Mind Series). The MIT Press, Cambridge (2008)
Bartocci, E., Grosu, R., Katsaros, P., Ramakrishnan, C.R., Smolka, S.A.: Model repair for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 326–340. Springer, Heidelberg (2011)
Bianco, A., Alfaro, L.D.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499–513. Springer, Heidelberg (1995)
Blackwell, D.: On the functional equation of dynamic programming. Journal of Mathematical Analysis and Applications 2(2), 273–276 (1961)
Blackwell, D.: Positive dynamic programming. In: Proceedings of the 5th Berkeley Symposium on Mathematical Statistics and Probability, pp. 415–418 (1967)
Bohnenkamp, H.C., van der Stok, P., Hermanns, H., Vaandrager, F.W.: Cost-optimization of the IPv4 Zeroconf protocol. In: DSN, pp. 531–540. IEEE Computer Society, Los Alamitos (2003)
van Dawen, R.: Finite state dynamic programming with the total reward criterion. Mathematical Methods of Operations Research 30, A1–A14 (1986)
Daws, C.: Symbolic and parametric model checking of discrete-time Markov chains. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 280–294. Springer, Heidelberg (2005)
Derisavi, S., Hermanns, H., Sanders, W.H.: Optimal state-space lumping in Markov chains. IPL 87(6), 309–315 (2003)
Dubins, L.E., Savage, L.: How to Gamble If You Must. McGraw-Hill, New York (1965)
Fränzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. JSAT 1(3-4), 209–236 (2007)
Fribourg, L., André, É.: An inverse method for policy iteration based algorithms. In: INFINITY, pp. 44–61. Open Publishing Association, EPTCS (2009)
Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: PARAM: A model checker for parametric Markov models. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 660–664. Springer, Heidelberg (2010)
Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. STTT 13, 3–19 (2010)
Han, T.: Diagnosis, synthesis and analysis of probabilistic models. Ph.D. thesis, RWTH Aachen University/University of Twente (2009)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. FAC 6, 102–111 (1994)
Haverkort, B.R., Cloth, L., Hermanns, H., Katoen, J.P., Baier, C.: Model checking performability properties. In: DSN, pp. 103–112 (2003)
Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to automata theory, languages, and computation. SIGACT News, 2nd edn. 32(1), 60–65 (2001)
Kwiatkowska, M., Norman, G., Segala, R.: Automated verification of a randomized distributed consensus protocol using Cadence SMV and PRISM. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 194–206. Springer, Heidelberg (2001)
Kwiatkowska, M.Z., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 220–270. Springer, Heidelberg (2007)
Lanotte, R., Maggiolo-Schettini, A., Troina, A.: Parametric probabilistic transition systems for system design and analysis. FAC 19(1), 93–109 (2007)
Passmore, G.O., Jackson, P.B.: Combined decision techniques for the existential theory of the reals. In: Carette, J., Dixon, L., Coen, C.S., Watt, S.M. (eds.) MKM 2009, Held as Part of CICM 2009. LNCS, vol. 5625, pp. 122–137. Springer, Heidelberg (2009)
Puterman, M.L.: Markov decision processes: Discrete stochastic dynamic programming. John Wiley and Sons, Chichester (1994)
Ratschan, S.: Efficient solving of quantified inequality constraints over the real numbers. CoRR cs.LO/0211016 (2002)
Ratschan, S.: Safety verification of non-linear hybrid systems is quasi-semidecidable. In: Kratochvíl, J., Li, A., Fiala, J., Kolman, P. (eds.) TAMC 2010. LNCS, vol. 6108, pp. 397–408. Springer, Heidelberg (2010)
Strauch, R.E.: Negative dynamic programming. Annals of Mathematical Statististics 37(4), 871–890 (1966)
van der Wal, J.: Stochastic dynamic programming. The Mathematical Centre, Amsterdam (1981)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hahn, E.M., Han, T., Zhang, L. (2011). Synthesis for PCTL in Parametric Markov Decision Processes. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds) NASA Formal Methods. NFM 2011. Lecture Notes in Computer Science, vol 6617. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20398-5_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-20398-5_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-20397-8
Online ISBN: 978-3-642-20398-5
eBook Packages: Computer ScienceComputer Science (R0)