{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:34:10Z","timestamp":1770287650983,"version":"3.49.0"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031377082","type":"print"},{"value":"9783031377099","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T00:00:00Z","timestamp":1689552000000},"content-version":"vor","delay-in-days":197,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a compositional model checking algorithm for Markov decision processes, in which they are composed in the categorical graphical language of<jats:italic>string diagrams<\/jats:italic>. The algorithm computes optimal expected rewards. Our theoretical development of the algorithm is supported by category theory, while what we call decomposition equalities for expected rewards act as a key enabler. Experimental evaluation demonstrates its performance advantages.<\/jats:p>","DOI":"10.1007\/978-3-031-37709-9_3","type":"book-chapter","created":{"date-parts":[[2023,7,16]],"date-time":"2023-07-16T10:01:21Z","timestamp":1689501681000},"page":"40-61","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Compositional Probabilistic Model Checking with\u00a0String Diagrams of\u00a0MDPs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4167-3370","authenticated-orcid":false,"given":"Kazuki","family":"Watanabe","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3009-6747","authenticated-orcid":false,"given":"Clovis","family":"Eberhart","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8782-2119","authenticated-orcid":false,"given":"Kazuyuki","family":"Asada","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8300-4650","authenticated-orcid":false,"given":"Ichiro","family":"Hasuo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,7,17]]},"reference":[{"key":"3_CR1","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-662-54580-5_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Baier","year":"2017","unstructured":"Baier, C., Klein, J., Kl\u00fcppelholz, S., Wunderlich, S.: Maximizing the conditional expected reward for reaching the goal. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 269\u2013285. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_16"},{"key":"3_CR3","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1145\/3290338","DOI":"10.1145\/3290338"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Long, D.E., McMillan, K.L.: Compositional model checking. In: Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS \u201989), Pacific Grove, California, USA, 5\u20138 June 1989, pp. 353\u2013362. IEEE Computer Society (1989). https:\/\/doi.org\/10.1109\/LICS.1989.39190","DOI":"10.1109\/LICS.1989.39190"},{"key":"3_CR5","unstructured":"Cruttwell, G.S.: Normed spaces and the change of base for enriched categories. Ph.D. thesis, Dalhousie University (2008)"},{"key":"3_CR6","doi-asserted-by":"publisher","unstructured":"Eilenberg, S., Kelly, G.M.: Closed categories. In: Eilenberg, S., Harrison, D.K., MacLane, S., R\u00f6hrl, H. (eds.) Proceedings of the Conference on Categorical Algebra: La Jolla 1965, pp. 421\u2013562. Springer, Heidelberg (1966). https:\/\/doi.org\/10.1007\/978-3-642-99902-4_22","DOI":"10.1007\/978-3-642-99902-4_22"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Girard, J.Y.: Geometry of interaction I: interpretation of System F. In: Studies in Logic and the Foundations of Mathematics, vol. 127, pp. 221\u2013260. Elsevier (1989)","DOI":"10.1016\/S0049-237X(08)70271-4"},{"key":"3_CR8","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198739623.001.0001","volume-title":"Categories for Quantum Theory: An Introduction","author":"C Heunen","year":"2019","unstructured":"Heunen, C., Vicary, J.: Categories for Quantum Theory: An Introduction. Oxford University Press, Oxford (2019)"},{"key":"3_CR9","doi-asserted-by":"publisher","unstructured":"Hoshino, N.: A representation theorem for unique decomposition categories. In: Berger, U., Mislove, M.W. (eds.) Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2012, Bath, UK, 6\u20139 June 2012. Electronic Notes in Theoretical Computer Science, vol. 286, pp. 213\u2013227. Elsevier (2012). https:\/\/doi.org\/10.1016\/j.entcs.2012.08.014","DOI":"10.1016\/j.entcs.2012.08.014"},{"issue":"3","key":"3_CR10","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1017\/S0305004100074338","volume":"119","author":"A Joyal","year":"1996","unstructured":"Joyal, A., Street, R., Verity, D.: Traced monoidal categories. Math. Proc. Cambridge Philos. Soc. 119(3), 447\u2013468 (1996)","journal-title":"Math. Proc. Cambridge Philos. Soc."},{"key":"3_CR11","doi-asserted-by":"publisher","unstructured":"Junges, S., Spaan, M.T.J.: Abstraction-refinement for hierarchical probabilistic models. In: Shoham, S., Vizel, Y. (eds.) CAV 2022, Part I. LNCS, vol. 13371, pp. 102\u2013123. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_6","DOI":"10.1007\/978-3-031-13185-1_6"},{"issue":"2","key":"3_CR12","doi-asserted-by":"publisher","first-page":"665","DOI":"10.2140\/agt.2002.2.665","volume":"2","author":"M Khovanov","year":"2002","unstructured":"Khovanov, M.: A functor-valued invariant of tangles. Algebraic Geom. Topol. 2(2), 665\u2013741 (2002)","journal-title":"Algebraic Geom. Topol."},{"key":"3_CR13","doi-asserted-by":"publisher","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","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"3_CR14","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). https:\/\/doi.org\/10.1016\/j.ic.2013.10.001","journal-title":"Inf. Comput."},{"key":"3_CR15","doi-asserted-by":"publisher","unstructured":"Mac Lane, S.: Categories for the Working Mathematician, 2nd edn. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/978-1-4757-4721-8","DOI":"10.1007\/978-1-4757-4721-8"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55\u201392 (1991)","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"3_CR17","doi-asserted-by":"publisher","unstructured":"Piedeleu, R., Kartsaklis, D., Coecke, B., Sadrzadeh, M.: Open system categorical quantum semantics in natural language processing. In: Moss, L.S., Sobocinski, P. (eds.) 6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015, 24\u201326 June 2015, Nijmegen, The Netherlands. LIPIcs, vol. 35, pp. 270\u2013289. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2015). https:\/\/doi.org\/10.4230\/LIPIcs.CALCO.2015.270","DOI":"10.4230\/LIPIcs.CALCO.2015.270"},{"key":"3_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-319-46520-3_4","volume-title":"Automated Technology for Verification and Analysis","author":"T Quatmann","year":"2016","unstructured":"Quatmann, T., Dehnert, C., Jansen, N., Junges, S., Katoen, J.-P.: Parameter synthesis for markov models: faster than ever. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 50\u201367. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_4"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Tsukada, T., Ong, C.L.: Compositional higher-order model checking via $$\\omega $$-regular games over B\u00f6hm trees. In: Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS \u201914, Vienna, Austria, 14\u201318 July 2014, pp. 78:1\u201378:10. ACM (2014)","DOI":"10.1145\/2603088.2603133"},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Watanabe, K., Eberhart, C., Asada, K., Hasuo, I.: A compositional approach to parity games. In: Sokolova, A. (ed.) Proceedings 37th Conference on Mathematical Foundations of Programming Semantics, MFPS 2021, Hybrid: Salzburg, Austria and Online, 30 August\u20132 September 2021. EPTCS, vol. 351, pp. 278\u2013295 (2021). https:\/\/doi.org\/10.4204\/EPTCS.351.17","DOI":"10.4204\/EPTCS.351.17"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Watanabe, K., Eberhart, C., Asada, K., Hasuo, I.: Compositional probabilistic model checking with string diagrams of MDPs (extended version) (2023), to appear in arXiv","DOI":"10.1007\/978-3-031-37709-9_3"}],"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-37709-9_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,17]],"date-time":"2023-12-17T05:00:51Z","timestamp":1702789251000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37709-9_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377082","9783031377099"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37709-9_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 July 2023","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":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","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":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","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":"67","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":"0","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":"26% - 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":"11","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)"}}]}}