{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:41:03Z","timestamp":1764402063867,"version":"3.46.0"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031906527"},{"type":"electronic","value":"9783031906534"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Two standard models for probabilistic systems are Markov chains (MCs) and Markov decision processes (MDPs). Classic objectives for such probabilistic models for control and planning problems are reachability and stochastic shortest path. The widely studied algorithmic approach for these problems is the Value Iteration (VI) algorithm which iteratively applies local updates called Bellman updates. There are many practical approaches for VI in the literature but they all require exponentially many Bellman updates for MCs in the worst case. A preprocessing step is an algorithm that is discrete, graph-theoretical, and requires linear space. An important open question is whether, after a polynomial-time preprocessing, VI can be achieved with sub-exponentially many Bellman updates. In this work, we present a new approach for VI based on guessing values. Our theoretical contributions are twofold. First, for MCs, we present an almost-linear-time preprocessing algorithm after which, along with guessing values, VI requires only subexponentially many Bellman updates. Second, we present an improved analysis of the speed of convergence of VI for MDPs. Finally, we present a practical algorithm for MDPs based on our new approach. Experimental results show that our approach provides a considerable improvement over existing VI-based approaches on several benchmark examples from the literature.<\/jats:p>","DOI":"10.1007\/978-3-031-90653-4_11","type":"book-chapter","created":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T09:24:55Z","timestamp":1746177895000},"page":"217-236","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Value Iteration with Guessing for Markov Chains and Markov Decision Processes"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4561-241X","authenticated-orcid":false,"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0002-0495-3805","authenticated-orcid":false,"given":"Mahdi","family":"JafariRaviz","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5103-038X","authenticated-orcid":false,"given":"Raimundo","family":"Saona","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1419-3267","authenticated-orcid":false,"given":"Jakub","family":"Svoboda","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"doi-asserted-by":"publisher","unstructured":"Aspnes, J., Herlihy, M.: Fast Randomized Consensus Using Shared Memory. Journal of Algorithms 11(3), 441\u2013461 (1990). https:\/\/doi.org\/10.1016\/0196-6774(90)90021-6","key":"11_CR1","DOI":"10.1016\/0196-6774(90)90021-6"},{"unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge, MA, USA (Apr 2008)","key":"11_CR2"},{"doi-asserted-by":"publisher","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: Computer Aided Verification, vol. 10426, pp. 160\u2013180 (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_8","key":"11_CR3","DOI":"10.1007\/978-3-319-63387-9_8"},{"doi-asserted-by":"publisher","unstructured":"Balaji, N., Kiefer, S., Novotn\u00fd, P., P\u00e9rez, G.A., Shirmohammadi, M.: On the Complexity of Value Iteration. ICALP 132, 102:1\u2013102:15 (2019). https:\/\/doi.org\/10.4230\/LIPICS.ICALP.2019.102","key":"11_CR4","DOI":"10.4230\/LIPICS.ICALP.2019.102"},{"doi-asserted-by":"publisher","unstructured":"Balbo, G., De\u00a0Pierro, M., Franceschinis, G.: Tagged Generalized Stochastic Petri Nets. In: Computer Performance Engineering, vol.\u00a05652, pp. 1\u201315 (2009). https:\/\/doi.org\/10.1007\/978-3-642-02924-0_1","key":"11_CR5","DOI":"10.1007\/978-3-642-02924-0_1"},{"doi-asserted-by":"crossref","unstructured":"Bellman, R.: A Markovian Decision Process. Journal of Mathematics and Mechanics 6(5), 679\u2013684 (1957)","key":"11_CR6","DOI":"10.1512\/iumj.1957.6.56038"},{"doi-asserted-by":"crossref","unstructured":"Boyd, S.P., Vandenberghe, L.: Convex Optimization. Cambridge University Press (2004)","key":"11_CR7","DOI":"10.1017\/CBO9780511804441"},{"doi-asserted-by":"publisher","unstructured":"Br\u00e1zdil, T., Bro\u017eek, V., Chatterjee, K., Forejt, V., Ku\u010dera, A.: Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. In: IEEE 26th Annual Symposium on Logic in Computer Science. pp. 33\u201342 (2011). https:\/\/doi.org\/10.1109\/LICS.2011.10","key":"11_CR8","DOI":"10.1109\/LICS.2011.10"},{"doi-asserted-by":"publisher","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Chmel\u00edk, M., Forejt, V., K\u0159et\u00ednsk\u00fd, J., Kwiatkowska, M., Parker, D., Ujma, M.: Verification of Markov Decision Processes Using Learning Algorithms. In: Automated Technology for Verification and Analysis, vol.\u00a08837, pp. 98\u2013114 (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_8","key":"11_CR9","DOI":"10.1007\/978-3-319-11936-6_8"},{"doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Dvo\u0159\u00e1k, W., Henzinger, M., Loitzenbauer, V.: Lower Bounds for Symbolic Computation on Graphs: Strongly Connected Components, Liveness, Safety, and Diameter. In: Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pp. 2341\u20132356 (2018). https:\/\/doi.org\/10.1137\/1.9781611975031.151","key":"11_CR10","DOI":"10.1137\/1.9781611975031.151"},{"doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Henzinger, M.: Faster and Dynamic Algorithms For Maximal End-Component Decomposition And Related Graph Problems In Probabilistic Verification. In: Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms (SODA). pp. 1318\u20131336 (2011). https:\/\/doi.org\/10.1137\/1.9781611973082.101","key":"11_CR11","DOI":"10.1137\/1.9781611973082.101"},{"doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Henzinger, M.: Efficient and Dynamic Algorithms for Alternating B\u00fcchi Games and Maximal End-Component Decomposition. Journal of the ACM 61(3), 1\u201340 (2014). https:\/\/doi.org\/10.1145\/2597631","key":"11_CR12","DOI":"10.1145\/2597631"},{"doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Henzinger, M., Joglekar, M., Shah, N.: Symbolic Algorithms for Qualitative Analysis of Markov Decision Processes with B\u00fcchi Objectives. Formal Methods in System Design 42(3), 301\u2013327 (2013). https:\/\/doi.org\/10.1007\/s10703-012-0180-2","key":"11_CR13","DOI":"10.1007\/s10703-012-0180-2"},{"doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Henzinger, T.A.: Value Iteration. In: 25 Years of Model Checking, vol.\u00a05000, pp. 107\u2013138 (2008). https:\/\/doi.org\/10.1007\/978-3-540-69850-0_7","key":"11_CR14","DOI":"10.1007\/978-3-540-69850-0_7"},{"doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Meggendorfer, T., Saona, R., Svoboda, J.: Faster Algorithm for Turn-based Stochastic Games with Bounded Treewidth. In: Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms (SODA). pp. 4590\u20134605 (2023). https:\/\/doi.org\/10.1137\/1.9781611977554.ch173","key":"11_CR15","DOI":"10.1137\/1.9781611977554.ch173"},{"doi-asserted-by":"publisher","unstructured":"Dombrowski, C., Junges, S., Katoen, J.P., Gross, J.: Model-Checking Assisted Protocol Design for Ultra-reliable Low-Latency Wireless Networks. In: IEEE 35th Symposium on Reliable Distributed Systems (SRDS). pp. 307\u2013316 (2016). https:\/\/doi.org\/10.1109\/SRDS.2016.048","key":"11_CR16","DOI":"10.1109\/SRDS.2016.048"},{"doi-asserted-by":"crossref","unstructured":"Even, S., Even, G.: Graph algorithms. Cambridge University Press, 2nd ed edn. (2012)","key":"11_CR17","DOI":"10.1017\/CBO9781139015165"},{"doi-asserted-by":"publisher","unstructured":"Even, S., Goldreich, O., Lempel, A.: A Randomized Protocol for Signing Contracts. Communications of the ACM 28(6), 637\u2013647 (Jun 1985). https:\/\/doi.org\/10.1145\/3812.3818","key":"11_CR18","DOI":"10.1145\/3812.3818"},{"doi-asserted-by":"publisher","unstructured":"Everett, H.: Recursive Games. In: Contributions to the Theory of Games III. vol.\u00a039, pp. 47\u201378 (1957). https:\/\/doi.org\/10.1515\/9781400882151-004","key":"11_CR19","DOI":"10.1515\/9781400882151-004"},{"doi-asserted-by":"publisher","unstructured":"Filar, J., Vrieze, K.: Competitive Markov Decision Processes (1997). https:\/\/doi.org\/10.1007\/978-1-4612-4054-9","key":"11_CR20","DOI":"10.1007\/978-1-4612-4054-9"},{"doi-asserted-by":"publisher","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated Verification Techniques for Probabilistic Systems. In: Formal Methods for Eternal Networked Software Systems, vol.\u00a06659, pp. 53\u2013113 (2011). https:\/\/doi.org\/10.1007\/978-3-642-21455-4_3","key":"11_CR21","DOI":"10.1007\/978-3-642-21455-4_3"},{"doi-asserted-by":"publisher","unstructured":"Fredman, M., Tarjan, R.: Fibonacci Heaps and their Uses in Improved Network Optimization Algorithms. In: 25th Annual Symposium onFoundations of Computer Science. pp. 338\u2013346 (1984). https:\/\/doi.org\/10.1109\/SFCS.1984.715934","key":"11_CR22","DOI":"10.1109\/SFCS.1984.715934"},{"doi-asserted-by":"publisher","unstructured":"Grover, K., Kret\u00ednsk\u00fd, J., Meggendorfer, T., Weininger, M.: Anytime Guarantees for Reachability in Uncountable Markov Decision Processes. In: International Conference on Concurrency Theory (CONCUR). vol.\u00a0243, pp. 11:1\u201311:20 (2022). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2022.11","key":"11_CR23","DOI":"10.4230\/LIPIcs.CONCUR.2022.11"},{"doi-asserted-by":"publisher","unstructured":"Haddad, S., Monmege, B.: Interval Iteration Algorithm for MDPs and IMDPs. Theoretical Computer Science 735, 111\u2013131 (2018). https:\/\/doi.org\/10.1016\/j.tcs.2016.12.003","key":"11_CR24","DOI":"10.1016\/j.tcs.2016.12.003"},{"doi-asserted-by":"publisher","unstructured":"Hartmanns, A.: Correct Probabilistic Model Checking with Floating-Point Arithmetic. In: Tools and Algorithms for the Construction and Analysis of Systems, vol. 13244, pp. 41\u201359 (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_3","key":"11_CR25","DOI":"10.1007\/978-3-030-99527-0_3"},{"doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Junges, S., Quatmann, T., Weininger, M.: A Practitioner\u2019s Guide to MDP Model Checking Algorithms. In: Tools and Algorithms for the Construction and Analysis of Systems, vol. 13993, pp. 469\u2013488 (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_24","key":"11_CR26","DOI":"10.1007\/978-3-031-30823-9_24"},{"doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Kaminski, B.L.: Optimistic Value Iteration. In: Computer Aided Verification (CAV), vol. 12225, pp. 488\u2013511 (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_26","key":"11_CR27","DOI":"10.1007\/978-3-030-53291-8_26"},{"doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The Quantitative Verification Benchmark Set. In: Tools and Algorithms for the Construction and Analysis of Systems, vol. 11427, pp. 344\u2013350 (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_20","key":"11_CR28","DOI":"10.1007\/978-3-030-17462-0_20"},{"doi-asserted-by":"publisher","unstructured":"Haverkort, B., Hermanns, H., Katoen, J.P.: On the Use of Model Checking Techniques for Dependability Evaluation. In: Proceedings of the IEEE Symposium on Reliable Distributed Systems. pp. 228\u2013237 (2000). https:\/\/doi.org\/10.1109\/RELDI.2000.885410","key":"11_CR29","DOI":"10.1109\/RELDI.2000.885410"},{"doi-asserted-by":"publisher","unstructured":"Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The Probabilistic Model Checker Storm. International Journal on Software Tools for Technology Transfer 24(4), 589\u2013610 (2022). https:\/\/doi.org\/10.1007\/s10009-021-00633-z","key":"11_CR30","DOI":"10.1007\/s10009-021-00633-z"},{"doi-asserted-by":"publisher","unstructured":"Ibe, O., Trivedi, K.: Stochastic Petri net models of polling systems. IEEE Journal on Selected Areas in Communications 8(9), 1649\u20131657 (1990). https:\/\/doi.org\/10.1109\/49.62852","key":"11_CR31","DOI":"10.1109\/49.62852"},{"doi-asserted-by":"publisher","unstructured":"Jansen, N., Dehnert, C., Kaminski, B.L., Katoen, J.P., Westhofen, L.: Bounded Model Checking for Probabilistic Programs. In: Automated Technology for Verification and Analysis, vol.\u00a09938, pp. 68\u201385 (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_5","key":"11_CR32","DOI":"10.1007\/978-3-319-46520-3_5"},{"doi-asserted-by":"publisher","unstructured":"Kwiatkowsa, M., Norman, G., Parker, D.: The PRISM Benchmark Suite. In: International Conference on Quantitative Evaluation of Systems. pp. 203\u2013204 (2012). https:\/\/doi.org\/10.1109\/QEST.2012.14","key":"11_CR33","DOI":"10.1109\/QEST.2012.14"},{"doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of Probabilistic Real-Time Systems. In: Computer Aided Verification (CAV), vol.\u00a06806, pp. 585\u2013591 (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47","key":"11_CR34","DOI":"10.1007\/978-3-642-22110-1_47"},{"unstructured":"Muppala, J., Ciardo, G., Trivedi, K.: Stochastic reward nets for reliability prediction. Communications in Reliability, Maintainability and Serviceability 1(2), 9\u201320 (1994)","key":"11_CR35"},{"doi-asserted-by":"publisher","unstructured":"Phalakarn, K., Takisaka, T., Haas, T., Hasuo, I.: Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games. In: Computer Aided Verification, vol. 12225, pp. 349\u2013371 (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_19","key":"11_CR36","DOI":"10.1007\/978-3-030-53291-8_19"},{"doi-asserted-by":"publisher","unstructured":"Pollack, M.: The Maximum Capacity Through a Network. Operations Research 8(5), 733\u2013736 (1960). https:\/\/doi.org\/10.1287\/opre.8.5.733","key":"11_CR37","DOI":"10.1287\/opre.8.5.733"},{"unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley (2014)","key":"11_CR38"},{"doi-asserted-by":"publisher","unstructured":"Qiu, Q., Wu, Q., Pedram, M.: Stochastic Modeling of a Power-Managed System: Construction and Optimization. In: Proceedings of the 1999 International Symposium on Low Power Electronics and Design - ISLPED \u201999. pp. 194\u2013199 (1999). https:\/\/doi.org\/10.1145\/313817.313923","key":"11_CR39","DOI":"10.1145\/313817.313923"},{"doi-asserted-by":"publisher","unstructured":"Quatmann, T., Katoen, J.P.: Sound Value Iteration. In: Computer Aided Verification (CAV), vol. 10981, pp. 643\u2013661 (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_37","key":"11_CR40","DOI":"10.1007\/978-3-319-96145-3_37"},{"doi-asserted-by":"publisher","unstructured":"Reiter, M.K., Rubin, A.D.: Crowds: Anonymity for Web Transactions. ACM Transactions on Information and System Security 1(1), 66\u201392 (1998). https:\/\/doi.org\/10.1145\/290163.290168","key":"11_CR41","DOI":"10.1145\/290163.290168"},{"doi-asserted-by":"publisher","unstructured":"Sidford, A., Wang, M., Wu, X., Ye, Y.: Variance Reduced Value Iteration and Faster Algorithms for Solving Markov Decision Processes. In: Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms (SODA). pp. 770\u2013787 (2018). https:\/\/doi.org\/10.1137\/1.9781611975031.50","key":"11_CR42","DOI":"10.1137\/1.9781611975031.50"},{"doi-asserted-by":"publisher","unstructured":"Stoelinga, M., Vaandrager, F.: Root Contention in IEEE 1394. In: Formal Methods for Real-Time and Probabilistic Systems, vol.\u00a01601, pp. 53\u201374 (1999). https:\/\/doi.org\/10.1007\/3-540-48778-6_4","key":"11_CR43","DOI":"10.1007\/3-540-48778-6_4"},{"doi-asserted-by":"crossref","unstructured":"Younes, H.L.S., Littman, M.L., Weissman, D., Asmuth, J.: The First Probabilistic Track of the International Planning Competition. Journal of Artificial Intelligence Research 24(1), 851\u2013887 (2005)","key":"11_CR44","DOI":"10.1613\/jair.1880"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90653-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:36:37Z","timestamp":1764401797000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90653-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906527","9783031906534"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90653-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}