{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:14:49Z","timestamp":1784837689726,"version":"3.55.0"},"publisher-location":"Cham","reference-count":53,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030995263","type":"print"},{"value":"9783030995270","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T00:00:00Z","timestamp":1648598400000},"content-version":"vor","delay-in-days":88,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We consider the problem: is the optimal expected total reward to reach a goal state in a partially observable Markov decision process (POMDP) below a given threshold? We tackle this\u2014generally undecidable\u2014problem by computing under-approximations on these total expected rewards. This is done by abstracting finite unfoldings of the infinite belief MDP of the POMDP. The key issue is to find a suitable under-approximation of the value function. We provide two techniques: a simple (cut-off) technique that uses a good policy on the POMDP, and a more advanced technique (belief clipping) that uses minimal shifts of probabilities between beliefs. We use mixed-integer linear programming (MILP) to find such minimal probability shifts and experimentally show that our techniques scale quite well while providing tight lower bounds on the expected total reward.<\/jats:p>","DOI":"10.1007\/978-3-030-99527-0_2","type":"book-chapter","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:37:21Z","timestamp":1648535841000},"page":"22-40","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Under-Approximating Expected Total Rewards in POMDPs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7026-228X","authenticated-orcid":false,"given":"Alexander","family":"Bork","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"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2843-5511","authenticated-orcid":false,"given":"Tim","family":"Quatmann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,3,30]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Amato, C., Bernstein, D.S., Zilberstein, S.: Optimizing fixed-size stochastic controllers for POMDPs and decentralized POMDPs. Auton. Agents Multi Agent Syst. 21(3), 293\u2013320 (2010)","DOI":"10.1007\/s10458-009-9103-z"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Ashok, P., Butkova, Y., Hermanns, H., Kret\u00ednsk\u00fd, J.: Continuous-time Markov decisions based on partial exploration. In: ATVA. Lecture Notes in Computer Science, vol. 11138, pp. 317\u2013334. Springer (2018)","DOI":"10.1007\/978-3-030-01090-4_19"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Astr\u00f6m, K.J.: Optimal control of Markov processes with incomplete state information. J. of Mathematical Analysis and Applications 10(1), 174\u2013205 (1965)","DOI":"10.1016\/0022-247X(65)90154-X"},{"key":"2_CR4","unstructured":"Baier, C., Katoen, J.P.: Principles of model checking. MIT Press (2008)"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Bellman, R.: A Markovian decision process. Journal of Mathematics and Mechanics 6, 679\u2013684 (1957)","DOI":"10.1512\/iumj.1957.6.56038"},{"key":"2_CR6","unstructured":"Bonet, B.: Solving large POMDPs using real time dynamic programming. In: AAAI Fall Symp. on POMDPs (1998)"},{"key":"2_CR7","unstructured":"Bonet, B., Geffner, H.: Solving POMDPs: RTDP-Bel vs. Point-based Algorithms. In: IJCAI. pp. 1641\u20131646 (2009)"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Bork, A., Junges, S., Katoen, J., Quatmann, T.: Verification of indefinite-horizon POMDPs. In: ATVA. Lecture Notes in Computer Science, vol. 12302, pp. 288\u2013304. Springer (2020)","DOI":"10.1007\/978-3-030-59152-6_16"},{"key":"2_CR9","doi-asserted-by":"publisher","unstructured":"Bork, A., Katoen, J.P., Quatmann, T.: Artifact for Paper: Under-Approximating Expected Total Rewards in POMDPs. Zenodo (2022). https:\/\/doi.org\/10.5281\/zenodo.5643643","DOI":"10.5281\/zenodo.5643643"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Bork, A., Katoen, J.P., Quatmann, T.: Under-Approximating Expected Total Rewards in POMDPs. arXiv e-print (2022), https:\/\/arxiv.org\/abs\/2201.08772","DOI":"10.1007\/978-3-030-99527-0_2"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Chmelik, M., Forejt, V., K\u0159et\u00ednsk\u1ef3, J., Kwiatkowska, M., Parker, D., Ujma, M.: Verification of Markov decision processes using learning algorithms. In: ATVA. Lecture Notes in Computer Science, vol.\u00a08837, pp. 98\u2013114. Springer (2014)","DOI":"10.1007\/978-3-319-11936-6_8"},{"key":"2_CR12","unstructured":"Braziunas, D., Boutilier, C.: Stochastic local search for POMDP controllers. In: AAAI. pp. 690\u2013696. AAAI Press \/ The MIT Press (2004)"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Carr, S., Jansen, N., Topcu, U.: Verifiable rnn-based policies for POMDPs under temporal logic constraints. In: IJCAI. pp. 4121\u20134127. ijcai.org (2020)","DOI":"10.24963\/ijcai.2020\/570"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Carr, S., Jansen, N., Wimmer, R., Serban, A.C., Becker, B., Topcu, U.: Counterexample-guided strategy improvement for POMDPs using recurrent neural networks. In: IJCAI. pp. 5532\u20135539. ijcai.org (2019)","DOI":"10.24963\/ijcai.2019\/768"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Chmel\u00edk, M., Davies, J.: A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs. In: AAAI. pp. 3225\u20133232 (2016)","DOI":"10.1609\/aaai.v30i1.10422"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Chmel\u00edk, M., Gupta, R., Kanodia, A.: Optimal cost almost-sure reachability in POMDPs. Artificial Intelligence 234, 26\u201348 (2016)","DOI":"10.1016\/j.artint.2016.01.007"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Doyen, L., Henzinger, T.A.: Qualitative analysis of partially-observable Markov decision processes. In: MFCS. Lecture Notes in Computer Science, vol.\u00a06281, pp. 258\u2013269. Springer (2010)","DOI":"10.1007\/978-3-642-15155-2_24"},{"key":"2_CR18","unstructured":"Cheng, H.T.: Algorithms for partially observable Markov decision processes. Ph.D. thesis, University of British Columbia (1988)"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Doshi, F., Pineau, J., Roy, N.: Reinforcement learning with limited reinforcement: Using Bayes risk for active learning in POMDPs. In: ICML. pp. 256\u2013263 (2008)","DOI":"10.1145\/1390156.1390189"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Eagle, J.N.: The optimal search for a moving target when the search path is constrained. Operations Research 32(5), 1107\u20131115 (1984)","DOI":"10.1287\/opre.32.5.1107"},{"key":"2_CR21","unstructured":"Gurobi Optimization, LLC: Gurobi Optimizer Reference Manual (2021), https:\/\/www.gurobi.com"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Hauskrecht, M.: Value-function approximations for partially observable Markov decision processes. J. Artif. Intell. Res. 13, 33\u201394 (2000)","DOI":"10.1613\/jair.678"},{"key":"2_CR23","doi-asserted-by":"publisher","unstructured":"Hensel, C., Junges, S., Katoen, J., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. on Software Tools for Technology Transfer (2021). https:\/\/doi.org\/10.1007\/s10009-021-00633-z","DOI":"10.1007\/s10009-021-00633-z"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Hor\u00e1k, K., Bo\u0161ansk\u00fd, B., Chatterjee, K.: Goal-HSVI: Heuristic Search Value Iteration for Goal POMDPs. In: IJCAI. pp. 4764\u20134770. ijcai.org (7 2018)","DOI":"10.24963\/ijcai.2018\/662"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Itoh, H., Nakamura, K.: Partially observable Markov decision processes with imprecise parameters. Artificial Intelligence 171(8-9), 453\u2013490 (2007)","DOI":"10.1016\/j.artint.2007.03.004"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"Jansen, N., Dehnert, C., Kaminski, B.L., Katoen, J., Westhofen, L.: Bounded model checking for probabilistic programs. In: ATVA. Lecture Notes in Computer Science, vol.\u00a09938, pp. 68\u201385 (2016)","DOI":"10.1007\/978-3-319-46520-3_5"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"Junges, S., Jansen, N., Seshia, S.A.: Enforcing almost-sure reachability in POMDPs. In: CAV (2). Lecture Notes in Computer Science, vol. 12760, pp. 602\u2013625. Springer (2021)","DOI":"10.1007\/978-3-030-81688-9_28"},{"key":"2_CR28","unstructured":"Junges, S., Jansen, N., Wimmer, R., Quatmann, T., Winterer, L., Katoen, J.P., Becker, B.: Finite-state Controllers of POMDPs via Parameter Synthesis. In: UAI. pp. 519\u2013529. AUAI Press (2018)"},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"Kaelbling, L.P., Littman, M.L., Cassandra, A.R.: Planning and acting in partially observable stochastic domains. Artificial Intelligence 101(1-2), 99\u2013134 (1998)","DOI":"10.1016\/S0004-3702(98)00023-X"},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Kurniawati, H., Hsu, D., Lee, W.S.: SARSOP: Efficient point-based POMDP planning by approximating optimally reachable belief spaces. In: Robotics: Science and Systems. vol.\u00a02008 (2008)","DOI":"10.15607\/RSS.2008.IV.009"},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: CAV. Lecture Notes in Computer Science, vol.\u00a06806, pp. 585\u2013591. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"2_CR32","doi-asserted-by":"crossref","unstructured":"Lovejoy, W.S.: Computationally feasible bounds for partially observed Markov decision processes. Operations Research 39(1), 162\u2013175 (1991)","DOI":"10.1287\/opre.39.1.162"},{"key":"2_CR33","unstructured":"Madani, O., Hanks, S., Condon, A.: On the undecidability of probabilistic planning and infinite-horizon partially observable Markov decision problems. In: AAAI\/IAAI. pp. 541\u2013548 (1999)"},{"key":"2_CR34","doi-asserted-by":"crossref","unstructured":"Madani, O., Hanks, S., Condon, A.: On the undecidability of probabilistic planning and related stochastic optimization problems. Artificial Intelligence 147(1-2), 5\u201334 (2003)","DOI":"10.1016\/S0004-3702(02)00378-8"},{"key":"2_CR35","unstructured":"Meuleau, N., Kim, K.E., Kaelbling, L.P., Cassandra, A.R.: Solving POMDPs by searching the space of finite policies. In: UAI. pp. 417\u2013426 (1999)"},{"key":"2_CR36","doi-asserted-by":"crossref","unstructured":"Monahan, G.E.: State of the art \u2014 a survey of partially observable Markov decision processes: theory, models, and algorithms. Management Science 28(1), 1\u201316 (1982)","DOI":"10.1287\/mnsc.28.1.1"},{"key":"2_CR37","doi-asserted-by":"crossref","unstructured":"Norman, G., Parker, D., Zou, X.: Verification and Control of Partially Observable Probabilistic Systems. Real-Time Systems 53(3), 354\u2013402 (2017)","DOI":"10.1007\/s11241-017-9269-4"},{"key":"2_CR38","unstructured":"Pineau, J., Gordon, G., Thrun, S.: Point-based value iteration: An anytime algorithm for POMDPs. In: IJCAI. vol.\u00a03, pp. 1025\u20131032 (2003)"},{"key":"2_CR39","doi-asserted-by":"crossref","unstructured":"Quatmann, T., Katoen, J.: Sound value iteration. In: CAV (1). Lecture Notes in Computer Science, vol. 10981, pp. 643\u2013661. Springer (2018)","DOI":"10.1007\/978-3-319-96145-3_37"},{"key":"2_CR40","unstructured":"Russell, S.J., Norvig, P.: Artificial Intelligence: A Modern Approach (4th Edition). Pearson (2020)"},{"key":"2_CR41","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. John Wiley & Sons (1986)"},{"key":"2_CR42","doi-asserted-by":"crossref","unstructured":"Shani, G., Pineau, J., Kaplow, R.: A survey of point-based POMDP solvers. Autonomous Agents and Multi-Agent Systems 27(1), 1\u201351 (2013)","DOI":"10.1007\/s10458-012-9200-2"},{"key":"2_CR43","unstructured":"Silver, D., Veness, J.: Monte-Carlo planning in large POMDPs. In: NIPS. pp. 2164\u20132172 (2010)"},{"key":"2_CR44","doi-asserted-by":"crossref","unstructured":"Smallwood, R.D., Sondik, E.J.: The optimal control of partially observable Markov processes over a finite horizon. Operations Research 21(5), 1071\u20131088 (1973)","DOI":"10.1287\/opre.21.5.1071"},{"key":"2_CR45","unstructured":"Smith, T., Simmons, R.: Heuristic search value iteration for POMDPs. In: UAI. pp. 520\u2013527 (2004)"},{"key":"2_CR46","unstructured":"Sondik, E.J.: The Optimal Control of Partially Observable Markov Processes. Ph.D. thesis, Stanford Univ Calif Stanford Electronics Labs (1971)"},{"key":"2_CR47","doi-asserted-by":"crossref","unstructured":"Sondik, E.J.: The optimal control of partially observable Markov processes over the infinite horizon: Discounted costs. Operations research 26(2), 282\u2013304 (1978)","DOI":"10.1287\/opre.26.2.282"},{"key":"2_CR48","doi-asserted-by":"crossref","unstructured":"Spaan, M.T., Vlassis, N.: Perseus: Randomized point-based value iteration for POMDPs. J. of Artificial Intelligence Research 24, 195\u2013220 (2005)","DOI":"10.1613\/jair.1659"},{"key":"2_CR49","doi-asserted-by":"crossref","unstructured":"Volk, M., Junges, S., Katoen, J.P.: Fast dynamic fault tree analysis by model checking techniques. IEEE Transactions on Industrial Informatics 14(1), 370\u2013379 (2017)","DOI":"10.1109\/TII.2017.2710316"},{"key":"2_CR50","unstructured":"Wang, Y., Chaudhuri, S., Kavraki, L.E.: Bounded Policy Synthesis for POMDPs with Safe-Reachability Objectives. In: AAMAS. pp. 238\u2013246 (2018)"},{"key":"2_CR51","doi-asserted-by":"crossref","unstructured":"Winterer, L., Junges, S., Wimmer, R., Jansen, N., Topcu, U., Katoen, J.P., Becker, B.: Motion planning under partial observability using game-based abstraction. In: CDC. pp. 2201\u20132208. IEEE (2017)","DOI":"10.1109\/CDC.2017.8263971"},{"key":"2_CR52","unstructured":"Zhang, N.L., Lee, S.S.: Planning with partially observable Markov decision processes: advances in exact solution method. In: UAI. pp. 523\u2013530 (1998)"},{"key":"2_CR53","doi-asserted-by":"crossref","unstructured":"Zhang, N.L., Zhang, W.: Speeding up the convergence of value iteration in partially observable Markov decision processes. Journal of Artificial Intelligence Research 14, 29\u201351 (2001)","DOI":"10.1613\/jair.761"}],"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-030-99527-0_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T08:45:31Z","timestamp":1710233131000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99527-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030995263","9783030995270"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99527-0_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"30 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"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":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers of the affiliated competition SV-Comp and 1 paper consisting of the competition report are also included in the proceedings","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}