{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T06:00:59Z","timestamp":1783490459806,"version":"3.55.0"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319961446","type":"print"},{"value":"9783319961453","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-96145-3_37","type":"book-chapter","created":{"date-parts":[[2018,7,20]],"date-time":"2018-07-20T22:25:55Z","timestamp":1532125555000},"page":"643-661","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":55,"title":["Sound Value Iteration"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2843-5511","authenticated-orcid":false,"given":"Tim","family":"Quatmann","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,7,18]]},"reference":[{"key":"37_CR1","doi-asserted-by":"crossref","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"ML Puterman","year":"1994","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, Hoboken (1994)"},{"key":"37_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-0805-2","volume-title":"Handbook of Markov Decision Processes: Methods and Applications","author":"EA Feinberg","year":"2002","unstructured":"Feinberg, E.A., Shwartz, A.: Handbook of Markov Decision Processes: Methods and Applications. Kluwer, Dordrecht (2002)"},{"key":"37_CR3","doi-asserted-by":"crossref","unstructured":"Katoen, J.P.: The probabilistic model checking landscape. In: LICS, pp. 31\u201345. ACM (2016)","DOI":"10.1145\/2933575.2934574"},{"key":"37_CR4","unstructured":"Baier, C.: Probabilistic model checking. In: Dependable Software Systems Engineering. NATO Science for Peace and Security Series - D: Information and Communication Security, vol. 45, pp. 1\u201323. IOS Press (2016)"},{"key":"37_CR5","unstructured":"Etessami, K.: Analysis of probabilistic processes and automata theory. In: Handbook of Automata Theory. European Mathematical Society (2016, to appear)"},{"key":"37_CR6","doi-asserted-by":"crossref","first-page":"963","DOI":"10.1007\/978-3-319-10575-8_28","volume-title":"Handbook of Model Checking","author":"C Baier","year":"2018","unstructured":"Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Probabilistic model checking. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 963\u2013999. Springer, Cham (2018)"},{"key":"37_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"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\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"37_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-319-63390-9_31","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2017","unstructured":"Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A Storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592\u2013600. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31"},{"key":"37_CR9","doi-asserted-by":"crossref","unstructured":"Katoen, J., Zapreev, I.S.: Safe on-the-fly steady-state detection for time-bounded reachability. In: QEST, pp. 301\u2013310. IEEE Computer Society (2006)","DOI":"10.1109\/QEST.2006.47"},{"issue":"4","key":"37_CR10","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1016\/0166-5316(94)00033-6","volume":"24","author":"M Malhotra","year":"1996","unstructured":"Malhotra, M.: A computationally efficient technique for transient analysis of repairable markovian systems. Perform. Eval. 24(4), 311\u2013331 (1996)","journal-title":"Perform. Eval."},{"issue":"2","key":"37_CR11","doi-asserted-by":"crossref","first-page":"12:1","DOI":"10.1145\/3060139","volume":"18","author":"P Daca","year":"2017","unstructured":"Daca, P., Henzinger, T.A., Kret\u00ednsk\u00fd, J., Petrov, T.: Faster statistical model checking for unbounded temporal properties. ACM Trans. Comput. Log. 18(2), 12:1\u201312:25 (2017)","journal-title":"ACM Trans. Comput. Log."},{"key":"37_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-319-63387-9_8","volume-title":"Computer Aided Verification","author":"C Baier","year":"2017","unstructured":"Baier, C., Klein, J., Leuschner, L., Parker, D., Wunderlich, S.: Ensuring the reliability of your model checker: interval iteration for markov decision processes. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 160\u2013180. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_8"},{"key":"37_CR13","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1016\/j.tcs.2016.12.003","volume":"735","author":"S Haddad","year":"2017","unstructured":"Haddad, S., Monmege, B.: Interval iteration algorithm for MDPs and IMDPs. Theor. Comput. Sci. 735, 111\u2013131 (2017)","journal-title":"Theor. Comput. Sci."},{"key":"37_CR14","first-page":"181","volume":"42","author":"P Dai","year":"2011","unstructured":"Dai, P., Weld, D.S., Goldsmith, J.: Topological value iteration algorithms. J. Artif. Intell. Res. 42, 181\u2013209 (2011)","journal-title":"J. Artif. Intell. Res."},{"key":"37_CR15","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"issue":"3","key":"37_CR16","doi-asserted-by":"crossref","first-page":"580","DOI":"10.1287\/moor.16.3.580","volume":"16","author":"DP Bertsekas","year":"1991","unstructured":"Bertsekas, D.P., Tsitsiklis, J.N.: An analysis of stochastic shortest path problems. Math. Oper. Res. 16(3), 580\u2013595 (1991)","journal-title":"Math. Oper. Res."},{"key":"37_CR17","doi-asserted-by":"crossref","unstructured":"Giro, S.: Efficient computation of exact solutions for quantitative model checking. In: QAPL. EPTCS, vol. 85, pp. 17\u201332 (2012)","DOI":"10.4204\/EPTCS.85.2"},{"key":"37_CR18","doi-asserted-by":"crossref","unstructured":"Bauer, M.S., Mathur, U., Chadha, R., Sistla, A.P., Viswanathan, M.: Exact quantitative probabilistic model checking through rational search. In: FMCAD, pp. 92\u201399. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102246"},{"key":"37_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-319-11936-6_8","volume-title":"Automated Technology for Verification and Analysis","author":"T Br\u00e1zdil","year":"2014","unstructured":"Br\u00e1zdil, T., et al.: Verification of Markov decision processes using learning algorithms. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 98\u2013114. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_8"},{"key":"37_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-319-11439-2_10","volume-title":"Reachability Problems","author":"S Haddad","year":"2014","unstructured":"Haddad, S., Monmege, B.: Reachability in MDPs: refining convergence of value iteration. In: Ouaknine, J., Potapov, I., Worrell, J. (eds.) RP 2014. LNCS, vol. 8762, pp. 125\u2013137. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11439-2_10"},{"key":"37_CR21","doi-asserted-by":"crossref","unstructured":"Quatmann, T., Katoen, J.P.: Sound value iteration. Technical report, CoRR abs\/1804.05001 (2018)","DOI":"10.1007\/978-3-319-96145-3_37"},{"key":"37_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-642-33386-6_25","volume-title":"Automated Technology for Verification and Analysis","author":"V Forejt","year":"2012","unstructured":"Forejt, V., Kwiatkowska, M., Parker, D.: Pareto curves for probabilistic model checking. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 317\u2013332. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33386-6_25"},{"key":"37_CR23","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: The PRISM benchmark suite. In: Proceedings of QEST, pp. 203\u2013204. IEEE CS (2012)","DOI":"10.1109\/QEST.2012.14"},{"key":"37_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-319-11936-6_13","volume-title":"Automated Technology for Verification and Analysis","author":"D Guck","year":"2014","unstructured":"Guck, D., Timmer, M., Hatefi, H., Ruijters, E., Stoelinga, M.: Modelling and analysis of markov reward automata. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 168\u2013184. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_13"},{"key":"37_CR25","unstructured":"Quatmann, T., Katoen, J.P.: Experimental Results for Sound Value Iteration. figshare (2018). https:\/\/doi.org\/10.6084\/m9.figshare.6139052"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-96145-3_37","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,5]],"date-time":"2025-07-05T23:02:46Z","timestamp":1751756566000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-96145-3_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319961446","9783319961453"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-96145-3_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}