Skip to main content
SpringerLink
Log in

Reward-Bounded Reachability Probability for Uncertain Weighted MDPs

  • Conference paper
  • First Online:
Verification, Model Checking, and Abstract Interpretation (VMCAI 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9583))

Abstract

In this paper we present a decision algorithm for computing maximal/minimal reward-bounded reachability probabilities in weighted MDPs with uncertainties. Even though an uncertain weighted MDP (\(\textit{UwMDP}\)) represents an equivalent weighted MDP which may be exponentially larger, our algorithm does not cause an exponentially blow-up and will terminate in polynomial time with respect to the size of \(\textit{UwMDP}\)s. We also define bisimulation relations for \(\textit{UwMDP}\)s, which are compositional and can be decided in polynomial time as well. We develop a prototype tool and apply it to some case studies to show its effectiveness.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    We only consider integer weights in this paper. The extension to rational weights is straightforward.

  2. 2.

    Here, \(\mathcal {B}\) is the standard \(\sigma \)-algebra over \( Paths ^{ inf }_{\mathcal {M}_{\mathcal {U}}}\) generated from the set of all cylinder sets \(\{ Paths _{{\mathcal {M}_{\mathcal {U}}}}^{ \xi } \mid \xi \in Paths ^{ fin }_{\mathcal {M}_{\mathcal {U}}}\}\). The unique probability measure is obtained by the application of the extension theorem (see, e.g. [7]) .

References

  1. Andova, S., Hermanns, H., Katoen, J.-P.: Discrete-time rewards model-checked. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  2. Aspnes, J., Herlihy, M.: Fast randomized consensus using shared memory. J. Algorithms 11(3), 441–461 (1990)

    Article  MATH  MathSciNet  Google Scholar 

  3. Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  4. Baier, C., Größer, M., Leucker, M., Bollig, B., Ciesinski, F.: Controller synthesis for probabilistic systems. In: Proceedings of IFIP TCS 2004. Kluwer (2004)

    Google Scholar 

  5. Benedikt, M., Lenhardt, R., Worrell, J.: LTL model checking of interval markov chains. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 32–46. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  6. Bernardo, M., Gorrieri, R.: Extended markovian process algebra. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119. Springer, Heidelberg (1996)

    Google Scholar 

  7. Billingsley, P.: Probability and Measure. John Wiley and Sons, New York (1979)

    MATH  Google Scholar 

  8. Böde, E., Herbstritt, M., Hermanns, H., Johr, S., Peikenkamp, T., Pulungan, R., Rakow, J., Wimmer, R., Becker, B.: Compositional dependability evaluation for STATEMATE. ITSE 35(2), 274–292 (2009)

    Article  Google Scholar 

  9. Boudali, H., Crouzen, P., Stoelinga, M.: A rigorous, compositional, and extensible framework for dynamic fault tree analysis. IEEE TDSC 7(2), 128–143 (2010)

    Google Scholar 

  10. Bozga, M., David, A., Hartmanns, A., Hermanns, H., Larsen, K.G., Legay, A., Tretmans, J.: State-of-the-art tools and techniques for quantitative modeling and analysis of embedded systems. In: DATE, pp. 370–375. IEEE, March 2012

    Google Scholar 

  11. Cantino, A.S., Roberts, D.L., Isbell, C.L.: Autonomous nondeterministic tour guides: improving quality of experience with TTD-MDPs. In: AAMAS, p. 22. IFAAMAS (2007)

    Google Scholar 

  12. Cattani, S., Segala, R.: Decision algorithms for probabilistic bisimulation. In: Brim, L., Jančar, P., Křetínský, M., Kučera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 371–385. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  13. Chehaibar, G., Garavel, H., Mounier, L., Tawbi, N., Zulian, F.: Specification and verification of the powerscale bus arbitration protocol: an industrial experiment with LOTOS. In: FORTE, pp. 435–450 (1996)

    Google Scholar 

  14. Chen, T., Han, T., Kwiatkowska, M.: On the complexity of model checking interval-valued discrete time Markov chains. Inf. Process. Lett. 113(7), 210–216 (2013)

    Article  MATH  MathSciNet  Google Scholar 

  15. Delahaye, B., Katoen, J.-P., Larsen, K.G., Legay, A., Pedersen, M.L., Sher, F., Wasowski, A.: New results on abstract probabilistic automata. In: ACSD, pp. 118–127 (2011)

    Google Scholar 

  16. Delahaye, B., Katoen, J.-P., Larsen, K.G., Legay, A., Pedersen, M.L., Sher, F., Wąsowski, A.: Abstract probabilistic automata. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 324–339. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  17. Delahaye, B., Larsen, K.G., Legay, A., Pedersen, M.L., Wąsowski, A.: Decision problems for interval markov chains. In: Dediu, A.-H., Inenaga, S., Martín-Vide, C. (eds.) LATA 2011. LNCS, vol. 6638, pp. 274–285. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  18. Fecher, H., Leucker, M., Wolf, V.: Don’t know in probabilistic systems. In: Valmari, A. (ed.) SPIN. LNCS, vol. 3925, pp. 71–88. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  19. Gebler, D., Hashemi, V., Turrini, A.: Computing behavioral relations for probabilistic concurrent systems. In: Remke, A., Stoelinga, M. (eds.) Stochastic Model Checking. LNCS, vol. 8453, pp. 117–155. Springer, Heidelberg (2014)

    Google Scholar 

  20. Givan, R., Leach, S.M., Dean, T.L.: Bounded-parameter markov decision processes. Artif. Intell. 122(1–2), 71–109 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  21. Hahn, E.M., Han, T., Zhang, L.: Synthesis for PCTL in parametric markov decision processes. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 146–161. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  22. Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: iscasMc: a web-based probabilistic model checker. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 312–317. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  23. Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Asp. Comput. 6(5), 512–535 (1994)

    Article  MATH  Google Scholar 

  24. Hashemi, V., Hatefi, H., Krčál, J.: Probabilistic bisimulations for PCTL model checking of interval mdps. In: SynCoP, pp. 19–33. EPTCS (2014)

    Google Scholar 

  25. Hashemi, V., Hermanss, H., Turrini, A.: On the efficiency of deciding probabilistic automata weak bisimulation. Electron. Commun. EASST, vol. 66 (2013)

    Google Scholar 

  26. Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS, pp. 266–277 (1991)

    Google Scholar 

  27. Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. I&C 86, 43–68 (1990)

    MATH  MathSciNet  Google Scholar 

  28. Katoen, J.-P., Klink, D., Neuhäußer, M.R.: Compositional abstraction for stochastic systems. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol. 5813, pp. 195–211. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  29. Kozine, I.O., Utkin, L.V.: Interval-valued finite markov chains. Reliable Comput. 8(2), 97–113 (2011)

    Article  MathSciNet  Google Scholar 

  30. Chatterjee, K., Sen, K., Henzinger, T.A.: Model-Checking \(\omega \)-regular properties of interval markov chains. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 302–317. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  31. Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  32. 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)

    Chapter  Google Scholar 

  33. Lynch, N.A., Segala, R., Vaandrager, F.W.: Compositionality for probabilistic automata. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 208–221. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  34. Marsan, M.A., Conte, G., Balbo, G.: A class of generalized stochastic Petri nets for the performance evaluation of multiprocessor systems. ACM Trans. Comput. Syst. 2(2), 93–122 (1984)

    Article  Google Scholar 

  35. Nilim, A., El Ghaoui, L.: Robust control of Markov decision processes with uncertain transition matrices. Oper. Res. 53(5), 780–798 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  36. Puggelli, A., Li, W., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Polynomial-time verification of PCTL properties of MDPs with convex uncertainties. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 527–542. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  37. Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Probability and Statistics, vol. 594. John Wiley & Sons Inc., New York (2005)

    Google Scholar 

  38. Segala, R.: Verification of randomized distributed algorithms. In: Brinksma, E., Hermanns, H., Katoen, J.-P. (eds.) EEF School 2000 and FMPA 2000. LNCS, vol. 2090, pp. 232–260. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  39. Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. Nord. J. Comput. 2(2), 250–273 (1995)

    MATH  MathSciNet  Google Scholar 

  40. Wolff, E.M., Topcu, U., Murray, R.M.: Robust control of uncertain markov decision processes with temporal logic specifications. In: CDC, pp. 3372–3379. IEEE (2012)

    Google Scholar 

  41. Wu, D., Koutsoukos, X.D.: Reachability analysis of uncertain systems using boundedparameter markov decision processes. Artif. Intell. 172(8–9), 945–954 (2008)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Acknowledgments

