{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T10:08:28Z","timestamp":1777889308583,"version":"3.51.4"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030591519","type":"print"},{"value":"9783030591526","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-59152-6_14","type":"book-chapter","created":{"date-parts":[[2020,10,11]],"date-time":"2020-10-11T23:02:35Z","timestamp":1602457355000},"page":"253-270","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Faster Algorithms for Quantitative Analysis of MCs and MDPs with Small Treewidth"],"prefix":"10.1007","author":[{"given":"Ali","family":"Asadi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Krishnendu","family":"Chatterjee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amir Kafshdar","family":"Goharshady","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kiarash","family":"Mohammadi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Pavlogiannis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,10,12]]},"reference":[{"key":"14_CR1","unstructured":"Asadi, A., et al.: Faster algorithms for quantitative analysis of Markov chains and Markov decision processes with small treewidth. arXiv preprint:2004.08828 (2020)"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Ashok, P., Chatterjee, K., Daca, P., K\u0159et\u00ednsk\u00fd, J., Meggendorfer, T.: Value iteration for long-run average reward in Markov decision processes. In: CAV (2017)","DOI":"10.1007\/978-3-319-63387-9_10"},{"key":"14_CR3","first-page":"679","volume":"6","author":"R Bellman","year":"1957","unstructured":"Bellman, R.: A Markovian decision process. J. Math. Mech. 6, 679\u2013684 (1957)","journal-title":"J. Math. Mech."},{"key":"14_CR4","unstructured":"Berkelaar, M., Eikland, K., Notebaert, P.: lpsolve linear programming system (2004)"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Blackburn, S.M., et al.: The DaCapo benchmarks: Java benchmarking development and analysis. In: OOPSLA (2006)","DOI":"10.1145\/1167473.1167488"},{"issue":"6","key":"14_CR6","doi-asserted-by":"publisher","first-page":"1305","DOI":"10.1137\/S0097539793251219","volume":"25","author":"HL Bodlaender","year":"1996","unstructured":"Bodlaender, H.L.: A linear-time algorithm for finding tree-decompositions of small treewidth. SIAM J. Comput. 25(6), 1305\u20131317 (1996)","journal-title":"SIAM J. Comput."},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Choudhary, B., Pavlogiannis, A.: Optimal Dyck reachability for data-dependence and alias analysis. In: POPL (2017)","DOI":"10.1145\/3158118"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Goharshady, A.K., Ibsen-Jensen, R., Pavlogiannis, A.: Optimal and perfectly parallel algorithms for on-demand data-flow analysis. In: ESOP (2020)","DOI":"10.1007\/978-3-030-44914-8_5"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-319-68167-2_4","volume-title":"Automated Technology for Verification and Analysis","author":"K Chatterjee","year":"2017","unstructured":"Chatterjee, K., Goharshady, A.K., Pavlogiannis, A.: JTDec: a tool for tree decompositions in soot. In: D\u2019Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 59\u201366. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-68167-2_4"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-540-69850-0_7","volume-title":"25 Years of Model Checking","author":"K Chatterjee","year":"2008","unstructured":"Chatterjee, K., Henzinger, T.A.: Value iteration. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 107\u2013138. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-69850-0_7"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, T.A., Jobstmann, B., Singh, R.: Measuring and synthesizing systems in probabilistic environments. In: CAV (2010)","DOI":"10.1007\/978-3-642-14295-6_34"},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/978-3-642-39799-8_36","volume-title":"Computer Aided Verification","author":"K Chatterjee","year":"2013","unstructured":"Chatterjee, K., \u0141\u0105cki, J.: Faster algorithms for Markov decision processes with low treewidth. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 543\u2013558. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39799-8_36"},{"issue":"3","key":"14_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3210257","volume":"40","author":"K Chatterjee","year":"2018","unstructured":"Chatterjee, K., et al.: Algorithms for algebraic path properties in concurrent systems of constant treewidth components. TOPLAS 40(3), 1\u201343 (2018)","journal-title":"TOPLAS"},{"key":"14_CR14","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). \nhttps:\/\/doi.org\/10.1007\/978-3-319-96142-2_13"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., et al.: Efficient parameterized algorithms for data packing. In: POPL (2019)","DOI":"10.1145\/3290366"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., et al.: Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth. TOPLAS 41(4), p. 23 (2019)","DOI":"10.1145\/3363525"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., et al.: The treewidth of smart contracts. In: SAC (2019)","DOI":"10.1145\/3297280.3297322"},{"key":"14_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-31862-0_21","volume-title":"Theoretical Aspects of Computing - ICTAC 2004","author":"C Daws","year":"2005","unstructured":"Daws, C.: Symbolic and parametric model checking of discrete-time Markov chains. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 280\u2013294. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/978-3-540-31862-0_21"},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-319-63390-9_31","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2017","unstructured":"Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592\u2013600. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-63390-9_31"},{"key":"14_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1007\/978-3-642-14162-1_46","volume-title":"Automata, Languages and Programming","author":"J Fearnley","year":"2010","unstructured":"Fearnley, J.: Exponential lower bounds for policy iteration. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 551\u2013562. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-14162-1_46"},{"key":"14_CR21","volume-title":"Handbook of Markov Decision Processes","author":"EA Feinberg","year":"2012","unstructured":"Feinberg, E.A.: Handbook of Markov Decision Processes. Springer, New York (2012)"},{"key":"14_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/11591191_34","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"A Ferrara","year":"2005","unstructured":"Ferrara, A., Pan, G., Vardi, M.Y.: Treewidth in verification: local vs. global. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 489\u2013503. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/11591191_34"},{"issue":"3","key":"14_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3186898","volume":"14","author":"FV Fomin","year":"2018","unstructured":"Fomin, F.V., et al.: Fully polynomial-time parameterized computations for graphs and matrices of low treewidth. TALG 14(3), 1\u201345 (2018)","journal-title":"TALG"},{"key":"14_CR24","doi-asserted-by":"publisher","first-page":"106665","DOI":"10.1016\/j.ress.2019.106665","volume":"193","author":"AK Goharshady","year":"2020","unstructured":"Goharshady, A.K., Mohammadi, F.: An efficient algorithm for computing network reliability in small treewidth. Reliab. Eng. Syst. Saf. 193, 106665 (2020)","journal-title":"Reliab. Eng. Syst. Saf."},{"key":"14_CR25","unstructured":"Gurobi Optimization, L.: Gurobi optimizer (2019). \nhttp:\/\/www.gurobi.com"},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"Gustedt, J., et al.: The treewidth of Java programs. In: ALENEX (2002)","DOI":"10.1007\/3-540-45643-0_7"},{"key":"14_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"660","DOI":"10.1007\/978-3-642-14295-6_56","volume-title":"Computer Aided Verification","author":"EM Hahn","year":"2010","unstructured":"Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: PARAM: a model checker for parametric markov models. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 660\u2013664. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-14295-6_56"},{"key":"14_CR28","unstructured":"Howard, R.A.: Dynamic programming and Markov processes (1960)"},{"key":"14_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/978-3-319-68167-2_25","volume-title":"Automated Technology for Verification and Analysis","author":"J K\u0159et\u00ednsk\u00fd","year":"2017","unstructured":"K\u0159et\u00ednsk\u00fd, J., Meggendorfer, T.: Efficient strategy iteration for mean payoff in Markov decision processes. In: D\u2019Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 380\u2013399. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-68167-2_25"},{"key":"14_CR30","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). \nhttps:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"14_CR31","unstructured":"MATLAB: The MathWorks Inc. (2018)"},{"key":"14_CR32","volume-title":"Markov Chains","author":"JR Norris","year":"1998","unstructured":"Norris, J.R.: Markov Chains. Cambridge University Press, Cambridge (1998)"},{"key":"14_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-540-45069-6_7","volume-title":"Computer Aided Verification","author":"J Obdr\u017e\u00e1lek","year":"2003","unstructured":"Obdr\u017e\u00e1lek, J.: Fast Mu-Calculus model checking when tree-width is bounded. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 80\u201392. Springer, Heidelberg (2003). \nhttps:\/\/doi.org\/10.1007\/978-3-540-45069-6_7"},{"key":"14_CR34","volume-title":"Markov Decision Processes","author":"ML Puterman","year":"2014","unstructured":"Puterman, M.L.: Markov Decision Processes. Wiley, Hoboken (2014)"},{"key":"14_CR35","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). \nhttps:\/\/doi.org\/10.1007\/978-3-319-96145-3_37"},{"issue":"1","key":"14_CR36","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/0095-8956(84)90013-3","volume":"36","author":"N Robertson","year":"1984","unstructured":"Robertson, N., Seymour, P.D.: Graph minors. iii. planar tree-width. J. Comb. Theor. Series B 36(1), 49\u201364 (1984)","journal-title":"J. Comb. Theor. Series B"},{"issue":"2","key":"14_CR37","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1006\/inco.1997.2697","volume":"142","author":"M Thorup","year":"1998","unstructured":"Thorup, M.: All structured programs have small tree width and good register allocation. Inf. Comput. 142(2), 159\u2013181 (1998)","journal-title":"Inf. Comput."}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-59152-6_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,11]],"date-time":"2020-10-11T23:06:02Z","timestamp":1602457562000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-59152-6_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030591519","9783030591526"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-59152-6_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"12 October 2020","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":"Hanoi","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Vietnam","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 October 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 October 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/fit.uet.vnu.edu.vn\/atva2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"75","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":"27","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":"36% - 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":"6","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)"}}]}}