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.
Keywords
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
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)
Bellman, R.: A Markovian decision process. Technical report, DTIC Document (1957)
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
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)
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
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
Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM (JACM) 42(4), 857–907 (1995)
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
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
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
Etessami, K., Yannakakis, M.: Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations. J. ACM (JACM) 56(1), 1 (2009)
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
Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. Int. J. Softw. Tools Technol. Transf. 13(1), 3–19 (2011)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512–535 (1994)
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)
O’Rourke, J.: Advanced problem 6369. Am. Math. Monthly 88(10), 769 (1981)
Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, Hoboken (2014)
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
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)
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
Rutten, J.J.M.M., Kwiatkowska, M., Norman, G., Parker, D.: Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. American Mathematical Society, Providence (2004)
Schaefer, M., Štefankovič, D.: Fixed points, Nash equilibria, and the existential theory of the reals. Theory Comput. Syst. 60, 172–193 (2011)
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
Tarski, A.: A Decision Method for Elementary Algebra and Geometry (1951)
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
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
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)