{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:19:59Z","timestamp":1778498399594,"version":"3.51.4"},"publisher-location":"Cham","reference-count":55,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031656323","type":"print"},{"value":"9783031656330","type":"electronic"}],"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>The de-facto standard approach in MDP verification is based on value iteration (VI). We propose<jats:italic>compositional VI<\/jats:italic>, a framework for model checking compositional MDPs, that addresses efficiency while maintaining soundness. Concretely, compositional MDPs naturally arise from the combination of individual components, and their structure can be expressed using, e.g., string diagrams. Towards efficiency, we observe that compositional VI repeatedly verifies individual components. We propose a technique called<jats:italic>Pareto caching<\/jats:italic>that allows to reuse verification results, even for previously unseen queries. Towards soundness, we present two stopping criteria: one generalizes the optimistic value iteration paradigm and the other uses Pareto caches in conjunction with recent baseline algorithms. Our experimental evaluations shows the promise of the novel algorithm and its variations, and identifies challenges for future work.<\/jats:p>","DOI":"10.1007\/978-3-031-65633-0_21","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:03:08Z","timestamp":1721890988000},"page":"467-491","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Compositional Value Iteration with\u00a0Pareto Caching"],"prefix":"10.1007","author":[{"given":"Kazuki","family":"Watanabe","sequence":"first","affiliation":[]},{"given":"Marck van der","family":"Vegt","sequence":"additional","affiliation":[]},{"given":"Sebastian","family":"Junges","sequence":"additional","affiliation":[]},{"given":"Ichiro","family":"Hasuo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"Ashok, P., Chatterjee, K., Kret\u00ednsk\u00fd, J., Weininger, M., Winkler, T.: Approximating values of generalized-reachability stochastic games. In: LICS, pp. 102\u2013115. ACM (2020)","DOI":"10.1145\/3373718.3394761"},{"key":"21_CR2","doi-asserted-by":"publisher","unstructured":"Azeem, M., Evangelidis, A., Kret\u00ednsk\u00fd, J., Slivinskiy, A., Weininger, M.: Optimistic and topological value iteration for simple stochastic games. In: Bouajjani, A., Hol\u00edk, L., Wu, Z. (eds.) Automated Technology for Verification and Analysis. ATVA 2022. LNCS, vol. 13505. Springer, Cham (2022).https:\/\/doi.org\/10.1007\/978-3-031-19992-9_18","DOI":"10.1007\/978-3-031-19992-9_18"},{"key":"21_CR3","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-319-63387-9_8","volume-title":"Computer Aided Verification","author":"C Baier","year":"2017","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: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 160\u2013180. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_8"},{"key":"21_CR5","unstructured":"Barry, J.L., Kaelbling, L.P., Lozano-P\u00e9rez, T.: Deth*: Approximate hierarchical solution of large Markov decision processes. In: IJCAI, pp. 1928\u20131935. IJCAI\/AAAI (2011)"},{"issue":"1\u20132","key":"21_CR6","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1023\/A:1022140919877","volume":"13","author":"AG Barto","year":"2003","unstructured":"Barto, A.G., Mahadevan, S.: Recent advances in hierarchical reinforcement learning. Discret. Event Dyn. Syst. 13(1\u20132), 41\u201377 (2003)","journal-title":"Discret. Event Dyn. Syst."},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/978-3-662-46681-0_50","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Bloem","year":"2015","unstructured":"Bloem, R., Chatterjee, K., Jacobs, S., K\u00f6nighofer, R.: Assume-guarantee synthesis for concurrent reactive programs with partial information. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 517\u2013532. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_50"},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"Bonchi, F., Gadducci, F., Kissinger, A., Sobocinski, P., Zanasi, F.: String diagram rewrite theory I: rewriting with Frobenius structure. J. ACM 69(2), 14:1\u201314:58 (2022)","DOI":"10.1145\/3502719"},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"Bonchi, F., Holland, J., Piedeleu, R., Sobocinski, P., Zanasi, F.: Diagrammatic algebra: from linear to concurrent systems. Proc. ACM Program. Lang. 3(POPL), 25:1\u201325:28 (2019)","DOI":"10.1145\/3290338"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-319-11936-6_8","volume-title":"Automated Technology for Verification and Analysis","author":"T Br\u00e1zdil","year":"2014","unstructured":"Br\u00e1zdil, T., et al.: Verification of Markov decision processes using learning algorithms. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 98\u2013114. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_8"},{"key":"21_CR11","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":"21_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-540-71209-1_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Chatterjee","year":"2007","unstructured":"Chatterjee, K., Henzinger, T.A.: Assume-guarantee synthesis. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 261\u2013275. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_21"},{"key":"21_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-642-40313-2_25","volume-title":"Mathematical Foundations of Computer Science 2013","author":"T Chen","year":"2013","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M., Simaitis, A., Wiltsche, C.: On stochastic games with multiple objectives. In: Chatterjee, K., Sgall, J. (eds.) MFCS 2013. LNCS, vol. 8087, pp. 266\u2013277. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40313-2_25"},{"key":"21_CR14","unstructured":"Ciosek, K., Silver, D.: Value iteration with options and state aggregation (2015). CoRR abs\/1501.03959"},{"key":"21_CR15","unstructured":"Dai, P., Mausam, Weld, D.S., Goldsmith, J.J.: Topological value iteration algorithms. Artif. Intell. Res. 42, 181\u2013209 (2011)"},{"key":"21_CR16","doi-asserted-by":"publisher","unstructured":"Dewes, R., Dimitrova, R.: Compositional high-quality synthesis. In: Andr\u00e9, \u00c9., Sun, J. (eds.) Automated Technology for Verification and Analysis. ATVA 2023. LNCS, vol. 14215. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-45329-8_16","DOI":"10.1007\/978-3-031-45329-8_16"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"Etessami, K., Kwiatkowska, M.Z., Vardi, M.Y., Yannakakis, M.: Multi-objective model checking of Markov decision processes. Log. Methods Comput. Sci. 4(4) (2008)","DOI":"10.2168\/LMCS-4(4:8)2008"},{"issue":"3","key":"21_CR18","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/s11334-022-00450-w","volume":"18","author":"B Finkbeiner","year":"2022","unstructured":"Finkbeiner, B., Passing, N.: Compositional synthesis of modular systems. Innov. Syst. Softw. Eng. 18(3), 455\u2013469 (2022)","journal-title":"Innov. Syst. Softw. Eng."},{"key":"21_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-642-19835-9_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V Forejt","year":"2011","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Quantitative multi-objective verification for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 112\u2013127. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_11"},{"key":"21_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-642-33386-6_25","volume-title":"Automated Technology for Verification and Analysis","author":"V Forejt","year":"2012","unstructured":"Forejt, V., Kwiatkowska, M., Parker, D.: Pareto curves for probabilistic model checking. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 317\u2013332. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33386-6_25"},{"key":"21_CR21","unstructured":"Gamrath, G., et al.: The SCIP optimization suite 7.0. Tech. Rep. 20-10, ZIB, Takustr. 7, 14195 Berlin (2020)"},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"Ghani, N., Hedges, J., Winschel, V., Zahn, P.: Compositional game theory. In: LICS, pp. 472\u2013481. ACM (2018)","DOI":"10.1145\/3209108.3209165"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Gopalan, N., et al.: Planning with abstract Markov decision processes. In: ICAPS, pp. 480\u2013488. AAAI Press (2017)","DOI":"10.1609\/icaps.v27i1.13867"},{"key":"21_CR24","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/j.tcs.2016.12.003","volume":"735","author":"S Haddad","year":"2018","unstructured":"Haddad, S., Monmege, B.: Interval iteration algorithm for MDPs and IMDPs. Theor. Comput. Sci. 735, 111\u2013131 (2018)","journal-title":"Theor. Comput. Sci."},{"key":"21_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-319-47677-3_6","volume-title":"Dependable Software Engineering: Theories, Tools, and Applications","author":"EM Hahn","year":"2016","unstructured":"Hahn, E.M., Hartmanns, A.: A comparison of time- and reward-bounded probabilistic model checking techniques. In: Fr\u00e4nzle, M., Kapur, D., Zhan, N. (eds.) SETTA 2016. LNCS, vol. 9984, pp. 85\u2013100. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47677-3_6"},{"key":"21_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-030-99527-0_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hartmanns","year":"2022","unstructured":"Hartmanns, A.: Correct probabilistic model checking with floating-point arithmetic. In: TACAS 2022. LNCS, vol. 13244, pp. 41\u201359. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_3"},{"key":"21_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/978-3-642-54862-8_51","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hartmanns","year":"2014","unstructured":"Hartmanns, A., Hermanns, H.: The modest toolset: an integrated environment for quantitative modelling and verification. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 593\u2013598. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_51"},{"issue":"7","key":"21_CR28","doi-asserted-by":"publisher","first-page":"1483","DOI":"10.1007\/s10817-020-09574-9","volume":"64","author":"A Hartmanns","year":"2020","unstructured":"Hartmanns, A., Junges, S., Katoen, J., Quatmann, T.: Multi-cost bounded tradeoff analysis in MDP. J. Autom. Reason. 64(7), 1483\u20131522 (2020)","journal-title":"J. Autom. Reason."},{"key":"21_CR29","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Junges, S., Quatmann, T., Weininger, M.: A practitioner\u2019s guide to MDP model checking algorithms. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2023. LNCS, vol. 13993. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_24","DOI":"10.1007\/978-3-031-30823-9_24"},{"key":"21_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1007\/978-3-030-53291-8_26","volume-title":"Computer Aided Verification","author":"A Hartmanns","year":"2020","unstructured":"Hartmanns, A., Kaminski, B.L.: Optimistic value iteration. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 488\u2013511. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_26"},{"key":"21_CR31","unstructured":"Hauskrecht, M., Meuleau, N., Kaelbling, L.P., Dean, T.L., Boutilier, C.: Hierarchical solution of Markov decision processes using macro-actions. In: UAI, pp. 220\u2013229. Morgan Kaufmann (1998)"},{"issue":"4","key":"21_CR32","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."},{"key":"21_CR33","unstructured":"Jothimurugan, K., Bansal, S., Bastani, O., Alur, R.: Compositional reinforcement learning from logical specifications. In: NeurIPS, pp. 10026\u201310039 (2021)"},{"key":"21_CR34","unstructured":"Jothimurugan, K., Bastani, O., Alur, R.: Abstract value iteration for hierarchical reinforcement learning. In: AISTATS. Proceedings of Machine Learning Research, vol.\u00a0130, pp. 1162\u20131170. PMLR (2021)"},{"key":"21_CR35","doi-asserted-by":"publisher","unstructured":"Junges, S., Spaan, M.T.J.: Abstraction-refinement for hierarchical probabilistic models. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification. CAV 2022. LNCS, vol. 13371. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_6","DOI":"10.1007\/978-3-031-13185-1_6"},{"key":"21_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-662-49674-9_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Klein","year":"2016","unstructured":"Klein, J., et al.: Advances in symbolic probabilistic model checking with PRISM. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 349\u2013366. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_20"},{"key":"21_CR37","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":"21_CR38","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1016\/j.ic.2013.10.001","volume":"232","author":"MZ Kwiatkowska","year":"2013","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D., Qu, H.: Compositional probabilistic verification through multi-objective model checking. Inf. Comput. 232, 38\u201365 (2013)","journal-title":"Inf. Comput."},{"key":"21_CR39","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Mallik, K., Schmuck, A., Zufferey, D.: Assume-guarantee distributed synthesis. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 39(11), 3215\u20133226 (2020)","DOI":"10.1109\/TCAD.2020.3012641"},{"key":"21_CR40","doi-asserted-by":"crossref","unstructured":"Neary, C., Verginis, C.K., Cubuktepe, M., Topcu, U.: Verifiable and compositional reinforcement learning systems. In: ICAPS, pp. 615\u2013623. AAAI Press (2022)","DOI":"10.1609\/icaps.v32i1.19849"},{"key":"21_CR41","doi-asserted-by":"crossref","unstructured":"Papadimitriou, C.H., Yannakakis, M.: On the approximability of trade-offs and optimal access of web sources. In: FOCS, pp. 86\u201392. IEEE Computer Society (2000)","DOI":"10.1109\/SFCS.2000.892068"},{"key":"21_CR42","first-page":"59","volume":"5","author":"D Park","year":"1969","unstructured":"Park, D.: Fixpoint induction and proofs of program properties. Machine intelligence 5, 59\u201378 (1969)","journal-title":"Machine intelligence"},{"key":"21_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-030-53291-8_19","volume-title":"Computer Aided Verification","author":"K Phalakarn","year":"2020","unstructured":"Phalakarn, K., Takisaka, T., Haas, T., Hasuo, I.: Widest paths and global propagation in bounded value iteration for stochastic games. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 349\u2013371. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_19"},{"key":"21_CR44","doi-asserted-by":"crossref","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics, Wiley, Hoboken (1994)","DOI":"10.1002\/9780470316887"},{"key":"21_CR45","doi-asserted-by":"publisher","unstructured":"Quatmann, T.: Verification of multi-objective Markov models. Phd thesis (2023). https:\/\/doi.org\/10.18154\/RWTH-2023-09669, https:\/\/publications.rwth-aachen.de\/record\/971553","DOI":"10.18154\/RWTH-2023-09669"},{"key":"21_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1007\/978-3-319-96145-3_37","volume-title":"Computer Aided Verification","author":"T Quatmann","year":"2018","unstructured":"Quatmann, T., Katoen, J.-P.: Sound value iteration. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 643\u2013661. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_37"},{"key":"21_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-030-72016-2_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Quatmann","year":"2021","unstructured":"Quatmann, T., Katoen, J.-P.: Multi-objective optimization of long-run average and total rewards. In: TACAS 2021. LNCS, vol. 12651, pp. 230\u2013249. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_13"},{"key":"21_CR48","unstructured":"Saxe, A.M., Earle, A.C., Rosman, B.: Hierarchy through composition with multitask LMDPs. In: ICML. Proceedings of Machine Learning Research, vol.\u00a070, pp. 3017\u20133026. PMLR (2017)"},{"key":"21_CR49","unstructured":"Silver, D., Ciosek, K.: Compositional planning using optimal option models. In: ICML. icml.cc \/ Omnipress (2012)"},{"issue":"1\u20132","key":"21_CR50","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/S0004-3702(99)00052-1","volume":"112","author":"RS Sutton","year":"1999","unstructured":"Sutton, R.S., Precup, D., Singh, S.: Between MDPs and semi-MDPs: a framework for temporal abstraction in reinforcement learning. Artif. Intell. 112(1\u20132), 181\u2013211 (1999)","journal-title":"Artif. Intell."},{"key":"21_CR51","doi-asserted-by":"crossref","unstructured":"Vien, N.A., Toussaint, M.: Hierarchical monte-carlo planning. In: AAAI, pp. 3613\u20133619. AAAI Press (2015)","DOI":"10.1609\/aaai.v29i1.9687"},{"key":"21_CR52","doi-asserted-by":"crossref","unstructured":"Watanabe, K., Eberhart, C., Asada, K., Hasuo, I.: A compositional approach to parity games. In: MFPS. EPTCS, vol.\u00a0351, pp. 278\u2013295 (2021)","DOI":"10.4204\/EPTCS.351.17"},{"key":"21_CR53","doi-asserted-by":"publisher","unstructured":"Watanabe, K., Eberhart, C., Asada, K., Hasuo, I.: Compositional probabilistic model checking with string diagrams of MDPs. In: Enea, C., Lal, A. (eds.) Computer Aided Verification. CAV 2023. LNCS, vol. 13966. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_3","DOI":"10.1007\/978-3-031-37709-9_3"},{"key":"21_CR54","doi-asserted-by":"publisher","unstructured":"Watanabe, K., van der Vegt, M., Hasuo, I., Rot, J., Junges, S.: Pareto curves for compositionally model checking string diagrams of MDPs. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2024. LNCS, vol. 14571. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57249-4_14","DOI":"10.1007\/978-3-031-57249-4_14"},{"key":"21_CR55","unstructured":"Watanabe, K., van\u00a0der Vegt, M., Junges, S., Hasuo, I.: Compositional value iteration with Pareto caching (2024). https:\/\/arxiv.org\/abs\/2405.10099, a longer version"}],"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_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,24]],"date-time":"2024-11-24T20:15:25Z","timestamp":1732479325000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65633-0_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656323","9783031656330"],"references-count":55,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65633-0_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"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"}}]}}