This work is supported by the EU 7th Framework Programme under grant agreements 295261 (MEALS) and 318490 (SENSATION), the DFG Transregional Collaborative Research Centre SFB/TR 14 AVACS, the CAS/SAFEA International Partnership Program for Creative Research Teams, the Australian Research Council under Grant DP130102764, and the National Natural Science Foundation of China under Grant Nos. 61428208, 61472473 and 61361136002.

Author information

Authors and Affiliations

  1. Max Planck Institute for Informatics, Saarbrücken, Germany

    Vahid Hashemi

  2. Department of Computer Science, Saarland University, Saarbrücken, Germany

    Vahid Hashemi & Holger Hermanns

  3. University of Technology, Sydney, Australia

    Lei Song

Authors
  1. Vahid Hashemi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Holger Hermanns
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Lei Song
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Vahid Hashemi .

Editor information

Editors and Affiliations

  1. EPFL IC-DO, Lausanne, Switzerland

    Barbara Jobstmann

  2. Microsoft Research, Redmond, Washington, USA

    K. Rustan M. Leino

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hashemi, V., Hermanns, H., Song, L. (2016). Reward-Bounded Reachability Probability for Uncertain Weighted MDPs. In: Jobstmann, B., Leino, K. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2016. Lecture Notes in Computer Science(), vol 9583. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-49122-5_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-49122-5_17

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-49121-8

  • Online ISBN: 978-3-662-49122-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation