Skip to main content
SpringerLink
Log in

Reachability in Augmented Interval Markov Chains

  • Conference paper
  • First Online:
Reachability Problems (RP 2019)

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

Included in the following conference series:

Abstract

In this paper we propose augmented interval Markov chains (AIMCs): a generalisation of the familiar interval Markov chains (IMCs) where uncertain transition probabilities are in addition allowed to depend on one another. This new model preserves the flexibility afforded by IMCs for describing stochastic systems where the parameters are unclear, for example due to measurement error, but also allows us to specify transitions with probabilities known to be identical, thereby lending further expressivity.

The focus of this paper is reachability in AIMCs. We study the qualitative, exact quantitative and approximate reachability problem, as well as natural subproblems thereof, and establish several upper and lower bounds for their complexity. We prove the exact reachability problem is at least as hard as the well-known square-root sum problem, but, encouragingly, the approximate version lies in \(\mathbf {NP}\) if the underlying graph is known, whilst the restriction of the exact problem to a constant number of uncertain edges is in \(\mathbf {P}\). Finally, we show that uncertainty in the graph structure affects complexity by proving \(\mathbf {NP}\)-completeness for the qualitative subproblem, in contrast with an easily-obtained upper bound of \(\mathbf {P}\) for the same subproblem with known graph structure.

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

References

  1. Allender, E., Bürgisser, P., Kjeldgaard-Pedersen, J., Miltersen, P.B.: On the complexity of numerical analysis. SIAM J. Comput. 38(5), 1987–2006 (2009)

    Article  MathSciNet  Google Scholar 

  2. Bellman, R.: A Markovian decision process. Technical report, DTIC Document (1957)

    Google Scholar 

  3. Benedikt, M., Lenhardt, R., Worrell, J.: LTL model checking of interval Markov chains. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 32–46. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36742-7_3

    Chapter  MATH  Google Scholar 

  4. Blum, L., Shub, M., Smale, S.: On a theory of computation and complexity over the real numbers: \(\mathit{NP}\)-completeness, recursive functions and universal machines. Bull. (New Ser.) Am. Math. Soc. 21(1), 1–46 (1989)

    Google Scholar 

  5. Chatterjee, K.: Robustness of structurally equivalent concurrent parity games. In: Birkedal, L. (ed.) FoSSaCS 2012. LNCS, vol. 7213, pp. 270–285. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28729-9_18

    Chapter  Google Scholar 

  6. Chatterjee, K., Sen, K., Henzinger, T.A.: Model-checking \({\omega }\)-regular properties of interval Markov chains. In: Amadio, R. (ed.) FoSSaCS 2008. LNCS, vol. 4962, pp. 302–317. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78499-9_22

    Chapter  MATH  Google Scholar 

  7. Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM (JACM) 42(4), 857–907 (1995)

    Article  MathSciNet  Google Scholar 

  8. Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.-P., Topcu, U.: Synthesis in pMDPs: a tale of 1001 parameters. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 160–176. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-01090-4_10

    Chapter  Google Scholar 

  9. 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). https://doi.org/10.1007/978-3-642-21254-3_21

    Chapter  Google Scholar 

  10. Delahaye, B., Lime, D., Petrucci, L.: Parameter synthesis for parametric interval Markov chains. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 372–390. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49122-5_18

    Chapter  Google Scholar 

  11. Etessami, K., Yannakakis, M.: Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations. J. ACM (JACM) 56(1), 1 (2009)

    Article  MathSciNet  Google Scholar 

  12. Garey, M.R., Graham, R.L., Johnson, D.S.: Some NP-complete geometric problems. In: Proceedings of the Eighth Annual ACM Symposium on Theory of Computing, STOC 1976, pp. 10–22. ACM, New York (1976). https://doi.org/10.1145/800113.803626

  13. Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. Int. J. Softw. Tools Technol. Transf. 13(1), 3–19 (2011)

    Article  Google Scholar 

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

    Article  Google Scholar 

  15. Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: Proceedings of Sixth Annual IEEE Symposium on Logic in Computer Science. LICS 1991, pp. 266–277. IEEE (1991)

    Google Scholar 

  16. O’Rourke, J.: Advanced problem 6369. Am. Math. Monthly 88(10), 769 (1981)

    Google Scholar 

  17. Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, Hoboken (2014)

    Google Scholar 

  18. Quatmann, T., Dehnert, C., Jansen, N., Junges, S., Katoen, J.-P.: Parameter synthesis for Markov models: faster than ever. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 50–67. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46520-3_4

    Chapter  MATH  Google Scholar 

  19. Randour, M., Raskin, J.F., Sankur, O.: Percentile queries in multi-dimensional Markov decision processes. Formal Methods Syst. Des. 50(2–3), 207–248 (2017)

    Article  Google Scholar 

  20. Renegar, J.: On the computational complexity and geometry of the first-order theory of the reals. Part I: Introduction. Preliminaries. The geometry of semi-algebraic sets. The decision problem for the existential theory of the reals. J. Symb. Comput. 13(3), 255–299 (1992). https://doi.org/10.1016/S0747-7171(10)80003-3

    Article  MathSciNet  Google Scholar 

  21. Rutten, J.J.M.M., Kwiatkowska, M., Norman, G., Parker, D.: Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. American Mathematical Society, Providence (2004)

    Google Scholar 

  22. Schaefer, M., Štefankovič, D.: Fixed points, Nash equilibria, and the existential theory of the reals. Theory Comput. Syst. 60, 172–193 (2011)

    Article  MathSciNet  Google Scholar 

  23. Sen, K., Viswanathan, M., Agha, G.: Model-checking Markov chains in the presence of uncertainties. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 394–410. Springer, Heidelberg (2006). https://doi.org/10.1007/11691372_26

    Chapter  MATH  Google Scholar 

  24. Tarski, A.: A Decision Method for Elementary Algebra and Geometry (1951)

    Google Scholar 

  25. Tiwari, P.: A problem that is easier to solve on the unit-cost algebraic RAM. J. Complex. 8(4), 393–397 (1992). https://doi.org/10.1016/0885-064X(92)90003-T

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. MPI-SWS, Saarbrücken, Germany

    Ventsislav Chonev

Authors
  1. Ventsislav Chonev
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ventsislav Chonev .

Editor information

Editors and Affiliations

  1. Université Libre de Bruxelles, Brussels, Belgium

    Emmanuel Filiot

  2. Université Catholique de Louvain, Louvain-la-Neuve, Belgium

    Raphaël Jungers

  3. University of Liverpool, Liverpool, UK

    Igor Potapov

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Chonev, V. (2019). Reachability in Augmented Interval Markov Chains. In: Filiot, E., Jungers, R., Potapov, I. (eds) Reachability Problems. RP 2019. Lecture Notes in Computer Science(), vol 11674. Springer, Cham. https://doi.org/10.1007/978-3-030-30806-3_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-30806-3_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-30805-6

  • Online ISBN: 978-3-030-30806-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation