{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T11:00:45Z","timestamp":1753182045238,"version":"3.40.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031656323"},{"type":"electronic","value":"9783031656330"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Partially observable Markov Decision Processes (POMDPs) are a standard model for agents making decisions in uncertain environments. Most work on POMDPs focuses on synthesizing strategies based on the available capabilities. However, system designers can often control an agent\u2019s observation capabilities, e.g. by placing or selecting sensors. This raises the question of how one should select an agent\u2019s sensors cost-effectively such that it achieves the desired goals. In this paper, we study the novel<jats:italic>optimal observability problem<\/jats:italic>(<jats:sc>oop<\/jats:sc>): Given a POMDP<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathscr {M}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>M<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>, how should one change<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathscr {M}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>M<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>\u2019s observation capabilities within a fixed budget such that its (minimal) expected reward remains below a given threshold? We show that the problem is undecidable in general and decidable when considering positional strategies only. We present two algorithms for a decidable fragment of the<jats:sc>oop<\/jats:sc>: one based on optimal strategies of<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathscr {M}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>M<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>\u2019s underlying Markov decision process and one based on parameter synthesis with SMT. We report promising results for variants of typical examples from the POMDP literature.<\/jats:p>","DOI":"10.1007\/978-3-031-65633-0_17","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:03:08Z","timestamp":1721890988000},"page":"373-394","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["What Should Be Observed for\u00a0Optimal Reward in\u00a0POMDPs?"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0206-5217","authenticated-orcid":false,"given":"Alyzia-Maria","family":"Konsta","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7405-0818","authenticated-orcid":false,"given":"Alberto","family":"Lluch Lafuente","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9151-0441","authenticated-orcid":false,"given":"Christoph","family":"Matheja","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"17_CR1","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1016\/0022-247X(65)90154-X","volume":"10","author":"KJ \u00c5str\u00f6m","year":"1965","unstructured":"\u00c5str\u00f6m, K.J.: Optimal control of Markov processes with incomplete state information I. J. Math. Anal. Appl. 10, 174\u2013205 (1965)","journal-title":"J. Math. Anal. Appl."},{"key":"17_CR2","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT press (2008)"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Canny, J.F.: Some algebraic and geometric computations in PSPACE. In: STOC, pp. 460\u2013467. ACM (1988)","DOI":"10.1145\/62212.62257"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-22110-1_20","volume-title":"Computer Aided Verification","author":"P \u010cern\u00fd","year":"2011","unstructured":"\u010cern\u00fd, P., Chatterjee, K., Henzinger, T.A., Radhakrishna, A., Singh, R.: Quantitative synthesis for concurrent programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 243\u2013259. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_20"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Chades, I., Carwardine, J., Martin, T.G., Nicol, S., Sabbadin, R., Buffet, O.: MOMDPs: a solution for modelling adaptive management problems. In: AAAI, pp. 267\u2013273. AAAI Press (2012)","DOI":"10.1609\/aaai.v26i1.8171"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Chmelik, M., Topcu, U.: Sensor synthesis for POMDPs with reachability objectives. In: Proceedings of the International Conference on Automated Planning and Scheduling, vol.\u00a028, pp. 47\u201355 (2018)","DOI":"10.1609\/icaps.v28i1.13875"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-15155-2_24","volume-title":"Mathematical Foundations of Computer Science 2010","author":"K Chatterjee","year":"2010","unstructured":"Chatterjee, K., Doyen, L., Henzinger, T.A.: Qualitative analysis of partially-observable Markov decision processes. In: Hlin\u011bn\u00fd, P., Ku\u010dera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 258\u2013269. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15155-2_24"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-030-01090-4_10","volume-title":"Automated Technology for Verification and Analysis","author":"M Cubuktepe","year":"2018","unstructured":"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\u2013176. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_10"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-319-21690-4_13","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2015","unstructured":"Dehnert, C., et al.: PROPhESY: a PRObabilistic ParamEter SYnthesis tool. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 214\u2013231. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_13"},{"issue":"1","key":"17_CR10","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10009-010-0146-x","volume":"13","author":"EM Hahn","year":"2011","unstructured":"Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. Int. J. Softw. Tools Technol. Transf. 13(1), 3\u201319 (2011)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"17_CR11","doi-asserted-by":"publisher","unstructured":"Hensel, C., Junges, S., Katoen, J.-P., Quatmann, T., Volk, M.: The probabilistic model checker storm. Int. J. Softw. Tools Technol. Transfer 24(4), 589\u2013610 (2022). https:\/\/doi.org\/10.1007\/s10009-021-00633-z, https:\/\/doi.org\/10.1007\/s10009-021-00633-z","DOI":"10.1007\/s10009-021-00633-z"},{"key":"17_CR12","doi-asserted-by":"publisher","unstructured":"Jansen, N., Junges, S., Katoen, J.-P.: Parameter synthesis in Markov models: a gentle survey. In: Raskin, JF., Chatterjee, K., Doyen, L., Majumdar, R. (eds.) Principles of Systems Design: Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday, vol. 13660, pp. 407\u2013437 (2022). https:\/\/doi.org\/10.1007\/978-3-031-22337-2_20","DOI":"10.1007\/978-3-031-22337-2_20"},{"key":"17_CR13","unstructured":"Jdeed, M., et al.: The CPSwarm technology for designing swarms of cyber-physical systems. In: STAF (Co-Located Events). CEUR Workshop Proceedings, vol.\u00a02405, pp. 85\u201390. CEUR-WS.org (2019)"},{"key":"17_CR14","unstructured":"Junges, S.: Parameter synthesis in Markov models. Ph.D. thesis, Dissertation, RWTH Aachen University, 2020 (2020)"},{"key":"17_CR15","doi-asserted-by":"publisher","unstructured":"Kaelbling, L.P., Littman, M.L., Cassandra, A.R.: Planning and acting in partially observable stochastic domains. Artif. Intell. 101(1), 99\u2013134 (1998). https:\/\/doi.org\/10.1016\/S0004-3702(98)00023-X, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S000437029800023X","DOI":"10.1016\/S0004-3702(98)00023-X"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Kochenderfer, M.J.: Decision Making Under Uncertainty: Theory and Application. MIT press (2015)","DOI":"10.7551\/mitpress\/10187.001.0001"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"Konsta, A.M., Lafuente, A.L., Matheja, C.: What should be observed for optimal reward in pomdps? arXiv preprint arXiv:2405.10768 (2024)","DOI":"10.1007\/978-3-031-65633-0_17"},{"key":"17_CR18","doi-asserted-by":"publisher","unstructured":"Krause, A., Singh, A.P., Guestrin, C.: Near-optimal sensor placements in gaussian processes: theory, efficient algorithms and empirical studies. J. Mach. Learn. Res. 9, 235\u2013284 (2008). https:\/\/doi.org\/10.5555\/1390681.1390689, https:\/\/dl.acm.org\/doi\/10.5555\/1390681.1390689","DOI":"10.5555\/1390681.1390689"},{"key":"17_CR19","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":"17_CR20","doi-asserted-by":"crossref","unstructured":"Littman, M.L.: Memoryless policies: theoretical limitations and practical results. In: From Animals to Animats 3: Proceedings of the third International Conference on Simulation of Adaptive Behavior, vol.\u00a03, p.\u00a0238. MIT Press Cambridge, MA, USA (1994)","DOI":"10.7551\/mitpress\/3117.003.0041"},{"key":"17_CR21","doi-asserted-by":"publisher","unstructured":"Littman, M.L., Cassandra, A.R., Kaelbling, L.P.: Learning policies for partially observable environments: scaling up. In: Prieditis, A., Russell, S. (eds.) Machine Learning Proceedings 1995, pp. 362\u2013370. Morgan Kaufmann, San Francisco (CA) (1995). https:\/\/doi.org\/10.1016\/B978-1-55860-377-6.50052-9, https:\/\/www.sciencedirect.com\/science\/article\/pii\/B9781558603776500529","DOI":"10.1016\/B978-1-55860-377-6.50052-9"},{"key":"17_CR22","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":"17_CR23","doi-asserted-by":"publisher","unstructured":"McCallum, R.A.: Overcoming incomplete perception with utile distinction memory. In: Machine Learning Proceedings 1993, pp. 190\u2013196. Morgan Kaufmann, San Francisco (CA) (1993). https:\/\/doi.org\/10.1016\/B978-1-55860-307-3.50031-9, https:\/\/www.sciencedirect.com\/science\/article\/pii\/B9781558603073500319","DOI":"10.1016\/B978-1-55860-307-3.50031-9"},{"issue":"10","key":"17_CR24","doi-asserted-by":"publisher","first-page":"2490","DOI":"10.1109\/TIFS.2018.2819967","volume":"13","author":"E Miehling","year":"2018","unstructured":"Miehling, E., Rasouli, M., Teneketzis, D.: A POMDP approach to the dynamic defense of large-scale cyber networks. IEEE Trans. Inf. Forensics Secur. 13(10), 2490\u20132505 (2018)","journal-title":"IEEE Trans. Inf. Forensics Secur."},{"key":"17_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"17_CR26","doi-asserted-by":"publisher","unstructured":"Pahalawatta, P., Pappas, T., Katsaggelos, A.: Optimal sensor selection for video-based target tracking in a wireless sensor network. In: 2004 International Conference on Image Processing, 2004. ICIP 2004, vol.\u00a05, pp. 3073\u20133076 (2004). https:\/\/doi.org\/10.1109\/ICIP.2004.1421762","DOI":"10.1109\/ICIP.2004.1421762"},{"key":"17_CR27","doi-asserted-by":"publisher","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics, Wiley (1994). https:\/\/doi.org\/10.1002\/9780470316887, https:\/\/doi.org\/10.1002\/9780470316887","DOI":"10.1002\/9780470316887"},{"key":"17_CR28","unstructured":"Russell, S., Norvig, P.: Artificial Intelligence: A Modern Approach, 4th edn. Pearson (2020)"},{"key":"17_CR29","doi-asserted-by":"publisher","unstructured":"Sheyner, O., Haines, J., Jha, S., Lippmann, R., Wing, J.: Automated generation and analysis of attack graphs. In: Proceedings 2002 IEEE Symposium on Security and Privacy, pp. 273\u2013284 (2002). https:\/\/doi.org\/10.1109\/SECPRI.2002.1004377","DOI":"10.1109\/SECPRI.2002.1004377"},{"key":"17_CR30","doi-asserted-by":"crossref","unstructured":"Spaan, M., Lima, P.: A decision-theoretic approach to dynamic sensor selection in camera networks. In: Proceedings of the International Conference on Automated Planning and Scheduling, vol.\u00a019, pp. 297\u2013304 (2009)","DOI":"10.1609\/icaps.v19i1.13381"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65633-0_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,24]],"date-time":"2024-11-24T20:15:10Z","timestamp":1732479310000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65633-0_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656323","9783031656330"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65633-0_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","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":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}