{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T19:32:18Z","timestamp":1757619138905,"version":"3.44.0"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031986789"},{"type":"electronic","value":"9783031986796"}],"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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T00:00:00Z","timestamp":1753142400000},"content-version":"vor","delay-in-days":202,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>This paper presents a novel symbolic algorithm for the <jats:italic>Maximal End Component (MEC)<\/jats:italic> decomposition of a <jats:italic>Markov Decision Process (MDP)<\/jats:italic>. The key idea behind our algorithm  is to interleave the computation of Strongly Connected Components (SCCs) with eager elimination of redundant state-action pairs, rather than performing these computations sequentially as done by existing state-of-the-art algorithms. Even though our approach has the same complexity as prior works, an empirical evaluation of  on the standardized Quantitative Verification Benchmark Set demonstrates that it solves <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\textbf{19}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mn>19<\/mml:mn>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            <jats:bold>more benchmarks<\/jats:bold> (out of 368) than the closest previous algorithm. On the 149 benchmarks that prior approaches can solve, we demonstrate a <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\mathbf {3.81 \\times }$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mn>3.81<\/mml:mn>\n                    <mml:mo>\u00d7<\/mml:mo>\n                  <\/mml:mrow>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            <jats:bold>average speedup<\/jats:bold> in runtime.<\/jats:p>","DOI":"10.1007\/978-3-031-98679-6_7","type":"book-chapter","created":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T09:20:42Z","timestamp":1753089642000},"page":"147-168","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["INTERLEAVE: A Faster Symbolic Algorithm for\u00a0Maximal End Component Decomposition"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0405-073X","authenticated-orcid":false,"given":"Suguman","family":"Bansal","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0001-3204-7562","authenticated-orcid":false,"given":"Ramneet","family":"Singh","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,22]]},"reference":[{"key":"7_CR1","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT press, Cambridge (2008)"},{"key":"7_CR2","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":"7_CR3","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Symbolic manipulation of boolean functions using a graphical representation. In: 22nd ACM\/IEEE Design Automation Conference, pp. 688\u2013694. IEEE (1985)","DOI":"10.1109\/DAC.1985.1586017"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Dvo\u0159\u00e1k, W., Henzinger, M., Loitzenbauer, V.: Model and objective separation with conditional lower bounds: Disjunction is harder than conjunction. In: Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science, pp. 197\u2013206 (2016)","DOI":"10.1145\/2933575.2935304"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Dvo\u0159\u00e1k, W., Henzinger, M., Svozil, A.: Symbolic time and space tradeoffs for probabilistic verification. In: 2021 36th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), pp. 1\u201313. IEEE (2021)","DOI":"10.1109\/LICS52264.2021.9470739"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-319-96142-2_13","volume-title":"Computer Aided Verification","author":"K Chatterjee","year":"2018","unstructured":"Chatterjee, K., Henzinger, M., Loitzenbauer, V., Oraee, S., Toman, V.: Symbolic algorithms for graphs and markov decision processes with fairness objectives. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 178\u2013197. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_13"},{"key":"7_CR7","unstructured":"De\u00a0Alfaro, L.: Formal verification of probabilistic systems. Stanford university (1998)"},{"key":"7_CR8","doi-asserted-by":"publisher","unstructured":"Faber, F.: Comparison of Maximal End Component Decomposition Algorithms: Data and Code (2023). https:\/\/doi.org\/10.5281\/zenodo.8311805","DOI":"10.5281\/zenodo.8311805"},{"key":"7_CR9","unstructured":"Faber, F.: Comparison of Symbolic Maximal End Component Decomposition Algorithms (2023). https:\/\/felixfaber.dev\/thesis.pdf. Accessed 21 June 2024"},{"key":"7_CR10","unstructured":"Gentilini, R., Piazza, C., Policriti, A., et\u00a0al.: Computing strongly connected components in a linear number of symbolic steps. In: SODA, vol.\u00a03, pp. 573\u2013582. Citeseer (2003)"},{"key":"7_CR11","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":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/978-3-030-17462-0_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Hartmanns","year":"2019","unstructured":"Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The quantitative verification benchmark set. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 344\u2013350. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_20"},{"key":"7_CR13","unstructured":"Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The probabilistic model checker storm. Int. J. Softw. Tools Technol. Transf., 1\u201322 (2022)"},{"key":"7_CR14","unstructured":"K\u0159et\u00ednsk\u1ef3, J., P\u00e9rez, G.A., Raskin, J.F.: Learning-based mean-payoff optimization in an unknown mdp under omega-regular constraints. arXiv preprint arXiv:1804.08924 (2018)"},{"key":"7_CR15","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":"7_CR16","unstructured":"Somenzi, F.: Cudd: Cu decision diagram package-release 2.4. 0. Univ. Colorado at Boulder 21 (2009)"}],"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-98679-6_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,7]],"date-time":"2025-09-07T16:17:52Z","timestamp":1757261872000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98679-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986789","9783031986796"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98679-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"22 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this paper.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"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":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}