{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T21:06:30Z","timestamp":1769720790962,"version":"3.49.0"},"publisher-location":"Cham","reference-count":58,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031787492","type":"print"},{"value":"9783031787508","type":"electronic"}],"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:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-78750-8_3","type":"book-chapter","created":{"date-parts":[[2025,2,11]],"date-time":"2025-02-11T12:15:43Z","timestamp":1739276143000},"page":"51-75","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Policies Grow on\u00a0Trees: Model Checking Families of\u00a0MDPs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1286-934X","authenticated-orcid":false,"given":"Roman","family":"Andriushchenko","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0300-9727","authenticated-orcid":false,"given":"Milan","family":"\u010ce\u0161ka","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0978-8466","authenticated-orcid":false,"given":"Sebastian","family":"Junges","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0004-4277-2751","authenticated-orcid":false,"given":"Filip","family":"Mac\u00e1k","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,2,12]]},"reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-030-72016-2_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Andriushchenko","year":"2021","unstructured":"Andriushchenko, R., \u010ce\u0161ka, M., Junges, S., Katoen, J.-P.: Inductive synthesis for probabilistic programs reaches new horizons. In: TACAS 2021. LNCS, vol. 12651, pp. 191\u2013209. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_11"},{"key":"3_CR2","unstructured":"Andriushchenko, R., \u010ce\u0161ka, M., Junges, S., Katoen, J.P.: Inductive synthesis of finite-state controllers for POMDPs. In: UAI, vol.\u00a0180, pp. 85\u201395. PMRL (2022)"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"856","DOI":"10.1007\/978-3-030-81685-8_40","volume-title":"Computer Aided Verification","author":"R Andriushchenko","year":"2021","unstructured":"Andriushchenko, R., \u010ce\u0161ka, M., Junges, S., Katoen, J.-P., Stupinsk\u00fd, \u0160: PAYNT: a tool for inductive synthesis of probabilistic programs. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 856\u2013869. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_40"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Andriushchenko, R., \u010ce\u0161ka, M., Junges, S., Mac\u00e1k, F.: Policies grow on trees: model checking families of MDPs (2024). https:\/\/arxiv.org\/abs\/2407.12552","DOI":"10.1007\/978-3-031-78750-8_3"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-319-99154-2_4","volume-title":"Quantitative Evaluation of Systems","author":"S Arming","year":"2018","unstructured":"Arming, S., Bartocci, E., Chatterjee, K., Katoen, J.-P., Sokolova, A.: Parameter-independent strategies for pMDPs via POMDPs. In: McIver, A., Horvath, A. (eds.) QEST 2018. LNCS, vol. 11024, pp. 53\u201370. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99154-2_4"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-030-72013-1_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Ashok","year":"2021","unstructured":"Ashok, P., Jackermeier, M., K\u0159et\u00ednsk\u00fd, J., Weinhuber, C., Weininger, M., Yadav, M.: dtControl 2.0: explainable strategy representation via decision tree learning steered by experts. In: TACAS 2021. LNCS, vol. 12652, pp. 326\u2013345. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_17"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-030-30281-8_9","volume-title":"Quantitative Evaluation of Systems","author":"P Ashok","year":"2019","unstructured":"Ashok, P., K\u0159et\u00ednsk\u00fd, J., Larsen, K.G., Le Co\u00ebnt, A., Taankvist, J.H., Weininger, M.: SOS: safe, optimal and small strategies for hybrid Markov decision processes. In: Parker, D., Wolf, V. (eds.) QEST 2019. LNCS, vol. 11785, pp. 147\u2013164. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30281-8_9"},{"key":"3_CR8","unstructured":"Azar, M.G., Lazaric, A., Brunskill, E.: Sequential transfer in multi-armed bandit with finite set of models. In: NIPS, pp. 2220\u20132228 (2013)"},{"issue":"5","key":"3_CR9","doi-asserted-by":"publisher","first-page":"803","DOI":"10.1007\/s10009-022-00673-z","volume":"24","author":"TS Badings","year":"2022","unstructured":"Badings, T.S., Cubuktepe, M., Jansen, N., Junges, S., Katoen, J., Topcu, U.: Scenario-based verification of uncertain parametric MDPs. Int. J. Softw. Tools Technol. Transf. 24(5), 803\u2013819 (2022)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"3_CR10","doi-asserted-by":"publisher","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.: Model checking probabilistic systems. In: Handbook of Model Checking, pp. 963\u2013999. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_28"},{"issue":"6","key":"3_CR11","doi-asserted-by":"publisher","first-page":"813","DOI":"10.1109\/43.766730","volume":"18","author":"L Benini","year":"1999","unstructured":"Benini, L., Bogliolo, A., Paleologo, G.A., De Micheli, G.: Policy optimization for dynamic power management. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 18(6), 813\u2013833 (1999)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Bork, A., Chakraborty, D., Grover, K., K\u0159et\u00ednsk\u00fd, J., Mohr, S.: Learning explainable and better performing representations of POMDP strategies. In: TACAS (2024, to appear)","DOI":"10.1007\/978-3-031-57249-4_15"},{"key":"3_CR13","unstructured":"Bresina, J.L., J\u00f3nsson, A.K., Morris, P.H., Rajan, K.: Activity planning for the mars exploration rovers. In: ICAPS, pp. 40\u201349. AAAI (2005)"},{"issue":"1","key":"3_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s00186-018-0653-1","volume":"89","author":"P Buchholz","year":"2019","unstructured":"Buchholz, P., Scheftelowitsch, D.: Computation of weighted sums of rewards for concurrent MDPs. Math. Methods Oper. Res. 89(1), 1\u201342 (2019)","journal-title":"Math. Methods Oper. Res."},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-030-83723-5_15","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends","author":"CE Budde","year":"2021","unstructured":"Budde, C.E., et al.: On correctness, precision, and performance in quantitative verification. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12479, pp. 216\u2013241. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-83723-5_15"},{"key":"3_CR16","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.: Task-aware verifiable RNN-based policies for partially observable Markov decision processes. J. Artif. Intell. Res. 72, 819\u2013847 (2021)","journal-title":"J. Artif. Intell. Res."},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-030-17465-1_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M \u010ce\u0161ka","year":"2019","unstructured":"\u010ce\u0161ka, M., Jansen, N., Junges, S., Katoen, J.-P.: Shepherding hordes of Markov chains. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 172\u2013190. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_10"},{"key":"3_CR18","unstructured":"Chades, I., Carwardine, J., Martin, T.G., Nicol, S., Sabbadin, R., Buffet, O.: MOMDPs: a solution for modelling adaptive management problems. In: AAAI. AAAI Press (2012)"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Chmel\u00edk, M., Karkhanis, D., Novotn\u00fd, P., Royer, A.: Multiple-environment Markov decision processes: Efficient analysis and applications. In: ICAPS, pp. 48\u201356. AAAI Press (2020)","DOI":"10.1609\/icaps.v30i1.6644"},{"issue":"1","key":"3_CR20","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.: ProFeat: feature-oriented engineering for family-based probabilistic model checking. Formal Asp. Comput. 30(1), 45\u201375 (2018)","journal-title":"Formal Asp. Comput."},{"key":"3_CR21","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/s10009-012-0234-1","volume":"14","author":"A Classen","year":"2012","unstructured":"Classen, A., Cordy, M., Heymans, P., Legay, A., Schobbens, P.Y.: Model checking software product lines with SNIP. Int. J. Softw. Tools Technol. Transf. 14, 589\u2013612 (2012)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"3_CR22","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1016\/j.scico.2013.09.019","volume":"80","author":"A Classen","year":"2014","unstructured":"Classen, A., Cordy, M., Heymans, P., Legay, A., Schobbens, P.Y.: Formal semantics, modular specification, and symbolic verification of product-line behaviour. Sci. Comput. Program. 80, 416\u2013439 (2014)","journal-title":"Sci. Comput. Program."},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Dr\u00e4ger, K., Forejt, V., Kwiatkowska, M.Z., Parker, D., Ujma, M.: Permissive controller synthesis for probabilistic systems. Log. Methods Comput. Sci. 11(2) (2015)","DOI":"10.2168\/LMCS-11(2:16)2015"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Dubslaff, C., Morozov, A., Baier, C., Janschek, K.: Iterative variable reordering: Taming huge system families. In: MARS. EPTCS, vol.\u00a0316, pp. 121\u2013133 (2020)","DOI":"10.4204\/EPTCS.316.5"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Feng, L., Wiltsche, C., Humphrey, L., Topcu, U.: Controller synthesis for autonomous systems interacting with human operators. In: ICCPS, pp. 70\u201379. Association for Computing Machinery (2015)","DOI":"10.1145\/2735960.2735973"},{"issue":"3","key":"3_CR26","doi-asserted-by":"publisher","first-page":"508","DOI":"10.1016\/j.infsof.2012.07.017","volume":"55","author":"C Ghezzi","year":"2013","unstructured":"Ghezzi, C., Sharifloo, A.M.: Model-based verification of quantitative non-functional properties for software product lines. Inf. Softw. Technol. 55(3), 508\u2013524 (2013)","journal-title":"Inf. Softw. Technol."},{"issue":"1\u20132","key":"3_CR27","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/S0004-3702(00)00047-3","volume":"122","author":"R Givan","year":"2000","unstructured":"Givan, R., Leach, S.M., Dean, T.L.: Bounded-parameter Markov decision processes. Artif. Intell. 122(1\u20132), 71\u2013109 (2000)","journal-title":"Artif. Intell."},{"key":"3_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-642-12002-2_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"EM Hahn","year":"2010","unstructured":"Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: PASS: abstraction refinement for infinite probabilistic models. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 353\u2013357. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_30"},{"issue":"1","key":"3_CR29","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."},{"issue":"4","key":"3_CR30","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/s10009-021-00633-z","volume":"24","author":"C Hensel","year":"2022","unstructured":"Hensel, C., Junges, S., Katoen, J., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Transf. 24(4), 589\u2013610 (2022)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"2","key":"3_CR31","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1287\/moor.1040.0129","volume":"30","author":"GN Iyengar","year":"2005","unstructured":"Iyengar, G.N.: Robust dynamic programming. Math. Oper. Res. 30(2), 257\u2013280 (2005)","journal-title":"Math. Oper. Res."},{"key":"3_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-030-20652-9_16","volume-title":"NASA Formal Methods","author":"N Jansen","year":"2019","unstructured":"Jansen, N., Humphrey, L., Tumova, J., Topcu, U.: Structured synthesis for probabilistic systems. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2019. LNCS, vol. 11460, pp. 237\u2013254. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-20652-9_16"},{"key":"3_CR33","unstructured":"Junges, S.: Parameter synthesis in Markov models. Ph.D. thesis, RWTH Aachen University, Germany (2020)"},{"key":"3_CR34","unstructured":"Junges, S., et al.: Parameter synthesis for Markov models. CoRR abs\/1903.07993 (2019)"},{"key":"3_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-662-49674-9_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Junges","year":"2016","unstructured":"Junges, S., Jansen, N., Dehnert, C., Topcu, U., Katoen, J.-P.: Safety-constrained reinforcement learning for MDPs. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 130\u2013146. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_8"},{"key":"3_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"602","DOI":"10.1007\/978-3-030-81688-9_28","volume-title":"Computer Aided Verification","author":"S Junges","year":"2021","unstructured":"Junges, S., Jansen, N., Seshia, S.A.: Enforcing almost-sure reachability in POMDPs. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 602\u2013625. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_28"},{"issue":"3","key":"3_CR37","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/s10703-010-0097-6","volume":"36","author":"M Kattenbelt","year":"2010","unstructured":"Kattenbelt, M., Kwiatkowska, M.Z., Norman, G., Parker, D.: A game-based abstraction-refinement framework for Markov decision processes. Formal Methods Syst. Des. 36(3), 246\u2013280 (2010)","journal-title":"Formal Methods Syst. Des."},{"key":"3_CR38","unstructured":"Kirk, R., Zhang, A., Grefenstette, E., Rockt\u00e4schel, T.: A survey of generalisation in deep reinforcement learning. CoRR abs\/2111.09794 (2021)"},{"issue":"2","key":"3_CR39","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/s10703-017-0276-9","volume":"51","author":"B K\u00f6nighofer","year":"2017","unstructured":"K\u00f6nighofer, B., et al.: Shield synthesis. Formal Methods Syst. Des. 51(2), 332\u2013361 (2017)","journal-title":"Formal Methods Syst. Des."},{"key":"3_CR40","doi-asserted-by":"crossref","unstructured":"Kretinsky, J., Ramneantu, E., Slivinskiy, A., Weininger, M.: Comparison of algorithms for simple stochastic games. Inf. Comput. 289 (2022)","DOI":"10.1016\/j.ic.2022.104885"},{"key":"3_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/978-3-030-53291-8_25","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2020","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: PRISM-games 3.0: stochastic game verification with concurrency, equilibria and time. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 475\u2013487. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_25"},{"key":"3_CR42","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":"3_CR43","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/j.infsof.2017.10.001","volume":"94","author":"A Lanna","year":"2018","unstructured":"Lanna, A., Castro, T., Alves, V., Rodrigues, G., Schobbens, P.Y., Apel, S.: Feature-family-based reliability analysis of software product lines. Inf. Softw. Technol. 94, 59\u201381 (2018)","journal-title":"Inf. Softw. Technol."},{"key":"3_CR44","unstructured":"Narvekar, S., Peng, B., Leonetti, M., Sinapov, J., Taylor, M.E., Stone, P.: Curriculum learning for reinforcement learning domains: a framework and survey. J. Mach. Learn. Res. 21, 181:1\u2013181:50 (2020)"},{"issue":"5","key":"3_CR45","doi-asserted-by":"publisher","first-page":"780","DOI":"10.1287\/opre.1050.0216","volume":"53","author":"A Nilim","year":"2005","unstructured":"Nilim, A., Ghaoui, L.E.: Robust control of Markov decision processes with uncertain transition matrices. Oper. Res. 53(5), 780\u2013798 (2005)","journal-title":"Oper. Res."},{"key":"3_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-642-39799-8_35","volume-title":"Computer Aided Verification","author":"A Puggelli","year":"2013","unstructured":"Puggelli, A., Li, W., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Polynomial-time verification of PCTL properties of MDPs with convex uncertainties. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 527\u2013542. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_35"},{"key":"3_CR47","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley (2014)"},{"key":"3_CR48","unstructured":"Raskin, J., Sankur, O.: Multiple-environment Markov decision processes. In: FSTTCS, vol.\u00a029, pp. 531\u2013543. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2014)"},{"key":"3_CR49","doi-asserted-by":"crossref","unstructured":"Rodrigues, G.N., et al.: Modeling and verification for probabilistic properties in software product lines. In: HASE, pp. 173\u2013180. IEEE Computer Society (2015)","DOI":"10.1109\/HASE.2015.34"},{"issue":"10","key":"3_CR50","doi-asserted-by":"publisher","first-page":"1095","DOI":"10.1073\/pnas.39.10.1095","volume":"39","author":"LS Shapley","year":"1953","unstructured":"Shapley, L.S.: Stochastic games*. Proc. Natl. Acad. Sci. U.S.A. 39(10), 1095\u20131100 (1953)","journal-title":"Proc. Natl. Acad. Sci. U.S.A."},{"issue":"10","key":"3_CR51","first-page":"1124","volume":"53","author":"LN Steimle","year":"2021","unstructured":"Steimle, L.N., Kaufman, D.L., Denton, B.T.: Multi-model Markov decision processes. IISE Trans. 53(10), 1124\u20131139 (2021)","journal-title":"IISE Trans."},{"key":"3_CR52","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1016\/j.ejcon.2016.04.009","volume":"30","author":"M Svorenova","year":"2016","unstructured":"Svorenova, M., Kwiatkowska, M.: Quantitative verification and strategy synthesis for stochastic games. Eur. J. Control. 30, 15\u201330 (2016)","journal-title":"Eur. J. Control."},{"issue":"4\u20135","key":"3_CR53","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1007\/s00165-021-00547-2","volume":"33","author":"M \u010ce\u0161ka","year":"2021","unstructured":"\u010ce\u0161ka, M., Hensel, C., Junges, S., Katoen, J.P.: Counterexample-guided inductive synthesis for probabilistic systems. Form. Asp. Comput. 33(4\u20135), 637\u2013667 (2021)","journal-title":"Form. Asp. Comput."},{"key":"3_CR54","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"508","DOI":"10.1007\/978-3-031-30823-9_26","volume-title":"TACAS 2023","author":"M van der Vegt","year":"2023","unstructured":"van der Vegt, M., Jansen, N., Junges, S.: Robust almost-sure reachability in multi-environment MDPs. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023. LNCS, vol. 13993, pp. 508\u2013526. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_26"},{"key":"3_CR55","doi-asserted-by":"crossref","unstructured":"Vos, D., Verwer, S.: Optimal decision tree policies for Markov decision processes. In: IJCAI, pp. 5457\u20135465 (2023)","DOI":"10.24963\/ijcai.2023\/606"},{"key":"3_CR56","doi-asserted-by":"crossref","unstructured":"Weininger, M., Meggendorfer, T., Kret\u00ednsk\u00fd, J.: Satisfiability bounds for $$\\omega $$-regular properties in bounded-parameter Markov decision processes. In: CDC, pp. 2284\u20132291. IEEE (2019)","DOI":"10.1109\/CDC40024.2019.9029460"},{"key":"3_CR57","unstructured":"Winkler, T., Junges, S., P\u00e9rez, G.A., Katoen, J.: On the complexity of reachability in parametric Markov decision processes. In: CONCUR, vol.\u00a0140, pp. 14:1\u201314:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019)"},{"issue":"3","key":"3_CR58","doi-asserted-by":"publisher","first-page":"1040","DOI":"10.1109\/TAC.2020.2990140","volume":"66","author":"L Winterer","year":"2021","unstructured":"Winterer, L., et al.: Strategy synthesis for POMDPs in robot planning via game-based abstractions. IEEE Trans. Autom. Control 66(3), 1040\u20131054 (2021)","journal-title":"IEEE Trans. Autom. Control"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-78750-8_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T10:08:35Z","timestamp":1769681315000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-78750-8_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031787492","9783031787508"],"references-count":58,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-78750-8_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"12 February 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Kyoto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","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":"21 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}