{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,5]],"date-time":"2026-05-05T12:03:29Z","timestamp":1777982609029,"version":"3.51.4"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T00:00:00Z","timestamp":1769904000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,2,20]],"date-time":"2026-02-20T00:00:00Z","timestamp":1771545600000},"content-version":"vor","delay-in-days":19,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Brno University of Technology"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2026,2]]},"DOI":"10.1007\/s10703-025-00488-z","type":"journal-article","created":{"date-parts":[[2026,2,20]],"date-time":"2026-02-20T16:38:17Z","timestamp":1771605497000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Search and explore: symbiotic policy synthesis in POMDPs"],"prefix":"10.1007","volume":"68","author":[{"given":"Roman","family":"Andriushchenko","sequence":"first","affiliation":[]},{"given":"Alexander","family":"Bork","sequence":"additional","affiliation":[]},{"given":"Milan","family":"\u010ce\u0161ka","sequence":"additional","affiliation":[]},{"given":"Sebastian","family":"Junges","sequence":"additional","affiliation":[]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[]},{"given":"Filip","family":"Mac\u00e1k","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2026,2,20]]},"reference":[{"key":"488_CR1","doi-asserted-by":"crossref","unstructured":"Puterman ML (1994) Markov decision processes: discrete stochastic dynamic programming","DOI":"10.1002\/9780470316887"},{"key":"488_CR2","doi-asserted-by":"crossref","unstructured":"Kwiatkowska MZ, Norman G, Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems 6806:585\u2013591. In: CAV. Lncs","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"488_CR3","doi-asserted-by":"crossref","unstructured":"Dehnert C, Junges S, Katoen J-P, Volk M (2017) A storm is coming: a modern probabilistic model checker 10427:592\u2013600. In: CAV. Lncs","DOI":"10.1007\/978-3-319-63390-9_31"},{"issue":"1","key":"488_CR4","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/S0004-3702(02)00378-8","volume":"147","author":"O Madani","year":"2003","unstructured":"Madani O, Hanks S, Condon A (2003) On the undecidability of probabilistic planning and related stochastic optimization problems. Artif Intel 147(1):5\u201334","journal-title":"Artif Intel"},{"issue":"5","key":"488_CR5","doi-asserted-by":"publisher","first-page":"1071","DOI":"10.1287\/opre.21.5.1071","volume":"21","author":"RD Smallwood","year":"1973","unstructured":"Smallwood RD, Sondik EJ (1973) The optimal control of partially observable Markov processes over a finite horizon. Oper Res 21(5):1071\u20131088","journal-title":"Oper Res"},{"issue":"1\u20132","key":"488_CR6","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/S0004-3702(98)00023-X","volume":"101","author":"LP Kaelbling","year":"1998","unstructured":"Kaelbling LP, Littman ML, Cassandra AR (1998) Planning and acting in partially observable stochastic domains. Artif Intell 101(1\u20132):99\u2013134","journal-title":"Artif Intell"},{"issue":"3","key":"488_CR7","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/s11241-017-9269-4","volume":"53","author":"G Norman","year":"2017","unstructured":"Norman G, Parker D, Zou X (2017) Verification and control of partially observable probabilistic systems. Real-Time Syst 53(3):354\u2013402","journal-title":"Real-Time Syst"},{"key":"488_CR8","first-page":"4764","volume-title":"Goal-HSVI: heuristic search value iteration for goal POMDPs","author":"K Horak","year":"2018","unstructured":"Horak K, Bosansky B, Chatterjee K (2018) Goal-HSVI: heuristic search value iteration for goal POMDPs. IJCAI, In, pp 4764\u20134770"},{"key":"488_CR9","doi-asserted-by":"crossref","unstructured":"Kurniawati H, Hsu D, Lee WS (2008) SARSOP: efficient point-based POMDP planning by approximating optimally reachable belief spaces. Robot: Sci Syst","DOI":"10.15607\/RSS.2008.IV.009"},{"key":"488_CR10","doi-asserted-by":"crossref","unstructured":"Wang Y, Chaudhuri S, Kavraki LE (2018) Bounded policy synthesis for POMDPs with safe-reachability objectives. AAMAS 238\u2013246","DOI":"10.65109\/ICED8892"},{"key":"488_CR11","doi-asserted-by":"publisher","first-page":"663","DOI":"10.1613\/jair.2567","volume":"32","author":"S Ross","year":"2008","unstructured":"Ross S, Pineau J, Paquet S, Chaib-Draa B (2008) Online planning algorithms for POMDPs. J Artif Intell Res 32:663\u2013704","journal-title":"J Artif Intell Res"},{"key":"488_CR12","unstructured":"Silver D, Veness J (2010) Monte-carlo planning in large POMDPs. NeurIPS 2164\u20132172"},{"key":"488_CR13","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1613\/jair.5328","volume":"58","author":"N Ye","year":"2017","unstructured":"Ye N, Somani A, Hsu D, Lee WS (2017) Despot: online POMDP planning with regularization. J Artif Intell Res 58:231\u2013266","journal-title":"J Artif Intell Res"},{"key":"488_CR14","doi-asserted-by":"crossref","unstructured":"Sunberg ZN, Kochenderfer MJ (2018) Online algorithms for POMDPs with continuous state, action, and observation spaces. ICAPS 259\u2013263","DOI":"10.1609\/icaps.v28i1.13882"},{"key":"488_CR15","unstructured":"Garg NP, Hsu D, Lee WS (2019) DESPOT-Alpha: online POMDP planning with large state and observation spaces. Robot: Sci Syst XV"},{"key":"488_CR16","doi-asserted-by":"crossref","unstructured":"Cai P, Luo Y, Hsu D, Lee WS (2021) HyP-DESPOT: a hybrid parallel algorithm for online planning under uncertainty. Int J Robot Res 40(2\u20133)","DOI":"10.1177\/0278364920937074"},{"key":"488_CR17","unstructured":"Wu C, Yang G, Zhang Z, Yu Y, Li D, Liu W, Hao J (2021) Adaptive online packing-guided search for POMDPs. NeurIPS 28419\u201328430"},{"key":"488_CR18","first-page":"2018","volume-title":"CAR-DESPOT: causally-informed online POMDP planning for robots in confounded environments","author":"R Cannizzaro","year":"2023","unstructured":"Cannizzaro R, Kunze L (2023) CAR-DESPOT: causally-informed online POMDP planning for robots in confounded environments. IROS, In, pp 2018\u20132025"},{"key":"488_CR19","first-page":"22","volume":"13244","author":"A Bork","year":"2022","unstructured":"Bork A, Katoen J-P, Quatmann T (2022) Under-approximating expected total rewards in POMDPs. TACAS (2) LNCS 13244:22\u201340","journal-title":"TACAS (2) LNCS"},{"key":"488_CR20","first-page":"211","volume-title":"Solving POMDPs by searching in policy space","author":"EA Hansen","year":"1998","unstructured":"Hansen EA (1998) Solving POMDPs by searching in policy space. UAI, In, pp 211\u2013219"},{"key":"488_CR21","first-page":"417","volume-title":"Solving POMDPs by searching the space of finite policies","author":"N Meuleau","year":"1999","unstructured":"Meuleau N, Kim K, Kaelbling LP, Cassandra AR (1999) Solving POMDPs by searching the space of finite policies. UAI, In, pp 417\u2013426"},{"key":"488_CR22","first-page":"2282","volume-title":"Isomorph-free branch and bound search for finite state controllers","author":"M Grze\u015b","year":"2013","unstructured":"Grze\u015b M, Poupart P, Hoey J (2013) Isomorph-free branch and bound search for finite state controllers. IJCAI, In, pp 2282\u20132290"},{"key":"488_CR23","doi-asserted-by":"crossref","unstructured":"Amato C, Bonet B, Zilberstein S (2010) Finite-state controllers based on mealy machines for centralized and decentralized POMDPs. AAAI 1052\u20131058","DOI":"10.1609\/aaai.v24i1.7748"},{"key":"488_CR24","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1609\/icaps.v25i1.13730","volume":"25","author":"A Kumar","year":"2015","unstructured":"Kumar A, Zilberstein S (2015) History-based controller design and optimization for partially observable MDPs. ICAPS 25:156\u2013164","journal-title":"ICAPS"},{"key":"488_CR25","first-page":"127","volume":"13182","author":"L Heck","year":"2022","unstructured":"Heck L, Spel J, Junges S, Moerman J, Katoen J (2022) Gradient-descent for randomized controllers under partial observability. VMCAI LNCS 13182:127\u2013150","journal-title":"VMCAI LNCS"},{"issue":"3","key":"488_CR26","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/s10458-009-9103-z","volume":"21","author":"C Amato","year":"2010","unstructured":"Amato C, Bernstein DS, Zilberstein S (2010) Optimizing fixed-size stochastic controllers for POMDPs and decentralized POMDPs. Auton Agents Multi-Agent Syst 21(3):293\u2013320","journal-title":"Auton Agents And Multi-Agent Syst"},{"key":"488_CR27","first-page":"519","volume-title":"Finite-state controllers of POMDPs via parameter synthesis","author":"S Junges","year":"2018","unstructured":"Junges S, Jansen N, Wimmer R, Quatmann T, Winterer L, Katoen J-P, Becker B (2018) Finite-state controllers of POMDPs via parameter synthesis. UAI, In, pp 519\u2013529"},{"key":"488_CR28","doi-asserted-by":"crossref","unstructured":"Cubuktepe M, Jansen N, Junges S, Marandi A, Suilen M, Topcu U (2021) Robust finite-state controllers for uncertain POMDPs. AAAI 11792\u201311800","DOI":"10.1609\/aaai.v35i13.17401"},{"key":"488_CR29","doi-asserted-by":"publisher","first-page":"819","DOI":"10.1613\/jair.1.12963","volume":"72","author":"S Carr","year":"2021","unstructured":"Carr S, Jansen N, Topcu U (2021) Task-aware verifiable RNN-based policies for partially observable Markov decision processes. J Artif Intell Res 72:819\u2013847","journal-title":"J Artif Intell Res"},{"key":"488_CR30","first-page":"5052","volume":"80","author":"A Verma","year":"2018","unstructured":"Verma A, Murali V, Singh R, Kohli P, Chaudhuri S (2018) Programmatically interpretable reinforcement learning. ICML 80:5052\u20135061","journal-title":"ICML"},{"key":"488_CR31","first-page":"85","volume":"180","author":"R Andriushchenko","year":"2022","unstructured":"Andriushchenko R, \u010ce\u0161ka M, Junges S, Katoen J-P (2022) Inductive synthesis of finite-state controllers for POMDPs. UAI 180:85\u201395","journal-title":"UAI"},{"key":"488_CR32","first-page":"856","volume":"12759","author":"R Andriushchenko","year":"2021","unstructured":"Andriushchenko R, \u010ce\u0161ka M, Junges S, Katoen J-P, Stupinsk\u00fd \u0160 (2021) PAYNT: a tool for inductive synthesis of probabilistic programs. CAV LNCS 12759:856\u2013869","journal-title":"CAV LNCS"},{"key":"488_CR33","first-page":"113","volume":"13966","author":"R Andriushchenko","year":"2023","unstructured":"Andriushchenko R, Bork A, \u010ce\u0161ka M, Junges S, Katoen J-P, Mac\u00e1k F (2023) Search and explore: symbiotic policy synthesis in POMDPs. CAV LNCS 13966:113\u2013135","journal-title":"CAV LNCS"},{"key":"488_CR34","doi-asserted-by":"crossref","unstructured":"Andriushchenko R, Bork A, \u010ce\u0161ka M, Junges S, Katoen J-P, Mac\u00e1k F (2023) Search and explore: symbiotic policy synthesis in POMDPs. arXiv preprint arXiv:2305.14149","DOI":"10.21203\/rs.3.rs-4363964\/v1"},{"key":"488_CR35","first-page":"191","volume":"12651","author":"R Andriushchenko","year":"2021","unstructured":"Andriushchenko R, \u010ce\u0161ka M, Junges S, Katoen J-P (2021) Inductive synthesis for probabilistic programs reaches new horizons. TACAS LNCS 12651:191\u2013209","journal-title":"TACAS LNCS"},{"key":"488_CR36","first-page":"172","volume":"11428","author":"M \u010ce\u0161ka","year":"2019","unstructured":"\u010ce\u0161ka M, Jansen N, Junges S, Katoen J-P (2019) Shepherding hordes of Markov chains. TACAS LNCS 11428:172\u2013190","journal-title":"TACAS LNCS"},{"key":"488_CR37","doi-asserted-by":"crossref","unstructured":"Bork A, Junges S, Katoen J-P, Quatmann T (2020) Verification of indefinitehorizon POMDPs 12302:288\u2013304. In: ATVA. Lncs","DOI":"10.1007\/978-3-030-59152-6_16"},{"key":"488_CR38","unstructured":"Hauskrecht M (1997) Incremental methods for computing bounds in partially observable Markov decision processes. AAAI\/IAAI 734\u2013739"},{"issue":"1","key":"488_CR39","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10458-012-9200-2","volume":"27","author":"G Shani","year":"2013","unstructured":"Shani G, Pineau J, Kaplow R (2013) A survey of point-based POMDP solvers. Auton Agents Multi Agent Syst 27(1):1\u201351","journal-title":"Auton Agents Multi Agent Syst"},{"key":"488_CR40","doi-asserted-by":"crossref","unstructured":"Krale M, Koops W, Junges S, Sim\u00e3o TD, Jansen N (2025) Tighter value-function approximations for pomdps. arXiv preprint arXiv:2502.06523","DOI":"10.65109\/KZNJ3826"},{"key":"488_CR41","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1016\/j.artint.2016.01.007","volume":"234","author":"K Chatterjee","year":"2016","unstructured":"Chatterjee K, Chmel\u00edk M, Gupta R, Kanodia A (2016) Optimal cost almost-sure reachability in POMDPs. Artif Intell 234:26\u201348","journal-title":"Artif Intell"},{"key":"488_CR42","first-page":"157","volume-title":"Game-based abstraction for Markov decision processes","author":"MZ Kwiatkowska","year":"2006","unstructured":"Kwiatkowska MZ, Norman G, Parker D (2006) Game-based abstraction for Markov decision processes. QEST, In, pp 157\u2013166"},{"issue":"1","key":"488_CR43","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/s00165-017-0432-4","volume":"30","author":"P Chrszon","year":"2018","unstructured":"Chrszon P, Dubslaff C, Kl\u00fcppelholz S, Baier C (2018) Profeat: feature-oriented engineering for family-based probabilistic model checking. Formal Aspects Comput 30(1):45\u201375","journal-title":"Formal Aspects Comput"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-025-00488-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-025-00488-z","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-025-00488-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T09:11:58Z","timestamp":1772788318000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-025-00488-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,2]]},"references-count":43,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,2]]}},"alternative-id":["488"],"URL":"https:\/\/doi.org\/10.1007\/s10703-025-00488-z","relation":{"has-preprint":[{"id-type":"doi","id":"10.21203\/rs.3.rs-4363964\/v1","asserted-by":"object"}]},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,2]]},"assertion":[{"value":"3 May 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 November 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 February 2026","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"Not applicable.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethical approval"}},{"value":"The authors declare no competing interests.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"4"}}