{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T06:59:29Z","timestamp":1779087569723,"version":"3.51.4"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031572487","type":"print"},{"value":"9783031572494","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,4,5]],"date-time":"2024-04-05T00:00:00Z","timestamp":1712275200000},"content-version":"vor","delay-in-days":95,"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>Computing schedulers that optimize reachability probabilities in MDPs is a standard verification task. To address scalability concerns, we focus on MDPs that are compositionally described in a high-level description formalism. In particular, this paper considers<jats:italic>string diagrams<\/jats:italic>, which specify an algebraic, sequential composition of subMDPs. Towards their compositional verification, the key challenge is to locally optimize schedulers on subMDPs without considering their context in the string diagram. This paper proposes to consider the schedulers in a subMDP which form a<jats:italic>Pareto curve<\/jats:italic>on a combination of local objectives. While considering all such schedulers is intractable, it gives rise to a highly efficient sound approximation algorithm. The prototype on top of the model checker Storm demonstrates the scalability of this approach.<\/jats:p>","DOI":"10.1007\/978-3-031-57249-4_14","type":"book-chapter","created":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T07:02:35Z","timestamp":1712214155000},"page":"279-298","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Pareto Curves for Compositionally Model Checking String Diagrams of MDPs"],"prefix":"10.1007","author":[{"given":"Kazuki","family":"Watanabe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marck","family":"van der Vegt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ichiro","family":"Hasuo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jurriaan","family":"Rot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sebastian","family":"Junges","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,4,5]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"\u00c1brah\u00e1m, E., Jansen, N., Wimmer, R., Katoen, J., Becker, B.: DTMC model checking by SCC reduction. In: QEST. pp. 37\u201346. IEEE Computer Society (2010)","DOI":"10.1109\/QEST.2010.13"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"de\u00a0Alfaro, L., Kwiatkowska, M.Z., Norman, G., Parker, D., Segala, R.: Symbolic model checking of probabilistic processes using MTBDDs and the Kronecker representation. In: TACAS. LNCS, vol.\u00a01785, pp. 395\u2013410. Springer (2000)","DOI":"10.1007\/3-540-46419-0_27"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Baier, C., Clarke, E.M., Hartonas-Garmhausen, V., Kwiatkowska, M.Z., Ryan, M.: Symbolic model checking for probabilistic processes. In: ICALP. LNCS, vol.\u00a01256, pp. 430\u2013440. Springer (1997)","DOI":"10.1007\/3-540-63165-8_199"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Baier, C., Hermanns, H., Katoen, J.: The 10, 000 facets of MDP model checking. In: Computing and Software Science, LNCS, vol. 10000, pp. 420\u2013451. Springer (2019)","DOI":"10.1007\/978-3-319-91908-9_21"},{"key":"14_CR5","unstructured":"Baier, C., Katoen, J.: Principles of model checking. MIT Press (2008)"},{"key":"14_CR6","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)"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Budde, C.E., Hartmanns, A., Klauck, M., Kret\u00ednsk\u00fd, J., Parker, D., Quatmann, T., Turrini, A., Zhang, Z.: On correctness, precision, and performance in quantitative verification - qcomp 2020 competition report. In: ISoLA (4). LNCS, vol. 12479, pp. 216\u2013241. Springer (2020)","DOI":"10.1007\/978-3-030-83723-5_15"},{"key":"14_CR8","doi-asserted-by":"publisher","unstructured":"Chatterjee, K.: Robustness of structurally equivalent concurrent parity games. In: FOSSACS. LNCS, vol.\u00a07213, pp. 270\u2013285. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-28729-9_18, https:\/\/doi.org\/10.1007\/978-3-642-28729-9_18","DOI":"10.1007\/978-3-642-28729-9_18 10.1007\/978-3-642-28729-9_18"},{"key":"14_CR9","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.2168\/LMCS-4(4:8)2008, https:\/\/doi.org\/10.2168\/LMCS-4(4:8)2008","DOI":"10.2168\/LMCS-4(4:8)2008 10.2168\/LMCS-4(4:8)2008"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Feng, L., Han, T., Kwiatkowska, M.Z., Parker, D.: Learning-based compositional verification for synchronous probabilistic systems. In: ATVA. LNCS, vol.\u00a06996, pp. 511\u2013521. Springer (2011)","DOI":"10.1007\/978-3-642-24372-1_40"},{"key":"14_CR11","doi-asserted-by":"publisher","unstructured":"Forejt, V., Kwiatkowska, M.Z., Norman, G., Parker, D., Qu, H.: Quantitative multi-objective verification for probabilistic systems. In: TACAS. LNCS, vol.\u00a06605, pp. 112\u2013127. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_11, https:\/\/doi.org\/10.1007\/978-3-642-19835-9_11","DOI":"10.1007\/978-3-642-19835-9_11 10.1007\/978-3-642-19835-9_11"},{"key":"14_CR12","doi-asserted-by":"publisher","unstructured":"Forejt, V., Kwiatkowska, M.Z., Parker, D.: Pareto curves for probabilistic model checking. In: ATVA. LNCS, vol.\u00a07561, pp. 317\u2013332. Springer (2012), https:\/\/doi.org\/10.1007\/978-3-642-33386-6_25","DOI":"10.1007\/978-3-642-33386-6_25"},{"key":"14_CR13","doi-asserted-by":"publisher","unstructured":"Hartmanns, A., Hermanns, H.: The Modest toolset: An integrated environment for quantitative modelling and verification. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS. LNCS, vol.\u00a08413, pp. 593\u2013598. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_51, https:\/\/doi.org\/10.1007\/978-3-642-54862-8_51","DOI":"10.1007\/978-3-642-54862-8_51 10.1007\/978-3-642-54862-8_51"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Junges, S., Katoen, J., Quatmann, T.: Multi-cost bounded tradeoff analysis in MDP. J. Autom. Reason. 64(7), 1483\u20131522 (2020)","DOI":"10.1007\/s10817-020-09574-9"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Junges, S., Quatmann, T., Weininger, M.: A practitioner\u2019s guide to MDP model checking algorithms. In: TACAS (1). LNCS, vol. 13993, pp. 469\u2013488. Springer (2023)","DOI":"10.1007\/978-3-031-30823-9_24"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Hartmanns, A., Kaminski, B.L.: Optimistic value iteration. In: CAV (2). LNCS, vol. 12225, pp. 488\u2013511. Springer (2020)","DOI":"10.1007\/978-3-030-53291-8_26"},{"key":"14_CR17","doi-asserted-by":"publisher","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). 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 10.1007\/s10009-021-00633-z"},{"key":"14_CR18","doi-asserted-by":"publisher","unstructured":"Hinze, R., Marsden, D.: Introducing String Diagrams: The Art of Category Theory. Cambridge University Press (2023). https:\/\/doi.org\/10.1017\/9781009317825","DOI":"10.1017\/9781009317825"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Holtzen, S., Junges, S., Vazquez-Chanlatte, M., Millstein, T.D., Seshia, S.A., den Broeck, G.V.: Model checking finite-horizon Markov chains with probabilistic inference. In: CAV (2). LNCS, vol. 12760, pp. 577\u2013601. Springer (2021)","DOI":"10.1007\/978-3-030-81688-9_27"},{"key":"14_CR20","unstructured":"Jothimurugan, K., Bansal, S., Bastani, O., Alur, R.: Compositional reinforcement learning from logical specifications. In: NeurIPS. pp. 10026\u201310039 (2021)"},{"key":"14_CR21","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 - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I. LNCS, vol. 13371, pp. 102\u2013123. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_6, https:\/\/doi.org\/10.1007\/978-3-031-13185-1_6","DOI":"10.1007\/978-3-031-13185-1_6 10.1007\/978-3-031-13185-1_6"},{"key":"14_CR22","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: CAV. LNCS, vol.\u00a06806, pp. 585\u2013591. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47, https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47","DOI":"10.1007\/978-3-642-22110-1_47 10.1007\/978-3-642-22110-1_47"},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D., Qu, H.: Assume-guarantee verification for probabilistic systems. In: TACAS. LNCS, vol.\u00a06015, pp. 23\u201337. Springer (2010)","DOI":"10.1007\/978-3-642-12002-2_3"},{"key":"14_CR24","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D., Qu, H.: Compositional probabilistic verification through multi-objective model checking. Inf. Comput. 232, 38\u201365 (2013). https:\/\/doi.org\/10.1016\/j.ic.2013.10.001, https:\/\/doi.org\/10.1016\/j.ic.2013.10.001","DOI":"10.1016\/j.ic.2013.10.001 10.1016\/j.ic.2013.10.001"},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"Mac\u00a0Lane, S.: Categories for the working mathematician, Graduate Texts in Mathematics, vol.\u00a05. Springer-Verlag, New York, second edn. (1978)","DOI":"10.1007\/978-1-4757-4721-8"},{"key":"14_CR26","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":"14_CR27","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1109\/SFCS.2000.892068, https:\/\/doi.org\/10.1109\/SFCS.2000.892068","DOI":"10.1109\/SFCS.2000.892068 10.1109\/SFCS.2000.892068"},{"key":"14_CR28","doi-asserted-by":"crossref","unstructured":"Pateria, S., Subagdja, B., Tan, A., Quek, C.: Hierarchical reinforcement learning: A comprehensive survey. ACM Comput. Surv. 54(5), 109:1\u2013109:35 (2021)","DOI":"10.1145\/3453160"},{"key":"14_CR29","doi-asserted-by":"publisher","unstructured":"Quatmann, T., Junges, S., Katoen, J.: Markov automata with multiple objectives. Formal Methods Syst. Des. 60(1), 33\u201386 (2022). https:\/\/doi.org\/10.1007\/s10703-021-00364-6, https:\/\/doi.org\/10.1007\/s10703-021-00364-6","DOI":"10.1007\/s10703-021-00364-6 10.1007\/s10703-021-00364-6"},{"key":"14_CR30","doi-asserted-by":"publisher","unstructured":"Quatmann, T., Katoen, J.: Multi-objective optimization of long-run average and total rewards. In: TACAS. LNCS, vol. 12651, pp. 230\u2013249. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_13, https:\/\/doi.org\/10.1007\/978-3-030-72016-2_13","DOI":"10.1007\/978-3-030-72016-2_13 10.1007\/978-3-030-72016-2_13"},{"key":"14_CR31","doi-asserted-by":"crossref","unstructured":"Selinger, P.: A survey of graphical languages for monoidal categories. New structures for physics pp. 289\u2013355 (2011)","DOI":"10.1007\/978-3-642-12821-9_4"},{"key":"14_CR32","doi-asserted-by":"publisher","unstructured":"Watanabe, K., Eberhart, C., Asada, K., Hasuo, I.: A compositional approach to parity games. In: MFPS. EPTCS, vol.\u00a0351, pp. 278\u2013295 (2021). https:\/\/doi.org\/10.4204\/EPTCS.351.17, https:\/\/doi.org\/10.4204\/EPTCS.351.17","DOI":"10.4204\/EPTCS.351.17 10.4204\/EPTCS.351.17"},{"key":"14_CR33","doi-asserted-by":"publisher","unstructured":"Watanabe, K., Eberhart, C., Asada, K., Hasuo, I.: Compositional probabilistic model checking with string diagrams of MDPs. In: CAV. LNCS, vol. 13966, pp. 40\u201361. Springer (2023), https:\/\/doi.org\/10.1007\/978-3-031-37709-9_3","DOI":"10.1007\/978-3-031-37709-9_3"},{"key":"14_CR34","doi-asserted-by":"crossref","unstructured":"Watanabe, K., van\u00a0der Vegt, M., Hasuo, I., Rot, J., Junges, S.: Pareto curves for compositionally model checking string diagrams of MDPs (2024), https:\/\/arxiv.org\/abs\/2401.08377, a longer version","DOI":"10.1007\/978-3-031-57249-4_14"},{"key":"14_CR35","doi-asserted-by":"crossref","unstructured":"Xu, D.N., G\u00f6\u00dfler, G., Girault, A.: Probabilistic contracts for component-based design. In: ATVA. LNCS, vol.\u00a06252, pp. 325\u2013340. Springer (2010)","DOI":"10.1007\/978-3-642-15643-4_24"}],"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-031-57249-4_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,15]],"date-time":"2024-11-15T17:16:12Z","timestamp":1731690972000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57249-4_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572487","9783031572494"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57249-4_14","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":"5 April 2024","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":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","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":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"53","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":"16","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":"33% - 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)"}}]}}